programs: very first tests with modules

Makefile.in

@@ -282,7 +282,7 @@ PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
 	       src/programs/pgm_lexer.ml
 
 PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
-	    pgm_types pgm_module pgm_typing # pgm_env pgm_wp pgm_main
+	    pgm_types pgm_module pgm_typing pgm_main # pgm_env pgm_wp
 
 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 
@@ -683,9 +683,12 @@ test: bin/why.byte $(TOOLS)
 	@for i in output_coq/*.v; do printf "coq $$i\\n" && coqc $$i ; done
 
 testl: bin/whyml.byte
-	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
+	ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
 	ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
 
+testl-debug: bin/whyml.byte
+	ocamlrun -bt bin/whyml.byte --debug-all tests/test-pgm-jcf.mlw
+
 testl-ide: bin/whyide.opt
 	bin/whyide.opt tests/test-pgm-jcf.mlw
 

bin/.gitignore

 whybench.opt
+whybench.byte

share/emacs/why.el

@@ -30,7 +30,7 @@
    ;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
    '("{\\([^}]*\\)}" . font-lock-type-face)
    `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type")) . font-lock-builtin-face)
-   `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses")) . font-lock-keyword-face)
+   `(,(why-regexp-opt '("and" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face)
    ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
    )
   "Minimal highlighting for Why mode")

src/programs/pgm_main.ml

@@ -21,35 +21,37 @@
 
 open Format
 open Why
-open Pgm_env
+open Ptree
+open Pgm_ptree
+open Pgm_module
 
-let type_and_wp ?(type_only=false) env gl dl =
-  let decl gl d = if type_only then gl else Pgm_wp.decl gl d in
-  let add gl d =
-    let gl, dl = Pgm_typing.decl env gl d in
-    List.fold_left decl gl dl
-  in
-  List.fold_left add gl dl
+let add_module ?(type_only=false) env tm m =
+  ignore (type_only);
+  let id = m.mod_name in
+  let uc = create_module (Ident.id_user id.id id.id_loc) in
+  let _uc = List.fold_left (Pgm_typing.decl env) uc m.mod_decl in
+  tm
 
 let read_channel env file c =
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
-  let dl = Pgm_lexer.parse_file lb in
+  let ml = Pgm_lexer.parse_file lb in
   if Debug.test_flag Typing.debug_parse_only then
     Theory.Mnm.empty
   else begin
     let type_only = Debug.test_flag Typing.debug_type_only in
-    let uc = Theory.create_theory (Ident.id_fresh "Pgm") in
-    let th = Env.find_theory env ["programs"] "Prelude" in
-    let uc = Theory.use_export uc th in
-    let gl = empty_env uc in
-    let gl = type_and_wp ~type_only env gl dl in
-    if type_only then
-      Theory.Mnm.empty
-    else begin
-      let th = Theory.close_theory gl.uc in
-      Theory.Mnm.add "Pgm" th Theory.Mnm.empty
-    end
+    List.fold_left (add_module ~type_only env) Theory.Mnm.empty ml
+  (*   let uc = Theory.create_theory (Ident.id_fresh "Pgm") in *)
+  (*   let th = Env.find_theory env ["programs"] "Prelude" in *)
+  (*   let uc = Theory.use_export uc th in *)
+  (*   let gl = empty_env uc in *)
+  (*   let gl = type_and_wp ~type_only env gl dl in *)
+  (*   if type_only then *)
+  (*     Theory.Mnm.empty *)
+  (*   else begin *)
+  (*     let th = Theory.close_theory gl.uc in *)
+  (*     Theory.Mnm.add "Pgm" th Theory.Mnm.empty *)
+  (*   end *)
   end
 
 let () = Env.register_format "whyml" ["mlw"] read_channel

src/programs/pgm_module.ml

@@ -77,10 +77,18 @@ type uc = {
 let namespace uc = List.hd uc.uc_import
 let theory_uc uc = uc.uc_th
 
+let add_pervasives uc =
+  (* type unit = () *)
+  let ts = 
+    Ty.create_tysymbol (id_fresh "unit") [] (Some (Ty.ty_app (Ty.ts_tuple 0) []))
+  in
+  add_ty_decl uc [ts, Decl.Tabstract]
+
 let create_module n =
   let uc = Theory.create_theory n in
   (* let th = Env.find_theory env ["programs"] "Prelude" in *)
   (* let uc = Theory.use_export uc th in *)
+  let uc = add_pervasives uc in
   { uc_name = id_register n;
     uc_th = uc;
     uc_decls = [];

src/programs/pgm_typing.ml

@@ -68,7 +68,7 @@ let find_ls uc s = ns_find_ls (get_namespace (theory_uc uc)) [s]
 (* TODO: improve efficiency *)
 let dty_bool uc = dty_app (find_ts uc "bool", [])
 let dty_int _uc = dty_app (Ty.ts_int, [])
-let dty_unit uc = dty_app (find_ts uc "unit", [])
+let dty_unit _uc = dty_app (ts_tuple 0, [])
 let dty_label uc = dty_app (find_ts uc "label", [])
 
 (* note: local variables are simultaneously in locals (to type programs)
@@ -397,7 +397,7 @@ and dexpr_desc env loc = function
       let bl = List.map branch bl in
       DEmatch (e1, bl), ty
   | Pgm_ptree.Eskip ->
-      DElogic (find_ls env.uc "Tuple0"), dty_unit env.uc
+      DElogic (fs_tuple 0), dty_unit env.uc
   | Pgm_ptree.Eabsurd ->
       DEabsurd, create_type_var loc
   | Pgm_ptree.Eraise (id, e) ->
@@ -600,8 +600,11 @@ let make_logic_app gl loc ty ls el =
   in
   make [] el
 
+let is_ts_ref gl ts =
+  try ts_equal ts (find_ts gl "ref") with Not_found -> false
+
 let is_reference_type gl ty  = match ty.ty_node with
-  | Ty.Tyapp (ts, _) -> Ty.ts_equal ts (find_ts gl "ref")
+  | Ty.Tyapp (ts, _) -> is_ts_ref gl ts
   | _ -> false
 
 (* same thing, but for an abritrary expression f (not an application)
@@ -686,7 +689,7 @@ and iexpr_desc gl env loc ty = function
       IEletrec (dl, e1)
 
   | DEsequence (e1, e2) ->
-      let vs = create_vsymbol (id_fresh "_") (ty_app (find_ts gl "unit") []) in
+      let vs = create_vsymbol (id_fresh "_") (ty_app (ts_tuple 0) []) in
       IElet (vs, iexpr gl env e1, iexpr gl env e2)
   | DEif (e1, e2, e3) ->
       IEif (iexpr gl env e1, iexpr gl env e2, iexpr gl env e3)
@@ -916,7 +919,7 @@ let mk_true  loc gl = mk_bool_constant loc gl (find_ls gl "True")
 let rec check_type ?(noref=false) gl loc ty = match ty.ty_node with
   | Ty.Tyapp (ts, tyl) when ts_equal ts ts_arrow ->
       List.iter (check_type gl loc) tyl
-  | Ty.Tyapp (ts, _) when noref && ts_equal ts (find_ts gl "ref") ->
+  | Ty.Tyapp (ts, _) when noref && is_ts_ref gl ts ->
       errorm ~loc "inner reference types are not allowed"
   | Ty.Tyapp (_, tyl) ->
       List.iter (check_type ~noref:true gl loc) tyl
@@ -947,7 +950,7 @@ let saturation loc ef (a,al) =
   in
   (a, List.map set_post (Sls.elements xs))
 
-let type_v_unit env = tpure (ty_app (find_ts env "unit") [])
+let type_v_unit _env = tpure (ty_app (ts_tuple 0) [])
 
 (* [expr] translates iexpr into expr
    [env : type_v Mvs.t] maps local variables to their types *)
@@ -1290,8 +1293,7 @@ let rec polymorphic_pure_type ty = match ty.ty_node with
   | Ty.Tyapp (_, tyl) -> List.exists polymorphic_pure_type tyl
 
 let cannot_be_generalized gl = function
-  | Tpure { ty_node = Ty.Tyapp (ts, [ty]) } 
-    when ts_equal ts (find_ts gl "ref") ->
+  | Tpure { ty_node = Ty.Tyapp (ts, [ty]) } when is_ts_ref gl ts ->
       polymorphic_pure_type ty
   | Tpure { ty_node = Ty.Tyvar _ } ->
       true
@@ -1332,7 +1334,7 @@ let decl env uc = function
       if cannot_be_generalized uc tyv then errorm ~loc "cannot be generalized";
       let ps, uc = add_global loc id.id tyv uc in
       let uc = add_global_if_pure uc ps in
-      add_decl (Dparam (ps, tyv)) uc
+      add_decl (Dparam (ps, tyv)) uc (* TODO: is it really needed? *)
   | Pgm_ptree.Dexn (id, ty) ->
       let ty = option_map (type_type uc) ty in
       add_exception id.id_loc id.id ty uc

tests/test-pgm-jcf.mlw

 
-(* for loop with invariant *)
-let test () =
-  let x = ref 0 in
-  for i = 1 to 10 do
-    invariant { !x = i-1 }
-    x := !x + 1
-  done;
-  assert { !x = 10 }
+module P
 
-(* we don't even enter *)
-let test2 () =
-  let x = ref 0 in
-  for i = 2 to 1 do
-    x := 1
-  done;
-  assert { !x = 0 }
+  { use import list.List }
 
-exception E
+  parameter x : list int
 
-(* the body raises an exception (for sure)
-   subtle: the invariant is required *)
-let test3 () =
-  { }
-  for i = 1 to 10 do invariant { i >= 2 -> false }
-    raise E
-  done
-  { false } | E -> { true }
+  let f (x : unit) = ()
 
-(* the body may raise an exception *)
-let test4 x =
-  { }
-  try
-    for i = 0 to 10 do
-      invariant { x < 0 or x >= i }
-      if i = x then raise E
-    done;
-    False
-  with E ->
-    True
-  end
-  { result=True <-> 0 <= x <= 10 }
-  
+end
 
 (*
 Local Variables: