Missing functions from Gospel Stdlib in [gospel.mlw]

dune-project

@@ -1,3 +1,4 @@
-(lang dune 2.4)
+(lang dune 2.7)
 (name why3gospel)
 (implicit_transitive_deps false)
+(cram enable)

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 sexplib0 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)

src/gospel.mlw

@@ -25,36 +25,23 @@ 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
   end
   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
-
-  scope Bag
-    use export bag.Bag
-  end
-  type bag 'a = Bag.bag 'a
+  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
 
   use export ref.Ref
 
-  scope Array
-    use export mach.array.Array63
-    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
-  end
-  type array 'a = Array.array 'a
-
   scope Set
     use import set.Fset as FS
 
@@ -72,22 +59,273 @@ module Stdlib
   end
   type set 'a = Set.FS.fset 'a
 
+  scope List
+
+    use export list.Length
+    use export list.HdTlNoOpt
+    use list.NthNoOpt as LNth
+    use list.Nth as LNthOpt
+    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 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 = reverse l
+
+    (* 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 }
+    = 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
+
+    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
+
+  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 : 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
 
-  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
 
+  (* 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) /\
@@ -103,6 +341,7 @@ module Stdlib
   scope Map
     use export map.Map
   end
+
 end
 
 module Comparable

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 =