From ebaf3deffea9ac78a2b8b2a6c128cc24ad8459ef Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 30 Jun 2005 14:27:19 +0000 Subject: [PATCH] lapply and fwd improved --- helm/matita/matitaEngine.ml | 27 ++- helm/matita/tests/fguidi.ma | 30 +-- .../cic_disambiguation/cicTextualParser2.ml | 35 ++-- helm/ocaml/cic_transformations/tacticAst.ml | 4 +- helm/ocaml/cic_transformations/tacticAstPp.ml | 16 +- helm/ocaml/tactics/.depend | 14 +- helm/ocaml/tactics/fwdSimplTactic.ml | 188 ++++++++---------- helm/ocaml/tactics/fwdSimplTactic.mli | 5 +- helm/ocaml/tactics/metadataQuery.ml | 11 +- helm/ocaml/tactics/tactics.mli | 7 +- 10 files changed, 159 insertions(+), 178 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 7239e98e3..1718529cc 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -56,8 +56,8 @@ let tactic_of_ast = function in Tactics.fold ~reduction ~pattern | TacticAst.Fourier _ -> Tactics.fourier - | TacticAst.FwdSimpl (_, term) -> - Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ()) + | TacticAst.FwdSimpl (_, hyp, names) -> + Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~hyp ~dbd:(MatitaDb.instance ()) | TacticAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern @@ -69,9 +69,9 @@ let tactic_of_ast = function | TacticAst.Intros (_, Some num, names) -> PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) () - | TacticAst.LApply (_, to_what, what, ident) -> + | TacticAst.LApply (_, how_many, to_what, what, ident) -> let names = match ident with None -> [] | Some id -> [id] in - Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?to_what what + Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what | TacticAst.Left _ -> Tactics.left | TacticAst.LetIn (loc,term,name) -> Tactics.letin term ~mk_fresh_name_callback:(namer_of [name]) @@ -444,9 +444,8 @@ let disambiguate_tactic status = function | TacticAst.Fold (loc,reduction_kind, pattern) -> let status, pattern = disambiguate_pattern status pattern in status, TacticAst.Fold (loc,reduction_kind, pattern) - | TacticAst.FwdSimpl (loc, term) -> - let status, term = disambiguate_term status term in - status, TacticAst.FwdSimpl (loc, term) + | TacticAst.FwdSimpl (loc, hyp, names) -> + status, TacticAst.FwdSimpl (loc, hyp, names) | TacticAst.Fourier loc -> status, TacticAst.Fourier loc | TacticAst.Generalize (loc,pattern,ident) -> let status, pattern = disambiguate_pattern status pattern in @@ -458,16 +457,14 @@ let disambiguate_tactic status = function status, TacticAst.Injection (loc,term) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) - | TacticAst.LApply (loc, to_what, what, ident) -> - let status, to_what = - match to_what with - None -> status,None - | Some to_what -> - let status, to_what = disambiguate_term status to_what in - status, Some to_what + | TacticAst.LApply (loc, depth, to_what, what, ident) -> + let f term (status, to_what) = + let status, term = disambiguate_term status term in + status, term :: to_what in + let status, to_what = List.fold_right f to_what (status, []) in let status, what = disambiguate_term status what in - status, TacticAst.LApply (loc, to_what, what, ident) + status, TacticAst.LApply (loc, depth, to_what, what, ident) | TacticAst.Left loc -> status, TacticAst.Left loc | TacticAst.LetIn (loc, term, name) -> let status, term = disambiguate_term status term in diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index c0662e78f..fc2c717eb 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -7,12 +7,12 @@ alias id "le" = "cic:/matita/fguidi/le.ind#xpointer(1/1)". alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con". alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". +alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". +alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias symbol "and" (instance 0) = "logical and". alias symbol "eq" (instance 0) = "leibnitz's equality". alias symbol "exists" (instance 0) = "exists". -alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". definition is_S: nat \to Prop \def \lambda n. match n with @@ -82,25 +82,17 @@ intros. elim H. elim H1. cut (S x1) = x. elim Hcut. auto. elim H2. auto. qed. theorem le_gen_S_S: \forall m,n. (le (S m) (S n)) \to (le m n). -intros. cut (\exists p. (S n) = (S p) \land (le m p)). -elim Hcut. elim H1. cut x = n. -elim Hcut1. auto. symmetry. auto. auto. +intros. +lapply le_gen_S_x to H using H0. elim H0. elim H1. +lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption. qed. theorem le_gen_S_S_cc: \forall m,n. (le m n) \to (le (S m) (S n)). intros. auto. qed. - -theorem le_gen_S_x_2: \forall m,x. (le (S m) x) \to - \exists n. x = (S n) \land (le m n). -intros. -lapply le_gen_S_x to H using H0. elim H0. elim H1. -exists. exact x1. auto. -qed. - -(* proof of le_gen_S_S with lapply *) -theorem le_gen_S_S_2: \forall m,n. (le (S m) (S n)) \to (le m n). -intros. -lapply le_gen_S_x_2 to H using H0. elim H0. elim H1. -lapply eq_gen_S_S to H2 using H4. rewrite > H4. assumption. -qed. +(* +theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z). +intros 1. +elim x. auto. +fwd H1 []. +*) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 9f6476d28..728ff94a0 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -318,6 +318,9 @@ EXTEND ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; + tactic_term_list1: [ + [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ] + ]; reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl @@ -363,7 +366,7 @@ EXTEND TacticAst.Assumption loc | IDENT "auto"; depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; - width = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ] -> + width = OPT [ IDENT "width"; SYMBOL "="; i = NUM -> int_of_string i ] -> TacticAst.Auto (loc,depth,width) | IDENT "clear"; id = IDENT -> TacticAst.Clear (loc,id) @@ -381,7 +384,7 @@ EXTEND TacticAst.Cut (loc, ident, t) | IDENT "decide"; IDENT "equality" -> TacticAst.DecideEquality loc - | IDENT "decompose"; where = term -> + | IDENT "decompose"; where = tactic_term -> TacticAst.Decompose (loc, where) | IDENT "discriminate"; t = tactic_term -> TacticAst.Discriminate (loc, t) @@ -399,25 +402,29 @@ EXTEND TacticAst.Fold (loc, kind, p) | IDENT "fourier" -> TacticAst.Fourier loc - | IDENT "fwd"; t = term -> - TacticAst.FwdSimpl (loc, t) + | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.FwdSimpl (loc, hyp, idents) | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> TacticAst.Generalize (loc,p,id) | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) | IDENT "id" -> TacticAst.IdTac loc - | IDENT "injection"; t = term -> + | IDENT "injection"; t = tactic_term -> TacticAst.Injection (loc, t) - | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> - let idents = match idents with None -> [] | Some idents -> idents in - TacticAst.Intros (loc, num, idents) | IDENT "intro"; ident = OPT IDENT -> let idents = match ident with None -> [] | Some id -> [id] in TacticAst.Intros (loc, Some 1, idents) - | IDENT "lapply"; what = tactic_term; - to_what = OPT [ "to" ; t = tactic_term -> t ]; - ident = OPT [ "using" ; id = IDENT -> id ] -> - TacticAst.LApply (loc, to_what, what, ident) + | IDENT "intros"; num = OPT [num = int -> num]; idents = OPT ident_list0 -> + let idents = match idents with None -> [] | Some idents -> idents in + TacticAst.Intros (loc, num, idents) + | IDENT "lapply"; + depth = OPT [ IDENT "depth"; SYMBOL "="; i = NUM -> int_of_string i ]; + what = tactic_term; + to_what = OPT [ "to" ; t = tactic_term_list1 -> t ]; + ident = OPT [ "using" ; ident = IDENT -> ident ] -> + let to_what = match to_what with None -> [] | Some to_what -> to_what in + TacticAst.LApply (loc, depth, to_what, what, ident) | IDENT "left" -> TacticAst.Left loc | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) @@ -427,7 +434,7 @@ EXTEND TacticAst.Reflexivity loc | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term -> TacticAst.Replace (loc, p, t) - | IDENT "rewrite" ; d = direction; t = term ; p = pattern_spec -> + | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec -> let (pt,_,_) = p in if pt <> None then raise @@ -454,7 +461,7 @@ EXTEND ] | "then" NONA [ tac = tactical; - PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" -> + PAREN "["; tacs = LIST0 tactical SEP SYMBOL "|"; PAREN "]" -> (TacticAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index d9f909a5f..3f6e74346 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -52,13 +52,13 @@ type ('term, 'ident) tactic = | Fail of loc | Fold of loc * reduction_kind * ('term, 'ident) pattern | Fourier of loc - | FwdSimpl of loc * 'term + | FwdSimpl of loc * string * 'ident list | Generalize of loc * ('term, 'ident) pattern * 'ident option | Goal of loc * int (* change current goal, argument is goal number 1-based *) | IdTac of loc | Injection of loc * 'term | Intros of loc * int option * 'ident list - | LApply of loc * 'term option * 'term * 'ident option + | LApply of loc * int option * 'term list * 'term * 'ident option | Left of loc | LetIn of loc * 'term * 'ident | Reduce of loc * reduction_kind * ('term, 'ident) pattern diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 83fdaf082..67b5733d2 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -37,6 +37,8 @@ let pp_term_cic term = CicPp.ppterm term let pp_idents idents = "[" ^ String.concat "; " idents ^ "]" +let pp_terms_ast terms = String.concat ", " (List.map pp_term_ast terms) + let pp_reduction_kind = function | `Reduce -> "reduce" | `Simpl -> "simplify" @@ -82,6 +84,9 @@ let rec pp_tactic = function | Exists _ -> "exists" | Fold (_, kind, pattern) -> sprintf "fold %s %s" (pp_reduction_kind kind) (pp_pattern pattern) + | FwdSimpl (_, hyp, idents) -> + sprintf "fwd %s%s" hyp + (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | Generalize (_, pattern, ident) -> sprintf "generalize %s%s" (pp_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) @@ -95,6 +100,12 @@ let rec pp_tactic = function sprintf "intros%s%s" (match num with None -> "" | Some num -> " " ^ string_of_int num) (match idents with [] -> "" | idents -> " " ^ pp_idents idents) + | LApply (_, level_opt, terms, term, ident_opt) -> + sprintf "lapply %s%s%s%s" + (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ") + (pp_term_ast term) + (match terms with [] -> "" | _ -> " to " ^ pp_terms_ast terms) + (match ident_opt with None -> "" | Some ident -> " using " ^ ident) | Left _ -> "left" | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident | Reduce (_, kind, pat) -> @@ -112,11 +123,6 @@ let rec pp_tactic = function | Split _ -> "split" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term - | FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term) - | LApply (_, term_opt, term, ident) -> - sprintf "lapply %s%s%s" (pp_term_ast term) - (match term_opt with None -> "" | Some t -> " to " ^ pp_term_ast t) - (match ident with None -> "" | Some id -> " using " ^ id) let pp_flavour = function | `Definition -> "Definition" diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 91e755580..ed8629532 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -33,9 +33,9 @@ proofEngineStructuralRules.cmo: proofEngineTypes.cmi \ proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ proofEngineStructuralRules.cmi primitiveTactics.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi + proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi primitiveTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmi + proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmi hashtbl_equiv.cmo: hashtbl_equiv.cmi hashtbl_equiv.cmx: hashtbl_equiv.cmi metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ @@ -88,10 +88,12 @@ fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \ fourierR.cmx: tacticals.cmx ring.cmx reductionTactics.cmx \ proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ fourier.cmx equalityTactics.cmx fourierR.cmi -fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ - primitiveTactics.cmi metadataQuery.cmi fwdSimplTactic.cmi -fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ - primitiveTactics.cmx metadataQuery.cmx fwdSimplTactic.cmi +fwdSimplTactic.cmo: tacticals.cmi proofEngineTypes.cmi \ + proofEngineStructuralRules.cmi primitiveTactics.cmi metadataQuery.cmi \ + fwdSimplTactic.cmi +fwdSimplTactic.cmx: tacticals.cmx proofEngineTypes.cmx \ + proofEngineStructuralRules.cmx primitiveTactics.cmx metadataQuery.cmx \ + fwdSimplTactic.cmi history.cmo: history.cmi history.cmx: history.cmi statefulProofEngine.cmo: proofEngineTypes.cmi history.cmi \ diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index ded28cc18..e7d25daae 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -23,148 +23,120 @@ * http://cs.unibo.it/helm/. *) -module MI = CicMkImplicit -module TC = CicTypeChecker -module PET = ProofEngineTypes +(* module PEH = ProofEngineHelpers +*) module U = CicUniv +module TC = CicTypeChecker +module PET = ProofEngineTypes module S = CicSubstitution module PT = PrimitiveTactics module T = Tacticals module FNG = FreshNamesGenerator +module MI = CicMkImplicit +module PESR = ProofEngineStructuralRules -let fail_msg1 = "no applicable simplification" +let fail_msg0 = "unexported clearbody: invalid argument" +let fail_msg1 = "fwd: argument is not premise in the current goal" +let fail_msg2 = "fwd: no applicable simplification" let error msg = raise (PET.Fail msg) +(* unexported tactics *******************************************************) + +let clearbody ~index = + let rec find_name index = function + | Some (Cic.Name name, _) :: _ when index = 1 -> name + | _ :: tail when index > 1 -> find_name (pred index) tail + | _ -> error fail_msg0 + in + let clearbody status = + let (proof, goal) = status in + let _, metasenv, _, _ = proof in + let _, context, _ = CicUtil.lookup_meta goal metasenv in + PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status + in + PET.mk_tactic clearbody + (* lapply *******************************************************************) -let strip_dependent_prods metasenv context t = +let strip_prods metasenv context ?how_many to_what term = let irl = MI.identity_relocation_list_for_metavariable context in - let mk_meta metasenv t = + let mk_meta metasenv its_type = let index = MI.new_meta metasenv [] in - let metasenv = [index, context, t] @ metasenv in - metasenv, Cic.Meta (index, irl) + let metasenv = [index, context, its_type] @ metasenv in + metasenv, Cic.Meta (index, irl), index in - 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 + let update_counters = function + | None, [] -> None, T.id_tac, [] + | None, to_what :: tail -> None, PT.apply_tac ~term:to_what, tail + | Some hm, [] -> Some (pred hm), T.id_tac, [] + | Some hm, to_what :: tail -> Some (pred hm), PT.apply_tac ~term:to_what, tail + in + let rec aux metasenv metas conts tw = function + | Some hm, _ when hm <= 0 -> metasenv, metas, conts + | xhm, Cic.Prod (Cic.Name _, t1, t2) -> + let metasenv, meta, index = mk_meta metasenv t1 in + aux metasenv (meta :: metas) ((T.id_tac, index) :: conts) tw (xhm, (S.subst meta t2)) + | xhm, Cic.Prod (Cic.Anonymous, t1, t2) -> + let xhm, tac, tw = update_counters (xhm, tw) in + let metasenv, meta, index = mk_meta metasenv t1 in + aux metasenv (meta :: metas) ((tac, index) :: conts) tw (xhm, (S.subst meta t2)) + | _, t -> metasenv, metas, conts in - aux metasenv [] t + aux metasenv [] [] to_what (how_many, term) let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - (* ?(substs = []) *) ?to_what what = + (* ?(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 = 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" + let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in + let conclusion = Cic.Appl (what :: List.rev metas) in + let tac = T.thens ~start:(letin_tac conclusion) + ~continuations:[clearbody ~index:1] + in + let proof = (xuri, metasenv, u, t) in + let aux (proof, goals) (tac, goal) = + let proof, new_goals = PET.apply_tactic tac (proof, goal) in + proof, goals @ new_goals + in + List.fold_left aux (proof, []) ((tac, goal) :: conts) in PET.mk_tactic lapply_tac -(* - - - -let skip_metas p = - let rec aux conts p = - if p <= 0 then conts else aux (T.id_tac :: conts) (pred p) - in - aux [] p - -let get_conclusion context t = - let rec aux p context = function - | Cic.Prod (name, t1, t2) -> - aux (succ p) (Some (name, Cic.Decl t1) :: context) t2 - | Cic.LetIn (name, u1, t2) -> - aux (succ p) (Some (name, Cic.Def (u1, None)) :: context) t2 - | Cic.Cast (t2, t1) -> aux p context t2 - | t -> p, context, t - in aux 0 context t +(* fwd **********************************************************************) -let get_conclusion_dependences context t = - let p, context, conclusion = get_conclusion context t in - let rec aux l q = - if q <= 0 then l else - let b = TC.does_not_occur context (pred q) q conclusion in - aux (b :: l) (pred q) +let fwd_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) + ~hyp ~dbd = + let find_type metasenv context = + let rec aux p = function + | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t + | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t + | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> + p, fst (TC.type_of_aux' metasenv tail u U.empty_ugraph) + | _ :: tail -> aux (succ p) tail + | [] -> error fail_msg1 + in + aux 1 context in - aux [] p - -let solve_independents ?with_what deps = - let rec aux p conts = function - | [] -> p, conts - | true :: tl -> - let cont = PT.apply_tac ~term:(Cic.Rel (succ p)) in - aux (succ p) (cont :: conts) tl - | false :: tl -> aux (succ p) conts tl - in - let p, conts = aux 0 [] deps in - match with_what with - | None -> conts - | Some t -> PT.apply_tac ~term:(S.lift p t) :: conts - -let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - (* ?(substs = []) *) ?to_what what = - let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in - let intros_tac () = PT.intros_tac ~mk_fresh_name_callback () in - let solve_conclusion_tac ?with_what p deps = - T.then_ ~start:(intros_tac ()) - ~continuation:( - T.thens ~start:(PT.apply_tac what) - ~continuations:( [ T.id_tac; T.id_tac; T.id_tac ] -(* skip_metas p @ solve_independents ?with_what deps *) - ) - ) + let lapply_tac to_what lemma = + lapply_tac ~mk_fresh_name_callback ~how_many:1 ~to_what:[to_what] lemma 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, p, Some premise, conclusion -> - let deps = get_conclusion_dependences context conclusion in - let inner_tac = match to_what with - | None -> - T.thens ~start:(cut_tac premise) - ~continuations:[ - solve_conclusion_tac ~with_what:(Cic.Rel 1) p deps; - T.id_tac - ] - | Some with_what -> - solve_conclusion_tac ~with_what p deps - in - let outer_tac = - T.thens ~start:(cut_tac conclusion) - ~continuations:[T.id_tac; T.id_tac (* inner_tac *)] - in -*) -(* fwd **********************************************************************) - -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, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in + let index, major = find_type metasenv context in match MetadataQuery.fwd_simpl ~dbd major with - | [] -> error fail_msg1 - | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, []) + | [] -> error fail_msg2 + | uri :: _ -> + Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr; + let start = lapply_tac (Cic.Rel index) (Cic.Const (uri, [])) in + let tac = T.thens ~start ~continuations:[PESR.clearbody hyp] in + PET.apply_tactic tac status in PET.mk_tactic fwd_simpl_tac diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli index 7d3355e97..f8101b34b 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.mli +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -25,7 +25,8 @@ val lapply_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic + ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic val fwd_simpl_tac: - what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + hyp:string -> dbd:Mysql.dbd -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index a3e774d1d..a01044e8c 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -500,8 +500,8 @@ let get_metadata t = let debug_metadata = function | None -> () | Some (outer, inners) -> - let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n uri in - Printf.eprintf "\n%s: %s\n" "fwd" outer; + let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in + Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer); List.iter f inners; prerr_newline () let fwd_simpl ~dbd t = @@ -525,8 +525,9 @@ let fwd_simpl ~dbd t = let compare (_, x) (_, y) = compare x y in let filter n (uri, rank) = if rank > 0 then Some (UriManager.uri_of_string uri) else None - in - match get_metadata t with + in + let metadata = get_metadata t in debug_metadata metadata; + match metadata with | None -> [] | Some (outer, inners) -> let select = "source, h_inner, h_index" in @@ -539,4 +540,4 @@ let fwd_simpl ~dbd t = let lemmas = Mysql.map result ~f:(map inners) in let ranked = List.fold_left rank [] lemmas in let ordered = List.rev (List.fast_sort compare ranked) in - map_filter filter 0 ordered + map_filter filter 0 ordered diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index f78624c97..187dc2be3 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -35,7 +35,9 @@ val fold : reduction:(Cic.context -> Cic.term -> Cic.term) -> pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val fourier : ProofEngineTypes.tactic -val fwd_simpl : what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic +val fwd_simpl : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + hyp:string -> dbd:Mysql.dbd -> ProofEngineTypes.tactic val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic @@ -47,7 +49,8 @@ val intros : unit -> ProofEngineTypes.tactic val lapply : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic + ?how_many:int -> + ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic val left : ProofEngineTypes.tactic val letin : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> -- 2.39.2