Universe is used only locally to tactics/

[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 1755fd08e808f22370e330403ee73bc73c78bf17..a01ca86913eedfbe9789997c54d3e9c0576bfb24 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -689,10 +689,10 @@ let universe_of_params metasenv context universe tl =
 (***************** applyS *******************)
 
 let new_metasenv_and_unify_and_t 
- dbd flags universe proof goal ?tables newmeta' metasenv' 
+ dbd flags automation_cache proof goal ?tables newmeta' metasenv' 
  context term' ty termty goal_arity 
 = 
- let ppterm = ppterm context in
+(*  let ppterm = ppterm context in *)
  let (consthead,newmetasenv,arguments,_) =
    TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in
  let term'' = 
@@ -728,6 +728,8 @@ let new_metasenv_and_unify_and_t
      (PrimitiveTactics.apply_tac term'')
      (proof''',goal) 
  in
+ (* XXX automation_cache *)
+ let universe = automation_cache.AutomationCache.univ in
  let (active, passive,bag), cache, maxm =
      init_cache_and_tables ~dbd flags.use_library false (* was true *) 
       true false universe
@@ -735,7 +737,7 @@ let new_metasenv_and_unify_and_t
    in
  match 
      Saturation.given_clause bag maxm (proof'''',newmeta) active passive 
-       10 10 flags.timeout
+       20 10 flags.timeout
  with
  | None, _,_,_ -> 
      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle"))) 
@@ -764,7 +766,7 @@ let rec count_prods context ty =
   | _ -> 0
 
 let apply_smart 
-  ~dbd ~term ~subst ~universe ?tables ~params:(univ,params) (proof, goal) 
+  ~dbd ~term ~subst ~automation_cache ?tables ~params:(univ,params) (proof, goal) 
 =
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -772,7 +774,11 @@ let apply_smart
   let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let flags = flags_of_params params ~for_applyS:true () in
+  (* XXX automation_cache *)
+  let universe = automation_cache.AutomationCache.univ in
   let universe = universe_of_params metasenv context universe univ in
+  let automation_cache = { automation_cache with AutomationCache.univ = universe } in
+  
   let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
@@ -813,7 +819,7 @@ let apply_smart
    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
    let proof, gl, active, passive =
-    new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
+    new_metasenv_and_unify_and_t dbd flags automation_cache proof goal ?tables
      newmeta' metasenv' context term' ty termty goal_arity
    in
     proof, gl, active, passive
@@ -1635,12 +1641,12 @@ let auto flags metasenv tables universe cache context metasenv gl =
       None,cache
 ;;
 
-let applyS_tac ~dbd ~term ~params ~universe =
+let applyS_tac ~dbd ~term ~params ~automation_cache =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try 
       let proof, gl,_,_ =
-       apply_smart ~dbd ~term ~subst:[] ~params ~universe status
+       apply_smart ~dbd ~term ~subst:[] ~params ~automation_cache status
       in 
        proof, gl
     with 
@@ -1648,10 +1654,12 @@ let applyS_tac ~dbd ~term ~params ~universe =
     | CicTypeChecker.TypeCheckerFailure msg ->
         raise (ProofEngineTypes.Fail msg))
 
-let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
+let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
   let _,metasenv,_subst,_,_, _ = proof in
   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
   let flags = flags_of_params params () in
+  (* XXX automation_cache *)
+  let universe = automation_cache.AutomationCache.univ in
   let universe = universe_of_params metasenv context universe univ in
   let use_library = flags.use_library in
   let tables,cache,newmeta =
@@ -1689,8 +1697,8 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~universe (proof, goal) =
         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 ;;
 
-let auto_tac ~dbd ~params ~universe = 
-  ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
+let auto_tac ~dbd ~params ~automation_cache = 
+  ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~automation_cache);;
 
 let eq_of_goal = function
   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
@@ -1700,10 +1708,12 @@ let eq_of_goal = function
 
 (* performs steps of rewrite with the universe, obtaining if possible 
  * a trivial goal *)
-let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)= 
+let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)= 
   let _,metasenv,_subst,_,_,_ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let steps = int_of_string (string params "steps" "1") in 
+  (* XXX automation_cache *)
+  let universe = automation_cache.AutomationCache.univ in
   let universe = universe_of_params metasenv context universe univ in
   let eq_uri = eq_of_goal ty in
   let (active,passive,bag), cache, maxm =
@@ -1736,8 +1746,8 @@ let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)=
         (ProofEngineTypes.Fail (lazy 
           ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
 ;;
-let solve_rewrite_tac ~params ~universe () =
-  ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params)
+let solve_rewrite_tac ~params ~automation_cache () =
+  ProofEngineTypes.mk_tactic (solve_rewrite_tac ~automation_cache ~params)
 ;;
 
 (* Demodulate thorem *)
@@ -1796,7 +1806,7 @@ let is_subsumed univ context ty =
       ) None candidates
 ;;
 
-let demodulate_theorem ~universe uri =
+let demodulate_theorem ~automation_cache uri =
   let eq_uri = 
     match LibraryObjects.eq_URI () with
       | Some (uri) -> uri
@@ -1819,6 +1829,8 @@ let demodulate_theorem ~universe uri =
       MetadataQuery.close_with_types set [] context 
   in
   (* retrieve equations from the universe universe *)
+  (* XXX automation_cache *)
+  let universe = automation_cache.AutomationCache.univ in
   let equations = 
     retrieve_equations true signature universe AutoCache.cache_empty context []
   in
@@ -1879,9 +1891,11 @@ let demodulate_theorem ~universe uri =
 
 
 (* NEW DEMODULATE *)
-let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)= 
+let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)= 
   let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+  (* XXX automation_cache *)
+  let universe = automation_cache.AutomationCache.univ in
   let universe = universe_of_params metasenv context universe univ in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let initgoal = [], metasenv, ty in
@@ -1933,8 +1947,8 @@ let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)=
       ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
 ;;
 
-let demodulate_tac ~dbd ~params ~universe = 
-  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);;
+let demodulate_tac ~dbd ~params ~automation_cache = 
+  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~automation_cache);;
 
 let pp_proofterm = Equality.pp_proofterm;;