From c6cc2a7227d6750076f591a62d7b1896ebf1ebfa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 May 2007 17:22:37 +0000 Subject: [PATCH] added a (for the moment) dummy field _subst to ProofengineTypes.proof. 36 file touched ;-) --- .../grafite_engine/grafiteEngine.ml | 21 +++++----- .../components/grafite_engine/grafiteTypes.ml | 14 +++---- helm/software/components/tactics/auto.ml | 39 ++++++++++--------- .../software/components/tactics/autoTactic.ml | 19 ++++----- .../components/tactics/declarative.ml | 8 ++-- .../tactics/discriminationTactics.ml | 8 ++-- .../components/tactics/eliminationTactics.ml | 6 +-- .../components/tactics/equalityTactics.ml | 18 ++++----- helm/software/components/tactics/fourierR.ml | 30 +++++++------- .../components/tactics/fwdSimplTactic.ml | 12 +++--- .../components/tactics/introductionTactics.ml | 2 +- helm/software/components/tactics/inversion.ml | 16 ++++---- .../components/tactics/inversion_principle.ml | 5 ++- .../components/tactics/metadataQuery.ml | 10 ++--- .../components/tactics/negationTactics.ml | 2 +- .../tactics/paramodulation/saturation.ml | 8 ++-- .../components/tactics/primitiveTactics.ml | 28 ++++++------- .../components/tactics/proofEngineHelpers.ml | 15 ++++--- .../components/tactics/proofEngineHelpers.mli | 2 +- .../tactics/proofEngineStructuralRules.ml | 12 +++--- .../components/tactics/proofEngineTypes.ml | 11 +++--- .../components/tactics/proofEngineTypes.mli | 2 +- .../components/tactics/reductionTactics.ml | 8 ++-- helm/software/components/tactics/ring.ml | 6 +-- helm/software/components/tactics/setoids.ml | 2 +- .../components/tactics/statefulProofEngine.ml | 25 ++++++------ .../components/tactics/substTactic.ml | 8 ++-- helm/software/components/tactics/tacticals.ml | 8 ++-- .../components/tactics/variousTactics.ml | 8 ++-- helm/software/matita/matita.ml | 8 ++-- helm/software/matita/matitaMathView.ml | 8 ++-- helm/software/matita/matitaScript.ml | 3 +- helm/software/matita/matitaWiki.ml | 2 +- 33 files changed, 194 insertions(+), 180 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 296625a1d..c961c58ae 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -332,14 +332,14 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = let after = ProofEngineTypes.goals_of_proof proof in let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in let proof, opened_goals = - let uri, metasenv_after_tactic, t, ty, attrs = proof in + let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in let reordered_metasenv, opened_goals = reorder_metasenv starting_metasenv metasenv_after_refinement metasenv_after_tactic opened goal always_opens_a_goal in - let proof' = uri, reordered_metasenv, t, ty, attrs in + let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in proof', opened_goals in let incomplete_proof = @@ -366,14 +366,14 @@ let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) ( let after = ProofEngineTypes.goals_of_proof proof in let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in let proof, opened_goals = - let uri, metasenv_after_tactic, t, ty, attrs = proof in + let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in let reordered_metasenv, opened_goals = reorder_metasenv starting_metasenv metasenv_after_refinement metasenv_after_tactic opened goal always_opens_a_goal in - let proof' = uri, reordered_metasenv, t, ty, attrs in + let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in proof', opened_goals in let incomplete_proof = @@ -681,16 +681,16 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status *) status,[] | GrafiteAst.Print (_,"proofterm") -> - let _,_,p,_, _ = GrafiteTypes.get_current_proof status in + let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in print_endline (AutoTactic.pp_proofterm p); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty, attrs = + let uri, metasenv, _subst, bo, ty, attrs = match status.GrafiteTypes.proof_status with - | GrafiteTypes.Proof (Some uri, metasenv, body, ty, attrs) -> - uri, metasenv, body, ty, attrs - | GrafiteTypes.Proof (None, metasenv, body, ty, attrs) -> + | GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) -> + uri, metasenv, subst, body, ty, attrs + | GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) -> raise (GrafiteTypes.Command_error ("Someone allows to start a theorem without giving the "^ "name/uri. This should be fixed!")) @@ -787,7 +787,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status ("Theorem already proved: " ^ UriManager.string_of_uri x ^ "\nPlease use a variant.")); end; - let initial_proof = (Some uri, metasenv', bo, ty, attrs) in + let _subst = [] in + let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in let initial_stack = Continuationals.Stack.of_metasenv metasenv' in { status with GrafiteTypes.proof_status = GrafiteTypes.Incomplete_proof diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index fe872c128..6e8be22bb 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -69,8 +69,8 @@ let get_current_proof status = let get_proof_metasenv status = match status.proof_status with | No_proof -> [] - | Proof (_, metasenv, _, _, _) - | Incomplete_proof { proof = (_, metasenv, _, _, _) } + | Proof (_, metasenv, _, _, _, _) + | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } | Intermediate metasenv -> metasenv @@ -93,11 +93,11 @@ let set_metasenv metasenv status = let proof_status = match status.proof_status with | No_proof -> Intermediate metasenv - | Incomplete_proof ({ proof = (uri, _, proof, ty, attrs) } as incomplete_proof) -> + | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) -> Incomplete_proof - { incomplete_proof with proof = (uri, metasenv, proof, ty, attrs) } + { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) } | Intermediate _ -> Intermediate metasenv - | Proof (_, metasenv', _, _, _) -> + | Proof (_, metasenv', _, _, _, _) -> assert (metasenv = metasenv'); status.proof_status in @@ -105,14 +105,14 @@ let set_metasenv metasenv status = let get_proof_context status goal = match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _, _) } -> + | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } -> let (_, context, _) = CicUtil.lookup_meta goal metasenv in context | _ -> [] let get_proof_conclusion status goal = match status.proof_status with - | Incomplete_proof { proof = (_, metasenv, _, _, _) } -> + | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } -> let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in conclusion | _ -> raise (Statement_error "no ongoing proof") diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index 3bec5b044..6f293ff4a 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/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) diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml index 79cf52e65..12041b2bc 100644 --- a/helm/software/components/tactics/autoTactic.ml +++ b/helm/software/components/tactics/autoTactic.ml @@ -56,7 +56,7 @@ let search_theorems_in_context status = let module S = CicSubstitution in let module PET = ProofEngineTypes in let module PT = PrimitiveTactics in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function | [] -> [] @@ -89,7 +89,7 @@ let search_theorems_in_context status = let compare_goals proof goal1 goal2 = - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1 @@ -129,7 +129,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals if List.mem ty already_seen_goals then [] else let already_seen_goals = ty::already_seen_goals in let facts = (depth = 1) in - let _,metasenv,p,_, _ = proof in + let _,metasenv,_subst, p,_, _ = proof in (* first of all we check if the goal has been already inspected *) assert (CicUtil.exists_meta goal metasenv); @@ -148,12 +148,13 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will be dropped *) - CicMetaSubst.apply_subst - [(goal,(ey, bo, Cic.Implicit None))] in + [(goal,(ey, bo, Cic.Implicit None))] + in + let _ = assert false in let (proof,_) = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof goal subst_in metasenv in - [(subst_in,(proof,[],sign))] + [(CicMetaSubst.apply_subst subst_in,(proof,[],sign))] | No d when (d >= depth) -> (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *) [] (* the empty list means no choices, i.e. failure *) @@ -228,7 +229,7 @@ let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals and auto_new dbd width already_seen_goals universe = function | [] -> [] | (subst,(proof, goals, sign))::tl -> - let _,metasenv,_,_, _ = proof in + let _,metasenv, _subst, _,_, _ = proof in let goals'= List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals in @@ -244,7 +245,7 @@ and auto_new_aux dbd width already_seen_goals universe = function (List.length goals) > width -> auto_new dbd width already_seen_goals universe tl | (subst,(proof, (goal,depth)::gtl, sign))::tl -> - let _,metasenv,p,_, _ = proof in + let _,metasenv,_subst,p,_, _ = proof in let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in match (auto_single dbd proof goal ey ty depth (width - (List.length gtl)) sign already_seen_goals) universe @@ -284,7 +285,7 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_, _ = proof in + let _,_,_subst,p,_, _ = proof in debug_print (lazy (CicPp.ppterm p)); debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); (proof,[]) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index e36c86037..2f012ed40 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -123,10 +123,10 @@ let we_need_to_prove t id ty = let existselim ~dbd ~universe t id1 t1 id2 t2 = let aux (proof, goal) = - let (n,metasenv,bo,ty,attrs) = proof in + let (n,metasenv,_subst,bo,ty,attrs) = proof in let metano,context,_ = CicUtil.lookup_meta goal metasenv in let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in - let proof' = (n,metasenv,bo,ty,attrs) in + let proof' = (n,metasenv,_subst,bo,ty,attrs) in ProofEngineTypes.apply_tactic ( Tacticals.thens ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)])) @@ -155,7 +155,7 @@ let andelim t id1 t1 id2 t2 = let rewritingstep ~dbd ~universe lhs rhs just last_step = let aux ((proof,goal) as status) = - let (curi,metasenv,proofbo,proofty, attrs) = proof in + let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in let _,context,gty = CicUtil.lookup_meta goal metasenv in let eq,trans = match LibraryObjects.eq_URI () with @@ -221,7 +221,7 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context (Cic.Name name) ~typ in - let proof = curi,metasenv,proofbo,proofty, attrs in + let proof = curi,metasenv,_subst,proofbo,proofty, attrs in let proof,goals = ProofEngineTypes.apply_tactic (Tacticals.thens diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index ccbf17ae6..9d83ad595 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/components/tactics/discriminationTactics.ml @@ -145,7 +145,7 @@ let discriminate_tac ~term = in let discriminate'_tac ~term status = let (proof, goal) = status in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph @@ -228,7 +228,7 @@ let rec injection_tac ~first_time ~term ~liftno ~continuation = in let injection_tac ~term status = let (proof, goal) = status in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst, _,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let term = CicSubstitution.lift liftno term in let termty,_ = @@ -335,7 +335,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = * differiscono (o potrebbero differire?) nell'i-esimo parametro * del costruttore *) let term = CicSubstitution.lift liftno term in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph @@ -467,7 +467,7 @@ and injection1_tac ~term ~i ~liftno ~continuation = (fun status -> debug_print (lazy "riempo il cut"); let (proof, goal) = status in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,gty =CicUtil.lookup_meta goal metasenv in let gty = Unshare.unshare gty in let new_t1' = diff --git a/helm/software/components/tactics/eliminationTactics.ml b/helm/software/components/tactics/eliminationTactics.ml index f18d2b333..29961db38 100644 --- a/helm/software/components/tactics/eliminationTactics.ml +++ b/helm/software/components/tactics/eliminationTactics.ml @@ -91,7 +91,7 @@ let rec check_type sorts metasenv context t = let rec scan_tac ~old_context_length ~index ~tactic = let scan_tac status = let (proof, goal) = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let context_length = List.length context in let rec aux index = @@ -111,7 +111,7 @@ let rec scan_tac ~old_context_length ~index ~tactic = let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what = let elim_clear_unfold_tac status = let (proof, goal) = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let index, ty = PEH.lookup_type metasenv context what in let tac = @@ -159,7 +159,7 @@ let decompose_tac ?(sorts=[CicPp.ppsort C.Prop; CicPp.ppsort C.CProp]) ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () = let decompose_tac status = let (proof, goal) = status in - let _, metasenv,_,_, _ = proof in + let _, metasenv, _subst, _,_, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in let old_context_length = List.length context in diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index f284a2d1d..bd73865af 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/components/tactics/equalityTactics.ml @@ -44,7 +44,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = let _rewrite_tac status = assert (wanted = None); (* this should be checked syntactically *) let proof,goal = status in - let curi, metasenv, pbo, pty, attrs = proof in + let curi, metasenv, _subst, pbo, pty, attrs = proof in let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in let gsort,_ = CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in @@ -196,7 +196,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = try let (proof',goals) = PET.apply_tactic - (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty, attrs),goal) + (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal) in let goals = goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv @@ -229,7 +229,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status = let _wanted, hyps_pat, concl_pat = pattern in let (proof, goal) = status in - let uri,metasenv,pbo,pty, attrs = proof in + let uri,metasenv,_subst,pbo,pty, attrs = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in assert (hyps_pat = []); (*CSC: not implemented yet *) let eq_URI = @@ -246,7 +246,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = let with_what = CicMetaSubst.apply_subst subst with_what in let pbo = CicMetaSubst.apply_subst subst pbo in let pty = CicMetaSubst.apply_subst subst pty in - let status = (uri,metasenv,pbo,pty, attrs),goal in + let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in let ty_of_with_what,u = CicTypeChecker.type_of_aux' metasenv context with_what CicUniv.empty_ugraph in @@ -288,7 +288,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = (ProofEngineTypes.Fail (lazy "Replace: one of the selected terms and the term to be replaced with have not convertible types")) ) l in - let rec aux n whats status = + let rec aux n whats (status : ProofEngineTypes.status) = match whats with [] -> ProofEngineTypes.apply_tactic T.id_tac status | (what,lazy_pattern)::tl -> @@ -313,7 +313,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = ~start:( ProofEngineTypes.mk_tactic (function ((proof,goal) as status) -> - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let hyps = try @@ -328,7 +328,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what = T.id_tac]) status and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in - aux 0 whats status + aux 0 whats (status : ProofEngineTypes.status) in ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what) ;; @@ -342,7 +342,7 @@ let reflexivity_tac = let symmetry_tac = let symmetry_tac (proof, goal) = - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) @@ -360,7 +360,7 @@ let symmetry_tac = let transitivity_tac ~term = let transitivity_tac ~term status = let (proof, goal) = status in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml index d9f0ce9a4..8e443447a 100644 --- a/helm/software/components/tactics/fourierR.ml +++ b/helm/software/components/tactics/fourierR.ml @@ -577,7 +577,7 @@ let tac_zero_inf_pos (n,d) = (*let cste = pf_parse_constr gl in*) let pall str (proof,goal) t = debug ("tac "^str^" :\n" ); - 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 debug ("th = "^ CicPp.ppterm t ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -675,7 +675,7 @@ let tac_zero_inf_false gl (n,d) = let tac_zero_infeq_false gl (n,d) = let tac_zero_infeq_false gl (n,d) status = let (proof, goal) = 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 goal metasenv in debug("faccio fold di " ^ CicPp.ppterm @@ -713,13 +713,13 @@ let tac_zero_infeq_false gl (n,d) = let apply_type_tac ~cast:t ~applist:al = let apply_type_tac ~cast:t ~applist:al (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 fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,t)::metasenv in - let proof' = curi,metasenv',pbo,pty, attrs in + let proof' = curi,metasenv',_subst,pbo,pty, attrs in let proof'',goals = apply_tactic (PrimitiveTactics.apply_tac @@ -734,13 +734,13 @@ let apply_type_tac ~cast:t ~applist:al = let my_cut ~term:c = let my_cut ~term:c (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 fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let metasenv' = (fresh_meta,context,c)::metasenv in - let proof' = curi,metasenv',pbo,pty, attrs in + let proof' = curi,metasenv',_subst,pbo,pty, attrs in let proof'',goals = apply_tactic (apply_type_tac @@ -762,7 +762,7 @@ let tac_use h = let tac_use h status = let (proof, goal) = status in debug("Inizio TC_USE\n"); - 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 debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -873,7 +873,7 @@ let equality_replace a b = debug("inizio EQ\n"); let module C = Cic in let proof,goal = 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 goal metasenv in let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in @@ -886,7 +886,7 @@ let equality_replace a b = ~direction:`LeftToRight ~pattern:(ProofEngineTypes.conclusion_pattern None) (C.Meta (fresh_meta,irl)) []) - ((curi,metasenv',pbo,pty, attrs),goal) + ((curi,metasenv',_subst,pbo,pty, attrs),goal) in let new_goals = fresh_meta::goals in debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " @@ -934,7 +934,7 @@ let contradiction_tac (proof,goal)= (* ********************* TATTICA ******************************** *) let rec fourier (s_proof,s_goal)= - let s_curi,s_metasenv,s_pbo,s_pty, attrs = s_proof in + let s_curi,s_metasenv,_subst,s_pbo,s_pty, attrs = s_proof in let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n"); debug_pcontext s_context; @@ -974,7 +974,7 @@ let rec fourier (s_proof,s_goal)= (* now we have all the right environment *) - 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 (* now we want to convert hp to inequations, but first we must lift @@ -1061,7 +1061,7 @@ let rec fourier (s_proof,s_goal)= (Tacticals.thens ~start:(mk_tactic (fun status -> debug ("inizio t1 strict\n"); - 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 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -1092,7 +1092,7 @@ let rec fourier (s_proof,s_goal)= tac1:=(Tacticals.thens ~start:(mk_tactic (fun status -> debug("INIZIO TAC 1 2\n"); - 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 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); @@ -1128,7 +1128,7 @@ let rec fourier (s_proof,s_goal)= ~continuations:[Tacticals.then_ ~start:( mk_tactic (fun status -> let (proof, goal) = 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 goal metasenv in apply_tactic (ReductionTactics.change_tac @@ -1167,7 +1167,7 @@ let rec fourier (s_proof,s_goal)= Tacticals.then_ ~start:(mk_tactic (fun status -> let (proof, goal) = 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 goal metasenv in (* check if ty is of type *) let w1 = diff --git a/helm/software/components/tactics/fwdSimplTactic.ml b/helm/software/components/tactics/fwdSimplTactic.ml index 60d43e7c7..8734837d1 100644 --- a/helm/software/components/tactics/fwdSimplTactic.ml +++ b/helm/software/components/tactics/fwdSimplTactic.ml @@ -47,7 +47,7 @@ let error msg = raise (PET.Fail (lazy msg)) let id_tac = let id_tac (proof,goal) = try - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in (proof,[goal]) with CicUtil.Meta_not_found _ -> (proof, []) @@ -62,7 +62,7 @@ let clearbody ~index = in let clearbody status = let (proof, goal) = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status in @@ -109,7 +109,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name (* ?(substs = []) *) ?how_many ?(to_what = []) what = let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in let lapply_tac (proof, goal) = - let xuri, metasenv, u, t, attrs = proof in + let xuri, metasenv, _subst, u, t, attrs = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in let lemma = FNG.clean_dummy_dependent_types lemma in @@ -121,7 +121,7 @@ let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name T.then_ ~start:(letin_tac conclusion) ~continuation:(clearbody ~index:1) in - let proof = (xuri, metasenv, u, t, attrs) in + let proof = (xuri, metasenv, _subst, u, t, attrs) in let aux (proof, goals) (tac, goal) = let proof, new_goals = PET.apply_tactic tac (proof, goal) in proof, goals @ new_goals @@ -134,7 +134,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what = let lapply_tac status = let proof, goal = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in let tac = @@ -159,7 +159,7 @@ let fwd_simpl_tac in let fwd_simpl_tac status = let (proof, goal) = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, context, ty = CicUtil.lookup_meta goal metasenv in let index, major = PEH.lookup_type metasenv context hyp in match FwdQueries.fwd_simpl ~dbd major with diff --git a/helm/software/components/tactics/introductionTactics.ml b/helm/software/components/tactics/introductionTactics.ml index 07a0c40b5..d8caf933b 100644 --- a/helm/software/components/tactics/introductionTactics.ml +++ b/helm/software/components/tactics/introductionTactics.ml @@ -28,7 +28,7 @@ let fake_constructor_tac ~n (proof, goal) = let module C = Cic in let module R = CicReduction in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in match (R.whd context ty) with (C.MutInd (uri, typeno, exp_named_subst)) diff --git a/helm/software/components/tactics/inversion.ml b/helm/software/components/tactics/inversion.ml index 5f90c45eb..19d0c739a 100644 --- a/helm/software/components/tactics/inversion.ml +++ b/helm/software/components/tactics/inversion.ml @@ -183,7 +183,7 @@ let private_inversion_tac ~term = let private_inversion_tac ~term (proof, goal) = (*DEBUG*) debug_print (lazy ("private inversion begins")); - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let uri_of_eq = match LibraryObjects.eq_URI () with None -> raise EqualityNotDefinedYet @@ -240,7 +240,7 @@ let private_inversion_tac ~term = (*DEBUG*) debug_print (lazy ("after apply HCUT;reflexivity in private inversion")); (* apply (ledx_ind( lambda x. lambda y, ...)) *) - let t1,metasenv,t3,t4, attrs = proof2 in + let t1,metasenv,_subst,t3,t4, attrs = proof2 in let goal2 = List.hd (List.tl gl1) in let (_,context,_) = CicUtil.lookup_meta goal2 metasenv in (* rightparameters type list *) @@ -265,13 +265,13 @@ let private_inversion_tac ~term = in (*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: " ^ CicPp.ppterm ref_t)); - let proof2 = (t1,metasenv'',t3,t4, attrs) in + let proof2 = (t1,metasenv'',_subst,t3,t4, attrs) in let my_apply_tac = let my_apply_tac status = let proof,goals = ProofEngineTypes.apply_tactic (P.apply_tac ref_t) status in let patched_new_goals = - let (_,metasenv''',_,_, _) = proof in + let (_,metasenv''',_subst,_,_, _) = proof in let new_goals = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in @@ -305,7 +305,7 @@ let inversion_tac ~term = let module PET = ProofEngineTypes in let inversion_tac ~term (proof, goal) = (*DEBUG*) debug_print (lazy ("inversion begins")); - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let uri, typeno = @@ -340,15 +340,15 @@ let inversion_tac ~term = Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1]) in let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in - let (t1,metasenv,t3,t4, attrs) = proof in + let (t1,metasenv,_subst,t3,t4, attrs) = proof in let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t CicUniv.empty_ugraph in - let proof = (t1,metasenv'',t3,t4, attrs) in + let proof = (t1,metasenv'',_subst,t3,t4, attrs) in let proof3,gl3 = ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in let patched_new_goals = - let (_,metasenv''',_,_, _) = proof3 in + let (_,metasenv''',_subst,_,_, _) = proof3 in let new_goals = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in diff --git a/helm/software/components/tactics/inversion_principle.ml b/helm/software/components/tactics/inversion_principle.ml index b0f4d236f..45ece4823 100644 --- a/helm/software/components/tactics/inversion_principle.ml +++ b/helm/software/components/tactics/inversion_principle.ml @@ -154,8 +154,9 @@ let build_inversion uri obj = let goal = CicMkImplicit.new_meta metasenv [] in let metasenv' = (goal,[],ref_theorem)::metasenv in let attrs = [`Class (`InversionPrinciple); `Generated] in + let _subst = [] in let proof= - (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in + (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in let _,applies = List.fold_right (fun _ (i,applies) -> @@ -186,7 +187,7 @@ let build_inversion uri obj = (proof,goal) in let metasenv,bo,ty, attrs = - match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs + match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs in assert (metasenv = []); Some diff --git a/helm/software/components/tactics/metadataQuery.ml b/helm/software/components/tactics/metadataQuery.ml index 2cfd95e9a..6b87de349 100644 --- a/helm/software/components/tactics/metadataQuery.ml +++ b/helm/software/components/tactics/metadataQuery.ml @@ -109,7 +109,7 @@ let filter_uris_backward ~dbd ~facts signature uris = intersect uris siguris let compare_goal_list proof goal1 goal2 = - let _,metasenv,_,_, _ = proof in + let _,metasenv, _subst, _,_, _ = proof in let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in let ty_sort1,_ = @@ -195,7 +195,7 @@ let cmatch' = Constr.cmatch' (* used only by te old auto *) let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) = - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = Constr.signature_of ty in let set = signature_of_hypothesis context metasenv in @@ -344,7 +344,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = ^ "\n}" in *) - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let main, sig_constants = match signature with @@ -394,7 +394,7 @@ let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) = let experimental_hint ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) = - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let (uris, (main, sig_constants)) = match signature with @@ -478,7 +478,7 @@ let new_experimental_hint ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe ((proof, goal) as status) = - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, ty) = CicUtil.lookup_meta goal metasenv in let (uris, (main, sig_constants)) = match signature with diff --git a/helm/software/components/tactics/negationTactics.ml b/helm/software/components/tactics/negationTactics.ml index e77fdf4de..fb904bf36 100644 --- a/helm/software/components/tactics/negationTactics.ml +++ b/helm/software/components/tactics/negationTactics.ml @@ -31,7 +31,7 @@ let absurd_tac ~term = let module C = Cic in let module U = UriManager in let module P = PrimitiveTactics in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let absurd_URI = match LibraryObjects.absurd_URI () with diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index f8b12c119..f8b0ff45f 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -1319,7 +1319,7 @@ let build_proof if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA" else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv); let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove, attrs = proof in + let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let names = Utils.names_of_context context in @@ -1394,7 +1394,7 @@ let build_proof *) let proof, real_metasenv = ProofEngineHelpers.subst_meta_and_metasenv_in_proof - proof goalno (CicMetaSubst.apply_subst final_subst) + proof goalno final_subst (List.filter (fun i,_,_ -> i<>goalno ) real_menv) in let open_goals = @@ -1568,7 +1568,7 @@ let pump_actives context bag maxm active passive saturation_steps max_time = let all_subsumed bag maxm status active passive = maxmeta := maxm; let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove, attrs = proof in + let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let env = metasenv,context,CicUniv.empty_ugraph in let cleaned_goal = Utils.remove_local_context type_of_goal in @@ -1615,7 +1615,7 @@ let given_clause let mp = max_l passive_l in *) let proof, goalno = status in - let uri, metasenv, meta_proof, term_to_prove, attrs = proof in + let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in let eq_uri = eq_of_goal type_of_goal in let cleaned_goal = Utils.remove_local_context type_of_goal in diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index c5aab0f5f..aeb0c0751 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -261,7 +261,7 @@ let apply_with_subst ~term ~subst ~maxmeta (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 = max (CicMkImplicit.new_meta metasenv subst) maxmeta in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = @@ -325,7 +325,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) = let subst_in = (* if we just apply the subtitution, the type is irrelevant: we may use Implicit, since it will be dropped *) - CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst) + ((metano,(context,bo',Cic.Implicit None))::subst) in let (newproof, newmetasenv''') = ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in @@ -373,7 +373,7 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_ = let module C = Cic in let module R = CicReduction in - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let (context',ty',bo') = @@ -393,7 +393,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic 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 goal metasenv in let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in let newmeta2 = newmeta1 + 1 in @@ -428,7 +428,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: term (proof, goal) = let module C = Cic in - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in (* occur check *) let occur i t = let m = CicUtil.metas_of_term t in @@ -464,7 +464,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst: let exact_tac ~term = let exact_tac ~term (proof, goal) = (* Assumption: the term bo must be closed in the current context *) - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let module T = CicTypeChecker in let module R = CicReduction in @@ -497,7 +497,7 @@ module RT = ReductionTactics let beta_after_elim_tac upto predicate = let beta_after_elim_tac status = let proof, goal = status in - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, _, ty = CicUtil.lookup_meta goal metasenv in let mk_pattern ~equality ~upto ~predicate ty = (* code adapted from ProceduralConversion.generalize *) @@ -564,7 +564,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = | _ -> raise (PET.Fail (lazy "not implemented")) in let ugraph = CicUniv.empty_ugraph in - let curi, metasenv, proofbo, proofty, attrs = proof in + let curi, metasenv, _subst, proofbo, proofty, attrs = proof in let conjecture = CicUtil.lookup_meta goal metasenv in let metano, context, ty = conjecture in let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in @@ -686,13 +686,13 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term = ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty, attrs in + let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_,_, _) = proof'' in + let (_,metasenv''',_subst,_,_, _) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' @@ -714,7 +714,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera let module U = UriManager in let module R = CicReduction in let module C = Cic in - let (curi,metasenv,proofbo,proofty, attrs) = proof in + let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in let termty = CicReduction.whd context termty in @@ -825,13 +825,13 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:metasenv'' in - let proof' = curi,metasenv'',proofbo,proofty, attrs in + let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in let proof'', new_goals' = PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal) in (* The apply_tactic can have closed some of the new_goals *) let patched_new_goals = - let (_,metasenv''',_,_,_) = proof'' in + let (_,metasenv''',_subst,_,_,_) = proof'' in List.filter (function i -> List.exists (function (j,_,_) -> j=i) metasenv''') new_goals @ new_goals' @@ -866,7 +866,7 @@ let letout_tac = let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in let term = C.Sort C.Set in let letout_tac (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 newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in diff --git a/helm/software/components/tactics/proofEngineHelpers.ml b/helm/software/components/tactics/proofEngineHelpers.ml index 2a6371353..85dba95ea 100644 --- a/helm/software/components/tactics/proofEngineHelpers.ml +++ b/helm/software/components/tactics/proofEngineHelpers.ml @@ -27,11 +27,11 @@ exception Bad_pattern of string Lazy.t -let new_meta_of_proof ~proof:(_, metasenv, _, _, _) = +let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) = CicMkImplicit.new_meta metasenv [] let subst_meta_in_proof proof meta term newmetasenv = - let uri,metasenv,bo,ty, attrs = proof in + let uri,metasenv,initial_subst,bo,ty, attrs = proof in (* empty context is ok for term since it wont be used by apply_subst *) (* hack: since we do not know the context and the type of term, we create a substitution with cc =[] and type = Implicit; they will be @@ -62,7 +62,7 @@ let subst_meta_in_proof proof meta term newmetasenv = * since the parser does not reject as statements terms with * metavariable therein *) let ty' = subst_in ty in - let newproof = uri,metasenv'',bo',ty', attrs in + let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in (newproof, metasenv'') (*CSC: commento vecchio *) @@ -77,8 +77,9 @@ let subst_meta_in_proof proof meta term newmetasenv = (*CSC: ci ripasso sopra apply_subst!!! *) (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *) (*CSC: [newmetasenv]. *) -let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = - let (uri,_,bo,ty, attrs) = proof in +let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv = + let (uri,_,initial_subst,bo,ty, attrs) = proof in + let subst_in = CicMetaSubst.apply_subst subst in let bo' = subst_in bo in (* Metavariables can appear also in the *statement* of the theorem * since the parser does not reject as statements terms with @@ -104,7 +105,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = | _ -> i ) newmetasenv [] in - let newproof = uri,metasenv',bo',ty', attrs in + (* qui da capire se per la fase transitoria si fa initial_subst @ subst + * oppure subst *) + let newproof = uri,metasenv',subst,bo',ty', attrs in (newproof, metasenv') let compare_metasenvs ~oldmetasenv ~newmetasenv = diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli index 0a053ece7..1eeb0aca3 100644 --- a/helm/software/components/tactics/proofEngineHelpers.mli +++ b/helm/software/components/tactics/proofEngineHelpers.mli @@ -35,7 +35,7 @@ val subst_meta_in_proof : ProofEngineTypes.proof * Cic.metasenv val subst_meta_and_metasenv_in_proof : ProofEngineTypes.proof -> - int -> (Cic.term -> Cic.term) -> Cic.metasenv -> + int -> Cic.substitution -> Cic.metasenv -> ProofEngineTypes.proof * Cic.metasenv (* returns the list of goals that are in newmetasenv and were not in diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index 636ea07c0..ea7586e16 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.ml +++ b/helm/software/components/tactics/proofEngineStructuralRules.ml @@ -30,7 +30,7 @@ module C = Cic let clearbody ~hyp = let clearbody (proof, goal) = - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let metano,_,_ = CicUtil.lookup_meta goal metasenv in let string_of_name = function @@ -93,13 +93,13 @@ let clearbody ~hyp = | t -> t ) metasenv in - (curi,metasenv',pbo,pty, attrs), [goal] + (curi,metasenv',_subst,pbo,pty, attrs), [goal] in PET.mk_tactic clearbody let clear_one ~hyp = let clear_one (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 @@ -151,7 +151,7 @@ let clear_one ~hyp = | t -> t ) metasenv in - (curi,metasenv',pbo,pty, attrs), [goal] + (curi,metasenv',_subst,pbo,pty, attrs), [goal] in PET.mk_tactic clear_one @@ -176,7 +176,7 @@ let rename ~froms ~tos = try List.combine froms tos with Invalid_argument _ -> raise (PET.Fail (lazy error)) in - let curi, metasenv, pbo, pty, attrs = proof in + let curi, metasenv, _subst, pbo, pty, attrs = proof in let metano, _, _ = CicUtil.lookup_meta goal metasenv in let rename_map = function | Some (Cic.Name hyp, decl_or_def) as entry -> @@ -191,6 +191,6 @@ let rename ~froms ~tos = | conjecture -> conjecture in let metasenv = List.map map metasenv in - (curi, metasenv, pbo, pty, attrs), [goal] + (curi, metasenv, _subst, pbo, pty, attrs), [goal] in PET.mk_tactic rename diff --git a/helm/software/components/tactics/proofEngineTypes.ml b/helm/software/components/tactics/proofEngineTypes.ml index eb48ff3e8..abe460775 100644 --- a/helm/software/components/tactics/proofEngineTypes.ml +++ b/helm/software/components/tactics/proofEngineTypes.ml @@ -28,7 +28,7 @@ (** current proof (proof uri * metas * (in)complete proof * term to be prooved) *) -type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list +type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list (** current goal, integer index *) type goal = int type status = proof * goal @@ -43,8 +43,9 @@ let initial_status ty metasenv attrs = aux max tl in let newmeta_idx = aux 0 metasenv in + let _subst = [] in let proof = - None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty, attrs + None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs in (proof, newmeta_idx) @@ -90,13 +91,13 @@ exception Fail of string Lazy.t calls the opaque tactic on the status *) let apply_tactic t status = - let (uri,metasenv,bo,ty, attrs), gl = t status in + let (uri,metasenv,subst,bo,ty, attrs), gl = t status in match CicRefine.pack_coercion_obj (Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs)) with | Cic.CurrentProof (_,metasenv,_,ty,_, attrs) -> - (uri,metasenv,bo,ty, attrs), gl + (uri,metasenv,subst,bo,ty, attrs), gl | _ -> assert false ;; @@ -104,5 +105,5 @@ let apply_tactic t status = type mk_fresh_name_type = Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name -let goals_of_proof (_,metasenv,_,_,_) = List.map (fun (g,_,_) -> g) metasenv +let goals_of_proof (_,metasenv,_subst,_,_,_) = List.map (fun (g,_,_) -> g) metasenv diff --git a/helm/software/components/tactics/proofEngineTypes.mli b/helm/software/components/tactics/proofEngineTypes.mli index f326a469f..6edcfeccc 100644 --- a/helm/software/components/tactics/proofEngineTypes.mli +++ b/helm/software/components/tactics/proofEngineTypes.mli @@ -27,7 +27,7 @@ current proof (proof uri * metas * (in)complete proof * term to be prooved) *) type proof = - UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list + UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list (** current goal, integer index *) type goal = int type status = proof * goal diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index 685baff9b..3afef8eed 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -30,7 +30,7 @@ open ProofEngineTypes (* Note: this code is almost identical to change_tac and * it could be unified by making the change function a callback *) let reduction_tac ~reduction ~pattern (proof,goal) = - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change subst where terms metasenv ugraph = if terms = [] then where, metasenv, ugraph @@ -88,7 +88,7 @@ let reduction_tac ~reduction ~pattern (proof,goal) = | _ as t -> t ) metasenv in - (curi,metasenv',pbo,pty, attrs), [metano] + (curi,metasenv',_subst,pbo,pty, attrs), [metano] ;; let simpl_tac ~pattern = @@ -137,7 +137,7 @@ exception NotConvertible term(s) to be replaced. *) let change_tac ~pattern with_what = let change_tac ~pattern ~with_what (proof, goal) = - let curi,metasenv,pbo,pty, attrs = proof in + let curi,metasenv,_subst,pbo,pty, attrs = proof in let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let change subst where terms metasenv ugraph = if terms = [] then where, metasenv, ugraph @@ -206,7 +206,7 @@ let change_tac ~pattern with_what = | _ as t -> t) metasenv in - (curi,metasenv',pbo,pty, attrs), [metano] + (curi,metasenv',_subst,pbo,pty, attrs), [metano] in mk_tactic (change_tac ~pattern ~with_what) diff --git a/helm/software/components/tactics/ring.ml b/helm/software/components/tactics/ring.ml index b2d303270..7695a4ff0 100644 --- a/helm/software/components/tactics/ring.ml +++ b/helm/software/components/tactics/ring.ml @@ -122,14 +122,14 @@ let cic_is_const ?(uri: uri option = None) term = @param proof a proof @return the uri of a given proof *) -let uri_of_proof ~proof:(uri, _, _, _, _) = uri +let uri_of_proof ~proof:(uri, _, _, _, _, _) = uri (** @param status current proof engine status @raise Failure if proof is None @return current goal's metasenv *) -let metasenv_of_status ((_,m,_,_, _), _) = m +let metasenv_of_status ((_,m,_,_,_, _), _) = m (** @param status a proof engine status @@ -447,7 +447,7 @@ let purge_hyps_tac ~count = (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status)) | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let (_, context, _) = CicUtil.lookup_meta goal metasenv in let proof',goal' = aux count context status in assert (goal = goal') ; diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml index 1e650cc7a..7d0e958cc 100644 --- a/helm/software/components/tactics/setoids.ml +++ b/helm/software/components/tactics/setoids.ml @@ -1816,7 +1816,7 @@ let setoid_replace_in id relation c1 c2 ~new_goals (*COQgl*) = let setoid_reflexivity_tac = let tac ((proof,goal) as status) = - let (_,metasenv,_,_, _) = proof in + let (_,metasenv,_subst,_,_, _) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in try let relation_class = diff --git a/helm/software/components/tactics/statefulProofEngine.ml b/helm/software/components/tactics/statefulProofEngine.ml index 4e3badea4..37800187a 100644 --- a/helm/software/components/tactics/statefulProofEngine.ml +++ b/helm/software/components/tactics/statefulProofEngine.ml @@ -52,11 +52,12 @@ class ['a] status incr next_id; !next_id in - let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ, attrs) in + let _subst = ([] : Cic.substitution) in + let initial_proof = ((uri: UriManager.uri option), metasenv, _subst, body, typ, attrs) in let next_goal (goals, proof) = match goals, proof with | goal :: _, _ -> Some goal - | [], (_, (goal, _, _) :: _, _, _, _) -> + | [], (_, (goal, _, _) :: _, _, _, _, _) -> (* the tactic left no open goal: let's choose the first open goal *) Some goal | _, _ -> None @@ -109,24 +110,24 @@ class ['a] status raise exn *) - method uri = let (uri, _, _, _, _) = _proof in uri - method metasenv = let (_, metasenv, _, _, _) = _proof in metasenv - method body = let (_, _, body, _, _) = _proof in body - method typ = let (_, _, _, typ, _) = _proof in typ - method attrs = let (_, _, _, _, attrs) = _proof in attrs + method uri = let (uri, _, _, _, _, _) = _proof in uri + method metasenv = let (_, metasenv, _, _, _, _) = _proof in metasenv + method body = let (_, _, _, body, _, _) = _proof in body + method typ = let (_, _, _, _, typ, _) = _proof in typ + method attrs = let (_, _, _, _, _, attrs) = _proof in attrs method set_metasenv metasenv = - let (uri, _, body, typ, attes) = _proof in - _proof <- (uri, metasenv, body, typ, attrs) + let (uri, _, _subst,body, typ, attes) = _proof in + _proof <- (uri, metasenv, _subst,body, typ, attrs) method set_uri uri = - let (old_uri, metasenv, body, typ, attrs) = _proof in + let (old_uri, metasenv, _subst,body, typ, attrs) = _proof in if old_uri <> None then raise Uri_redefinition; - _proof <- (Some uri, metasenv, body, typ, attrs) + _proof <- (Some uri, metasenv, _subst,body, typ, attrs) method conjecture goal = - let (_, metasenv, _, _, _) = _proof in + let (_, metasenv, _subst, _, _, _) = _proof in CicUtil.lookup_meta goal metasenv method apply_tactic tactic = diff --git a/helm/software/components/tactics/substTactic.ml b/helm/software/components/tactics/substTactic.ml index cc107451e..feff68f3f 100644 --- a/helm/software/components/tactics/substTactic.ml +++ b/helm/software/components/tactics/substTactic.ml @@ -40,7 +40,7 @@ module TC = CicTypeChecker let lift_rewrite_tac ~context ~direction ~pattern equality = let lift_rewrite_tac status = let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let _, new_context, _ = CicUtil.lookup_meta goal metasenv in let n = List.length new_context - List.length context in let equality = S.lift n equality in @@ -51,7 +51,7 @@ let lift_rewrite_tac ~context ~direction ~pattern equality = let lift_destruct_tac ~context ~what = let lift_destruct_tac status = let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let _, new_context, _ = CicUtil.lookup_meta goal metasenv in let n = List.length new_context - List.length context in let what = S.lift n what in @@ -79,7 +79,7 @@ let rec subst_tac ~try_tactic ~hyp = in let subst_tac status = let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let what = match PEH.get_rel context hyp with | Some t -> t @@ -148,7 +148,7 @@ let subst_tac = | _ -> None in let (proof, goal) = status in - let (_, metasenv, _, _, _) = proof in + let (_, metasenv, _subst, _, _, _) = proof in let _, context, _ = CicUtil.lookup_meta goal metasenv in let tactics = HEL.list_rev_map_filter map context in let result = PET.apply_tactic (T.seq ~tactics) status in diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml index 3e9c1db2c..f3f779303 100644 --- a/helm/software/components/tactics/tacticals.ml +++ b/helm/software/components/tactics/tacticals.ml @@ -42,7 +42,7 @@ module PET = ProofEngineTypes let id_tac = let id_tac (proof,goal) = - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in (proof,[goal]) in @@ -50,7 +50,7 @@ let id_tac = let fail_tac = let fail_tac (proof,goal) = - let _, metasenv, _, _, _ = proof in + let _, metasenv, _subst, _ , _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in raise (PET.Fail (lazy "fail tactical")) in @@ -255,8 +255,8 @@ let solve_tactics ~tactics = let progress_tactic ~tactic = let msg = lazy "Failed to progress" in - let progress_tactic (((_,metasenv,_,_,_),_) as istatus) = - let ((_,metasenv',_,_,_),_) as ostatus = + let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) = + let ((_,metasenv',_subst,_,_,_),_) as ostatus = PET.apply_tactic tactic istatus in (*CSC: Warning diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml index 16a9c2267..3a3db7db4 100644 --- a/helm/software/components/tactics/variousTactics.ml +++ b/helm/software/components/tactics/variousTactics.ml @@ -38,7 +38,7 @@ let assumption_tac = let module R = CicReduction in let module S = CicSubstitution in let module PT = PrimitiveTactics in - let _,metasenv,_,_, _ = proof in + let _,metasenv,_subst,_,_, _ = proof in let _,context,ty = CicUtil.lookup_meta goal metasenv in let rec find n = function hd::tl -> @@ -83,7 +83,7 @@ let generalize_tac let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in - let uri,metasenv,pbo,pty, attrs = proof in + let uri,metasenv,_subst,pbo,pty, attrs = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in let subst,metasenv,u,selected_hyps,terms_with_context = ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph @@ -157,7 +157,7 @@ let generalize_tac else u1 ) u terms_with_context) ; - let status = (uri,metasenv',pbo,pty, attrs),goal in + let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in let proof,goals = PET.apply_tactic (T.thens @@ -177,7 +177,7 @@ let generalize_tac T.id_tac]) status in - let _,metasenv'',_,_, _ = proof in + let _,metasenv'',_subst,_,_, _ = proof in (* CSC: the following is just a bad approximation since a meta can be closed and then re-opened! *) (proof, diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 5df8656cd..5873b2251 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -167,8 +167,8 @@ let _ = (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status with | GrafiteTypes.No_proof -> (Cic.Implicit None) - | Incomplete_proof i -> let _,_,p,_, _ = i.GrafiteTypes.proof in p - | Proof p -> let _,_,p,_, _ = p in p + | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p + | Proof p -> let _,_,_subst,p,_, _ = p in p | Intermediate _ -> assert false))); addDebugItem "Print current proof (natural language) to stderr" (fun _ -> @@ -179,9 +179,9 @@ let _ = with | GrafiteTypes.No_proof -> assert false | Incomplete_proof i -> - let _,m,p,ty, attrs = i.GrafiteTypes.proof in + let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs) - | Proof (_,m,p,ty, attrs) -> + | Proof (_,m,_subst,p,ty, attrs) -> Cic.CurrentProof ("current proof",m,p,ty,[],attrs) | Intermediate _ -> assert false))); (* addDebugItem "ask record choice" diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 3b4c566e2..8d66ff56d 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -650,7 +650,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- []; self#script#setGoal None - method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } = + method load_sequents + { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } + = _metasenv <- metasenv; pages <- 0; let win goal_switch = @@ -1092,11 +1094,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private home () = self#_showMath; match self#script#grafite_status.proof_status with - | Proof (uri, metasenv, bo, ty, attrs) -> + | Proof (uri, metasenv, _subst, bo, ty, attrs) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in self#_loadObj obj - | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } -> + | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in self#_loadObj obj diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 9eb1dbf69..fe8e69120 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -226,7 +226,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; [], "", parsed_text_length | TA.WHint (loc, term) -> - let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in + let _subst = [] in + let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l; diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index aea67623e..b8eb18b46 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -155,7 +155,7 @@ let rec interactive_loop () = let watch_statuses lexicon_status grafite_status = match grafite_status.GrafiteTypes.proof_status with GrafiteTypes.Incomplete_proof - {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ; + {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ; GrafiteTypes.stack = stack } -> let open_goals = Continuationals.Stack.open_goals stack in print_endline -- 2.39.2