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 41ea1e5e44386f35ec74959a6784bdfb0a095deb..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 [] ;;
@@ -90,7 +98,7 @@ let find_library_theorems dbd proof goal =
   let terms = List.map CicUtil.term_of_uri univ in
   List.map 
     (fun t -> 
-       (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph))) 
+       (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph))) 
     terms
 
 let find_context_theorems context metasenv =
@@ -131,13 +139,9 @@ let is_unit_equation context metasenv oldnewmeta term =
           let _,_,mt = CicUtil.lookup_meta i metasenv in
           let sort,u = 
             CicTypeChecker.type_of_aux' metasenv context mt 
-              CicUniv.empty_ugraph
+              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
@@ -163,7 +167,7 @@ let get_candidates universe cache t =
 let only signature context metasenv t =
   try
     let ty,_ = 
-      CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph 
+      CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph 
     in
     let consts = MetadataConstraints.constants_of ty in
     let b = MetadataConstraints.UriManagerSet.subset consts signature in
@@ -268,7 +272,7 @@ let init_cache_and_tables
       (fun t -> 
          let ty,_ =
            CicTypeChecker.type_of_aux' 
-             metasenv context t CicUniv.empty_ugraph 
+             metasenv context t CicUniv.oblivion_ugraph
          in
          (* retrieve_equations could also return flexible terms *)
          if is_an_equality ty then Some(t,ty) 
@@ -285,7 +289,7 @@ let init_cache_and_tables
   in
   (* SIMPLIFICATION STEP 
   let equalities = 
-    let env = (metasenv, context, CicUniv.empty_ugraph) in 
+    let env = (metasenv, context, CicUniv.oblivion_ugraph) in 
     let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
     Saturation.simplify_equalities bag eq_uri env units 
   in 
@@ -312,13 +316,9 @@ let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.u
           let _,_,mt = CicUtil.lookup_meta i metasenv in
           let sort,u = 
             CicTypeChecker.type_of_aux' metasenv context mt 
-              CicUniv.empty_ugraph
-          in
-          let b, _ = 
-            CicReduction.are_convertible ~metasenv context 
-              sort (Cic.Sort Cic.Prop) u
+              CicUniv.oblivion_ugraph
           in
-          if b then Some i else None 
+          if is_propositional context sort then Some i else None 
       | _ -> assert false)
     args
   in
@@ -401,7 +401,8 @@ let close_more tables maxmeta context status auto universe cache =
     HExtlib.filter_map 
       (fun t -> 
          let ty,_ =
-           CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+           CicTypeChecker.type_of_aux' metasenv context t
+           CicUniv.oblivion_ugraph in
            (* retrieve_equations could also return flexible terms *)
            if is_an_equality ty then Some(t,ty) else None)
       equations in
@@ -663,7 +664,7 @@ let apply_smart
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
    in
    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
@@ -677,21 +678,21 @@ let apply_smart
 (****************** AUTO ********************)
 
 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
-let ugraph = CicUniv.empty_ugraph;;
+let ugraph = CicUniv.oblivion_ugraph;;
 let typeof = CicTypeChecker.type_of_aux';;
 let ppterm ctx t = 
   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
   CicPp.pp t names
 ;;
 let is_in_prop context subst metasenv ty =
-  let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
-  fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+  let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
+  is_propositional context sort
 ;;
 
 let assert_proof_is_valid proof metasenv context goalty =
   if debug then
     begin
-      let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+      let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
       let b,_ = CicReduction.are_convertible context ty goalty u in
         if not b then
           begin
@@ -722,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 -> 
@@ -749,10 +747,11 @@ let split_goals_with_metas metasenv subst gl =
 let order_new_goals metasenv subst open_goals ppterm =
   let prop,rest = split_goals_in_prop metasenv subst open_goals in
   let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
+  let closed_type, open_type = split_goals_with_metas metasenv subst rest in
   let open_goals =
-    (List.map (fun x -> x,P) (closed_prop @ open_prop)) 
+    (List.map (fun x -> x,P) (open_prop @ closed_prop)) 
     @ 
-    (List.map (fun x -> x,T) rest)
+    (List.map (fun x -> x,T) (open_type @ closed_type))
   in
   let tys = 
     List.map 
@@ -808,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
@@ -838,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
@@ -891,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 " | " 
@@ -1130,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 
@@ -1209,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
@@ -1636,7 +1635,7 @@ let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)=
     (* we demodulate using both actives passives *)
     List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
   in
-  let env = metasenv,context,CicUniv.empty_ugraph in
+  let env = metasenv,context,CicUniv.oblivion_ugraph in
   match Indexing.solve_demodulating bag env table initgoal steps with 
   | Some (proof, metasenv, newty) ->
       let refl = 
@@ -1681,7 +1680,7 @@ let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)=
   in
   let changed,(newproof,newmetasenv, newty) = 
     Indexing.demodulation_goal bag
-      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
+      (metasenv,context,CicUniv.oblivion_ugraph) table initgoal 
   in
   if changed then
     begin