store the qualifier prefix in Theory.theory.th_path

For built-in and local theories the prefix is empty.

src/core/env.ml

@@ -41,7 +41,7 @@ type find_channel = fformat -> pathname -> filename * in_channel
 
 type env = {
   env_find : find_channel;
-  env_memo : (string list, theory Mstr.t) Hashtbl.t;
+  env_memo : (pathname, theory Mstr.t) Hashtbl.t;
   env_tag  : Hashweak.tag;
 }
 
@@ -51,7 +51,8 @@ module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)
 
 (** Input formats *)
 
-type read_channel = env -> filename -> in_channel -> theory Mstr.t
+type read_channel =
+  env -> pathname -> filename -> in_channel -> theory Mstr.t
 
 let read_channel_table = Hashtbl.create 17 (* format name -> read_channel *)
 let extensions_table   = Hashtbl.create 17 (* suffix -> format name *)
@@ -76,12 +77,15 @@ let get_format file =
   try Hashtbl.find extensions_table ext
   with Not_found -> raise (UnknownExtension ext)
 
-let read_channel ?format env file ic =
+let real_read_channel ?format env path file ic =
   let name = match format with
     | Some name -> name
     | None -> get_format file in
   let rc,_ = lookup_format name in
-  rc env file ic
+  rc env path file ic
+
+let read_channel ?format env file ic =
+  real_read_channel ?format env [] file ic
 
 let read_file ?format env file =
   let ic = open_in file in
@@ -143,7 +147,7 @@ let find_library env sl =
   let file, ic = env.env_find "why" sl in
   try
     Hashtbl.replace env.env_memo sl Mstr.empty;
-    let mth = read_channel ~format:"why" env file ic in
+    let mth = real_read_channel ~format:"why" env sl file ic in
     Hashtbl.replace env.env_memo sl mth;
     close_in ic;
     mth

src/core/env.mli

@@ -44,7 +44,8 @@ exception TheoryNotFound of pathname * string
 
 open Theory
 
-type read_channel = env -> filename -> in_channel -> theory Util.Mstr.t
+type read_channel =
+  env -> pathname -> filename -> in_channel -> theory Util.Mstr.t
 (** a function of type [read_channel] parses a channel using
     its own syntax. The string argument indicates the origin of
     the stream (e.g. file name) to be used in error messages. *)
@@ -57,8 +58,9 @@ val register_format : fformat -> extension list -> read_channel -> unit
 
     @raise KnownFormat [name] if the format is already registered *)
 
-val read_channel : ?format:fformat -> read_channel
-(** [read_channel ?format env file ch] returns the theories in [ch].
+val read_channel :
+  ?format:fformat -> env -> filename -> in_channel -> theory Util.Mstr.t
+(** [read_channel ?format env path file ch] returns the theories in [ch].
     When given, [format] enforces the format, otherwise we choose
     the format according to [file]'s extension. Nothing ensures
     that [ch] corresponds to the contents of [f].

src/core/theory.ml

@@ -157,6 +157,7 @@ let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table []
 
 type theory = {
   th_name   : ident;      (* theory name *)
+  th_path   : string list;(* environment qualifiers *)
   th_decls  : tdecl list; (* theory declarations *)
   th_export : namespace;  (* exported namespace *)
   th_known  : known_map;  (* known identifiers *)
@@ -255,6 +256,7 @@ let td_hash td = td.td_tag
 
 type theory_uc = {
   uc_name   : ident;
+  uc_path   : string list;
   uc_decls  : tdecl list;
   uc_import : namespace list;
   uc_export : namespace list;
@@ -266,8 +268,9 @@ type theory_uc = {
 exception CloseTheory
 exception NoOpenedNamespace
 
-let empty_theory n = {
+let empty_theory n p = {
   uc_name   = id_register n;
+  uc_path   = p;
   uc_decls  = [];
   uc_import = [empty_ns];
   uc_export = [empty_ns];
@@ -279,6 +282,7 @@ let empty_theory n = {
 let close_theory uc = match uc.uc_export with
   | [e] -> {
       th_name   = uc.uc_name;
+      th_path   = uc.uc_path;
       th_decls  = List.rev uc.uc_decls;
       th_export = e;
       th_known  = uc.uc_known;
@@ -735,24 +739,25 @@ let on_meta _meta fn acc theory =
 (** Base theories *)
 
 let builtin_theory =
-  let uc = empty_theory (id_fresh "BuiltIn") in
+  let uc = empty_theory (id_fresh "BuiltIn") [] in
   let uc = add_ty_decl uc [ts_int, Tabstract] in
   let uc = add_ty_decl uc [ts_real, Tabstract] in
   let uc = add_logic_decl uc [ps_equ, None] in
   close_theory uc
 
 let highord_theory =
-  let uc = empty_theory (id_fresh "HighOrd") in
+  let uc = empty_theory (id_fresh "HighOrd") [] in
   let uc = add_ty_decl uc [ts_func, Tabstract] in
   let uc = add_ty_decl uc [ts_pred, Tabstract] in
   let uc = add_logic_decl uc [fs_func_app, None] in
   let uc = add_logic_decl uc [ps_pred_app, None] in
   close_theory uc
 
-let create_theory n = use_export (empty_theory n) builtin_theory
+let create_theory ?(path=[]) n =
+  use_export (empty_theory n path) builtin_theory
 
 let tuple_theory = Util.memo_int 17 (fun n ->
-  let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) in
+  let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) [] in
   let uc = add_ty_decl uc [ts_tuple n, Talgebraic [fs_tuple n]] in
   close_theory uc)
 

src/core/theory.mli

@@ -83,6 +83,7 @@ val list_metas  : unit -> meta list
 
 type theory = private {
   th_name   : ident;      (* theory name *)
+  th_path   : string list;(* environment qualifiers *)
   th_decls  : tdecl list; (* theory declarations *)
   th_export : namespace;  (* exported namespace *)
   th_known  : known_map;  (* known identifiers *)
@@ -118,7 +119,7 @@ val td_hash : tdecl -> int
 
 type theory_uc  (* a theory under construction *)
 
-val create_theory : preid -> theory_uc
+val create_theory : ?path:string list -> preid -> theory_uc
 val close_theory  : theory_uc -> theory
 
 val open_namespace  : theory_uc -> theory_uc

src/parser/lexer.mli

@@ -19,7 +19,8 @@
 
 (** parsing entry points *)
 
-val parse_logic_file : Env.env -> Lexing.lexbuf -> Theory.theory Util.Mstr.t
+val parse_logic_file :
+  Env.env -> string list -> Lexing.lexbuf -> Theory.theory Util.Mstr.t
 
 val parse_program_file : Lexing.lexbuf -> Ptree.program_file
 

src/parser/lexer.mll

@@ -314,16 +314,16 @@ and string = parse
       | Loc.Located _ as e -> raise e
       | e -> raise (Loc.Located (loc lb, e))
 
-  let parse_logic_file env lb =
-    pre_logic_file token (Lexing.from_string "") env;
+  let parse_logic_file env path lb =
+    pre_logic_file token (Lexing.from_string "") env path;
     with_location (logic_file token) lb
 
   let parse_program_file = with_location (program_file token)
 
-  let read_channel env file c =
+  let read_channel env path file c =
     let lb = Lexing.from_channel c in
     Loc.set_file file lb;
-    parse_logic_file env lb
+    parse_logic_file env path lb
 
   let () = Env.register_format "why" ["why"] read_channel
 }

src/parser/parser.mly

@@ -22,6 +22,7 @@ module Incremental = struct
   let env_ref  = ref []
   let lenv_ref = ref []
   let uc_ref   = ref []
+  let path_ref = ref []
 
   let ref_get  ref = List.hd !ref
   let ref_tail ref = List.tl !ref
@@ -31,14 +32,19 @@ module Incremental = struct
   let ref_push ref v = ref := v :: !ref
   let ref_set  ref v = ref := v :: ref_tail ref
 
-  let open_logic_file env =
-    ref_push env_ref env; ref_push lenv_ref Util.Mstr.empty
+  let open_logic_file env path =
+    ref_push env_ref env;
+    ref_push path_ref path;
+    ref_push lenv_ref Util.Mstr.empty
 
   let close_logic_file () =
-    ref_drop env_ref; ref_pop lenv_ref
+    ref_drop path_ref;
+    ref_drop env_ref;
+    ref_pop lenv_ref
 
   let open_theory id =
-    ref_push uc_ref (Theory.create_theory (Denv.create_user_id id))
+    let path = ref_get path_ref in
+    ref_push uc_ref (Theory.create_theory ~path (Denv.create_user_id id))
 
   let close_theory loc =
     let uc = ref_pop uc_ref in
@@ -252,7 +258,7 @@ end
 
 /* Entry points */
 
-%type <Env.env -> unit> pre_logic_file
+%type <Env.env -> string list -> unit> pre_logic_file
 %start pre_logic_file
 %type <Theory.theory Util.Mstr.t> logic_file
 %start logic_file

src/programs/pgm_env.ml

@@ -30,7 +30,7 @@ type t = {
   memo     : (string list, module_file) Hashtbl.t;
 }
 
-and retrieve_module = t -> string -> in_channel -> module_file
+and retrieve_module = t -> string list -> string -> in_channel -> module_file
 
 let get_env penv = penv.env
 
@@ -48,7 +48,7 @@ let find_library penv sl =
   with Not_found ->
     Hashtbl.add penv.memo sl (Mstr.empty, Mstr.empty);
     let file, c = Env.find_channel penv.env "whyml" sl in
-    let r = penv.retrieve penv file c in
+    let r = penv.retrieve penv sl file c in
     close_in c;
     Hashtbl.replace penv.memo sl r;
     r

src/programs/pgm_env.mli

@@ -27,7 +27,7 @@ val get_env : t -> Env.env
 
 type module_file = Theory.theory Util.Mstr.t * Pgm_module.t Util.Mstr.t
 
-type retrieve_module = t -> string -> in_channel -> module_file
+type retrieve_module = t -> string list -> string -> in_channel -> module_file
 
 val create : Env.env -> retrieve_module -> t
 

src/programs/pgm_main.ml

@@ -34,10 +34,10 @@ 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 add_theory env path 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 th = Theory.create_theory ~path (Denv.create_user_id id) in
   let rec add_decl th = function
     | Dlogic d ->
         Typing.add_decl env lenv th d
@@ -50,12 +50,12 @@ let add_theory env lenv m =
   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 add_module ?(type_only=false) env penv path (ltm, lmod) m =
   let id = m.mod_name in
   let loc = id.id_loc in
   if Mstr.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 uc = create_module ~path (Ident.id_user id.id loc) in
   let prelude = Env.find_theory env ["bool"] "Bool" in
   let uc = use_export_theory uc prelude in
   let uc =
@@ -65,11 +65,11 @@ let add_module ?(type_only=false) env penv (ltm, lmod) m =
   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 add_theory_module ?(type_only=false) env penv path (ltm, lmod) = function
+  | Ptheory t -> add_theory env path ltm t, lmod
+  | Pmodule m -> add_module ~type_only env penv path (ltm, lmod) m
 
-let retrieve penv file c =
+let retrieve penv path file c =
   let lb = Lexing.from_channel c in
   Loc.set_file file lb;
   let ml = Lexer.parse_program_file lb in
@@ -78,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_theory_module ~type_only env penv)
+    List.fold_left (add_theory_module ~type_only env penv path)
       (Mstr.empty, Mstr.empty) ml
 
 let pgm_env_of_env =
@@ -91,9 +91,9 @@ let pgm_env_of_env =
       Env.Wenv.set h env penv;
       penv
 
-let read_channel env file c =
+let read_channel env path file c =
   let penv = pgm_env_of_env env in
-  let tm, _ = retrieve penv file c in
+  let tm, _ = retrieve penv path file c in
   tm
 
 let () = Env.register_format "whyml" ["mlw"] read_channel

src/programs/pgm_module.ml

@@ -193,13 +193,13 @@ let th_prelude =
   let uc = add_logic_decl uc [fs_old, None] in
   close_theory uc
 
-let empty_module n =
+let empty_module path n =
   let m = {
-    uc_name = id_register n;
-    uc_impure = Theory.create_theory n;
-    uc_effect = Theory.create_theory n;
-    uc_pure = Theory.create_theory n;
-    uc_decls = [];
+    uc_name   = id_register n;
+    uc_impure = Theory.create_theory ~path n;
+    uc_effect = Theory.create_theory ~path n;
+    uc_pure   = Theory.create_theory ~path n;
+    uc_decls  = [];
     uc_import = [empty_ns];
     uc_export = [empty_ns]; }
   in
@@ -267,8 +267,8 @@ let use_export_theory uc th =
   in
   add_ns th.th_export uc
 
-let create_module id =
-  let uc = empty_module id in
+let create_module ?(path=[]) id =
+  let uc = empty_module path id in
   use_export_theory uc th_prelude
 
 let add_impure_pdecl env ltm d uc =

src/programs/pgm_module.mli

@@ -51,7 +51,7 @@ type t = private {
   m_export : namespace;
 }
 
-val create_module : preid -> uc
+val create_module : ?path:string list -> preid -> uc
 val close_module : uc -> t
 
 val open_namespace  : uc -> uc

src/tptp2why/tptp2whymain.ml

@@ -69,13 +69,13 @@ end = struct
     TptpParser.tptp TptpLexer.token lb
 
 
-  let read_channel _env file c =
+  let read_channel _env path file c =
     let decls = getDeclsFromChan c in
     if Debug.test_flag Typing.debug_parse_only ||
        Debug.test_flag Typing.debug_type_only
     then Util.Mstr.empty
     else
-      let my_theory = theory_of_decls file decls in
+      let my_theory = theory_of_decls path file decls in
       Util.Mstr.add "Tptp" my_theory Util.Mstr.empty
 
 end

src/tptp2why/tptpTranslate.ml

@@ -298,8 +298,8 @@ module Translate = struct
 
 
   (** from a list of untyped declarations, translates them into a why theory *)
-  let theory_of_decls theoryName decls =
-    let theory = Theory.create_theory (Ident.id_fresh theoryName) in
+  let theory_of_decls path theoryName decls =
+    let theory = Theory.create_theory ~path (Ident.id_fresh theoryName) in
     let theory = Theory.add_ty_decl theory [ts, Decl.Tabstract] in
     let theory = S.fold addAtomForwardDecl (Summary.findAllAtoms decls) theory in
     (* Format.eprintf "atoms forward decls finished.@."; *)

src/tptp2why/tptpTranslate.mli

@@ -19,5 +19,6 @@
 (**************************************************************************)
 
 
-val theory_of_decls : string -> TptpTree.decl list -> Why3.Theory.theory
+val theory_of_decls :
+  string list -> string -> TptpTree.decl list -> Why3.Theory.theory