From 98c386d8d12a2fe4d64017e0b1bf684b22fe6423 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 24 Jun 2005 18:43:43 +0000 Subject: [PATCH] lapply tactic continued --- helm/matita/matitaEngine.ml | 2 +- helm/ocaml/tactics/fwdSimplTactic.ml | 80 ++++++++++++++++++--------- helm/ocaml/tactics/fwdSimplTactic.mli | 2 +- helm/ocaml/tactics/tactics.mli | 2 +- 4 files changed, 58 insertions(+), 28 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 522a51570..37143ea23 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -78,7 +78,7 @@ let tactic_of_ast = function else EqualityTactics.rewrite_back_tac ~where:pattern ~term:t () | TacticAst.FwdSimpl (_, term) -> - Tactics.fwd_simpl ~term ~dbd:(MatitaDb.instance ()) + Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) | TacticAst.LApply (_, term) -> let f (name, term) = Cic.Name name, term in Tactics.lapply term diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index 98125f5e7..918ecd605 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -26,6 +26,7 @@ module MI = CicMkImplicit module TC = CicTypeChecker module PET = ProofEngineTypes +module PEH = ProofEngineHelpers module U = CicUniv module S = CicSubstitution module PT = PrimitiveTactics @@ -36,42 +37,71 @@ let error msg = raise (PET.Fail msg) (* lapply *******************************************************************) -let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) what = - let rec strip_dependent_prods metasenv context ss = function - | Cic.Prod (name, t1, t2) as t -> - if TC.does_not_occur context 0 1 t2 then metasenv, ss, t else - let metasenv, index = MI.mk_implicit metasenv [] context in - let rs = MI.identity_relocation_list_for_metavariable context in - let e, s = Some (name, Cic.Decl t1), Some (Cic.Meta (index, rs)) in - strip_dependent_prods metasenv (e :: context) (s :: ss) t2 - | t -> metasenv, ss, t +let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + (* ?(substs = []) *) what = + let count_dependent_prods context t = + let rec aux context p = function + | Cic.Prod (name, t1, t2) -> + if TC.does_not_occur context 0 1 t2 then p else + let e = Some (name, Cic.Decl t1) in + aux (e :: context) (succ p) t2 + | t -> p + in + aux context 0 t in - let update_metasenv metasenv ((xuri, _, u,t), goal) = - ((xuri, metasenv, u,t), goal) + let rec pad_context p context add_context = + if List.length add_context >= p then add_context @ context + else pad_context p context (None :: add_context) in - let lapply_tac status = - let (proof, goal) = status in - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in + let strip_dependent_prods metasenv context p t = + let rec aux metasenv add_context q = function + | Cic.Prod (name, t1, t2) when q > 0 -> + let context_for_meta = pad_context p context add_context in + let metasenv, index = MI.mk_implicit metasenv [] context_for_meta in + let rs = MI.identity_relocation_list_for_metavariable context_for_meta in + let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, rs) in + aux metasenv (e :: add_context) (pred q) (S.subst s t2) + | t -> metasenv, add_context, t + in + aux metasenv [] p t + in + let mk_body bo = function + | Some (name, Cic.Decl t1) -> Cic.Lambda (name, t1, bo) + | _ -> failwith "mk_body" + in + let lapply_tac (proof, goal) = + let xuri, metasenv, u, t = proof in +(* preliminaries *) + let metano, context, ty = CicUtil.lookup_meta goal metasenv in let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in - let metasenv, substs, stripped_lemma = strip_dependent_prods metasenv context [] lemma in - let status = update_metasenv metasenv status in - let holed_lemma = S.subst_meta substs stripped_lemma in + let p = count_dependent_prods context lemma in +(* stripping *) + let metasenv, add_context, holed_lemma = strip_dependent_prods metasenv context p lemma in + let proof = xuri, metasenv, u, t in + let newmeta = MI.new_meta metasenv [] in + let context = add_context @ context in + let irl = MI.identity_relocation_list_for_metavariable context in + let bo = List.fold_left mk_body (Cic.Meta (newmeta, irl)) add_context in + let ty = S.lift p ty in + let (xuri, metasenv, u, t), _ = + PEH.subst_meta_in_proof proof metano bo [newmeta, context, ty] + in + prerr_endline (CicPp.ppterm holed_lemma); +(* cut *) + let status = (xuri, metasenv, u, t), newmeta in PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status in PET.mk_tactic lapply_tac (* fwd **********************************************************************) -let fwd_simpl_tac ~term ~dbd = +let fwd_simpl_tac ~what ~dbd = let fwd_simpl_tac status = let (proof, goal) = status in - let _,metasenv,_,_ = proof in - let _,context,ty = CicUtil.lookup_meta goal metasenv in - let major,_ = - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph - in - match MetadataQuery.fwd_simpl ~dbd major with + let _, metasenv, _, _ = proof in + let _, context, ty = CicUtil.lookup_meta goal metasenv in + let major, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in + match MetadataQuery.fwd_simpl ~dbd major with | [] -> error fail_msg1 | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, []) in diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli index 705569fdc..1c221ee01 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.mli +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -28,4 +28,4 @@ val lapply_tac: Cic.term -> ProofEngineTypes.tactic val fwd_simpl_tac: - term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic + what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index cddc6d3b2..9e5a4ce47 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -32,7 +32,7 @@ val fold : reduction:(Cic.context -> Cic.term -> Cic.term) -> also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic -val fwd_simpl : term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic +val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic -- 2.39.2