add useful construction shortcuts to Theory

src/core/theory.ml

@@ -86,8 +86,8 @@ type theory = {
   th_name   : ident;        (* theory name *)
   th_decls  : tdecl list;   (* theory declarations *)
   th_export : namespace;    (* exported namespace *)
-  th_clone  : clone_map;    (* cloning history *)
   th_known  : known_map;    (* known identifiers *)
+  th_clone  : clone_map;    (* cloning history *)
   th_used   : use_map;      (* referenced theories *)
   th_local  : Sid.t;        (* locally declared idents *)
 }
@@ -126,8 +126,8 @@ let builtin_theory =
   { th_name   = id_register (id_fresh "BuiltIn");
     th_decls  = decls;
     th_export = export;
-    th_clone  = Mid.empty;
     th_known  = kn_neq;
+    th_clone  = Mid.empty;
     th_used   = Mid.empty;
     th_local  = Sid.empty }
 
@@ -139,8 +139,8 @@ type theory_uc = {
   uc_decls  : tdecl list;
   uc_import : namespace list;
   uc_export : namespace list;
-  uc_clone  : clone_map;
   uc_known  : known_map;
+  uc_clone  : clone_map;
   uc_used   : use_map;
   uc_local  : Sid.t;
 }
@@ -153,8 +153,8 @@ let empty_theory n =
     uc_decls  = [];
     uc_import = [empty_ns];
     uc_export = [empty_ns];
-    uc_clone  = Mid.empty;
     uc_known  = Mid.empty;
+    uc_clone  = Mid.empty;
     uc_used   = Mid.empty;
     uc_local  = Sid.empty; }
 
@@ -163,8 +163,8 @@ let close_theory uc = match uc.uc_export with
       { th_name   = uc.uc_name;
         th_decls  = List.rev uc.uc_decls;
         th_export = e;
-        th_clone  = uc.uc_clone;
         th_known  = uc.uc_known;
+        th_clone  = uc.uc_clone;
         th_used   = uc.uc_used;
         th_local  = uc.uc_local; }
   | _ ->
@@ -247,17 +247,16 @@ let add_decl uc d =
   { uc with uc_decls = Decl d :: uc.uc_decls;
             uc_known = known_add_decl uc.uc_known d }
 
-let merge_clone cl th sl =
-  let get m id = try Mid.find id m with Not_found -> Sid.empty in
-  let add m m' (id,id') =
-    Mid.add id' (Sid.add id (Sid.union (get m id) (get m' id'))) m'
-  in
-  List.fold_left (add th.th_clone) cl sl
+(** Declaration constructors + add_decl *)
 
-let add_clone uc th sl =
-  let decls = Clone (th,sl) :: uc.uc_decls in
-  let clone = merge_clone uc.uc_clone th sl in
-  { uc with uc_decls = decls; uc_clone = clone }
+let add_ty_decl uc dl = add_decl uc (create_ty_decl dl)
+let add_logic_decl uc dl = add_decl uc (create_logic_decl dl)
+let add_ind_decl uc dl = add_decl uc (create_ind_decl dl)
+let add_prop_decl uc k p f = add_decl uc (create_prop_decl k p f)
+
+let add_ty_decls uc dl = List.fold_left add_decl uc (create_ty_decls dl)
+let add_logic_decls uc dl = List.fold_left add_decl uc (create_logic_decls dl)
+let add_ind_decls uc dl = List.fold_left add_decl uc (create_ind_decls dl)
 
 
 (** Clone *)
@@ -474,6 +473,18 @@ let cl_add_decl cl inst d = match d.d_node with
       let pr',f' = cl_new_prop cl (pr,f) in
       Some (create_prop_decl k' pr' f')
 
+let merge_clone cl th sl =
+  let get m id = try Mid.find id m with Not_found -> Sid.empty in
+  let add m m' (id,id') =
+    Mid.add id' (Sid.add id (Sid.union (get m id) (get m' id'))) m'
+  in
+  List.fold_left (add th.th_clone) cl sl
+
+let add_clone uc th sl =
+  let decls = Clone (th,sl) :: uc.uc_decls in
+  let clone = merge_clone uc.uc_clone th sl in
+  { uc with uc_decls = decls; uc_clone = clone }
+
 let cl_add_tdecl cl inst uc td = match td with
   | Decl d ->
       begin match cl_add_decl cl inst d with

src/core/theory.mli

@@ -47,8 +47,8 @@ type theory = private {
   th_name   : ident;        (* theory name *)
   th_decls  : tdecl list;   (* theory declarations *)
   th_export : namespace;    (* exported namespace *)
-  th_clone  : clone_map;    (* cloning history *)
   th_known  : known_map;    (* known identifiers *)
+  th_clone  : clone_map;    (* cloning history *)
   th_used   : use_map;      (* referenced theories *)
   th_local  : Sid.t;        (* locally declared idents *)
 }
@@ -79,6 +79,17 @@ val close_namespace : theory_uc -> bool -> string option -> theory_uc
 
 val get_namespace : theory_uc -> namespace
 
+(** Declaration constructors + add_decl *)
+
+val add_ty_decl : theory_uc -> ty_decl list -> theory_uc
+val add_logic_decl : theory_uc -> logic_decl list -> theory_uc
+val add_ind_decl : theory_uc -> ind_decl list -> theory_uc
+val add_prop_decl : theory_uc -> prop_kind -> prsymbol -> fmla -> theory_uc
+
+val add_ty_decls : theory_uc -> ty_decl list -> theory_uc
+val add_logic_decls : theory_uc -> logic_decl list -> theory_uc
+val add_ind_decls : theory_uc -> ind_decl list -> theory_uc
+
 (** Clone *)
 
 type th_inst = {

src/parser/typing.ml

@@ -684,7 +684,7 @@ let add_types dl th =
       ts
   in
   let tsl = List.rev_map (fun d -> visit d.td_ident.id, Tabstract) dl in 
-  let th' = try add_decl th (create_ty_decl tsl) 
+  let th' = try add_ty_decl th tsl
     with ClashSymbol s -> error ~loc:(Mstr.find s def).td_loc (Clash s)
   in
   let csymbols = Hashtbl.create 17 in
@@ -717,8 +717,7 @@ let add_types dl th =
     in
     ts, d
   in
-  let dl = List.map decl dl in
-  try List.fold_left add_decl th (create_ty_decls dl)
+  try add_ty_decls th (List.map decl dl)
   with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
 
 let env_of_vsymbol_list vl =
@@ -740,12 +739,12 @@ let add_logics dl th =
       | None -> (* predicate *)
 	  let ps = create_psymbol v pl in
 	  Hashtbl.add psymbols id ps;
-	  add_decl th (create_logic_decl [ps, None])
+	  add_logic_decl th [ps, None]
       | Some t -> (* function *)
 	  let t = type_ty (None, t) in
 	  let fs = create_fsymbol v pl t in
 	  Hashtbl.add fsymbols id fs;
-	  add_decl th (create_logic_decl [fs, None])
+	  add_logic_decl th [fs, None]
     with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
   in
   let th' = List.fold_left create_symbol th dl in
@@ -799,8 +798,7 @@ let add_logics dl th =
 	      make_fs_defn fs vl (term env t)
         end
   in
-  let dl = List.map type_decl dl in
-  List.fold_left add_decl th (create_logic_decls dl)
+  add_logic_decls th (List.map type_decl dl)
 
 let type_term denv env t =
   let t = dterm denv t in
@@ -815,9 +813,8 @@ let type_fmla denv env f =
 let fmla uc = type_fmla (create_denv uc) Mstr.empty
 
 let add_prop k loc s f th =
-  let f = fmla th f in
-  try
-    add_decl th (create_prop_decl k (create_prsymbol (id_user s.id loc)) f)
+  let pr = create_prsymbol (id_user s.id loc) in
+  try add_prop_decl th k pr (fmla th f)
   with ClashSymbol s -> error ~loc (Clash s)
 
 let loc_of_id id = match id.id_origin with
@@ -835,7 +832,7 @@ let add_inductives dl th =
     let pl = List.map type_ty d.in_params in
     let ps = create_psymbol v pl in
     Hashtbl.add psymbols id ps;
-    try add_decl th (create_logic_decl [ps, None])
+    try add_logic_decl th [ps, None]
     with ClashSymbol s -> error ~loc:d.in_loc (Clash s)
   in
   let th' = List.fold_left create_symbol th dl in
@@ -850,9 +847,7 @@ let add_inductives dl th =
     in
     ps, List.map clause d.in_def
   in
-  let dl = List.map type_decl dl in
-  try
-    List.fold_left add_decl th (create_ind_decls dl)
+  try add_ind_decls th (List.map type_decl dl)
   with
   | ClashSymbol s -> error ~loc:(Hashtbl.find propsyms s) (Clash s)
   | InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)