lazy proof term to increase sharing and decrease memory consumption.

[helm.git] / helm / software / components / tactics / auto.ml

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index c3e2b6b4894929dc84648e5549a3c7be412bf6f2..3c8c89468e0f46d9334eb95e4819ca32ff2c2ebe 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -807,7 +807,7 @@ type menv = Cic.metasenv
 type subst = Cic.substitution
 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 let candidate_no = ref 0;;
-type candidate = int * Cic.term
+type candidate = int * Cic.term Lazy.t
 type cache = AutoCache.cache
 type tables = 
   Saturation.active_table * Saturation.passive_table * Equality.equality_bag
@@ -837,8 +837,8 @@ type auto_result =
 (* the status exported to the external observer *)  
 type auto_status = 
   (* context, (goal,candidate) list, and_list, history *)
-  Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list * 
-  (int * Cic.term * int) list * Cic.term list
+  Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * 
+  (int * Cic.term * int) list * Cic.term Lazy.t list
 
 let d_prefix l =
   let rec aux acc = function
@@ -890,7 +890,7 @@ let pp_status ctx status =
     | None -> Printf.sprintf "D(%d, _, %d)" gi d
   in
   let string_of_s m su k (ci,ct) gi =
-    Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
+    Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
   in
   let string_of_ol m su l =
     String.concat " | " 
@@ -1129,7 +1129,7 @@ let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
   subst, metasenv
 ;;
 let mk_fake_proof metasenv subst (goalno,_,_) goalty context = 
-  None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, [] 
+  None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, [] 
 ;;
 let equational_case 
   tables maxm cache depth fake_proof goalno goalty subst context 
@@ -1208,7 +1208,7 @@ let try_candidate
     let open_goals = order_new_goals metasenv subst open_goals ppterm in
     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
     incr candidate_no;
-    Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
+    Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta
   with 
     | ProofEngineTypes.Fail s -> None,tables, maxm
     | CicUnification.Uncertain s ->  None,tables, maxm