From 90c15accf8c385a3dc44aa5f6df13f707514e2cd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 25 Jun 2005 19:14:00 +0000 Subject: [PATCH] firs wrking (?) version of lapply --- .../cic_disambiguation/cicTextualLexer2.ml | 2 +- .../cic_disambiguation/cicTextualParser2.ml | 4 +- helm/ocaml/cic_transformations/tacticAst.ml | 2 +- helm/ocaml/tactics/fwdSimplTactic.ml | 58 ++++++++++++++++++- helm/ocaml/tactics/fwdSimplTactic.mli | 2 +- helm/ocaml/tactics/tacticals.ml | 7 ++- helm/ocaml/tactics/tactics.mli | 2 +- 7 files changed, 68 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index 5127f2138..d5a06db88 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -66,7 +66,7 @@ let keywords = Hashtbl.create 17 let _ = List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword)) [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with"; - "in"; "and" ] + "in"; "and"; "to" ] let error lexbuf msg = raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg)) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index e54185a1b..9a88a2cbe 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -417,8 +417,8 @@ EXTEND TacticAst.Transitivity (loc, t) | [ IDENT "fwd" ]; t = term -> TacticAst.FwdSimpl (loc, t) - | [ IDENT "lapply" ]; t = term -> - TacticAst.LApply (loc, t) + | [ IDENT "lapply" ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term -> t ] -> + TacticAst.LApply (loc, to_what, what) ] ]; tactical: diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 269ba553a..3c659bb60 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -63,7 +63,7 @@ type ('term, 'ident) tactic = | Symmetry of loc | Transitivity of loc * 'term | FwdSimpl of loc * 'term - | LApply of loc * 'term + | LApply of loc * 'term option * 'term type thm_flavour = [ `Definition diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index 918ecd605..d75a7c5f8 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -30,6 +30,7 @@ module PEH = ProofEngineHelpers module U = CicUniv module S = CicSubstitution module PT = PrimitiveTactics +module T = Tacticals let fail_msg1 = "no applicable simplification" @@ -38,7 +39,60 @@ let error msg = raise (PET.Fail msg) (* lapply *******************************************************************) let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - (* ?(substs = []) *) what = + (* ?(substs = []) *) ?to_what what = + let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in + let apply_tac term = PT.apply_tac term in + 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, t2 + | t -> metasenv, p, None, t + in + aux metasenv 0 context t + in + let rec mk_continuations p l = + if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l) + 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 + match strip_dependent_prods metasenv context lemma with + | metasenv, p, Some premise, conclusion -> + let premise_tac = + match to_what with + | None -> T.id_tac + | Some term -> PT.apply_tac term + in + let status = (xuri, metasenv, u, t), goal in + let tac = T.thens ~start:(cut_tac premise) + ~continuations:[ + T.thens ~start:(cut_tac conclusion) + ~continuations:[ T.id_tac; + T.thens ~start:(PT.apply_tac what) + ~continuations:(mk_continuations p [PT.apply_tac ~term:(Cic.Rel 1)]) + ]; premise_tac ] + in + PET.apply_tactic tac status + | metasenv, p, None, conclusion -> + failwith "lapply_tac: not implemented" + in + PET.mk_tactic lapply_tac + + + + + + + + + +(* let count_dependent_prods context t = let rec aux context p = function | Cic.Prod (name, t1, t2) -> @@ -92,7 +146,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status in PET.mk_tactic lapply_tac - +*) (* fwd **********************************************************************) let fwd_simpl_tac ~what ~dbd = diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli index 1c221ee01..7d3355e97 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.mli +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -25,7 +25,7 @@ val lapply_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> ProofEngineTypes.tactic + ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic val fwd_simpl_tac: what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 4e0e04914..62f1ce322 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -94,7 +94,12 @@ let thens ~start ~continuations = (proof',goals@new_goals') ) (proof,[]) new_goals continuations with - Invalid_argument _ -> raise (Fail "thens: wrong number of new goals") + Invalid_argument _ -> +(* FG: more debugging information *) + let debug = Printf.sprintf "thens: expected %i new goals, found %i" + (List.length continuations) (List.length new_goals) + in + raise (Fail debug) in mk_tactic (thens ~start ~continuations ) diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index 9e5a4ce47..2fbb409cd 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -43,7 +43,7 @@ val intros : unit -> ProofEngineTypes.tactic val lapply : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - Cic.term -> ProofEngineTypes.tactic + ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic val left : ProofEngineTypes.tactic val letin : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> -- 2.39.2