programs: avoid clashes between theories and modules

bench/programs/bad-typing/alias5.mlw

@@ -0,0 +1,14 @@
+module M
+
+  use import module ref.Ref
+
+  let foo (x : ref int) (y: ref int) =
+    x := 1;
+    y := 2
+
+  val r : ref int
+
+  let rec test () =
+    foo r r
+
+end

bench/programs/bad-typing/theory1.mlw

@@ -0,0 +1,8 @@
+(* a theory is not a module *)
+
+theory T
+end
+
+module M
+  use import module T
+end

bench/programs/bad-typing/theory2.mlw

@@ -0,0 +1,8 @@
+(* a module is not a theory *)
+
+module M
+end
+
+module M1
+  use import M
+end

src/parser/parser.mly

@@ -937,9 +937,9 @@ list1_theory_or_module_:
 
 theory_or_module_:
 | THEORY uident labels list0_full_decl END
-   { { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
+   { Ptheory { pth_name = add_lab $2 $3; pth_decl = $4; } }
 | MODULE uident labels list0_program_decl END
-   { { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
+   { Pmodule { mod_name = add_lab $2 $3; mod_decl = $4; } }
 ;
 
 list0_full_decl:

src/parser/ptree.ml

@@ -245,11 +245,19 @@ type program_decl =
   | Duse    of qualid * imp_exp * (*as:*) ident option
   | Dnamespace of loc * ident option * (* import: *) bool * program_decl list
 
+type theory = {
+  pth_name   : ident;
+  pth_decl   : program_decl list;
+}
+
 type module_ = {
   mod_name   : ident;
-  mod_labels : label list;
   mod_decl   : program_decl list;
 }
 
-type program_file = module_ list
+type theory_module =
+  | Ptheory of theory
+  | Pmodule of module_
+
+type program_file = theory_module list
 

src/programs/pgm_main.ml

@@ -24,6 +24,7 @@ open Why3
 open Util
 open Ident
 open Theory
+open Typing
 open Ptree
 open Pgm_module
 
@@ -33,6 +34,22 @@ let () = Exn_printer.register (fun fmt e -> match e with
   | ClashModule m -> fprintf fmt "clash with previous module %s" m
   | _ -> raise e)
 
+let add_theory env lenv m =
+  let id = m.pth_name in
+  let loc = id.id_loc in
+  let th = Theory.create_theory (Denv.create_user_id id) in
+  let rec add_decl th = function
+    | Dlogic d ->
+        Typing.add_decl env lenv th d
+    | Dnamespace (loc, name, import, dl) ->
+        let th = Theory.open_namespace th in
+        let th = List.fold_left add_decl th dl in
+        Typing.close_namespace loc import name th
+    | Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ -> assert false
+  in
+  let th = List.fold_left add_decl th m.pth_decl in
+  close_theory loc lenv th
+
 let add_module ?(type_only=false) env penv (ltm, lmod) m =
   let id = m.mod_name in
   let loc = id.id_loc in
@@ -44,9 +61,13 @@ let add_module ?(type_only=false) env penv (ltm, lmod) m =
   let uc =
     List.fold_left (Pgm_typing.decl ~wp env penv ltm lmod) uc m.mod_decl
   in
-  let m = close_module uc in
-  Mstr.add id.id m.m_pure ltm,
-  Mstr.add id.id m lmod
+  let md = close_module uc in
+  Mstr.add ("WP " ^ id.id) md.m_pure ltm, (* avoids a theory/module clash *)
+  Mstr.add id.id md lmod
+
+let add_theory_module ?(type_only=false) env penv (ltm, lmod) = function
+  | Ptheory t -> add_theory env ltm t, lmod
+  | Pmodule m -> add_module ~type_only env penv (ltm, lmod) m
 
 let retrieve penv file c =
   let lb = Lexing.from_channel c in
@@ -57,7 +78,7 @@ let retrieve penv file c =
   else
     let type_only = Debug.test_flag Typing.debug_type_only in
     let env = Pgm_env.get_env penv in
-    List.fold_left (add_module ~type_only env penv)
+    List.fold_left (add_theory_module ~type_only env penv)
       (Mstr.empty, Mstr.empty) ml
 
 let pgm_env_of_env =

src/programs/pgm_typing.ml

@@ -295,8 +295,8 @@ let rec dtype ~user env = function
       let mt = get_mtsymbol ts in
       let np = List.length p in
       if np <> a - mt.mt_regions then
-        errorm ~loc "@[the type %a expects %d argument(s),@
-                       but is applied to %d argument(s)@]"
+        errorm ~loc
+        "@[type %a expects %d argument(s),@ but is applied to %d argument(s)@]"
           print_qualid x (a - mt.mt_regions) np;
       let tyl = List.map (dtype ~user env) p in
       let tyl = create_regions ~user mt.mt_regions @ tyl in

tests/test-pgm-jcf.mlw

@@ -1,3 +1,11 @@
+theory M1
+  type t 'a = {| a : 'a |}
+end
+
+module M2
+  use import M1
+  let f (x: t int) = x.a
+end
 
 (*
 module MutualRec
@@ -15,28 +23,6 @@ module MutualRec
 end
 *)
 
-(*
-module PoorArrays
-
-  use import int.Int
-  use import module ref.Ref
-  use import map.Map as M
-
-  type array_contents 'a = {| length: int; elts : map int 'a |}
-  type array 'a = ref (array_contents 'a)
-
-  val get (a: array 'a) (i: int) :
-    { 0 <= i < length !a } 'a { result = M.get !a.elts i }
-
-  val set (a: array 'a) (i: int) (v: 'a) :
-    { 0 <= i < length !a }
-    unit writes a
-    { !a.length = !(old a).length && !a.elts = M.set !(old a).elts i v }
-
-end
-*)
-
-(*
 module M
 
   use import int.Int
@@ -60,8 +46,6 @@ module M
 (*   let test3 () = let x = ref 0 in begin foo x (); assert { !x = 0 } end *)
 
 end
-*)
-
 
 (*
 Local Variables: