From f1d49aeeb0ddcc3773a393ebef57c9cfa1e87f8e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 29 Jun 2005 15:00:26 +0000 Subject: [PATCH] lapply reimplemented using letin_tac --- helm/ocaml/tactics/fwdSimplTactic.ml | 63 +++++++++++++++++++--------- 1 file changed, 44 insertions(+), 19 deletions(-) diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index 5160ea929..ded28cc18 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -31,6 +31,7 @@ module U = CicUniv module S = CicSubstitution module PT = PrimitiveTactics module T = Tacticals +module FNG = FreshNamesGenerator let fail_msg1 = "no applicable simplification" @@ -40,16 +41,45 @@ let error msg = raise (PET.Fail msg) let strip_dependent_prods metasenv context t = let irl = MI.identity_relocation_list_for_metavariable context in - let rec aux metasenv p xcontext = function - | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) -> - let index = MI.new_meta metasenv [] in - let metasenv = [index, context, t1] @ metasenv in - let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in - aux metasenv (succ p) (e :: xcontext) (S.subst s t2) - | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, (S.subst (Cic.Rel 1) t2) - | t -> metasenv, p, None, t + let mk_meta metasenv t = + let index = MI.new_meta metasenv [] in + let metasenv = [index, context, t] @ metasenv in + metasenv, Cic.Meta (index, irl) in - aux metasenv 0 context t + let rec aux metasenv metas = function + | Cic.Prod (Cic.Name _ as name, t1, t2) -> + let metasenv, meta = mk_meta metasenv t1 in + aux metasenv (meta :: metas) (S.subst meta t2) + | Cic.Prod (Cic.Anonymous, t1, _) -> + let metasenv, meta = mk_meta metasenv t1 in + metasenv, metas, Some meta + | t -> metasenv, metas, None + in + aux metasenv [] t + +let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + (* ?(substs = []) *) ?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 = 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 + match strip_dependent_prods metasenv context lemma with + | metasenv, metas, Some meta -> + let pippo = Cic.Appl (what :: List.rev (meta :: metas)) in + Printf.eprintf "lapply: %s\n" (CicPp.ppterm pippo); flush stderr; + let outer_tac = letin_tac pippo in + let status = (xuri, metasenv, u, t), goal in + PET.apply_tactic outer_tac status + | metasenv, metas, None -> + failwith "lapply_tac: not implemented" + in + PET.mk_tactic lapply_tac + +(* + + let skip_metas p = let rec aux conts p = @@ -97,8 +127,8 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub T.then_ ~start:(intros_tac ()) ~continuation:( T.thens ~start:(PT.apply_tac what) - ~continuations:( - skip_metas p @ solve_independents ?with_what deps + ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ] +(* skip_metas p @ solve_independents ?with_what deps *) ) ) in @@ -106,6 +136,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub let xuri, metasenv, u, t = 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 match strip_dependent_prods metasenv context lemma with | metasenv, p, Some premise, conclusion -> let deps = get_conclusion_dependences context conclusion in @@ -121,15 +152,9 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub in let outer_tac = T.thens ~start:(cut_tac conclusion) - ~continuations:[T.id_tac; inner_tac] + ~continuations:[T.id_tac; T.id_tac (* inner_tac *)] in - let status = (xuri, metasenv, u, t), goal in - PET.apply_tactic outer_tac status - | metasenv, p, None, conclusion -> - failwith "lapply_tac: not implemented" - in - PET.mk_tactic lapply_tac - +*) (* fwd **********************************************************************) let fwd_simpl_tac ~what ~dbd = -- 2.39.2