reintegrate use_map and clone_map into the task structure.

This will allow transformations to apply use and clone.
Also, this will allow to simplify the driver structure.
Memoisation modulo env/clone/use requires some further 
adaptation (but this would be needed anyway).

src/core/register.ml

@@ -21,7 +21,7 @@ open Env
 open Task
 open Trans
 
-type 'a value = env option -> clone option -> 'a
+type 'a value = env option -> (*clone option ->*) 'a
 
 type 'a registered = {
   mutable value    : 'a value;
@@ -52,24 +52,29 @@ let memo0 tag f = memo f tag (Hashtbl.create 7)
 
 let unused0 f = fun _ -> f
 
+(*
 let cl_tag cl = cl.cl_tag
+*)
 
-let store0 memo_env memo_cl f =
+let store0 memo_env (*memo_cl*) f =
   let gen () =
+(*
     let f2 = memo_env (f ()) in
     fun env -> memo_cl (f2 env)
+*)
+    memo_env (f ())
   in
   create gen
 
-let store       f = store0 unused0         unused0        f
-let store_env   f = store0 (memo0 env_tag) unused0        f
-let store_clone f = store0 (memo0 env_tag) (memo0 cl_tag) f
+let store       f = store0 unused0         (*unused0       *) f
+let store_env   f = store0 (memo0 env_tag) (*unused0       *) f
+let store_clone f = store0 (memo0 env_tag) (*(memo0 cl_tag)*) f
 
-let apply0 reg env clone = Trans.apply (reg.value env clone)
+let apply0 reg env (*clone*) = Trans.apply (reg.value env (*clone*))
 
-let apply_clone reg env clone = apply0 reg (Some env) (Some clone)
-let apply_env   reg env       = apply0 reg (Some env) None
-let apply       reg           = apply0 reg None       None
+(*let apply_clone reg env clone = apply0 reg (Some env) (Some clone)*)
+let apply_env   reg env       = apply0 reg (Some env) (*None*)
+let apply       reg           = apply0 reg None       (*None*)
 
 let clear reg = reg.value <- reg.generate ()
 
@@ -77,7 +82,7 @@ let combine comb reg1 reg2 =
   let gen () =
     let reg1 = reg1.generate () in
     let reg2 = reg2.generate () in
-    fun env cl -> comb (reg1 env cl) (reg2 env cl) in
+    fun env (*cl*) -> comb (reg1 env (*cl*)) (reg2 env (*cl*)) in
   create gen
 
 let compose   r1 r2 = combine (fun t1 t2 -> Trans.compose   t1 t2) r1 r2
@@ -86,7 +91,7 @@ let compose_l r1 r2 = combine (fun t1 t2 -> Trans.compose_l t1 t2) r1 r2
 let conv_res conv reg1 =
   let gen () =
     let reg1 = reg1.generate () in
-    fun env cl -> conv (reg1 env cl) in
+    fun env (*cl*) -> conv (reg1 env (*cl*)) in
   create gen
 
 let singleton reg = conv_res Trans.singleton reg

src/core/register.mli

@@ -26,11 +26,15 @@ type 'a tlist_reg = 'a list trans_reg
 
 val store       : (unit ->                 'a trans) -> 'a trans_reg
 val store_env   : (unit -> env ->          'a trans) -> 'a trans_reg
+(*
 val store_clone : (unit -> env -> clone -> 'a trans) -> 'a trans_reg
+*)
 
 exception ArgumentNeeded
 
+(*
 val apply_clone : 'a trans_reg -> env -> clone -> task -> 'a
+*)
 val apply_env   : 'a trans_reg -> env ->          task -> 'a
 val apply       : 'a trans_reg ->                 task -> 'a
 

src/core/task.ml

@@ -24,152 +24,133 @@ open Term
 open Decl
 open Theory
 
-(** Cloning map *)
-
-type clone = {
-  cl_map : clone_map;
-  cl_tag : int
-}
-
-let empty_clone = {
-  cl_map = Mid.empty;
-  cl_tag = 0;
-}
-
-let cloned_from cl i1 i2 =
-  try i1 = i2 || Sid.mem i2 (Mid.find i1 cl.cl_map)
-  with Not_found -> false
-
-let add_clone =
-  let r = ref 0 in
-  fun cl th sl ->
-    incr r;
-    { cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
-
-
 (** Task *)
 
 type task = task_hd option
 
 and task_hd = {
-  task_decl  : decl;
-  task_prev  : task;
-  task_known : known_map;
-  task_tag   : int;
+  task_decl  : tdecl;       (* last declaration *)
+  task_prev  : task;        (* context *)
+  task_known : known_map;   (* known identifiers *)
+  task_clone : clone_map;   (* cloning history *)
+  task_used  : use_map;     (* referenced theories *)
+  task_tag   : int;         (* unique task tag *)
 }
 
 module Task = struct
   type t = task_hd
 
+  let equal_pair (il1,ir1) (il2,ir2) = il1 == il2 && ir1 == ir2
+
+  let equal_tdecl td1 td2 = match td1,td2 with
+    | Decl d1, Decl d2 -> d1 == d2
+    | Use th1, Use th2 -> th1.th_name == th2.th_name
+    | Clone (th1,sl1), Clone (th2,sl2) ->
+        th1.th_name == th2.th_name && list_all2 equal_pair sl1 sl2
+    | _,_ -> false
+
   let equal a b =
-    a.task_decl == b.task_decl &&
+    equal_tdecl a.task_decl b.task_decl &&
     match a.task_prev, b.task_prev with
       | Some na, Some nb -> na == nb
       | None, None -> true
       | _ -> false
 
+  let hash_pair (il,ir) = Hashcons.combine il.id_tag ir.id_tag
+
+  let hash_tdecl = function
+    | Decl d -> Hashcons.combine 3 d.d_tag
+    | Use th -> Hashcons.combine 5 th.th_name.id_tag
+    | Clone (th,i) ->
+        Hashcons.combine_list hash_pair th.th_name.id_tag i
+
   let hash task =
+    let decl = hash_tdecl task.task_decl in
     let prev = match task.task_prev with
       | Some task -> 1 + task.task_tag
       | None -> 0
     in
-    Hashcons.combine task.task_decl.d_tag prev
+    Hashcons.combine decl prev
 
   let tag i task = { task with task_tag = i }
 end
 module Htask = Hashcons.Make(Task)
 
-let mk_task decl prev known = Htask.hashcons {
+let mk_task decl prev known clone used = Some (Htask.hashcons {
   task_decl  = decl;
   task_prev  = prev;
   task_known = known;
+  task_clone = clone;
+  task_used  = used;
   task_tag   = -1;
-}
+})
 
 exception LemmaFound
 exception GoalFound
 
-let push_decl task d =
-  begin match task.task_decl.d_node with
-    | Dprop (Pgoal,_,_) -> raise GoalFound
-    | _ -> ()
-  end;
-  try mk_task d (Some task) (known_add_decl task.task_known d)
-  with KnownIdent _ -> task
-
-let init_decl d =
-  try mk_task d None (known_add_decl Mid.empty d)
-  with KnownIdent _ -> assert false
-
-let add_decl opt d =
-  begin match d.d_node with
-    | Dprop (Plemma,_,_) -> raise LemmaFound
-    | _ -> ()
-  end;
-  match opt with
-    | Some task -> Some (push_decl task d)
-    | None      -> Some (init_decl d)
-
-let rec flat_theory used cl task th =
-  if Mid.mem th.th_name used then used,cl,task else
-  let acc = Mid.add th.th_name th used, cl, task in
-  List.fold_left flat_tdecl acc th.th_decls
-
-and flat_tdecl (used, cl, task) = function
-  | Use th ->
-      flat_theory used cl task th
-  | Clone (th,sl) ->
-      used, add_clone cl th sl, task
-  | Decl d ->
-      begin match d.d_node with
-        | Dprop (Pgoal,_,_) ->
-            used, cl, task
-        | Dprop (Plemma,pr,f) ->
-            let d = create_prop_decl Paxiom pr f in
-            used, cl, add_decl task d
-        | Dprop (Paxiom,_,_) ->
-            used, cl, add_decl task d
-        | Dtype _ | Dlogic _ | Dind _  ->
-            used, cl, add_decl task d
-      end
-
-let split_tdecl names (res, used, cl, task) = function
-  | Use th ->
-      let used, cl, task = flat_theory used cl task th in
-      res, used, cl, task
-  | Clone (th,sl) ->
-      res, used, add_clone cl th sl, task
-  | Decl d ->
-      begin match d.d_node with
-        | Dprop (Pgoal,pr,_)
-          when option_apply true (Spr.mem pr) names ->
-            let t = add_decl task d, cl, used in
-            t :: res, used, cl, task
-        | Dprop (Pgoal,_,_) ->
-            res, used, cl, task
-        | Dprop (Plemma,pr,f)
-          when option_apply true (Spr.mem pr) names ->
-            let d = create_prop_decl Pgoal pr f in
-            let t = add_decl task d, cl, used in
-            let d = create_prop_decl Paxiom pr f in
-            t :: res, used, cl, add_decl task d
-        | Dprop (Plemma,pr,f) ->
-            let d = create_prop_decl Paxiom pr f in
-            res, used, cl, add_decl task d
-        | Dprop (Paxiom,_,_) ->
-            res, used, cl, add_decl task d
-        | Dtype _ | Dlogic _ | Dind _  ->
-            res, used, cl, add_decl task d
-      end
+let add_tdecl task td =
+  let kn,cl,us = match task with
+    | Some {task_decl=Decl{d_node=Dprop(Pgoal,_,_)}} -> raise GoalFound
+    | Some task -> task.task_known, task.task_clone, task.task_used
+    | None -> Mid.empty, Mid.empty, Mid.empty
+  in
+  match td with
+    | Decl { d_node = Dprop (Plemma,_,_) } -> raise LemmaFound
+    | Decl d ->
+        begin try mk_task td task (known_add_decl kn d) cl us
+        with KnownIdent _ -> task end
+    | Use th ->
+        if Mid.mem th.th_name us then task else
+        mk_task td task kn cl (merge_used us th)
+    | Clone (th,sl) ->
+        mk_task td task kn (merge_clone cl th sl) us
+
+let add_decl task d = add_tdecl task (Decl d)
+
+(* declaration constructors + add_decl *)
+
+let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)
+let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
+let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
+let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)
+
+let add_ty_decls tk dl = List.fold_left add_decl tk (create_ty_decls dl)
+let add_logic_decls tk dl = List.fold_left add_decl tk (create_logic_decls dl)
+let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)
+
+(* use, clone and split_theory *)
+
+let rec use_export task th = match task with
+  | Some task_hd when Mid.mem th.th_name task_hd.task_used -> task
+  | _ -> add_tdecl (List.fold_left flat_tdecl task th.th_decls) (Use th)
+
+and flat_tdecl task td = match td with
+  | Decl { d_node = Dprop (Pgoal,_,_) } -> task
+  | Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
+  | Decl _  -> add_tdecl task td
+  | Clone _ -> add_tdecl task td
+  | Use th -> use_export task th
+
+let clone_export = clone_theory flat_tdecl
+
+let split_tdecl names (res,task) td = match td with
+  | Decl { d_node = Dprop (Pgoal,pr,_) }
+    when option_apply true (Spr.mem pr) names ->
+      add_tdecl task td :: res, task
+  | Decl { d_node = Dprop (Pgoal,_,_) } ->
+      res, task
+  | Decl { d_node = Dprop (Plemma,pr,f) }
+    when option_apply true (Spr.mem pr) names ->
+      add_prop_decl task Pgoal pr f :: res,
+      add_prop_decl task Paxiom pr f
+  | Decl { d_node = Dprop (Plemma,pr,f) } ->
+      res, add_prop_decl task Paxiom pr f
+  | Decl _  -> res, add_tdecl task td
+  | Clone _ -> res, add_tdecl task td
+  | Use th -> res, use_export task th
 
 let split_theory th names =
-  let acc = [], Mid.empty, empty_clone, None in
-  let res,_,_,_ = List.fold_left (split_tdecl names) acc th.th_decls in
-  res
-
-let flat_theory task th =
-  let _,_,task = flat_theory Mid.empty empty_clone task th in
-  task
+  fst (List.fold_left (split_tdecl names) ([],None) th.th_decls)
 
 (* Generic utilities *)
 
@@ -181,11 +162,14 @@ let rec task_iter fn = function
   | Some task -> fn task.task_decl; task_iter fn task.task_prev
   | None      -> ()
 
-let task_decls = task_fold (fun acc d -> d::acc) []
+let task_tdecls = task_fold (fun acc d -> d::acc) []
+
+let task_decls =
+  task_fold (fun acc -> function Decl d -> d::acc | _ -> acc) []
 
 exception GoalNotFound
 
 let task_goal = function
-  | Some { task_decl = { d_node = Dprop (Pgoal,pr,_) }} -> pr
+  | Some { task_decl = Decl { d_node = Dprop (Pgoal,pr,_) }} -> pr
   | _ -> raise GoalNotFound
 

src/core/task.mli

@@ -23,42 +23,48 @@ open Term
 open Decl
 open Theory
 
-(** Cloning map *)
-
-type clone = private {
-  cl_map : clone_map;
-  cl_tag : int
-}
-
-val cloned_from : clone -> ident -> ident -> bool
-
 (** Task *)
 
 type task = task_hd option
 
 and task_hd = private {
-  task_decl  : decl;
-  task_prev  : task;
-  task_known : known_map;
-  task_tag   : int;
+  task_decl  : tdecl;       (* last declaration *)
+  task_prev  : task;        (* context *)
+  task_known : known_map;   (* known identifiers *)
+  task_clone : clone_map;   (* cloning history *)
+  task_used  : use_map;     (* referenced theories *)
+  task_tag   : int;         (* unique task tag *)
 }
 
 (* constructors *)
 
+val add_tdecl : task -> tdecl -> task
 val add_decl : task -> decl -> task
 
-val split_theory : theory -> Spr.t option -> (task * clone * use_map) list
+val use_export : task -> theory -> task
+val clone_export : task -> theory -> th_inst -> task
 
-val flat_theory : task -> theory -> task
+(* declaration constructors + add_decl *)
 
-(* bottom-up, tail-recursive traversal functions *)
+val add_ty_decl : task -> ty_decl list -> task
+val add_logic_decl : task -> logic_decl list -> task
+val add_ind_decl : task -> ind_decl list -> task
+val add_prop_decl : task -> prop_kind -> prsymbol -> fmla -> task
 
-val task_fold : ('a -> decl -> 'a) -> 'a -> task -> 'a
+val add_ty_decls : task -> ty_decl list -> task
+val add_logic_decls : task -> logic_decl list -> task
+val add_ind_decls : task -> ind_decl list -> task
 
-val task_iter : (decl -> unit) -> task -> unit
+(* utilities *)
 
-val task_decls : task -> decl list
+val split_theory : theory -> Spr.t option -> task list
+
+(* bottom-up, tail-recursive traversal functions *)
 
+val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
+val task_iter : (tdecl -> unit) -> task -> unit
+val task_tdecls : task -> tdecl list
+val task_decls : task -> decl list
 val task_goal : task -> prsymbol
 
 (* exceptions *)

src/core/theory.ml

@@ -473,6 +473,20 @@ 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 clone_theory cl add_tdecl acc th inst =
+  let add acc = function
+    | Decl d ->
+        begin match cl_add_decl cl inst d with
+          | Some d -> add_tdecl acc (Decl d)
+          | None -> acc
+        end
+    | td -> add_tdecl acc td
+  in
+  let acc = List.fold_left add acc th.th_decls in
+  let add_idid id id' acc = (id,id') :: acc in
+  let sl = Hid.fold add_idid cl.id_table [] in
+  add_tdecl acc (Clone (th,sl))
+
 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') =
@@ -480,34 +494,26 @@ let merge_clone cl th sl =
   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
-        | Some d -> { uc with
-            uc_decls = Decl d :: uc.uc_decls;
-            uc_known = known_add_decl uc.uc_known d }
-        | None -> uc
-      end
-  | Use th -> if Mid.mem th.th_name uc.uc_used then uc else { uc with
-      uc_used  = merge_used uc.uc_used th;
+let cloned_from cl i1 i2 =
+  try i1 = i2 || Sid.mem i2 (Mid.find i1 cl)
+  with Not_found -> false
+
+let cl_add_tdecl uc td = match td with
+  | Decl d -> { uc with
+      uc_decls = td :: uc.uc_decls;
+      uc_known = known_add_decl uc.uc_known d }
+  | Use th when Mid.mem th.th_name uc.uc_used -> uc
+  | Use th -> { uc with
+      uc_decls = td :: uc.uc_decls;
       uc_known = merge_known uc.uc_known th.th_known;
-      uc_decls = td :: uc.uc_decls }
-  | Clone (th,sl) ->
-      add_clone uc th sl
+      uc_used  = merge_used uc.uc_used th }
+  | Clone (th,sl) -> { uc with
+      uc_decls = td :: uc.uc_decls;
+      uc_clone = merge_clone uc.uc_clone th sl }
 
 let clone_export uc th inst =
   let cl = cl_init th inst in
-  let add_tdecl = cl_add_tdecl cl inst in
-  let uc = List.fold_left add_tdecl uc th.th_decls in
-
-  let add_idid id id' acc = (id,id') :: acc in
-  let sl = Hid.fold add_idid cl.id_table [] in
-  let uc = add_clone uc th sl in
+  let uc = clone_theory cl cl_add_tdecl uc th inst in
 
   let add_local id' () acc = Sid.add id' acc in
   let lc = Hid.fold add_local cl.nw_local uc.uc_local in
@@ -553,3 +559,6 @@ let clone_export uc th inst =
     | _ ->
         assert false
 
+let clone_theory add_tdecl acc th inst =
+  clone_theory (cl_init th inst) add_tdecl acc th inst
+

src/core/theory.mli

@@ -53,7 +53,7 @@ type theory = private {
   th_local  : Sid.t;        (* locally declared idents *)
 }
 
-and tdecl = private
+and tdecl =
   | Decl  of decl
   | Use   of theory
   | Clone of theory * (ident * ident) list
@@ -73,6 +73,7 @@ val close_theory  : theory_uc -> theory
 
 val add_decl : theory_uc -> decl -> theory_uc
 val use_export : theory_uc -> theory -> theory_uc
+val merge_used : use_map -> theory -> use_map
 
 val open_namespace  : theory_uc -> theory_uc
 val close_namespace : theory_uc -> bool -> string option -> theory_uc
@@ -107,9 +108,10 @@ val create_inst :
   lemma : prsymbol list ->
   goal  : prsymbol list -> th_inst
 
+val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
 val clone_export : theory_uc -> theory -> th_inst -> theory_uc
-
 val merge_clone  : clone_map -> theory -> (ident * ident) list -> clone_map
+val cloned_from  : clone_map -> ident -> ident -> bool
 
 (* exceptions *)
 

src/core/trans.ml

@@ -22,6 +22,7 @@ open Ident
 open Ty
 open Term
 open Decl
+open Theory
 open Task
 
 (** Task transformation *)
@@ -104,14 +105,20 @@ let map_l fn = fold_l (fun t1 t2 -> fn t1 t2)
 
 let decl fn =
   let memo_t = Hashtbl.create 63 in
-  let fn task = memo fn decl_tag memo_t task.task_decl in
-  let fn task acc = List.fold_left add_decl acc (fn task) in
+  let fn d = memo fn decl_tag memo_t d in
+  let fn task acc = match task.task_decl with
+    | Decl d -> List.fold_left add_decl acc (fn d)
+    | td -> add_tdecl acc td
+  in
   map fn
 
 let decl_l fn =
   let memo_t = Hashtbl.create 63 in
-  let fn task = memo fn decl_tag memo_t task.task_decl in
-  let fn task acc = List.rev_map (List.fold_left add_decl acc) (fn task) in
+  let fn d = memo fn decl_tag memo_t d in
+  let fn task acc = match task.task_decl with
+    | Decl d -> List.rev_map (List.fold_left add_decl acc) (fn d)
+    | td -> [add_tdecl acc td]
+  in
   map_l fn
 
 let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])

src/driver/driver.ml

@@ -136,8 +136,8 @@ and raw_driver = {
 
 and driver = {
   drv_raw         : raw_driver;
-  drv_clone       : clone;
-  drv_used        : theory Mid.t;
+  drv_clone       : Theory.clone_map;
+  drv_used        : Theory.use_map;
   drv_env         : env;
   drv_thprelude   : string list Hid.t;
   (* the first is the translation only for this ident, the second is
@@ -361,7 +361,7 @@ let query_ident drv id =
     Hid.find drv.drv_with_task id
   with Not_found ->
     let r = try
-      Mid.find id drv.drv_clone.cl_map
+      Mid.find id drv.drv_clone
     with Not_found -> Sid.empty in
     let tr = try fst (Hid.find drv.drv_theory id) 
     with Not_found -> Tag Sstr.empty in 
@@ -382,7 +382,8 @@ let syntax_arguments s print fmt l =
 (** using drivers *)
 
 let apply_transforms drv = 
-  apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone
+(*  apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone *)
+  apply_env drv.drv_raw.drv_transforms drv.drv_env
 
 let cook_driver env clone used drv = 
   let drv = { drv_raw        = drv;

src/driver/driver.mli

@@ -32,7 +32,8 @@ val load_driver : string -> env -> raw_driver
 (** cooked driver *)
 type driver
 
-val cook_driver : env -> clone -> Theory.use_map -> raw_driver -> driver
+val cook_driver : 
+  env -> Theory.clone_map -> Theory.use_map -> raw_driver -> driver
 
 (** querying drivers *)
 

src/main.ml

@@ -172,9 +172,11 @@ let transform env l =
 let extract_goals ?filter = 
   fun env drv acc th ->
     let l = split_theory th filter in
-    let l = List.rev_map (fun (task,cl,used) -> 
-      let drv = Driver.cook_driver env cl (Ident.Mid.add th.th_name th used) drv in
-      (th,task,drv)) l in
+    let l = List.rev_map (fun task -> 
+      let cl = Util.option_apply Ident.Mid.empty (fun t -> t.task_clone) task in
+      let us = Util.option_apply Ident.Mid.empty (fun t -> t.task_used) task in
+      let us = Ident.Mid.add th.th_name th us in
+      let drv = Driver.cook_driver env cl us drv in (th,task,drv)) l in
     List.rev_append l acc
 
 let file_sanitizer = None (* We should remove which character? *)

src/transform/compile_match.ml

@@ -19,6 +19,7 @@
 
 open Term
 open Decl
+open Theory
 open Task
 
 let rec rewriteT kn t = match t.t_node with
@@ -40,7 +41,9 @@ and rewriteF kn f = match f.f_node with
 let comp t task =
   let fnT = rewriteT t.task_known in
   let fnF = rewriteF t.task_known in
-  add_decl task (decl_map fnT fnF t.task_decl)
+  match t.task_decl with
+  | Decl d -> add_decl task (decl_map fnT fnF d)
+  | td -> add_tdecl task td
 
 let comp = Register.store (fun () -> Trans.map comp None)
 

src/transform/eliminate_algebraic.ml

@@ -22,6 +22,7 @@ open Ident
 open Ty
 open Term
 open Decl
+open Theory