added a (for the moment) dummy field _subst to ProofengineTypes.proof.

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

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 3bec5b0444d47e53f6bab870eb6d6b5ad36dffd6..6f293ff4a8b56e298d262c5c4a8ff68032f314d8 100644 (file)
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -225,7 +225,7 @@ let empty_tables =
 let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
   (* the local cache in initially empty  *)
   let cache = AutoCache.cache_empty in
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _subst,_, _, _ = proof in
   let signature = MetadataQuery.signature_of metasenv goal in
   let newmeta = CicMkImplicit.new_meta metasenv [] in
   let _,context,_ = CicUtil.lookup_meta goal metasenv in
@@ -368,7 +368,7 @@ let build_equalities auto context metasenv tables universe cache newmeta equatio
 let close_more tables maxmeta context status auto universe cache =
   let (active,passive,bag) = tables in
   let proof, goalno = status in
-  let _, metasenv,_,_, _ = proof in  
+  let _, metasenv,_subst,_,_, _ = proof in  
   let signature = MetadataQuery.signature_of metasenv goalno in
   let equations = retrieve_equations signature universe cache context in
   let eqs_and_types =
@@ -401,7 +401,7 @@ let find_context_equalities
   let module C = Cic in
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
-  let _,metasenv,_,_, _ = proof in
+  let _,metasenv,_subst,_,_, _ = proof in
   let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
   (* if use_auto is true, we try to close the hypothesis of equational
     statements using auto; a naif, and probably wrong approach *)
@@ -468,8 +468,8 @@ let new_metasenv_and_unify_and_t
    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) 
  in
  let proof',oldmetasenv =
-  let (puri,metasenv,pbo,pty, attrs) = proof in
-   (puri,newmetasenv,pbo,pty, attrs),metasenv
+  let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
+   (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
  in
  let goal_for_paramod =
   match LibraryObjects.eq_URI () with
@@ -479,7 +479,10 @@ let new_metasenv_and_unify_and_t
  in
  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
+ let proof'' = 
+   let uri,_,_subst,p,ty, attrs = proof' in 
+   uri,metasenv_for_paramod,_subst,p,ty, attrs 
+ in
  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
  let proof''',goals =
   ProofEngineTypes.apply_tactic
@@ -504,7 +507,7 @@ let new_metasenv_and_unify_and_t
  | Some (_,proof''''',_), active,passive,_  ->
      subst,proof''''',
      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
-       ~newmetasenv:(let _,m,_,_, _ = proof''''' in m),  active, passive
+       ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m),  active, passive
 ;;
 
 let rec count_prods context ty =
@@ -516,7 +519,7 @@ let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
-  let (_,metasenv,_,_, _) = proof in
+  let (_,metasenv,_subst,_,_, _) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let newmeta = CicMkImplicit.new_meta metasenv subst in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
@@ -1011,7 +1014,7 @@ let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
   subst, metasenv
 ;;
 let mk_fake_proof metasenv (goalno,_,_) goalty context = 
-  None,metasenv,Cic.Meta(goalno,mk_irl context),goalty, [] 
+  None,metasenv,[],Cic.Meta(goalno,mk_irl context),goalty, [] 
 ;;
 let equational_case 
   tables maxm cache depth fake_proof goalno goalty subst context 
@@ -1033,7 +1036,7 @@ let equational_case
         with 
           | None, active, passive, maxmeta -> 
               [], (active,passive,bag), cache, maxmeta, flags
-          | Some(subst',(_,metasenv,proof,_, _),open_goals),active,
+          | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
             passive,maxmeta ->
               assert_subst_are_disjoint subst subst';
               let subst = subst@subst' in
@@ -1059,7 +1062,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,proof,_, _),open_goals ->
+            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals = 
@@ -1081,7 +1084,7 @@ let try_candidate
 =
   let ppterm = ppterm context in
   try 
-    let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
+    let subst', ((_,metasenv,_subst,_,_, _), open_goals), maxmeta =
       PrimitiveTactics.apply_with_subst 
         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno) 
     in
@@ -1752,7 +1755,7 @@ let rec position_of i x = function
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   Saturation.reset_refs();
   let proof,goalno = status in 
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
   let eq_uri,tty = eq_and_ty_of_goal ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
@@ -1858,7 +1861,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
         ~target ~table ~subterms_only ~demod_table (proof,goal)
   | false -> 
       (* this is the real auto *)
-      let _,metasenv,_,_, _ = proof in
+      let _,metasenv,_subst,_,_, _ = proof in
       let _,context,goalty = CicUtil.lookup_meta goal metasenv in
       let flags = flags_of_params params () in
       (* just for testing *)
@@ -1873,7 +1876,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
               auto_all_solutions universe cache 
         else tables,cache,newmeta in
       let initial_time = Unix.gettimeofday() in
-      let (_,oldmetasenv,_,_, _) = proof in
+      let (_,oldmetasenv,_subst,_,_, _) = proof in
       hint := None;
       let elem = 
         metasenv,[],1,[D (goal,flags.maxdepth,P)],[]
@@ -1890,7 +1893,7 @@ let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
             *)
             let proof,metasenv = 
             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
-              proof goal (CicMetaSubst.apply_subst subst) metasenv
+              proof goal subst metasenv
             in
             let opened = 
               ProofEngineHelpers.compare_metasenvs ~oldmetasenv
@@ -1915,7 +1918,7 @@ let eq_of_goal = function
 
 (* DEMODULATE *)
 let demodulate_tac ~dbd ~universe (proof,goal)= 
-  let curi,metasenv,pbo,pty, attrs = proof in
+  let curi,metasenv,_subst,pbo,pty, attrs = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let initgoal = [], [], ty in
@@ -1942,7 +1945,7 @@ let demodulate_tac ~dbd ~universe (proof,goal)=
       in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
-          (curi,extended_metasenv,pbo,pty, attrs),goal in
+          (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
         let (status,newgoals) = 
           ProofEngineTypes.apply_tactic 
             (PrimitiveTactics.apply_tac ~term:proofterm)