tests: run why3 config

dune-project

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

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

src/trans.ml

@@ -327,7 +327,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 = [];
@@ -396,17 +397,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 =

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

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

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
+  

why3gospel.opam

@@ -23,13 +23,13 @@ build: [
 
 depends: [
   "ocaml" {>= "4.07"}
-  "dune" {>= "2.4.0"}
+  "dune" {>= "2.7.0"}
   "gospel"
   "why3" {>= "1.4.0"}
   "ppxlib" {>= "0.23.0"}
   "ocaml-compiler-libs"
 ]
 
 pin-depends: [
-  [ "gospel.dev" "git+https://github.com/ocaml-gospel/gospel#65587404d2167840bd5f09bbb9da29c49ee3fb83" ]
+  [ "gospel.dev" "git+https://github.com/ocaml-gospel/gospel#da93ff37b69fb0b0759c4a096b691e583fea0144" ]
 ]