merge of the branch 'modules'

.gitignore

@@ -10,6 +10,7 @@ why.conf
 *.cmo
 *.cmi
 *.cmxs
+*.annot
 \#*\#
 
 # /

Makefile.in

@@ -283,8 +283,8 @@ install_no_local::
 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_env pgm_typing pgm_wp pgm_main
+PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer \
+	    pgm_types pgm_module pgm_wp pgm_env pgm_typing pgm_main
 
 PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
 
@@ -729,9 +729,12 @@ test: bin/why.byte plugins.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

examples/use_api.ml

@@ -84,7 +84,7 @@ let alt_ergo : Whyconf.config_prover =
     exit 0
 
 (* builds the environment from the [loadpath] *)
-let env : Env.env = Env.create_env (Lexer.retrieve (Whyconf.loadpath main)) 
+let env : Env.env = Lexer.create_env (Whyconf.loadpath main)
 (* loading the Alt-Ergo driver *)
 let alt_ergo_driver : Driver.driver = Driver.load_driver env alt_ergo.Whyconf.driver
 

share/emacs/why.el

@@ -29,8 +29,8 @@
    ;; Note: comment font-lock is guaranteed by suitable syntax entries
    ;; '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . 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 '("use" "clone" "namespace" "import" "export" "inductive" "external" "logic" "parameter" "exception" "axiom" "lemma" "goal" "type" "mutable" "model")) . 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" "module")) . font-lock-keyword-face)
    ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face)
    )
   "Minimal highlighting for Why mode")

src/bench/.gitignore

-bench.annot
-whybench.annot

src/bench/benchrc.ml

@@ -51,7 +51,7 @@ let read_tools absf wc map (name,section) =
   let timelimit = get_int ~default:(timelimit wc_main) section "timelimit" in
   let memlimit = get_int ~default:(memlimit wc_main) section "memlimit" in
   (* env *)
-  let env = Env.create_env (Lexer.retrieve loadpath) in
+  let env = Lexer.create_env loadpath in
   (* transformations *)
   let transforms = get_stringl ~default:[] section "transform" in
   let lookup acc t = Trans.compose (Trans.lookup_transform t env) acc in

src/bench/whybench.ml

@@ -303,7 +303,7 @@ let () =
   in
   opt_task := List.fold_left add_meta !opt_task !opt_metas;
 
-  let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
+  let env = Lexer.create_env !opt_loadpath in
   let map_prover s =
     let prover = try Mstr.find s (get_provers config) with
       | Not_found -> eprintf "Prover %s not found.@." s; exit 1

src/coq-plugin/whytac.ml

@@ -46,7 +46,7 @@ let cprovers = Whyconf.get_provers config
 
 let timelimit = timelimit main
 
-let env = Env.create_env (Lexer.retrieve (loadpath main))
+let env = Lexer.create_env (loadpath main)
 
 let provers = Hashtbl.create 17
 

src/core/env.ml

@@ -22,7 +22,10 @@ open Theory
 
 (** Environment *)
 
+type retrieve_channel = string list -> string * in_channel
+
 type env = {
+  env_ret_chan : retrieve_channel;
   env_retrieve : retrieve_theory;
   env_memo     : (string list, theory Mnm.t) Hashtbl.t;
   env_tag      : Hashweak.tag;
@@ -35,7 +38,8 @@ let create_memo () =
   Hashtbl.add ht [] Mnm.empty;
   ht
 
-let create_env = let c = ref (-1) in fun retrieve -> {
+let create_env = let c = ref (-1) in fun ret_chan retrieve -> {
+  env_ret_chan = ret_chan;
   env_retrieve = retrieve;
   env_memo     = create_memo ();
   env_tag      = (incr c; Hashweak.create_tag !c) }
@@ -70,6 +74,8 @@ let find_theory env sl s =
   else try Mnm.find s (find_library env sl)
   with Not_found -> raise (TheoryNotFound (sl, s))
 
+let find_channel env = env.env_ret_chan
+
 let env_tag env = env.env_tag
 
 module Wenv = Hashweak.Make(struct type t = env let tag = env_tag end)

src/core/env.mli

@@ -27,9 +27,13 @@ val env_tag : env -> Hashweak.tag
 
 module Wenv : Hashweak.S with type key = env
 
-type retrieve_theory = env -> string list -> theory Mnm.t
+type retrieve_channel = string list -> string * in_channel
+  (** retrieves a channel from a given path; a filename is also returned, 
+      for printing purposes only *)
 
-val create_env : retrieve_theory -> env
+type retrieve_theory  = env -> string list -> theory Mnm.t
+
+val create_env : retrieve_channel -> retrieve_theory -> env
 
 exception TheoryNotFound of string list * string
 
@@ -37,6 +41,8 @@ val find_theory : env -> string list -> string -> theory
   (** [find_theory e p n] finds the theory named [p.n] in environment [e]
       @raise TheoryNotFound if theory not present in env [e] *)
 
+val find_channel : env -> string list -> string * in_channel
+
 (** Parsers *)
 
 type read_channel = env -> string -> in_channel -> theory Mnm.t

src/ide/gconfig.ml

@@ -111,10 +111,10 @@ let load_config config =
   let provers = get_provers config in
 *)
 (*
-  let env = Env.create_env (Lexer.retrieve main.loadpath) in
+  let env = Lexer.create_env main.loadpath in
 *)
   (* temporary sets env to empty *)
-  let env = Env.create_env (Lexer.retrieve []) in
+  let env = Lexer.create_env [] in
   { window_height = ide.ide_window_height;
     window_width  = ide.ide_window_width;
     tree_width    = ide.ide_tree_width;

src/ide/gmain.ml

@@ -166,7 +166,7 @@ let source_text fname =
 let gconfig =
   let c = Gconfig.config in
   let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes in
-  c.env <- Env.create_env (Lexer.retrieve loadpath);
+  c.env <- Lexer.create_env loadpath;
   let provers = Whyconf.get_provers c.Gconfig.config in
   c.provers <-
     Util.Mstr.fold (Gconfig.get_prover_data c.env) provers Util.Mstr.empty;

src/main.ml

@@ -444,7 +444,7 @@ let do_input env drv = function
 
 let () =
   try
-    let env = Env.create_env (Lexer.retrieve !opt_loadpath) in
+    let env = Lexer.create_env !opt_loadpath in
     let drv = Util.option_map (load_driver env) !opt_driver in
     Queue.iter (do_input env drv) opt_queue
   with e when not (Debug.test_flag Debug.stack_trace) ->

src/parser/denv.ml

@@ -50,6 +50,8 @@ and type_var = {
   type_var_loc : loc option;
 }
 
+let tvsymbol_of_type_var tv = tv.tvsymbol
+
 let rec print_dty fmt = function
   | Tyvar { type_val = Some t } ->
       print_dty fmt t
@@ -58,10 +60,9 @@ let rec print_dty fmt = function
   | Tyapp (s, []) ->
       fprintf fmt "%s" s.ts_name.id_string
   | Tyapp (s, [t]) ->
-      fprintf fmt "%a %s" print_dty t s.ts_name.id_string
+      fprintf fmt "%s %a" s.ts_name.id_string print_dty t
   | Tyapp (s, l) ->
-      fprintf fmt "(%a) %s"
-	(print_list comma print_dty) l s.ts_name.id_string
+      fprintf fmt "%s %a" s.ts_name.id_string (print_list comma print_dty) l
 
 let create_ty_decl_var =
   let t = ref 0 in

src/parser/denv.mli

@@ -95,3 +95,6 @@ val specialize_term : loc:Ptree.loc -> type_var Htv.t -> term -> dterm
 
 val specialize_fmla : loc:Ptree.loc -> type_var Htv.t -> fmla -> dfmla
 
+(** exported for programs *)
+
+val tvsymbol_of_type_var : type_var -> tvsymbol

src/parser/lexer.mli

@@ -21,7 +21,7 @@ open Theory
 
 (** parsing entry points *)
 
-val retrieve : string list -> Env.retrieve_theory
+val create_env : string list -> Env.env
   (** creates a new typing environment for a given loadpath *)
 
 val parse_list0_decl :

src/parser/lexer.mll

@@ -271,21 +271,32 @@ and string = parse
     Loc.set_file file lb;
     parse_logic_file env lb
 
-  let retrieve lp env sl =
-    let f = List.fold_left Filename.concat "" sl ^ ".why" in
+  (* searches file [f] in loadpath [lp] *)
+  let locate_file lp f =
     let fl = List.map (fun dir -> Filename.concat dir f) lp in
-    let file = match List.filter Sys.file_exists fl with
+    match List.filter Sys.file_exists fl with
       | [] -> raise Not_found
       | [file] -> file
       | file1 :: file2 :: _ -> raise (AmbiguousPath (file1, file2))
+
+  let create_env lp =
+    let ret_chan sl = 
+      let f = List.fold_left Filename.concat "" sl in
+      let file = locate_file lp f in
+      file, open_in file
+    in
+    let retrieve env sl =
+      let f = List.fold_left Filename.concat "" sl ^ ".why" in
+      let file = locate_file lp f in
+      let c = open_in file in
+      try
+	let tl = read_channel env file c in
+	close_in c;
+	tl
+      with
+	| e -> close_in c; raise e
     in
-    let c = open_in file in
-    try
-      let tl = read_channel env file c in
-      close_in c;
-      tl
-    with
-      | e -> close_in c; raise e
+    Env.create_env ret_chan retrieve
 
   let () = Env.register_format "why" ["why"] read_channel
 }

src/parser/typing.ml

@@ -146,6 +146,9 @@ let mem_var x denv = Mstr.mem x denv.dvars
 let find_var x denv = Mstr.find x denv.dvars
 let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
 
+let print_denv fmt denv =
+  Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars
+
 (* parsed types -> intermediate types *)
 
 let rec qloc = function

src/parser/typing.mli

@@ -71,6 +71,10 @@ val dfmla : ?localize:bool -> denv -> Ptree.lexpr -> Denv.dfmla
 val dpat : denv -> Ptree.pattern -> denv * Denv.dpattern
 val dpat_list : denv -> Denv.dty -> Ptree.pattern -> denv * Denv.dpattern
 
+val print_denv : Format.formatter -> denv -> unit
+
+val split_qualid : Ptree.qualid -> string list * string
+val string_list_of_qualid : string list -> Ptree.qualid -> string list
 val qloc : Ptree.qualid -> Loc.position
 
 val ts_tuple : int -> Ty.tysymbol

src/programs/TODO

+
+o refs -> mutable types
+
+o loadpath: how to retrieve program files? (cannot use "env")
+
+o what about pervasives old, at, label, exn, unit = (), lt_nat

src/programs/pgm_env.mli

@@ -18,104 +18,18 @@
 (**************************************************************************)
 
 open Why
-open Util
-open Ident
-open Ty
-open Theory
-open Term
-open Decl
+open Pgm_module
 
-(* types *)
+type t
 
-type effect = Pgm_effect.t
-type reference = Pgm_effect.reference
+val get_env : t -> Env.env
 
-type pre = Term.fmla
+type retrieve_module = t -> string -> in_channel -> Pgm_module.t Mnm.t
 
-type post_fmla = Term.vsymbol (* result *) * Term.fmla
-type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
+val create : Env.env -> retrieve_module -> t
 
-type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
+exception ModuleNotFound of string list * string
 
-type type_v = private
-  | Tpure of Ty.ty
-  | Tarrow of binder list * type_c
-
-and type_c =
-  { c_result_type : type_v;
-    c_effect      : effect;
-    c_pre         : pre;
-    c_post        : post; }
-
-and binder = Term.vsymbol * type_v
-
-val tpure : Ty.ty -> type_v
-val tarrow : binder list -> type_c -> type_v
-
-(* environments *)
-
-type env = private {
-  uc      : theory_uc;
-  globals : (lsymbol * type_v) Mstr.t;
-  exceptions : lsymbol Mstr.t;
-  (* predefined symbols *)
-  ts_arrow: tysymbol;
-  ts_bool : tysymbol;
-  ts_label: tysymbol;
-  ts_ref  : tysymbol;
-  ts_exn  : tysymbol;
-  ts_unit : tysymbol;
-  ls_at   : lsymbol;
-  ls_bang : lsymbol;
-  ls_old  : lsymbol;
-  ls_True : lsymbol;
-  ls_False: lsymbol;
-  ls_andb : lsymbol;
-  ls_orb  : lsymbol;
-  ls_notb : lsymbol;
-  ls_unit : lsymbol;
-  ls_lt   : lsymbol;
-  ls_gt   : lsymbol;
-  ls_le   : lsymbol;
-  ls_ge   : lsymbol;
-  ls_add  : lsymbol;
-}
-
-val empty_env : theory_uc -> env
-
-val add_global : preid -> type_v -> env -> lsymbol * env
-
-val add_decl : decl -> env -> env
-
-val logic_lexpr : Loc.position * string -> Ptree.lexpr
-
-val logic_decls : Loc.position * string -> Env.env -> env -> env
-
-val add_exception : preid -> ty option -> env -> lsymbol * env
-
-val t_True : env -> term
-
-val type_v_unit : env -> type_v
-
-val purify : env -> type_v -> ty
-
-val apply_type_v     : env -> type_v -> vsymbol   -> type_c
-val apply_type_v_ref : env -> type_v -> reference -> type_c
-
-val occur_type_v : reference -> type_v -> bool
-
-val v_result : ty -> vsymbol
-val exn_v_result : Why.Term.lsymbol -> Why.Term.vsymbol option
-
-val post_map : (fmla -> fmla) -> post -> post
-
-val subst1 : vsymbol -> term -> term Mvs.t
-
-val eq_type_v : type_v -> type_v -> bool
-
-
-(* pretty-printers *)
-
-val print_type_v : Format.formatter -> type_v -> unit
-val print_type_c : Format.formatter -> type_c -> unit
-val print_post   : Format.formatter -> post   -> unit
+val find_module : t -> string list -> string -> Pgm_module.t
+  (** [find_module e p n] finds the module named [p.n] in environment [e]
+      @raise ModuleNotFound if module not present in env [e] *)

src/programs/pgm_fastwp.ml

@@ -29,7 +29,7 @@ open Theory
 open Pgm_ttree
 open Pgm_typing
 
-module E = Pgm_effect
+module E = Pgm_types.E
 
 module State : sig
   type t

src/programs/pgm_lexer.mll

@@ -50,17 +50,23 @@
 	"done", DONE;
  	"downto", DOWNTO;
         "else", ELSE;
+	"export", EXPORT;
 	"end", END;
 	"exception", EXCEPTION;
 	"for", FOR;
 	"fun", FUN;
 	"ghost", GHOST;
 	"if", IF;
+	"import", IMPORT;
 	"in", IN;
 	"invariant", INVARIANT;
 	"label", LABEL;
 	"let", LET;
 	"match", MATCH;
+	"model", MODEL;
+	"module", MODULE;
+	"mutable", MUTABLE;
+	"namespace", NAMESPACE;
 	"not", NOT;
 	"of", OF;
 	"parameter", PARAMETER;
@@ -72,6 +78,7 @@
 	"to", TO;
 	"try", TRY;
 	"type", TYPE;
+	"use", USE;
 	"variant", VARIANT;
 	"while", WHILE;
 	"with", WITH;

src/programs/pgm_main.ml

@@ -21,36 +21,47 @@
 
 open Format
 open Why
-open Pgm_env
+open Util
+open Ident
+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 penv lmod m =
+  let wp = not type_only in
+  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 ~wp env penv lmod) uc m.mod_decl in
+  let m = close_module uc in
+  Mnm.add id.id m lmod
 
-let read_channel env file c =
+let retrieve penv 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
+    Mnm.empty
+  else
     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
-  end
+    let env = Pgm_env.get_env penv in
+    List.fold_left (add_module ~type_only env penv) Mnm.empty ml
+
+let pgm_env_of_env =
+  let h = Env.Wenv.create 17 in
+  fun env -> 
+    try 
+      Env.Wenv.find h env 
+    with Not_found -> 
+      let penv = Pgm_env.create env retrieve in 
+      Env.Wenv.set h env penv; 
+      penv
+
+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 () = Env.register_format "whyml" ["mlw"] read_channel
 

src/programs/pgm_module.ml

+
+open Why
+open Util
+open Ident
+open Theory
+open Term
+
+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*)
+  ns_mt : mtsymbol  Mnm.t;  (* mutable types *)
+  ns_ns : namespace Mnm.t;  (* inner namespaces *)
+}
+
+let empty_ns = {
+  ns_pr = Mnm.empty;
+  ns_ex = Mnm.empty;
+  ns_mt = Mnm.empty;
+  ns_ns = Mnm.empty;
+}
+
+exception ClashSymbol of string
+
+let ns_replace eq chk x vo vn =
+  if not chk then vn else
+  if eq vo vn then vo else
+  raise (ClashSymbol x)
+
+let ns_union eq chk =
+  Mnm.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
+
+let rec merge_ns chk ns1 ns2 =
+  let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
+  { ns_pr = ns_union p_equal  chk ns1.ns_pr ns2.ns_pr;
+    ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
+    ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
+    ns_ns = Mnm.union fusion      ns1.ns_ns ns2.ns_ns; }
+
+let nm_add chk x ns m = Mnm.change x (function
+  | None -> Some ns
+  | Some os -> Some (merge_ns chk ns os)) m
+
+let ns_add eq chk x v m = Mnm.change x (function
+  | None -> Some v
+  | Some vo -> Some (ns_replace eq chk x vo v)) m
+
+let pr_add = ns_add p_equal
+let ex_add = ns_add ls_equal
+let mt_add = ns_add mt_equal
+
+let add_pr chk x ts ns = { ns with ns_pr = pr_add chk x ts ns.ns_pr }
+let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
+let add_mt chk x mt ns = { ns with ns_mt = mt_add chk x mt ns.ns_mt }
+let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
+
+let rec ns_find get_map ns = function
+  | []   -> assert false
+  | [a]  -> Mnm.find a (get_map ns)
+  | a::l -> ns_find get_map (Mnm.find a ns.ns_ns) l
+
+let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
+let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
+let ns_find_mt = ns_find (fun ns -> ns.ns_mt)
+let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
+
+(* modules under construction *)
+
+type uc = {
+  uc_name   : Ident.ident;
+  uc_th     : theory_uc; (* the logic theory used to type annotations *)
+  uc_decls  : decl list; (* the program declarations *)
+  uc_import : namespace list;
+  uc_export : namespace list;
+}
+
+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 uc = add_pervasives uc in *)
+  { uc_name = id_register n;
+    uc_th = uc;
+    uc_decls = [];
+    uc_import = [empty_ns];
+    uc_export = [empty_ns];
+  }
+
+let open_namespace uc = match uc.uc_import with
+  | ns :: _ -> { uc with
+      uc_th     = Theory.open_namespace uc.uc_th;
+      uc_import =       ns :: uc.uc_import;
+      uc_export = empty_ns :: uc.uc_export; }
+  | [] -> assert false
+
+exception NoOpenedNamespace
+
+let close_namespace uc import s =
+  match uc.uc_import, uc.uc_export with
+  | _ :: i1 :: sti, e0 :: e1 :: ste ->
+      let i1 = if import then merge_ns false e0 i1 else i1 in
+      let _  = if import then merge_ns true  e0 e1 else e1 in
+      let i1 = match s with Some s -> add_ns false s e0 i1 | _ -> i1 in
+      let e1 = match s with Some s -> add_ns true  s e0 e1 | _ -> e1 in
+      let th = Theory.close_namespace uc.uc_th import s in
+      { uc with uc_th = th; uc_import = i1 :: sti; uc_export = e1 :: ste; }
+  | [_], [_] -> raise NoOpenedNamespace
+  | _ -> assert false
+
+(** Insertion of new declarations *)
+
+let add_symbol add id v uc =
+  match uc.uc_import, uc.uc_export with
+  | i0 :: sti, e0 :: ste -> { uc with
+      uc_import = add false id.id_string v i0 :: sti;
+      uc_export = add true  id.id_string v e0 :: ste }
+  | _ -> assert false
+
+let add_psymbol ps uc =
+  add_symbol add_pr ps.p_name ps uc
+
+let add_esymbol ls uc =
+  add_symbol add_ex ls.ls_name ls uc
+
+let add_mtsymbol mt uc =
+  add_symbol add_mt mt.mt_name mt uc
+
+let add_decl d uc =
+  { uc with uc_decls = d :: uc.uc_decls }
+
+let add_logic_decl d uc =
+  let th = Typing.with_tuples Theory.add_decl uc.uc_th d in
+  { uc with uc_th = th }
+
+(** Modules *)
+
+type t = {
+  m_name   : Ident.ident;
+  m_th     : theory;
+  m_decls  : decl list;
+  m_export : namespace;
+}
+
+exception CloseModule
+
+let close_module uc = match uc.uc_export with
+  | [e] ->
+      { m_name = uc.uc_name;
+	m_decls = List.rev uc.uc_decls;
+	m_export = e;
+	m_th = close_theory uc.uc_th; }
+  | _ ->
+      raise CloseModule
+
+(** Use *)
+
+let use_export uc m =
+  match uc.uc_import, uc.uc_export with
+  | i0 :: sti, e0 :: ste -> { uc with
+      uc_import = merge_ns false m.m_export i0 :: sti;
+      uc_export = merge_ns true  m.m_export e0 :: ste;
+      uc_th = Theory.use_export uc.uc_th m.m_th; }
+  | _ -> assert false
+
+(* parsing LOGIC strings using functions from src/parser/
+   requires proper relocation *)