programs: theories local to .mlw files

src/parser/parser.pre.mly

@@ -838,28 +838,51 @@ bar_:
 /****************************************************************************/
 
 program_file:
-| list0_module_ EOF { $1 }
+| list0_theory_or_module_ EOF { $1 }
 ;
 
-list0_module_:
+list0_theory_or_module_:
 | /* epsilon */
    { [] }
-| list1_module_
+| list1_theory_or_module_
    { $1 }
 ;
 
-list1_module_:
-| module_
+list1_theory_or_module_:
+| theory_or_module_
    { [$1] }
-| module_ list1_module_
+| theory_or_module_ list1_theory_or_module_
    { $1 :: $2 }
 ;
 
-module_:
+theory_or_module_:
+| THEORY uident labels list0_full_decl END
+   { { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
 | MODULE uident labels list0_program_decl END
    { { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
 ;
 
+list0_full_decl:
+| /* epsilon */
+   { [] }
+| list1_full_decl
+   { $1 }
+;
+
+list1_full_decl:
+| full_decl
+   { [$1] }
+| full_decl list1_full_decl
+   { $1 :: $2 }
+;
+
+full_decl:
+| NAMESPACE namespace_import namespace_name list0_full_decl END
+   { Dnamespace (loc_i 3, $3, $2, $4) }
+| decl
+   { Dlogic $1 }
+;
+
 list0_program_decl:
 | /* epsilon */
    { [] }
@@ -891,8 +914,8 @@ program_decl:
     { Dexn (add_lab $2 $3, Some $4) }
 | USE use_module
     { $2 }
-| NAMESPACE namespace_import uident list0_program_decl END
-    { Dnamespace ($3, $2, $4) }
+| NAMESPACE namespace_import namespace_name list0_program_decl END
+    { Dnamespace (loc_i 3, $3, $2, $4) }
 | ABSTRACT TYPE lident type_args model
     { Dmodel_type (false, $3, $4, $5) }
 | MUTABLE TYPE lident type_args model

src/parser/ptree.ml

@@ -229,7 +229,7 @@ type program_decl =
   | Dexn    of ident * pty option
   (* modules *)
   | Duse    of qualid * imp_exp * (*as:*) ident option
-  | Dnamespace of ident * (* import: *) bool * program_decl list
+  | Dnamespace of loc * ident option * (* import: *) bool * program_decl list
   | Dmodel_type of bool * ident * ident list * pty option
 
 type module_ = {

src/programs/pgm_env.ml

@@ -18,15 +18,18 @@
 (**************************************************************************)
 
 open Why
+open Theory
 open Pgm_module
 
+type module_file = Theory.theory Mnm.t * Pgm_module.t Mnm.t
+
 type t = {
   env      : Env.env;
   retrieve : retrieve_module;
-  memo     : (string list, Pgm_module.t Mnm.t) Hashtbl.t;
+  memo     : (string list, module_file) Hashtbl.t;
 }
 
-and retrieve_module = t -> string -> in_channel -> Pgm_module.t Mnm.t
+and retrieve_module = t -> string -> in_channel -> module_file
 
 let get_env penv = penv.env
 
@@ -44,15 +47,16 @@ let rec add_suffix = function
   | p :: f -> p :: add_suffix f
 
 let find_library penv sl =
-  try Hashtbl.find penv.memo sl
+  try 
+    Hashtbl.find penv.memo sl
   with Not_found ->
-    Hashtbl.add penv.memo sl Mnm.empty;
+    Hashtbl.add penv.memo sl (Mnm.empty, Mnm.empty);
     let file, c = Env.find_channel penv.env (add_suffix sl) in
-    let m = penv.retrieve penv file c in
+    let r = penv.retrieve penv file c in
     close_in c;
-    Hashtbl.replace penv.memo sl m;
-    m
+    Hashtbl.replace penv.memo sl r;
+    r
 
 let find_module penv sl s =
-  try Mnm.find s (find_library penv sl)
+  try Mnm.find s (snd (find_library penv sl))
   with Not_found -> raise (ModuleNotFound (sl, s))

src/programs/pgm_env.mli

@@ -18,13 +18,16 @@
 (**************************************************************************)
 
 open Why
+open Theory
 open Pgm_module
 
 type t
 
 val get_env : t -> Env.env
 
-type retrieve_module = t -> string -> in_channel -> Pgm_module.t Mnm.t
+type module_file = Theory.theory Mnm.t * Pgm_module.t Mnm.t
+
+type retrieve_module = t -> string -> in_channel -> module_file
 
 val create : Env.env -> retrieve_module -> t
 

src/programs/pgm_main.ml

@@ -23,17 +23,29 @@ open Format
 open Why
 open Util
 open Ident
+open Theory
 open Ptree
 open Pgm_module
 
-let add_module ?(type_only=false) env penv lmod m =
-  let wp = not type_only in
+exception ClashModule of string
+
+let () = Exn_printer.register (fun fmt e -> match e with
+  | ClashModule m -> fprintf fmt "clash with previous module %s" m
+  | _ -> raise e)
+
+let add_module ?(type_only=false) env penv (ltm, lmod) m =
   let id = m.mod_name in
-  let uc = create_module (Ident.id_user id.id id.id_loc) in
+  let loc = id.id_loc in
+  if Mnm.mem id.id lmod then raise (Loc.Located (loc, ClashModule id.id));
+  let wp = not type_only in
+  let uc = create_module (Ident.id_user id.id loc) in
   let prelude = Env.find_theory env ["programs"] "Prelude" in
   let uc = use_export_theory uc prelude in
-  let uc = List.fold_left (Pgm_typing.decl ~wp env penv lmod) uc m.mod_decl in
+  let uc = 
+    List.fold_left (Pgm_typing.decl ~wp env penv ltm lmod) uc m.mod_decl 
+  in
   let m = close_module uc in
+  Mnm.add id.id m.m_th ltm,
   Mnm.add id.id m lmod
 
 let retrieve penv file c =
@@ -41,11 +53,12 @@ let retrieve penv file c =
   Loc.set_file file lb;
   let ml = Lexer.parse_program_file lb in
   if Debug.test_flag Typing.debug_parse_only then
-    Mnm.empty
+    Mnm.empty, Mnm.empty
   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) Mnm.empty ml
+    List.fold_left (add_module ~type_only env penv) 
+      (Mnm.empty, Mnm.empty) ml
 
 let pgm_env_of_env =
   let h = Env.Wenv.create 17 in
@@ -59,10 +72,8 @@ let pgm_env_of_env =
 
 let read_channel env file c =
   let penv = pgm_env_of_env env in
-  let mm = retrieve penv file c in
-  Mnm.fold 
-    (fun _ m tm -> Theory.Mnm.add m.m_name.id_string m.m_th tm) 
-    mm Theory.Mnm.empty
+  let tm, _ = retrieve penv file c in
+  tm
 
 let () = Env.register_format "whyml" ["mlw"] read_channel
 

src/programs/pgm_module.ml

@@ -9,8 +9,6 @@ open Pgm_types
 open Pgm_types.T
 open Pgm_ttree
 
-module Mnm = Mstr
-
 type namespace = {
   ns_pr : psymbol   Mnm.t;  (* program symbols *)
   ns_ex : esymbol   Mnm.t;  (* exceptions*)
@@ -182,8 +180,8 @@ let use_export uc m =
 let use_export_theory uc th =
   { uc with uc_th = Theory.use_export uc.uc_th th }
 
-let add_logic_pdecl env d uc =
-  { uc with uc_th = Typing.add_decl env Theory.Mnm.empty  uc.uc_th d }
+let add_logic_pdecl env ltm d uc =
+  { uc with uc_th = Typing.add_decl env ltm uc.uc_th d }
 
 
 

src/programs/pgm_module.mli

@@ -2,11 +2,10 @@
 open Why
 open Ident
 open Term
+open Theory
 open Pgm_types
 open Pgm_types.T
 
-module Mnm : Map.S with type key = string
-
 type namespace = private {
   ns_pr : psymbol   Mnm.t;  (* program symbols *)
   ns_ex : esymbol   Mnm.t;  (* exception symbols *)
@@ -52,7 +51,8 @@ val add_mtsymbol : mtsymbol -> uc -> uc
 val add_decl : Pgm_ttree.decl -> uc -> uc
 val add_logic_decl : Decl.decl -> uc -> uc
 
-val add_logic_pdecl : Env.env -> Ptree.decl -> uc -> uc
+val add_logic_pdecl : 
+  Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc
 
 (** exceptions *)
 

src/programs/pgm_typing.ml

@@ -1524,9 +1524,9 @@ let find_module penv lmod q id = match q with
 (* env = to retrieve theories from the loadpath
    penv = to retrieve modules from the loadpath
    lmod = local modules *)
-let rec decl ~wp env penv lmod uc = function
+let rec decl ~wp env penv ltm lmod uc = function
   | Ptree.Dlogic d ->
-      Pgm_module.add_logic_pdecl env d uc
+      Pgm_module.add_logic_pdecl env ltm d uc
   | Ptree.Dlet (id, e) ->
       let e = type_expr uc e in
       if Debug.test_flag debug then
@@ -1598,11 +1598,11 @@ let rec decl ~wp env penv lmod uc = function
       with ClashSymbol s -> 
 	errorm ~loc "clash with previous symbol %s" s
       end
-  | Ptree.Dnamespace (id, import, dl) ->
-      let loc = id.id_loc in
+  | Ptree.Dnamespace (loc, id, import, dl) ->
       let uc = open_namespace uc in
-      let uc = List.fold_left (decl ~wp env penv lmod) uc dl in
-      begin try close_namespace uc import (Some id.id)
+      let uc = List.fold_left (decl ~wp env penv ltm lmod) uc dl in
+      let id = option_map (fun id -> id.id) id in
+      begin try close_namespace uc import id
       with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
   | Ptree.Dmodel_type (mut, id, args, model) ->
       let loc = id.id_loc in

src/programs/pgm_typing.mli

@@ -23,5 +23,7 @@ open Util
 val debug : Debug.flag
 
 val decl : 
-  wp:bool -> Env.env -> Pgm_env.t -> Pgm_module.t Pgm_module.Mnm.t -> 
+  wp:bool -> Env.env -> Pgm_env.t -> 
+  Theory.theory Theory.Mnm.t -> 
+  Pgm_module.t Theory.Mnm.t -> 
   Pgm_module.uc -> Ptree.program_decl -> Pgm_module.uc

tests/test-pgm-jcf.mlw

 
-(* theory T *)
-(*   type t *)
-(* end *)
+theory A
+  type t
+end
 
 module P
 
+  use import module A
   use import int.Int
   use import module stdlib.Array
 
+  logic c : int
+
   let foo (t : array int) = 
-    { A.length t >= 1 && t[0] = 1 }
+    { length t >= 1 && t[0] = 1 }
     t[0 <- 1];
     t[0] + 3
     { result = 3 }
 
 end
 
+
 (*
 Local Variables: 
 compile-command: "unset LANG; make -C .. testl-ide"