From bd9bc0823b48bb3411af61e0d310de4c16a08d41 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Tue, 19 Oct 2021 18:47:30 +0100
Subject: [PATCH 01/12] Remove sexplib0 from the plugin

---
 src/dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/dune b/src/dune
index 91ab18d..978f8f6 100644
--- a/src/dune
+++ b/src/dune
@@ -3,7 +3,7 @@
  (name why3gospel)
  (modes plugin)
  (libraries ocaml-compiler-libs.shadow ppxlib.astlib ppxlib why3 gospel)
- (embed_in_plugin_libraries compiler-libs.common sexplib0 ppxlib.stdppx
+ (embed_in_plugin_libraries compiler-libs.common ppxlib.stdppx
    ppxlib.astlib ppxlib.ast ppxlib fmt gospel))
 
 (install

From b33cb72848f63cf99f697bc48a2133c32ca3530d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Fri, 22 Oct 2021 10:57:08 +0100
Subject: [PATCH 02/12] gospel.mlw

---
 src/gospel.mlw | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/gospel.mlw b/src/gospel.mlw
index 2f4c1a5..d6e8f6a 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -52,6 +52,8 @@ module Stdlib
 
     predicate permut (a1 a2: array 'a) = P.permut_all a1 a2
     predicate permut_sub (a1 a2: array 'a) (l u: int) = P.permut_sub a1 a2 l u
+
+    function to_seq (a: array 'a) : seq 'a = a.elts
   end
   type array 'a = Array.array 'a
 
@@ -84,7 +86,7 @@ module Stdlib
 
   let constant max_int : int = I.max_int63
   let constant min_int : int = I.min_int63
-  
+
   function fst (x : ('a, 'b)) : 'a = let (f, _) = x in f
   function snd (x : ('a, 'b)) : 'b = let (_, s) = x in s
 

From 2e9ce49ec4763e9fbfc4985af9abeb08eafca922 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Tue, 19 Oct 2021 19:35:20 +0100
Subject: [PATCH 03/12] Apply fmt in dune file.

---
 src/dune | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/dune b/src/dune
index 978f8f6..e186ca4 100644
--- a/src/dune
+++ b/src/dune
@@ -3,8 +3,8 @@
  (name why3gospel)
  (modes plugin)
  (libraries ocaml-compiler-libs.shadow ppxlib.astlib ppxlib why3 gospel)
- (embed_in_plugin_libraries compiler-libs.common ppxlib.stdppx
-   ppxlib.astlib ppxlib.ast ppxlib fmt gospel))
+ (embed_in_plugin_libraries compiler-libs.common ppxlib.stdppx ppxlib.astlib
+   ppxlib.ast ppxlib fmt gospel))
 
 (install
  (section lib_root)

From 85486006f4957081ee21f1a22580bf80cff06296 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Wed, 20 Oct 2021 11:54:16 +0100
Subject: [PATCH 04/12] Gospel.mlw: added more functions from module [List]
 (wip).

---
 src/gospel.mlw | 44 ++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 40 insertions(+), 4 deletions(-)

diff --git a/src/gospel.mlw b/src/gospel.mlw
index d6e8f6a..b466ac6 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -32,10 +32,10 @@ module Stdlib
   type seq 'a = Seq.seq 'a
 
   function (++) (s t: seq 'a) : seq 'a = Seq.(++) s t
-  function ([]) (s: seq 'a) (i:integer): 'a = Seq.([]) s i
-  function ([..]) (s: seq 'a) (i1 i2: int): seq 'a = Seq.([..]) s i1 i2
-  function ([.._]) (s: seq 'a) (i: int): seq 'a = Seq.([.._]) s i
-  function ([_..]) (s: seq 'a) (i: int): seq 'a = Seq.([_..]) s i
+  function ([]) (s: seq 'a) (i: integer): 'a = Seq.([]) s i
+  function ([..]) (s: seq 'a) (i1 i2: integer): seq 'a = Seq.([..]) s i1 i2
+  function ([.._]) (s: seq 'a) (i: integer): seq 'a = Seq.([.._]) s i
+  function ([_..]) (s: seq 'a) (i: integer): seq 'a = Seq.([_..]) s i
 
   scope Bag
     use export bag.Bag
@@ -74,6 +74,42 @@ module Stdlib
   end
   type set 'a = Set.FS.fset 'a
 
+  scope List
+
+    use list.Length as LL
+    use list.HdTlNoOpt as LOpt
+    use list.NthNoOpt as LNth
+    use list.Nth as LNthOpt
+    use list.Reverse as LRev
+    use list.Mem as LMem
+
+    type t 'a = list 'a
+
+    function length (l: t 'a) : integer = LL.length l
+
+    function hd (l: t 'a) : 'a = LOpt.hd l
+    function tl (l: t 'a) : t 'a = LOpt.tl l
+
+    function nth (l: t 'a) (i: integer) : 'a = LNth.nth i l
+    function nth_opt (l: t 'a) (i: integer) : option 'a = LNthOpt.nth i l
+
+    function rev (l: t 'a) : t 'a = LRev.reverse l
+
+    (* FIXME? Should we provide pre-conditions for [init_aux] and [init] ? *)
+    let rec function init_aux (i n: integer) (f: integer -> 'a) : t 'a
+      variant { n - i }
+    = if i >= n then Nil
+      else Cons (f i) (init_aux (i+1) n f)
+
+    function init (n: integer) (f: integer -> 'a) : t 'a
+    = init_aux 0 n f
+
+    predicate mem (x: 'a) (l: t 'a) = LMem.mem x l
+
+    function to_seq (l: t 'a) : seq 'a = Seq.of_list l
+
+  end
+
   use int.ComputerDivision
   function (/) (x y: int) : int = div x y
 

From f9f38733437497c5abca37dffd4a0688418e64cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Fri, 22 Oct 2021 10:45:25 +0100
Subject: [PATCH 05/12] All functions from module [List] are now included.

---
 src/gospel.mlw | 84 ++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 71 insertions(+), 13 deletions(-)

diff --git a/src/gospel.mlw b/src/gospel.mlw
index b466ac6..f58b666 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -76,38 +76,96 @@ module Stdlib
 
   scope List
 
-    use list.Length as LL
-    use list.HdTlNoOpt as LOpt
+    use export list.Length
+    use export list.HdTlNoOpt
     use list.NthNoOpt as LNth
     use list.Nth as LNthOpt
-    use list.Reverse as LRev
+    use export list.Reverse
     use list.Mem as LMem
+    use seq.ToList as SL
+    use list.FoldLeft as LFoldl
+    use list.FoldRight as LFoldr
+    use list.Quant as LQuant
 
     type t 'a = list 'a
 
-    function length (l: t 'a) : integer = LL.length l
-
-    function hd (l: t 'a) : 'a = LOpt.hd l
-    function tl (l: t 'a) : t 'a = LOpt.tl l
-
     function nth (l: t 'a) (i: integer) : 'a = LNth.nth i l
     function nth_opt (l: t 'a) (i: integer) : option 'a = LNthOpt.nth i l
 
-    function rev (l: t 'a) : t 'a = LRev.reverse l
+    function rev (l: t 'a) : t 'a = reverse l
 
     (* FIXME? Should we provide pre-conditions for [init_aux] and [init] ? *)
     let rec function init_aux (i n: integer) (f: integer -> 'a) : t 'a
       variant { n - i }
     = if i >= n then Nil
-      else Cons (f i) (init_aux (i+1) n f)
-
-    function init (n: integer) (f: integer -> 'a) : t 'a
-    = init_aux 0 n f
+      else Cons (f i) (init_aux (i + 1) n f)
+
+    function init (n: integer) (f: integer -> 'a) : t 'a =
+      init_aux 0 n f
+
+    function map (f: 'a -> 'b) (l: t 'a) : t 'b =
+      match l with
+      | Nil -> Nil
+      | Cons x r -> Cons (f x) (map f r)
+      end
+
+    function mapi_aux (i: integer) (f: integer -> 'a -> 'b) (l: list 'a) :
+      list 'b
+    = match l with
+      | Nil -> Nil
+      | Cons x r -> Cons (f i x) (mapi_aux (i + 1) f r)
+      end
+
+    function mapi (f: integer -> 'a -> 'b) (l: t 'a) : t 'b =
+      mapi_aux 0 f l
+
+    function fold_left (f: 'a -> 'b -> 'a) (init: 'a) (l: t 'b) : 'a =
+      LFoldl.fold_left f init l
+
+    function fold_right (f: 'b -> 'a -> 'a) (l: t 'b) (init: 'a) : 'a =
+      LFoldr.fold_right f l init
+
+    let rec function map2 (f: 'a -> 'b -> 'c) (l: t 'a) (l': t 'b) : t 'c
+      requires { length l = length l' }
+      variant  { l }
+    = match l, l' with
+      | Nil, Nil -> Nil
+      | Cons a1 l1, Cons a2 l2 -> Cons (f a1 a2) (map2 f l1 l2)
+      | _ -> absurd
+      end
+
+    predicate for_all (f: 'a -> bool) (l: t 'a) =
+      LQuant.for_all f l
+
+    predicate _exists (f: 'a -> bool) (l: t 'a) =
+      LQuant.for_some f l
+
+    (* Cannot use [let predicate] because of the [absurd] case *)
+    (* FIXME? Should we provide post-conditions to the following functions ? *)
+    let rec function for_all2 (f: 'a -> 'b -> bool) (l: t 'a) (l': t 'b) : bool
+      requires { length l = length l' }
+      variant  { l }
+    = match l, l' with
+      | Nil, Nil -> true
+      | Cons a1 l1, Cons a2 l2 -> f a1 a2 && for_all2 f l1 l2
+      | _ -> absurd
+      end
+
+    let rec function _exists2 (f: 'a -> 'b -> bool) (l: t 'a) (l': t 'b) : bool
+      requires { length l = length l' }
+      variant  { l }
+    = match l, l' with
+      | Nil, Nil -> false
+      | Cons a1 l1, Cons a2 l2 -> f a1 a2 || _exists2 f l1 l2
+      | _ -> absurd
+      end
 
     predicate mem (x: 'a) (l: t 'a) = LMem.mem x l
 
     function to_seq (l: t 'a) : seq 'a = Seq.of_list l
 
+    function of_seq (l: seq 'a) : t 'a = SL.to_list l
+
   end
 
   use int.ComputerDivision

From 0288c7e7eba6c9981159f06618bf9971cae267db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Fri, 22 Oct 2021 10:45:51 +0100
Subject: [PATCH 06/12] Added functions from [Bag] module (wip).

---
 src/gospel.mlw | 70 ++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 68 insertions(+), 2 deletions(-)

diff --git a/src/gospel.mlw b/src/gospel.mlw
index f58b666..974e37a 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -38,14 +38,80 @@ module Stdlib
   function ([_..]) (s: seq 'a) (i: integer): seq 'a = Seq.([_..]) s i
 
   scope Bag
-    use export bag.Bag
+    use bag.Bag as B
+
+    type t 'a = B.bag 'a
+
+    function occurrences (x: 'a) (b: t 'a): integer =
+      B.nb_occ x b
+
+    (*@ function compare (b b': 'a t) : int *)
+
+    function empty : t 'a = B.empty_bag
+
+    predicate is_empty (b: t 'a) = b = empty
+
+    predicate mem (x: 'a) (b: t 'a) = B.mem x b
+
+    function add (x: 'a) (b: t 'a) : t 'a = B.add x b
+
+    function singleton (x: 'a) : t 'a = B.singleton
+
+    function remove (x: 'a) (b: t 'a) : t 'a =
+      B.diff b (B.singleton x)
+
+    function union (b b': t 'a) : t 'a
+
+    (*@ function sum (b b': 'a t) : 'a t *)
+
+    (*@ function inter (b b': 'a t) : 'a t *)
+
+    (*@ predicate disjoint (b b': 'a t) *)
+
+    (*@ function diff (b b': 'a t) : 'a t *)
+
+    (*@ predicate subset (b b': 'a t) *)
+
+    (*@ function choose (b: 'a t) : integer *)
+
+    (*@ function choose_opt (b: 'a t) : 'a option *)
+
+    (*@ function map (f: 'a -> 'b) (b: 'a t) : 'b t *)
+
+    (*@ function fold (f: 'a -> 'b -> 'b) (b: 'a t) : 'b *)
+
+    (*@ predicate for_all (f: 'a -> bool) (b: 'a t) *)
+
+    (*@ predicate _exists (f: 'a -> bool) (b: 'a t) *)
+
+    (*@ function filter (f: 'a -> bool) (b: 'a t) : 'a t *)
+
+    (*@ function filter_map (f: 'a -> 'a option) (b: 'a t) : 'a t *)
+
+    (*@ function partition (f: 'a -> bool) (b: 'a t) : ('a t * 'a t) *)
+
+    (*@ function cardinal (b: 'a t) : int *)
+
+    (*@ function elements (b: 'a t) : 'a list *)
+
+    (*@ function to_list (b: 'a t) : 'a list *)
+    function of_list (l: list 'a) : t 'a
+
+    (*@ function to_seq (b: 'a t) : 'a Seq.t *)
+    (*@ function of_seq (s: 'a Seq.t) : 'a t *)
+
+    (*@ function of_array (a: 'a array) : 'a t *)
+
   end
-  type bag 'a = Bag.bag 'a
+  type bag 'a = Bag.B.bag 'a
 
   use export ref.Ref
 
   scope Array
     use export mach.array.Array63
+
+    type t 'a = array 'a
+
     function get (a : array 'a) (i: int) : 'a = a[i]
 
     use mach.array.Array63Permut as P

From 40cb277546884fd5859f9e2c6a313d8e29e52c14 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Fri, 22 Oct 2021 10:49:25 +0100
Subject: [PATCH 07/12] Test files for symbols from the Gospel Stdlib.

  - [list_stdlib]: all functions covered
  - [bag_stdlib]: wip
---
 tests/positive/bag_stdlib.mli  | 31 ++++++++++++++++++
 tests/positive/list_stdlib.mli | 58 ++++++++++++++++++++++++++++++++++
 2 files changed, 89 insertions(+)
 create mode 100644 tests/positive/bag_stdlib.mli
 create mode 100644 tests/positive/list_stdlib.mli

diff --git a/tests/positive/bag_stdlib.mli b/tests/positive/bag_stdlib.mli
new file mode 100644
index 0000000..be89c77
--- /dev/null
+++ b/tests/positive/bag_stdlib.mli
@@ -0,0 +1,31 @@
+type 'a t
+(*@ model view : 'a bag *)
+
+(*@ function to_bag (t: 'a t) : 'a bag = t.view *)
+(*@ coercion *)
+
+val f1 : 'a -> 'a t -> int
+(*@ r = f1 x t
+      ensures r = Bag.occurrences x t *)
+
+val f2 : 'a t -> bool
+(*@ b = f2 t
+      ensures b <-> Bag.is_empty t
+      ensures b <-> t = Bag.empty *)
+
+val f3 : 'a -> 'a t -> bool
+(*@ b = f3 x t
+      ensures b <-> Bag.mem x t *)
+
+val f4 : 'a -> 'a t -> 'a t
+(*@ r = f4 x t
+      ensures r = Bag.add x t
+      ensures r = Bag.(union t (singleton x)) *)
+
+val f5 : 'a -> 'a t
+(*@ r = f5 x
+      ensures r = Bag.singleton x *)
+
+val f6 : 'a t -> unit
+(*@ f6 t
+      ensures forall x: 'a. Bag.(remove x (add x t)) = t *)
diff --git a/tests/positive/list_stdlib.mli b/tests/positive/list_stdlib.mli
new file mode 100644
index 0000000..5b4e915
--- /dev/null
+++ b/tests/positive/list_stdlib.mli
@@ -0,0 +1,58 @@
+val f1 : 'a list -> unit
+(*@ f1 l [l': 'a List.t] *)
+
+val f2 : 'a list -> int
+(*@ r = f2 l
+      ensures r = List.length l *)
+
+val f3 : 'a list -> 'a * 'a list
+(*@ a, r = f3 l
+      requires List.length l > 0
+      ensures  a = List.hd l && r = List.tl l *)
+
+val f4 : 'a list -> int -> 'a option
+(*@ r = f4 l i
+      ensures r = List.nth_opt l i
+      ensures match r with
+              | Some v -> v = List.nth l i && v = l[i]
+              | _ -> false *)
+
+val f5 : 'a list -> 'a list
+(*@ r = f5 l
+      ensures r = List.rev l *)
+
+val f6 : 'a -> int -> 'a list
+(*@ r = f6 x n
+      ensures r = List.init n (fun _i -> x) *)
+
+val f7 : 'a list -> 'a list
+(*@ r = f7 l
+      ensures r = List.map (fun x -> x) l
+      ensures r = List.mapi (fun _i x -> x) l *)
+
+val f8 : 'a list -> 'b -> 'b
+(*@ r = f8 l acc
+      ensures r = List.fold_left (fun a _x -> a) acc l
+      ensures r = List.fold_right (fun _x a -> a) l acc *)
+
+val f9 : 'a list -> 'b list -> 'a list
+(*@ r = f9 l1 l2
+      ensures r = List.map2 (fun x _y -> x) l1 l2 *)
+
+val f10 : 'a list -> 'a -> bool
+(*@ b = f10 l x
+      ensures b <-> List.for_all (fun y -> x = y) l
+      ensures b <-> List._exists (fun y -> x = y) l *)
+
+val f11 : 'a list -> 'a list -> bool
+(*@ b = f11 l1 l2
+      ensures b <-> List.for_all2 (fun x y -> x = y) l1 l2
+      ensures b <-> List._exists2 (fun x y -> x = y) l1 l2 *)
+
+val f12 : 'a list -> 'a -> bool
+(*@ b = f12 l x
+      ensures b <-> List.mem x l *)
+
+val f13 : 'a list -> unit
+(*@ f13 l
+      ensures List.(of_seq (to_seq l)) = l *)

From 9459ff861b65c27e709c78f2568afba4807d5fda Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Fri, 22 Oct 2021 11:11:59 +0100
Subject: [PATCH 08/12] Dune file for tests.

---
 tests/positive/dune | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 tests/positive/dune

diff --git a/tests/positive/dune b/tests/positive/dune
new file mode 100644
index 0000000..4764aad
--- /dev/null
+++ b/tests/positive/dune
@@ -0,0 +1,13 @@
+(rule
+ (targets list_stdlib.mli.output)
+ (action
+  (with-outputs-to
+   %{targets}
+   (with-accepted-exit-codes
+    (or :standard 125)
+    (system "why3 prove %{dep:list_stdlib.mli}")))))
+
+(rule
+ (alias runtest)
+ (action
+  (diff %{dep:list_stdlib.mli.expected} %{dep:list_stdlib.mli.output})))

From bc4fddf5d26841b720943149cb4e7ca489ab5d8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Fri, 22 Oct 2021 11:14:22 +0100
Subject: [PATCH 09/12] Dune file for tests.

---
 tests/positive/dune | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/tests/positive/dune b/tests/positive/dune
index 4764aad..00defa8 100644
--- a/tests/positive/dune
+++ b/tests/positive/dune
@@ -1,13 +1,5 @@
-(rule
- (targets list_stdlib.mli.output)
- (action
-  (with-outputs-to
-   %{targets}
-   (with-accepted-exit-codes
-    (or :standard 125)
-    (system "why3 prove %{dep:list_stdlib.mli}")))))
-
 (rule
  (alias runtest)
  (action
-  (diff %{dep:list_stdlib.mli.expected} %{dep:list_stdlib.mli.output})))
+  (with-accepted-exit-codes 0
+    (system "why3 prove %{dep:list_stdlib.mli}"))))

From 473ee307cd5285a652833b5a089b2aee06f69b4b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?M=C3=A1rio=20Pereira?= <mjp.pereira@fct.unl.pt>
Date: Mon, 25 Oct 2021 13:11:48 +0100
Subject: [PATCH 10/12] More functions from the [Bag] module.

---
 src/gospel.mlw | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/gospel.mlw b/src/gospel.mlw
index 974e37a..98b9620 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -62,19 +62,30 @@ module Stdlib
 
     function union (b b': t 'a) : t 'a
 
-    (*@ function sum (b b': 'a t) : 'a t *)
+    axiom def_union:
+      forall x: 'a, b b': t 'a.
+      occurrences x (union b b') = max (occurrences x b) (occurrences x b')
 
-    (*@ function inter (b b': 'a t) : 'a t *)
+    function sum (b b': t 'a) : t 'a =
+      B.union b b'
 
-    (*@ predicate disjoint (b b': 'a t) *)
+    function inter (b b': t 'a) : t 'a =
+      B.inter b b'
 
-    (*@ function diff (b b': 'a t) : 'a t *)
+    predicate disjoint (b b': t 'a) =
+      B.inter b b' = empty
 
-    (*@ predicate subset (b b': 'a t) *)
+    function diff (b b': t 'a) : t 'a =
+      B.diff b b'
 
-    (*@ function choose (b: 'a t) : integer *)
+    predicate subset (b b': 'a t) =
+      forall x. occurrences x b <= occurrences x b'
 
-    (*@ function choose_opt (b: 'a t) : 'a option *)
+    function choose (b: 'a t) : integer =
+      B.choose b
+
+    function choose_opt (b: 'a t) : 'a option =
+      if b = empty then None else Some (choose b)
 
     (*@ function map (f: 'a -> 'b) (b: 'a t) : 'b t *)
 

From 21383bb33921429e689bf5bd9de374862f056c17 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pascutto?= <clement@pascutto.fr>
Date: Wed, 3 Nov 2021 10:46:29 +0100
Subject: [PATCH 11/12] tests: run why3 config

---
 dune-project         |  3 ++-
 src/gospel.mlw       | 34 +++++++++++++++++-----------------
 src/trans.ml         | 26 ++++++++++++++------------
 src/why3gospel.ml    | 19 -------------------
 tests/positive/dune  |  8 +++-----
 tests/positive/run.t | 29 +++++++++++++++++++++++++++++
 why3gospel.opam      |  4 ++--
 7 files changed, 67 insertions(+), 56 deletions(-)
 create mode 100644 tests/positive/run.t

diff --git a/dune-project b/dune-project
index ddaa894..3a59510 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,4 @@
-(lang dune 2.4)
+(lang dune 2.7)
 (name why3gospel)
 (implicit_transitive_deps false)
+(cram enable)
diff --git a/src/gospel.mlw b/src/gospel.mlw
index 98b9620..35530bf 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -55,7 +55,7 @@ module Stdlib
 
     function add (x: 'a) (b: t 'a) : t 'a = B.add x b
 
-    function singleton (x: 'a) : t 'a = B.singleton
+    function singleton (x: 'a) : t 'a = B.singleton x
 
     function remove (x: 'a) (b: t 'a) : t 'a =
       B.diff b (B.singleton x)
@@ -78,40 +78,40 @@ module Stdlib
     function diff (b b': t 'a) : t 'a =
       B.diff b b'
 
-    predicate subset (b b': 'a t) =
+    predicate subset (b b': t 'a) =
       forall x. occurrences x b <= occurrences x b'
 
-    function choose (b: 'a t) : integer =
+    function choose (b: t 'a) : 'a =
       B.choose b
 
-    function choose_opt (b: 'a t) : 'a option =
+    function choose_opt (b: t 'a) : option 'a =
       if b = empty then None else Some (choose b)
 
-    (*@ function map (f: 'a -> 'b) (b: 'a t) : 'b t *)
+    (*@ function map (f: 'a -> 'b) (b: t 'a) : t 'b *)
 
-    (*@ function fold (f: 'a -> 'b -> 'b) (b: 'a t) : 'b *)
+    (*@ function fold (f: 'a -> 'b -> 'b) (b: t 'a) : 'b *)
 
-    (*@ predicate for_all (f: 'a -> bool) (b: 'a t) *)
+    (*@ predicate for_all (f: 'a -> bool) (b: t 'a) *)
 
-    (*@ predicate _exists (f: 'a -> bool) (b: 'a t) *)
+    (*@ predicate _exists (f: 'a -> bool) (b: t 'a) *)
 
-    (*@ function filter (f: 'a -> bool) (b: 'a t) : 'a t *)
+    (*@ function filter (f: 'a -> bool) (b: t 'a) : t 'a *)
 
-    (*@ function filter_map (f: 'a -> 'a option) (b: 'a t) : 'a t *)
+    (*@ function filter_map (f: 'a -> option 'a) (b: t 'a) : t 'a *)
 
-    (*@ function partition (f: 'a -> bool) (b: 'a t) : ('a t * 'a t) *)
+    (*@ function partition (f: 'a -> bool) (b: t 'a) : (t 'a * t 'a) *)
 
-    (*@ function cardinal (b: 'a t) : int *)
+    (*@ function cardinal (b: t 'a) : int *)
 
-    (*@ function elements (b: 'a t) : 'a list *)
+    (*@ function elements (b: t 'a) : list 'a *)
 
-    (*@ function to_list (b: 'a t) : 'a list *)
+    (*@ function to_list (b: t 'a) : list 'a *)
     function of_list (l: list 'a) : t 'a
 
-    (*@ function to_seq (b: 'a t) : 'a Seq.t *)
-    (*@ function of_seq (s: 'a Seq.t) : 'a t *)
+    (*@ function to_seq (b: t 'a) : Seq.t 'a *)
+    (*@ function of_seq (s: Seq.t 'a) : t 'a *)
 
-    (*@ function of_array (a: 'a array) : 'a t *)
+    (*@ function of_array (a: array 'a) : t 'a *)
 
   end
   type bag 'a = Bag.B.bag 'a
diff --git a/src/trans.ml b/src/trans.ml
index 32f0f51..d2ce5a3 100644
--- a/src/trans.ml
+++ b/src/trans.ml
@@ -326,7 +326,8 @@ let spec_with_checks info val_spec pre checks =
 
 let spec info val_spec =
   {
-    sp_pre = List.map (fun t -> term info t) val_spec.T.sp_pre;
+    sp_pre =
+      List.map (fun t -> term info t) (val_spec.T.sp_pre @ val_spec.T.sp_checks);
     sp_post = sp_post info val_spec.sp_ret val_spec.sp_post;
     sp_xpost = sp_xpost info val_spec.sp_xpost;
     sp_reads = [];
@@ -395,17 +396,18 @@ let val_decl info vd g =
     in
     match vd.T.vd_spec with
     | None -> [ mk_val (mk_id vd_str) params ret pat mask empty_spec ]
-    | Some s -> (
-        match (s.sp_pre, s.sp_checks) with
-        | _, [] -> [ mk_val (mk_id vd_str) params ret pat mask (spec info s) ]
-        | pre, checks ->
-            let id_unsafe = mk_id ("unsafe_" ^ vd_str) in
-            let checks_term = List.map (term info) checks in
-            let spec_checks = spec_with_checks info s pre checks_term in
-            [
-              mk_val id_unsafe params ret pat mask (spec info s);
-              mk_val (mk_id vd_str) params ret pat mask spec_checks;
-            ])
+    | Some s ->
+        let unsafe_spec = spec info s in
+        if s.sp_checks = [] then
+          [ mk_val (mk_id vd_str) params ret pat mask unsafe_spec ]
+        else
+          let id_unsafe = mk_id ("unsafe_" ^ vd_str) in
+          let checks_term = List.map (term info) s.sp_checks in
+          let spec_checks = spec_with_checks info s s.sp_pre checks_term in
+          [
+            mk_val id_unsafe params ret pat mask unsafe_spec;
+            mk_val (mk_id vd_str) params ret pat mask spec_checks;
+          ]
   in
   let params, ret, pat, mask =
     let params, pat, mask =
diff --git a/src/why3gospel.ml b/src/why3gospel.ml
index 840c3e1..4be10bd 100644
--- a/src/why3gospel.ml
+++ b/src/why3gospel.ml
@@ -14,7 +14,6 @@ open Why3
 open Ptree
 module Mstr = Why3.Wstdlib.Mstr
 
-let debug = ref true
 let print_modules = Debug.lookup_flag "print_modules"
 
 let mk_id ?(loc = Loc.dummy_position) name =
@@ -109,7 +108,6 @@ let read_extra_file file =
 
 let read_channel env path file c =
   let open Typing in
-  if !debug then Format.eprintf "reading file '%s'@." file;
   let extra_uses, extra_vals = read_extra_file file in
   let nm =
     let f = Filename.basename file in
@@ -132,23 +130,6 @@ let read_channel env path file c =
         Typing.close_scope ~import:true loc
   in
   let f = List.flatten sigs in
-  (* FIXME *)
-  (* For debugging only: *)
-  let rec pp_list pp fmt l =
-    match l with
-    | [] -> ()
-    | x :: r ->
-        Format.eprintf "%a" pp x;
-        pp_list pp fmt r
-  in
-  let rec pp_decl _ d =
-    match d with
-    | Gdecl d -> Format.eprintf "%a@." Mlw_printer.pp_decl d
-    | Gmodule (_loc, id, dl) ->
-        Format.eprintf "@[<hv 2>scope %s@\n%a@]@\nend@." id.id_str
-          (pp_list pp_decl) dl
-  in
-  pp_list pp_decl Format.err_formatter f;
   List.iter add_decl f;
   close_module Loc.dummy_position;
   let mm = close_file () in
diff --git a/tests/positive/dune b/tests/positive/dune
index 00defa8..7b2fa28 100644
--- a/tests/positive/dune
+++ b/tests/positive/dune
@@ -1,5 +1,3 @@
-(rule
- (alias runtest)
- (action
-  (with-accepted-exit-codes 0
-    (system "why3 prove %{dep:list_stdlib.mli}"))))
+(cram
+ (deps
+  (source_tree .)))
diff --git a/tests/positive/run.t b/tests/positive/run.t
new file mode 100644
index 0000000..b0cd251
--- /dev/null
+++ b/tests/positive/run.t
@@ -0,0 +1,29 @@
+  $ why3 config detect > /dev/null
+
+  $ why3 prove *.mli 
+  theory Sig
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use why3.Bool.Bool *)
+    
+    (* use why3.Unit.Unit *)
+    
+    (* use gospel.Stdlib *)
+    
+    type t 'a
+    
+    function view (t 'a) : bag 'a
+    
+    function to_bag (t:t 'a) : bag 'a = view t
+  end
+  
+  theory Sig1
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use why3.Bool.Bool *)
+    
+    (* use why3.Unit.Unit *)
+    
+    (* use gospel.Stdlib *)
+  end
+  
diff --git a/why3gospel.opam b/why3gospel.opam
index 842b905..2df66b2 100644
--- a/why3gospel.opam
+++ b/why3gospel.opam
@@ -23,7 +23,7 @@ build: [
 
 depends: [
   "ocaml" {>= "4.07"}
-  "dune" {>= "2.4.0"}
+  "dune" {>= "2.7.0"}
   "gospel"
   "why3" {>= "1.4.0"}
   "ppxlib" {>= "0.23.0"}
@@ -31,5 +31,5 @@ depends: [
 ]
 
 pin-depends: [
-  [ "gospel.dev" "git+https://github.com/ocaml-gospel/gospel#65587404d2167840bd5f09bbb9da29c49ee3fb83" ]
+  [ "gospel.dev" "git+https://github.com/ocaml-gospel/gospel#da93ff37b69fb0b0759c4a096b691e583fea0144" ]
 ]

From f834abeb041c604f3385683c385e7a2083aac809 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Tue, 9 Nov 2021 15:13:19 +0100
Subject: [PATCH 12/12] translate a larger part of Gospel stdlib

---
 src/gospel.mlw                | 274 +++++++++++++++++++++-------------
 tests/positive/arith.mli      |   6 +
 tests/positive/arrays.mli     |  24 +++
 tests/positive/bag_stdlib.mli |   7 +-
 tests/positive/run.t          |  27 +++-
 5 files changed, 230 insertions(+), 108 deletions(-)
 create mode 100644 tests/positive/arith.mli
 create mode 100644 tests/positive/arrays.mli

diff --git a/src/gospel.mlw b/src/gospel.mlw
index 35530bf..4cec100 100644
--- a/src/gospel.mlw
+++ b/src/gospel.mlw
@@ -25,6 +25,9 @@ module Stdlib
 
   scope Seq
     use export seq.Seq
+
+    type t 'a = seq 'a
+
     function init (i: int) (f: int -> 'a) : seq 'a = create i f
 
     use export seq.OfList
@@ -37,103 +40,8 @@ module Stdlib
   function ([.._]) (s: seq 'a) (i: integer): seq 'a = Seq.([.._]) s i
   function ([_..]) (s: seq 'a) (i: integer): seq 'a = Seq.([_..]) s i
 
-  scope Bag
-    use bag.Bag as B
-
-    type t 'a = B.bag 'a
-
-    function occurrences (x: 'a) (b: t 'a): integer =
-      B.nb_occ x b
-
-    (*@ function compare (b b': 'a t) : int *)
-
-    function empty : t 'a = B.empty_bag
-
-    predicate is_empty (b: t 'a) = b = empty
-
-    predicate mem (x: 'a) (b: t 'a) = B.mem x b
-
-    function add (x: 'a) (b: t 'a) : t 'a = B.add x b
-
-    function singleton (x: 'a) : t 'a = B.singleton x
-
-    function remove (x: 'a) (b: t 'a) : t 'a =
-      B.diff b (B.singleton x)
-
-    function union (b b': t 'a) : t 'a
-
-    axiom def_union:
-      forall x: 'a, b b': t 'a.
-      occurrences x (union b b') = max (occurrences x b) (occurrences x b')
-
-    function sum (b b': t 'a) : t 'a =
-      B.union b b'
-
-    function inter (b b': t 'a) : t 'a =
-      B.inter b b'
-
-    predicate disjoint (b b': t 'a) =
-      B.inter b b' = empty
-
-    function diff (b b': t 'a) : t 'a =
-      B.diff b b'
-
-    predicate subset (b b': t 'a) =
-      forall x. occurrences x b <= occurrences x b'
-
-    function choose (b: t 'a) : 'a =
-      B.choose b
-
-    function choose_opt (b: t 'a) : option 'a =
-      if b = empty then None else Some (choose b)
-
-    (*@ function map (f: 'a -> 'b) (b: t 'a) : t 'b *)
-
-    (*@ function fold (f: 'a -> 'b -> 'b) (b: t 'a) : 'b *)
-
-    (*@ predicate for_all (f: 'a -> bool) (b: t 'a) *)
-
-    (*@ predicate _exists (f: 'a -> bool) (b: t 'a) *)
-
-    (*@ function filter (f: 'a -> bool) (b: t 'a) : t 'a *)
-
-    (*@ function filter_map (f: 'a -> option 'a) (b: t 'a) : t 'a *)
-
-    (*@ function partition (f: 'a -> bool) (b: t 'a) : (t 'a * t 'a) *)
-
-    (*@ function cardinal (b: t 'a) : int *)
-
-    (*@ function elements (b: t 'a) : list 'a *)
-
-    (*@ function to_list (b: t 'a) : list 'a *)
-    function of_list (l: list 'a) : t 'a
-
-    (*@ function to_seq (b: t 'a) : Seq.t 'a *)
-    (*@ function of_seq (s: Seq.t 'a) : t 'a *)
-
-    (*@ function of_array (a: array 'a) : t 'a *)
-
-  end
-  type bag 'a = Bag.B.bag 'a
-
   use export ref.Ref
 
-  scope Array
-    use export mach.array.Array63
-
-    type t 'a = array 'a
-
-    function get (a : array 'a) (i: int) : 'a = a[i]
-
-    use mach.array.Array63Permut as P
-
-    predicate permut (a1 a2: array 'a) = P.permut_all a1 a2
-    predicate permut_sub (a1 a2: array 'a) (l u: int) = P.permut_sub a1 a2 l u
-
-    function to_seq (a: array 'a) : seq 'a = a.elts
-  end
-  type array 'a = Array.array 'a
-
   scope Set
     use import set.Fset as FS
 
@@ -171,11 +79,10 @@ module Stdlib
 
     function rev (l: t 'a) : t 'a = reverse l
 
-    (* FIXME? Should we provide pre-conditions for [init_aux] and [init] ? *)
+    (* the list [f i; f (i+1); ...; f (i+n-1)] *)
     let rec function init_aux (i n: integer) (f: integer -> 'a) : t 'a
-      variant { n - i }
-    = if i >= n then Nil
-      else Cons (f i) (init_aux (i + 1) n f)
+      variant { n }
+    = if n <= 0 then Nil else Cons (f i) (init_aux (i + 1) (n - 1) f)
 
     function init (n: integer) (f: integer -> 'a) : t 'a =
       init_aux 0 n f
@@ -245,22 +152,180 @@ module Stdlib
 
   end
 
+  scope Bag
+    use bag.Bag as B
+
+    type t 'a = B.bag 'a
+
+    function occurrences (x: 'a) (b: t 'a): integer =
+      B.nb_occ x b
+
+    (*@ function compare (b b': 'a t) : int *)
+
+    function empty : t 'a = B.empty_bag
+
+    predicate is_empty (b: t 'a) = b = empty
+
+    predicate mem (x: 'a) (b: t 'a) = B.mem x b
+
+    function add (x: 'a) (b: t 'a) : t 'a = B.add x b
+
+    function singleton (x: 'a) : t 'a = B.singleton x
+
+    function remove (x: 'a) (b: t 'a) : t 'a =
+      B.diff b (B.singleton x)
+
+    function union (b b': t 'a) : t 'a
+
+    axiom def_union:
+      forall x: 'a, b b': t 'a.
+      occurrences x (union b b') = max (occurrences x b) (occurrences x b')
+
+    function sum (b b': t 'a) : t 'a =
+      B.union b b'
+
+    function inter (b b': t 'a) : t 'a =
+      B.inter b b'
+
+    predicate disjoint (b b': t 'a) =
+      B.inter b b' = empty
+
+    function diff (b b': t 'a) : t 'a =
+      B.diff b b'
+
+    predicate subset (b b': t 'a) =
+      forall x. occurrences x b <= occurrences x b'
+
+    function choose (b: t 'a) : 'a =
+      B.choose b
+
+    function choose_opt (b: t 'a) : option 'a =
+      if b = empty then None else Some (choose b)
+
+    (* TODO give defs/axioms to the following *)
+    function map (f: 'a -> 'b) (b: t 'a) : t 'b
+
+    function fold (f: 'a -> 'b -> 'b) (b: t 'a) : 'b
+
+    predicate for_all (f: 'a -> bool) (b: t 'a)
+
+    predicate _exists (f: 'a -> bool) (b: t 'a)
+
+    function filter (f: 'a -> bool) (b: t 'a) : t 'a
+
+    function filter_map (f: 'a -> option 'a) (b: t 'a) : t 'a
+
+    function partition (f: 'a -> bool) (b: t 'a) : (t 'a, t 'a)
+
+    function cardinal (b: t 'a) : integer = B.card b
+
+    let rec ghost function to_list (b: t 'a) : list 'a
+      variant { cardinal b }
+    = if is_empty b then Nil
+      else let x = choose b in Cons x (to_list (remove x b))
+
+    function of_list (l: list 'a) : t 'a
+    = match l with Nil -> empty | Cons x l -> add x (of_list l) end
+
+    function to_seq (b: t 'a) : Seq.t 'a = Seq.of_list (to_list b)
+    function of_seq (s: Seq.t 'a) : t 'a = of_list (List.of_seq s)
+
+  end
+  type bag 'a = Bag.B.bag 'a
+
+  scope Array
+    use export mach.array.Array63
+
+    type t 'a = array 'a
+
+    function get (a: array 'a) (i: int) : 'a = a[i]
+
+    use mach.array.Array63Permut as P
+
+    function to_seq (a: array 'a) : seq 'a = a.elts
+
+    (*@ function make (n: integer) (x: 'a) : 'a t *)
+
+    (*@ function init (n: integer) (f: integer -> 'a) : 'a t *)
+
+    function append (a b: t 'a) : t 'a
+    axiom append_def:
+      forall a b: t 'a. to_seq (append a b) = to_seq a ++ to_seq b
+
+    (*@ function concat (a: 'a t list) : 'a t *)
+
+    function sub (a: t 'a) (i len: integer) : t 'a
+    axiom sub_def:
+      forall a: t 'a, i len. to_seq (sub a i len) = (to_seq a)[i..i+len]
+
+    (*@ function map (f: 'a -> 'b) (a: 'a t) : 'b t *)
+
+    (*@ function mapi (f: integer -> 'a -> 'b) (a: 'a t) : 'b t *)
+
+    (*@ function fold_left (f: 'a -> 'b -> 'a) (init: 'a) (a: 'b t) : 'a *)
+
+    (*@ function fold_right (f: 'b -> 'a -> 'a) (a: 'b t) (init: 'a) : 'a *)
+
+    (*@ function map2 (f: 'a -> 'b -> 'c) (a: 'a t) (b: 'b t) : 'c t *)
+
+    predicate for_all (f: 'a -> bool) (a: t 'a) =
+      forall i. 0 <= i < Seq.length a -> f a[i]
+
+    predicate _exists (f: 'a -> bool) (a: t 'a) =
+      exists i. 0 <= i < Seq.length a /\ f a[i]
+
+    (*@ predicate for_all2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t) *)
+
+    (*@ predicate _exists2 (f: 'a -> 'b -> bool) (a: 'a t) (b: 'b t) *)
+
+    (*@ predicate mem (x: 'a) (a: 'a t) *)
+
+    (*@ function to_list (a: 'a t) : 'a list *)
+    (*@ function of_list (l: 'a list) : 'a t *)
+
+    (*@ function of_seq (s: 'a Seq.t) : 'a t *)
+
+    (*@ function to_bag (a: 'a t) : 'a bag *)
+
+    predicate permut (a1 a2: array 'a) = P.permut_all a1 a2
+    predicate permut_sub (a1 a2: array 'a) (l u: int) = P.permut_sub a1 a2 l u
+
+  end
+  type array 'a = Array.array 'a
+
+  (* Arithmetic *)
+
   use int.ComputerDivision
-  function (/) (x y: int) : int = div x y
+  function (/) (x y: integer) : integer = div x y
 
   use int.Power as P
-  function pow (x y: int) : int = P.power x y
+  function pow (x y: integer) : integer = P.power x y
 
   use mach.int.Int63 as I
   type int63 = I.int63
-  function integer_of_int (x: int63) : int = I.to_int x
+  function integer_of_int (x: int63) : integer = I.to_int x
 
-  let constant max_int : int = I.max_int63
-  let constant min_int : int = I.min_int63
+  let constant max_int : integer = I.max_int63
+  let constant min_int : integer = I.min_int63
+
+  function succ (x: integer) : integer = [@inline:trivial] x+1
+  function pred (x: integer) : integer = [@inline:trivial] x-1
+
+  use export int.Abs
 
   function fst (x : ('a, 'b)) : 'a = let (f, _) = x in f
   function snd (x : ('a, 'b)) : 'b = let (_, s) = x in s
 
+  (* TODO give defs/axioms to the following *)
+  function logand (x y: integer) : integer
+  function logor (x y: integer) : integer
+  function logxor (x y: integer) : integer
+  function lognot (x: integer) : integer
+  function shift_left (x y: integer) : integer
+  function shift_right (x y: integer) : integer
+  function shift_right_trunc (x y: integer) : integer
+
+
   scope Order
     predicate is_pre_order (cmp: 'a -> 'a -> int63) =
       (forall x. cmp x x = 0) /\
@@ -276,6 +341,7 @@ module Stdlib
   scope Map
     use export map.Map
   end
+
 end
 
 module Comparable
diff --git a/tests/positive/arith.mli b/tests/positive/arith.mli
new file mode 100644
index 0000000..b79053f
--- /dev/null
+++ b/tests/positive/arith.mli
@@ -0,0 +1,6 @@
+val f1 : int -> int
+(*@ y = f1 x
+      requires x < max_int
+      requires abs x = x
+      ensures y = succ x
+      ensures y = pow x 42 *)
diff --git a/tests/positive/arrays.mli b/tests/positive/arrays.mli
new file mode 100644
index 0000000..bcd5d27
--- /dev/null
+++ b/tests/positive/arrays.mli
@@ -0,0 +1,24 @@
+val f1 : int array -> unit
+(*@ f1 a
+      requires Array.length a > 0
+      requires forall i. 0 <= i < Array.length a -> a.(i) >= 0
+      requires Array.for_all (fun x:int -> x >= 0) a
+      modifies a
+      ensures Array._exists (fun x:int -> x = 42) a
+*)
+
+val f2 : 'a array -> 'a array -> 'a array
+(*@ c = f2 a b
+     ensures c = Array.append a b *)
+
+val f3 : unit -> int array
+(*@ a = f3 ()
+     ensures Array.length a = 42
+     ensures Array.for_all (fun x:int -> x = 0) a *)
+
+val f4 : (int -> int) -> int array
+(*@ a = f4 f
+     ensures Array.length a = 42
+     ensures forall i:int. 0 <= i < Array.length a -> a.(i) = f i
+       (* Note: can't have i:integer here, since f expects an int *)
+*)
diff --git a/tests/positive/bag_stdlib.mli b/tests/positive/bag_stdlib.mli
index be89c77..d388199 100644
--- a/tests/positive/bag_stdlib.mli
+++ b/tests/positive/bag_stdlib.mli
@@ -4,8 +4,11 @@ type 'a t
 (*@ function to_bag (t: 'a t) : 'a bag = t.view *)
 (*@ coercion *)
 
-val f1 : 'a -> 'a t -> int
-(*@ r = f1 x t
+val f1 : int -> 'a -> 'a t -> int
+(*@ r = f1 a x t
+      requires a = 0
+      requires Bag.occurrences x t = 42
+      requires Bag.cardinal t = 42
       ensures r = Bag.occurrences x t *)
 
 val f2 : 'a t -> bool
diff --git a/tests/positive/run.t b/tests/positive/run.t
index b0cd251..4c350c1 100644
--- a/tests/positive/run.t
+++ b/tests/positive/run.t
@@ -1,6 +1,6 @@
   $ why3 config detect > /dev/null
 
-  $ why3 prove *.mli 
+  $ why3 prove bag_stdlib.mli
   theory Sig
     (* use why3.BuiltIn.BuiltIn *)
     
@@ -17,7 +17,30 @@
     function to_bag (t:t 'a) : bag 'a = view t
   end
   
-  theory Sig1
+  $ why3 prove list_stdlib.mli
+  theory Sig
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use why3.Bool.Bool *)
+    
+    (* use why3.Unit.Unit *)
+    
+    (* use gospel.Stdlib *)
+  end
+  
+  $ why3 prove arith.mli
+  theory Sig
+    (* use why3.BuiltIn.BuiltIn *)
+    
+    (* use why3.Bool.Bool *)
+    
+    (* use why3.Unit.Unit *)
+    
+    (* use gospel.Stdlib *)
+  end
+  
+  $ why3 prove arrays.mli
+  theory Sig
     (* use why3.BuiltIn.BuiltIn *)
     
     (* use why3.Bool.Bool *)