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 37f0939bd16e447e48d6420514ed5537b8d26c1f..3c8c89468e0f46d9334eb95e4819ca32ff2c2ebe 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -30,6 +30,14 @@ let debug = false;;
 let debug_print s = 
   if debug then prerr_endline (Lazy.force s);;
 
+let is_propositional context sort = 
+  match CicReduction.whd context sort with
+  | Cic.Sort Cic.Prop 
+  | Cic.Sort (Cic.CProp _) -> true
+  | _-> false
+;;
+
+
 type auto_params = Cic.term list * (string * string) list 
 
 let elems = ref [] ;;
@@ -133,11 +141,7 @@ let is_unit_equation context metasenv oldnewmeta term =
             CicTypeChecker.type_of_aux' metasenv context mt 
               CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -314,11 +318,7 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u
             CicTypeChecker.type_of_aux' metasenv context mt 
               CicUniv.oblivion_ugraph
           in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
-          in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -686,7 +686,7 @@ let ppterm ctx t =
 ;;
 let is_in_prop context subst metasenv ty =
   let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
-  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+  is_propositional context sort
 ;;
 
 let assert_proof_is_valid proof metasenv context goalty =
@@ -723,10 +723,7 @@ let split_goals_in_prop metasenv subst gl =
       let _,context,ty = CicUtil.lookup_meta g metasenv in
       try
         let sort,u = typeof ~subst metasenv context ty ugraph in
-        let b,_ = 
-          CicReduction.are_convertible 
-            ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
-        b
+        is_propositional context sort
       with 
       | CicTypeChecker.AssertFailure s 
       | CicTypeChecker.TypeCheckerFailure s -> 
@@ -810,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
@@ -840,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
@@ -893,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 " | " 
@@ -1132,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 
@@ -1211,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