From b71c265049723824235d7cec0522880492e6a0b1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 24 Jun 2005 06:50:43 +0000 Subject: [PATCH] Asts generalized: a lot of tactics where restricted to identifiers in place of patterns or terms. --- helm/matita/matitaEngine.ml | 26 +++++++++---------- .../cic_disambiguation/cicTextualParser2.ml | 24 ++++++----------- helm/ocaml/cic_transformations/tacticAst.ml | 10 +++---- .../cic_transformations/tacticAst2Box.ml | 26 ++++++++----------- helm/ocaml/cic_transformations/tacticAstPp.ml | 17 ++++++------ helm/ocaml/tactics/fwdSimplTactic.ml | 19 ++++---------- helm/ocaml/tactics/fwdSimplTactic.mli | 5 ++-- helm/ocaml/tactics/tactics.mli | 20 +++++++------- 8 files changed, 62 insertions(+), 85 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 669d7b62f..522a51570 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -77,11 +77,11 @@ let tactic_of_ast = function EqualityTactics.rewrite_tac ~where:pattern ~term:t () else EqualityTactics.rewrite_back_tac ~where:pattern ~term:t () - | TacticAst.FwdSimpl (_, name) -> - Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ()) - | TacticAst.LApply (_, term, substs) -> + | TacticAst.FwdSimpl (_, term) -> + Tactics.fwd_simpl ~term ~dbd:(MatitaDb.instance ()) + | TacticAst.LApply (_, term) -> let f (name, term) = Cic.Name name, term in - Tactics.lapply ~substs:(List.map f substs) term + Tactics.lapply term let eval_tactical status tac = let apply_tactic tactic = @@ -404,10 +404,11 @@ let disambiguate_tactic status = function let status, cic1 = disambiguate_term status what in let status, cic2 = disambiguate_term status with_what in status, TacticAst.Replace (loc, cic1, cic2) - | TacticAst.Change (loc, what, with_what, ident) -> + | TacticAst.Change (loc, what, with_what, pattern) -> let status, cic1 = disambiguate_term status what in let status, cic2 = disambiguate_term status with_what in - status, TacticAst.Change (loc, cic1, cic2, ident) + let pattern = disambiguate_pattern status.aliases pattern in + status, TacticAst.Change (loc, cic1, cic2, pattern) | TacticAst.Generalize (loc,term,pattern) -> let status,term = disambiguate_term status term in let pattern = disambiguate_pattern status.aliases pattern in @@ -448,15 +449,12 @@ let disambiguate_tactic status = function | TacticAst.Split loc -> status, TacticAst.Split loc | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g) - | TacticAst.FwdSimpl (loc, name) -> status, TacticAst.FwdSimpl (loc, name) - | TacticAst.LApply (loc, term, substs) -> - let f (status, substs) (name, term) = - let status, term = disambiguate_term status term in - status, (name, term) :: substs - in + | TacticAst.FwdSimpl (loc, term) -> + let status, term = disambiguate_term status term in + status, TacticAst.FwdSimpl (loc, term) + | TacticAst.LApply (loc, term) -> let status, term = disambiguate_term status term in - let status, substs = List.fold_left f (status, []) substs in - status, TacticAst.LApply (loc, term, substs) + status, TacticAst.LApply (loc, term) let rec disambiguate_tactical status = function | TacticAst.Tactic (loc, tactic) -> diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 737673e14..e54185a1b 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -312,16 +312,10 @@ EXTEND | PAREN "("; t = term; PAREN ")" -> return_term loc t ] ]; - tactic_where: [ - [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] - ]; tactic_term: [ [ t = term -> t ] ]; ident_list0: [ [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] ]; - ident_list1: [ - [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ] - ]; reduction_kind: [ [ [ IDENT "reduce" ] -> `Reduce | [ IDENT "simplify" ] -> `Simpl @@ -355,8 +349,7 @@ EXTEND | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> TacticAst.Auto (loc,num) | [ IDENT "change" ]; - t1 = tactic_term; "with"; t2 = tactic_term; - where = tactic_where -> + t1 = tactic_term; "with"; t2 = tactic_term; where = pattern_spec -> TacticAst.Change (loc, t1, t2, where) (* TODO Change_pattern *) | [ IDENT "contradiction" ] -> @@ -364,9 +357,8 @@ EXTEND | [ IDENT "cut" ]; t = tactic_term -> TacticAst.Cut (loc, t) - | [ IDENT "decompose" ]; - principles = ident_list1; where = IDENT -> - TacticAst.Decompose (loc, where, principles) + | [ IDENT "decompose" ]; where = term -> + TacticAst.Decompose (loc, where) | [ IDENT "discriminate" ]; t = tactic_term -> TacticAst.Discriminate (loc, t) @@ -386,8 +378,8 @@ EXTEND | [ IDENT "fourier" ] -> TacticAst.Fourier loc | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) - | [ IDENT "injection" ]; ident = IDENT -> - TacticAst.Injection (loc, ident) + | [ IDENT "injection" ]; t = term -> + TacticAst.Injection (loc, t) | [ IDENT "intros" ]; num = OPT [ num = int -> num ]; idents = OPT ident_list0 -> @@ -423,10 +415,10 @@ EXTEND | [ IDENT "transitivity" ]; t = tactic_term -> TacticAst.Transitivity (loc, t) - | [ IDENT "fwd" ]; name = IDENT -> - TacticAst.FwdSimpl (loc, name) + | [ IDENT "fwd" ]; t = term -> + TacticAst.FwdSimpl (loc, t) | [ IDENT "lapply" ]; t = term -> - TacticAst.LApply (loc, t, []) + TacticAst.LApply (loc, t) ] ]; tactical: diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 12b7774cd..269ba553a 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -36,10 +36,10 @@ type ('term, 'ident) tactic = | Apply of loc * 'term | Auto of loc * int option | Assumption of loc - | Change of loc * 'term * 'term * 'ident option (* what, with what, where *) + | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *) | Contradiction of loc | Cut of loc * 'term - | Decompose of loc * 'ident * 'ident list (* where, which principles *) + | Decompose of loc * 'term | Discriminate of loc * 'term | Elim of loc * 'term * 'term option (* what to elim, which principle to use *) | ElimType of loc * 'term @@ -49,7 +49,7 @@ type ('term, 'ident) tactic = | Fourier of loc | Generalize of loc * 'term * ('term, 'ident) pattern | Goal of loc * int (* change current goal, argument is goal number 1-based *) - | Injection of loc * 'ident + | Injection of loc * 'term | Intros of loc * int option * 'ident list | Left of loc | LetIn of loc * 'term * 'ident @@ -62,8 +62,8 @@ type ('term, 'ident) tactic = | Split of loc | Symmetry of loc | Transitivity of loc * 'term - | FwdSimpl of loc * 'ident - | LApply of loc * 'term * ('ident * 'term) list + | FwdSimpl of loc * 'term + | LApply of loc * 'term type thm_flavour = [ `Definition diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index f43091c75..1c6723186 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -44,18 +44,18 @@ let rec count_tactic current_size tac = | Auto _ -> current_size + 4 | Assumption _ -> current_size + 10 | Change (_, t1, t2, where) -> +(* let size1 = countterm (current_size + 12) t1 in (* change, with *) let size2 = countterm size1 t2 in (match where with None -> size2 | Some ident -> size2 + 3 + String.length ident) +*) assert false (* | Change_pattern _ -> assert false (* TODO *) *) | Contradiction _ -> current_size + 13 | Cut (_, term) -> countterm (current_size + 4) term - | Decompose (_, ident, principles) -> - List.fold_left - (fun size s -> size + (String.length s)) - (current_size + 11 + String.length ident) principles + | Decompose (_, term) -> + countterm (current_size + 11) term | Discriminate (_, term) -> countterm (current_size + 12) term | Elim (_, term, using) -> let size1 = countterm (current_size + 5) term in @@ -70,7 +70,8 @@ let rec count_tactic current_size tac = | Fourier _ -> current_size + 7 | Generalize (_,term,pattern) -> assert false (* TODO *) | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) - | Injection (_, ident) -> current_size + 10 + (String.length ident) + | Injection (_, term) -> + countterm (current_size + 10) term | Intros (_, num, idents) -> List.fold_left (fun size s -> size + (String.length s)) @@ -137,6 +138,7 @@ and big_tactic2box = function | Assumption _ -> Box.Text([],"assumption") | Auto _ -> Box.Text([],"auto") | Change (_, t1, t2, where) -> +(* let where = (match where with None -> [] @@ -151,19 +153,15 @@ and big_tactic2box = function (pretty_append [Box.Text([],"with")] t2)@where) +*) assert false (* | Change_pattern _ -> assert false (* TODO *) *) | Contradiction _ -> Box.Text([],"contradiction") | Cut (_, term) -> Box.V([],[Box.Text([],"cut"); Box.indent(ast2astBox term)]) - | Decompose (_, ident, principles) -> - let principles = - List.map (fun x -> Box.Text([],x)) principles in + | Decompose (_, term) -> Box.V([],[Box.Text([],"decompose"); - Box.H([],[Box.Text([],"["); - Box.V([],principles); - Box.Text([],"]")]); - Box.Text([],ident)]) + Box.indent(ast2astBox term)]) | Discriminate (_, term) -> Box.V([],pretty_append [Box.Text([],"discriminate")] term) | Elim (_, term, using) -> @@ -193,9 +191,7 @@ and big_tactic2box = function | Fourier _ -> Box.Text([],"fourier") | Generalize _ -> assert false (* TODO *) | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) - | Injection (_, ident) -> - Box.V([],[Box.Text([],"transitivity"); - Box.indent (Box.Text([],ident))]) + | Injection (_, term) -> assert false (* TODO *) | Intros (_, num, idents) -> let num = (match num with diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 52f7b1ab2..263382ef1 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -57,7 +57,8 @@ let pp_pattern (hyp, goal) = let separator = if hyp <> [] then " \vdash " else " " in - pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal + "in " ^ pp_hyp_pattern hyp ^ separator ^ pp_goal_pattern goal + let rec pp_tactic = function | Absurd (_, term) -> "absurd" ^ pp_term_ast term | Apply (_, term) -> "apply " ^ pp_term_ast term @@ -65,12 +66,12 @@ let rec pp_tactic = function | Assumption _ -> "assumption" | Change (_, t1, t2, where) -> sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2) - (match where with None -> "" | Some ident -> "in " ^ ident) + (pp_pattern where) (* | Change_pattern (_, _, _, _) -> assert false (* TODO *) *) | Contradiction _ -> "contradiction" | Cut (_, term) -> "cut " ^ pp_term_ast term - | Decompose (_, ident, principles) -> - sprintf "decompose %s %s" (pp_idents principles) ident + | Decompose (_, term) -> + sprintf "decompose %s" (pp_term_ast term) | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term | Elim (_, term, using) -> sprintf "elim " ^ pp_term_ast term ^ @@ -84,7 +85,7 @@ let rec pp_tactic = function sprintf "generalize %s %s" (pp_term_ast term) (pp_pattern pattern) | Goal (_, n) -> "goal " ^ string_of_int n | Fourier _ -> "fourier" - | Injection (_, ident) -> "injection " ^ ident + | Injection (_, term) -> "injection " ^ pp_term_ast term | Intros (_, None, []) -> "intro" | Intros (_, num, idents) -> sprintf "intros%s%s" @@ -103,13 +104,13 @@ let rec pp_tactic = function (* sprintf "%s in hyp %s" (pp_reduction_kind kind) *) (* (String.concat ", " (List.map pp_term_ast terms)) *) | Reduce (_, kind, pat) -> - sprintf "%s in %s" (pp_reduction_kind kind) (pp_pattern pat) + sprintf "%s %s" (pp_reduction_kind kind) (pp_pattern pat) | Reflexivity _ -> "reflexivity" | Replace (_, t1, t2) -> sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2) (* | Replace_pattern (_, _, _) -> assert false (* TODO *) *) | Rewrite (_, pos, t, pattern) -> - sprintf "rewrite %s %s in %s" + sprintf "rewrite %s %s %s" (if pos = `Left then "left" else "right") (pp_term_ast t) (pp_pattern pattern) | Right _ -> "right" @@ -117,7 +118,7 @@ let rec pp_tactic = function | Split _ -> "split" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term - | FwdSimpl (_, ident) -> sprintf "fwd %s" ident + | FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term) let pp_flavour = function | `Definition -> "Definition" diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index 7981ac875..98125f5e7 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -30,24 +30,13 @@ module U = CicUniv module S = CicSubstitution module PT = PrimitiveTactics -(* -let module R = CicReduction -*) - -let fail_msg0 = "not a declaration of the current context" let fail_msg1 = "no applicable simplification" let error msg = raise (PET.Fail msg) -let rec declaration name = function - | [] -> error fail_msg0 - | Some (hyp, Cic.Decl ty) :: _ when hyp = name -> ty - | _ :: tail -> declaration name tail - (* lapply *******************************************************************) -let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) - ?(substs = []) what = +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 @@ -74,12 +63,14 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub (* fwd **********************************************************************) -let fwd_simpl_tac ~hyp ~dbd = +let fwd_simpl_tac ~term ~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 = declaration hyp context in + let major,_ = + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph + in match MetadataQuery.fwd_simpl ~dbd major with | [] -> error fail_msg1 | uri :: _ -> prerr_endline (UriManager.string_of_uri uri); (proof, []) diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli index 0b065f920..705569fdc 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.mli +++ b/helm/ocaml/tactics/fwdSimplTactic.mli @@ -25,8 +25,7 @@ val lapply_tac: ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?substs:(Cic.name * Cic.term) list -> Cic.term -> - ProofEngineTypes.tactic + Cic.term -> ProofEngineTypes.tactic val fwd_simpl_tac: - hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic + term:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli index b656fe58c..cddc6d3b2 100644 --- a/helm/ocaml/tactics/tactics.mli +++ b/helm/ocaml/tactics/tactics.mli @@ -23,8 +23,8 @@ val decompose : list) -> Cic.term -> ProofEngineTypes.tactic val discriminate : term:Cic.term -> ProofEngineTypes.tactic -val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic val elim_intros : term:Cic.term -> ProofEngineTypes.tactic +val elim_intros_simpl : term:Cic.term -> ProofEngineTypes.tactic val elim_type : term:Cic.term -> ProofEngineTypes.tactic val exact : term:Cic.term -> ProofEngineTypes.tactic val exists : ProofEngineTypes.tactic @@ -32,29 +32,33 @@ 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 generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> term:Cic.term -> ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val set_goal : int -> ProofEngineTypes.tactic val injection : term:Cic.term -> ProofEngineTypes.tactic val intros : ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> unit -> ProofEngineTypes.tactic +val lapply : + ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> + Cic.term -> ProofEngineTypes.tactic val left : ProofEngineTypes.tactic val letin : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> ProofEngineTypes.tactic +val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reduce : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic -val rewrite_back : +val rewrite : ?where:ProofEngineTypes.pattern -> term:Cic.term -> unit -> ProofEngineTypes.tactic -val rewrite_back_simpl : +val rewrite_back : ?where:ProofEngineTypes.pattern -> term:Cic.term -> unit -> ProofEngineTypes.tactic -val rewrite : +val rewrite_back_simpl : ?where:ProofEngineTypes.pattern -> term:Cic.term -> unit -> ProofEngineTypes.tactic val rewrite_simpl : @@ -62,13 +66,9 @@ val rewrite_simpl : term:Cic.term -> unit -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic +val set_goal : int -> ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val symmetry : ProofEngineTypes.tactic val transitivity : term:Cic.term -> ProofEngineTypes.tactic val whd : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val normalize : pattern:ProofEngineTypes.pattern -> ProofEngineTypes.tactic -val fwd_simpl : hyp:Cic.name -> dbd:Mysql.dbd -> ProofEngineTypes.tactic -val lapply : - ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> - ?substs:(Cic.name * Cic.term) list -> Cic.term -> ProofEngineTypes.tactic -- 2.39.2