#+PROPERTY: results silent scalar
#+title:A collection of examples for ob-ada-spark tests

* Simple programs

** Hello world
:PROPERTIES:
:ID: 778e63c2-2644-4a6f-8e7d-f956fa3d9241
:END:

#+name: Hello world
#+begin_src ada :results silent
   with Ada.Text_IO;
   procedure Hello_World is
   begin
      Ada.Text_IO.Put_Line ("Hello world");
   end Hello_World;
#+end_src

** Recursive Fibonacci
:PROPERTIES:
:ID: 6281cb40-26cc-423e-88c8-e8f26901ee4a
:END:

#+name: Recursive Fibonacci
#+begin_src ada :unit fibonacci :results silent
   with Ada.Text_IO;
   procedure Fibonacci is
      function fib (n : Natural) return Natural is
        (if n <= 2 then 1 else fib (n-1) + fib (n-2));
      Fib_15 : Natural;
   begin
      Fib_15 := fib (15);
      Ada.Text_IO.Put_Line (Fib_15'Image);
   end Fibonacci;
#+end_src

** Sequential Fibonacci
:PROPERTIES:
:ID: 41b4514b-0d46-4011-b5fa-7997aecf75a9
:END:

#+name Sequential Fibonacci
#+begin_src ada :unit fibonacci :results silent
   with Ada.Text_IO; use Ada.Text_IO;
   procedure Fibonacci is
      function fib (n : Natural) return Natural is
      fn1, fn2 : Natural := 1;
      begin
         return result : Natural := 1 do
            for i in reverse 3 .. n loop
               result := fn1 + fn2;
               fn2 := fn1;
               fn1 := result;
            end loop;
         end return;
      end fib;
      Fib_15 : constant Natural := fib (15);
   begin
     Ada.Text_IO.Put_Line (Fib_15'Image);
   end Fibonacci;
#+end_src

** UTF8 identifiers
:PROPERTIES:
:ID: 06e4dc5b-5566-486b-81af-cb7c547d46f1
:END:

#+name: UTF8 indetifiers
#+begin_src ada :unit average :results silent
   with Ada.Text_IO; use Ada.Text_IO;
   procedure Average is
      Σ_numbers : Natural := 0;
      α, β, Δ_x : Natural := 1;
      Average   : Float;
   begin
      loop
         Σ_numbers := @ + α;
         exit when α > 100;
         α := @ + Δ_x;
         β := @ + 1;
         Δ_X := @ * 2;
      end loop;
      Average := Float (Σ_numbers) / Float (β);
      Put_Line ("Average:" & Natural (Average)'Image);
   end Average;
#+end_src

* Using templates

** Main template
:PROPERTIES:
:ID: a2a64153-a7b6-4c32-84c5-a589f0caac93
:END:

#+name: Main template
#+begin_src ada :template ada-main :results silent
begin
   Put_Line ("Hello world");
#+end_src

** Fibonacci
:PROPERTIES:
:ID: cbef4ee3-63e3-4295-8b26-e2470e30b1ff
:END:

#+name: Fibonacci
#+begin_src ada :template ada-main :results silent
   --  declaratiions
   function fib (n : Natural) return Natural is
      (if n <= 2 then 1 else fib (n-1) + fib (n-2));
   Fib_15 : Natural;

begin
   Fib_15 := fib (15);
   Put_Line (Fib_15'Image);
#+end_src

** Invalid template name
:PROPERTIES:
:ID: 3fb0ac1c-dfed-4d2f-9803-d1dea18eec45
:END:

#+name: Invalid template
#+begin_src ada :template foo-bar :results silent
begin
   Put_Line ("Hello world");
#+end_src

* Literate programming

** Hello noweb
:PROPERTIES:
:ID: 5386221e-da6f-411f-8dd5-3045e14b2e15
:END:

#+name: __Say_Hello_Noweb__
#+begin_src ada
   Put_Line ("Hello noweb");
#+end_src

#+header: :noweb yes
#+name: Hello noweb
#+begin_src ada :unit hello_world :results silent scalar
   with Ada.Text_IO; use Ada.Text_IO;
   procedure Hello_World is
   begin
      <<__Say_Hello_Noweb__>>
   end Hello_World;
#+end_src

** Constant literals
:PROPERTIES:
:ID: 1bc1f537-e31f-4b8e-adb3-bdd474673e17
:END:

#+name: __Say_Hello__
#+begin_src ada
   Put ("Hello");
#+end_src

#+header: :noweb yes
#+header: :var __TIMES__=3
#+name: Constant literals
#+begin_src ada :template ada-main :results silent scalar
begin
   for I in 1 .. __TIMES__ loop
      Put (I'Image & " ");
      <<__Say_Hello__>>
   end loop;
#+end_src

#+header: :var __MESSAGE__="Hellow world"
#+name: Constant literals - invalid literal name
#+begin_src ada :template ada-main :results silent scalar
   Put_Line ("Message: " &  __MSG__);
#+end_src

** Evaluated literals
:PROPERTIES:
:ID: 7cc220c1-a917-4af4-a497-7e247f1c15ae
:END:

#+header: :var __SUM__=(+ 1 1 3 5 8 13 34 55 89 144)
#+name: Variable evaluation
#+begin_src ada :template ada-main :results silent scalar
begin
   Put_Line ("SUM is __SUM__");
#+end_src

* User-Defined templates

For the test, the template =ob-ada-spark-template:test= is defined in
the file =test-ob-ada-spark.el=.

** Test
:PROPERTIES:
:ID: 70feb9e8-19f1-402b-b1d0-4c8ccdf2cfe4
:END:

#+name: Test
#+begin_src ada :template test
   Write_Answer (42);
#+end_src

** Using and evaluated literals
:PROPERTIES:
:ID: 2a05b182-07bf-4ba5-9cca-128919cb837e
:END:

#+header: :var __Answer__=(* 21 2)
#+name: Using evaluated literals
#+begin_src ada :template test
   Write_Answer (__Answer__);
#+end_src

** Using noweb and evaluated literals
:PROPERTIES:
:ID: 69e852b1-a278-4051-8719-917cfb59c582
:END:

#+name: __Write_Answer__
#+begin_src ada :template test
   Write_Answer (__Answer__);
#+end_src

#+header: :noweb yes
#+header: :var __Answer__=(* 21 2)
#+name: Using noweb and evaluated literals
#+begin_src ada :template test
   <<__Write_Answer__>>
#+end_src

* Proving SPARK code

** Increment

#+name: __Increment__
#+begin_src ada
   subtype Nat16 is Natural range 0 .. 2**16;
   Number : Nat16 := Nat16'Last - 1;

   procedure Increment (X : in out Nat16) with
      Global  => null,
      Depends => (X => X),
      Pre     => (X < Nat16'Last),
      Post    => (X = X'Old + 1)
   is
   begin
      X := X + 1;
   end Increment;

begin
   Increment (Number);
   Put_Line ("Last Nat16 is" & Number'Image);
#+end_src

** Stone
:PROPERTIES:
:ID: fd628dbb-aacc-4931-aab5-5816f7c85b46
:END:

#+name: Stone
#+header: :noweb yes
#+begin_src ada :template spark-main :pflags --mode=stone :results scalar
   <<__Increment__>>
#+end_src

** Bronze
:PROPERTIES:
:ID: 79b4ca15-8127-467d-b239-dd190cb45f2d
:END:

#+name: Bronze
#+header: :noweb yes
#+begin_src ada :template spark-main :pflags --mode=bronze :results scalar
   <<__Increment__>>
#+end_src

** Silver
:PROPERTIES:
:ID: 4529e47f-835a-4410-883a-b3fab0026553
:END:

#+name: Silver
#+header: :noweb yes
#+begin_src ada :template spark-main :pflags --mode=silver :results scalar
   <<__Increment__>>
#+end_src

** Gold
:PROPERTIES:
:ID: 371d0f89-4281-48b4-a70b-d0b51d515423
:END:

#+name: Gold
#+header: :noweb yes
#+begin_src ada :template spark-main :pflags --mode=gold :results scalar
   <<__Increment__>>
#+end_src