From 0eab2248345360e8e4b261f653f897db645998a7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 11:00:17 +0000 Subject: [PATCH] More tactics are now available to matita. --- .../cic_disambiguation/cicTextualParser2.ml | 92 +++++++++---------- helm/ocaml/cic_transformations/tacticAst.ml | 7 +- .../cic_transformations/tacticAst2Box.ml | 46 ++-------- helm/ocaml/cic_transformations/tacticAstPp.ml | 15 +-- 4 files changed, 60 insertions(+), 100 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index d3d6e28ae..19d5c5b14 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -340,86 +340,82 @@ EXTEND | SYMBOL "<" -> `Right ] ]; tactic: [ - [ [ IDENT "absurd" ]; t = tactic_term -> + [ IDENT "absurd"; t = tactic_term -> TacticAst.Absurd (loc, t) - | [ IDENT "apply" ]; t = tactic_term -> + | IDENT "apply"; t = tactic_term -> TacticAst.Apply (loc, t) - | [ IDENT "assumption" ] -> + | IDENT "assumption" -> TacticAst.Assumption loc - | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> + | IDENT "auto"; num = OPT [ i = NUM -> int_of_string i ] -> TacticAst.Auto (loc,num) - | [ IDENT "change" ]; - t1 = tactic_term; "with"; t2 = tactic_term; where = pattern_spec -> + | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term; + where = pattern_spec -> TacticAst.Change (loc, t1, t2, where) - (* TODO Change_pattern *) - | [ IDENT "contradiction" ] -> + | IDENT "compare"; t = tactic_term -> + TacticAst.Compare (loc,t) + | IDENT "constructor"; n = NUM -> + TacticAst.Constructor (loc,int_of_string n) + | IDENT "contradiction" -> TacticAst.Contradiction loc - | [ IDENT "cut" ]; - t = tactic_term -> + | IDENT "cut"; t = tactic_term -> TacticAst.Cut (loc, t) - | [ IDENT "decompose" ]; where = term -> + | IDENT "decide"; IDENT "equality" -> + TacticAst.DecideEquality loc + | IDENT "decompose"; where = term -> TacticAst.Decompose (loc, where) - | [ IDENT "discriminate" ]; - t = tactic_term -> + | IDENT "discriminate"; t = tactic_term -> TacticAst.Discriminate (loc, t) - | [ IDENT "elimType" ]; t = tactic_term -> + | IDENT "elimType"; t = tactic_term -> TacticAst.ElimType (loc, t) - | [ IDENT "elim" ]; - t1 = tactic_term; + | IDENT "elim"; t1 = tactic_term; using = OPT [ "using"; using = tactic_term -> using ] -> TacticAst.Elim (loc, t1, using) - | [ IDENT "exact" ]; t = tactic_term -> + | IDENT "exact"; t = tactic_term -> TacticAst.Exact (loc, t) - | [ IDENT "exists" ] -> + | IDENT "exists" -> TacticAst.Exists loc - | [ IDENT "fold" ]; - kind = reduction_kind; t = tactic_term -> + | IDENT "fold"; kind = reduction_kind; t = tactic_term -> TacticAst.Fold (loc, kind, t) - | [ IDENT "fourier" ] -> + | IDENT "fourier" -> TacticAst.Fourier loc - | IDENT "goal"; n = NUM -> TacticAst.Goal (loc, int_of_string n) - | [ IDENT "injection" ]; t = term -> + | IDENT "goal"; n = NUM -> + TacticAst.Goal (loc, int_of_string n) + | IDENT "injection"; t = term -> TacticAst.Injection (loc, t) - | [ IDENT "intros" ]; - num = OPT [ num = int -> num ]; - idents = OPT ident_list0 -> + | 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" ] -> - TacticAst.Intros (loc, Some 1, []) - | [ IDENT "left" ] -> TacticAst.Left loc - | [ IDENT "letin" ]; - where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> + | IDENT "intro"; ident = OPT IDENT -> + let idents = match ident with None -> [] | Some id -> [id] in + TacticAst.Intros (loc, Some 1, idents) + | IDENT "left" -> TacticAst.Left loc + | IDENT "letin"; where = IDENT ; SYMBOL <:unicode> ; t = tactic_term -> TacticAst.LetIn (loc, t, where) - | kind = reduction_kind; - p = OPT [ pattern_spec ] -> + | kind = reduction_kind; p = OPT [ pattern_spec ] -> let p = match p with None -> [], None | Some p -> p in TacticAst.Reduce (loc, kind, p) | IDENT "generalize"; t = tactic_term; p = OPT [ pattern_spec ] -> let p = match p with None -> [], None | Some p -> p in TacticAst.Generalize (loc,t,p) - | [ IDENT "reflexivity" ] -> + | IDENT "reflexivity" -> TacticAst.Reflexivity loc - | [ IDENT "replace" ]; - t1 = tactic_term; "with"; t2 = tactic_term -> + | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term -> TacticAst.Replace (loc, t1, t2) - | IDENT "rewrite" ; d = direction; t = term ; - p = OPT [ pattern_spec ] -> + | IDENT "rewrite" ; d = direction; t = term ; p = OPT [ pattern_spec ] -> let p = match p with None -> [], None | Some p -> p in TacticAst.Rewrite (loc, d, t, p) - | [ IDENT "right" ] -> TacticAst.Right loc - | [ IDENT "ring" ] -> TacticAst.Ring loc - | [ IDENT "split" ] -> TacticAst.Split loc - | [ IDENT "symmetry" ] -> + | IDENT "right" -> TacticAst.Right loc + | IDENT "ring" -> TacticAst.Ring loc + | IDENT "split" -> TacticAst.Split loc + | IDENT "symmetry" -> TacticAst.Symmetry loc - | [ IDENT "transitivity" ]; - t = tactic_term -> + | IDENT "transitivity"; t = tactic_term -> TacticAst.Transitivity (loc, t) - | [ IDENT "fwd" ]; t = term -> + | IDENT "fwd"; t = term -> TacticAst.FwdSimpl (loc, t) - | [ IDENT "lapply" ]; what = tactic_term; - to_what = OPT [ "to" ; t = tactic_term -> t ] -> - TacticAst.LApply (loc, to_what, what) + | 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 3c659bb60..63314d96f 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -37,8 +37,11 @@ type ('term, 'ident) tactic = | Auto of loc * int option | Assumption of loc | Change of loc * 'term * 'term * ('term,'ident) pattern (* what, with what, where *) + | Compare of loc * 'term + | Constructor of loc * int | Contradiction of loc | Cut of loc * 'term + | DecideEquality of loc | Decompose of loc * 'term | Discriminate of loc * 'term | Elim of loc * 'term * 'term option (* what to elim, which principle to use *) @@ -47,10 +50,12 @@ type ('term, 'ident) tactic = | Exists of loc | Fold of loc * reduction_kind * 'term | Fourier of loc + | FwdSimpl of loc * 'term | Generalize of loc * 'term * ('term, 'ident) pattern | Goal of loc * int (* change current goal, argument is goal number 1-based *) | Injection of loc * 'term | Intros of loc * int option * 'ident list + | LApply of loc * 'term option * 'term | Left of loc | LetIn of loc * 'term * 'ident | Reduce of loc * reduction_kind * ('term, 'ident) pattern @@ -62,8 +67,6 @@ type ('term, 'ident) tactic = | Split of loc | Symmetry of loc | Transitivity of loc * 'term - | FwdSimpl of loc * 'term - | LApply of loc * 'term option * 'term type thm_flavour = [ `Definition diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 1c6723186..0eb2fbde1 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -43,17 +43,11 @@ let rec count_tactic current_size tac = | Apply (_, term) -> countterm (current_size + 6) term | 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 *) *) + | Compare (_, term) -> countterm (current_size + 7) term + | Constructor (_, n) -> current_size + 12 | Contradiction _ -> current_size + 13 | Cut (_, term) -> countterm (current_size + 4) term + | DecideEquality _ -> current_size + 15 | Decompose (_, term) -> countterm (current_size + 11) term | Discriminate (_, term) -> countterm (current_size + 12) term @@ -68,7 +62,6 @@ let rec count_tactic current_size tac = | Fold (_, kind, term) -> countterm (current_size + 5) term | Fourier _ -> current_size + 7 - | Generalize (_,term,pattern) -> assert false (* TODO *) | Goal (_, n) -> current_size + 4 + int_of_float (ceil (log10 (float n))) | Injection (_, term) -> countterm (current_size + 10) term @@ -79,14 +72,10 @@ let rec count_tactic current_size tac = | Left _ -> current_size + 4 | LetIn (_, term, ident) -> countterm (current_size + 5 + String.length ident) term -(* | Reduce _ *) - | Reduce _ -> assert false (* TODO *) | Reflexivity _ -> current_size + 11 | Replace (_, t1, t2) -> let size1 = countterm (current_size + 14) t1 in (* replace, with *) countterm size1 t2 -(* | Replace_pattern _ -> assert false (* TODO *) *) - | Rewrite _ -> assert false (* TODO *) | Right _ -> current_size + 5 | Ring _ -> current_size + 4 | Split _ -> current_size + 5 @@ -137,28 +126,15 @@ and big_tactic2box = function ast2astBox term]) | Assumption _ -> Box.Text([],"assumption") | Auto _ -> Box.Text([],"auto") - | Change (_, t1, t2, where) -> -(* - let where = - (match where with - None -> [] - | Some ident -> - [Box.Text([],"in"); - Box.smallskip; - Box.Text([],ident)]) in - Box.V([], - (pretty_append - [Box.Text([],"change")] - t1)@ - (pretty_append - [Box.Text([],"with")] - t2)@where) -*) assert false -(* | Change_pattern _ -> assert false (* TODO *) *) + | Compare (_, term) -> + Box.V([],[Box.Text([],"compare"); + Box.indent(ast2astBox term)]) + | Constructor (_,n) -> Box.Text ([],"constructor " ^ string_of_int n) | Contradiction _ -> Box.Text([],"contradiction") | Cut (_, term) -> Box.V([],[Box.Text([],"cut"); Box.indent(ast2astBox term)]) + | DecideEquality _ -> Box.Text([],"decide equality") | Decompose (_, term) -> Box.V([],[Box.Text([],"decompose"); Box.indent(ast2astBox term)]) @@ -189,9 +165,7 @@ and big_tactic2box = function Box.Text([],string_of_kind kind)]); Box.indent(ast2astBox term)]) | Fourier _ -> Box.Text([],"fourier") - | Generalize _ -> assert false (* TODO *) | Goal (_, n) -> Box.Text([],"goal " ^ string_of_int n) - | Injection (_, term) -> assert false (* TODO *) | Intros (_, num, idents) -> let num = (match num with @@ -210,8 +184,6 @@ and big_tactic2box = function Box.smallskip; Box.Text([],"=")]); Box.indent (ast2astBox term)]) -(* | Reduce _ *) - | Reduce _ -> assert false (* TODO *) | Reflexivity _ -> Box.Text([],"reflexivity") | Replace (_, t1, t2) -> Box.V([], @@ -221,8 +193,6 @@ and big_tactic2box = function (pretty_append [Box.Text([],"with")] t2)) -(* | Replace_pattern _ -> assert false (* TODO *) *) - | Rewrite _ -> assert false (* TODO *) | Right _ -> Box.Text([],"right") | Ring _ -> Box.Text([],"ring") | Split _ -> Box.Text([],"split") diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index f916a2b86..eeaa500cd 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -67,9 +67,11 @@ let rec pp_tactic = function | Change (_, t1, t2, where) -> sprintf "change %s with %s%s" (pp_term_ast t1) (pp_term_ast t2) (pp_pattern where) -(* | Change_pattern (_, _, _, _) -> assert false (* TODO *) *) + | Compare (_,term) -> "compare " ^ pp_term_ast term + | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" | Cut (_, term) -> "cut " ^ pp_term_ast term + | DecideEquality _ -> "decide equality" | Decompose (_, term) -> sprintf "decompose %s" (pp_term_ast term) | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term @@ -93,22 +95,11 @@ let rec pp_tactic = function (match idents with [] -> "" | idents -> " " ^ pp_idents idents) | Left _ -> "left" | LetIn (_, term, ident) -> sprintf "let %s in %s" (pp_term_ast term) ident -(* | Reduce (_, kind, None) *) -(* | Reduce (_, kind, Some ([], `Goal)) -> pp_reduction_kind kind *) -(* | Reduce (_, kind, Some ([], `Everywhere)) -> *) -(* sprintf "%s in hyp" (pp_reduction_kind kind) *) -(* | Reduce (_, kind, Some (terms, `Goal)) -> *) -(* sprintf "%s %s" (pp_reduction_kind kind) *) -(* (String.concat ", " (List.map pp_term_ast terms)) *) -(* | Reduce (_, kind, Some (terms, `Everywhere)) -> *) -(* sprintf "%s in hyp %s" (pp_reduction_kind kind) *) -(* (String.concat ", " (List.map pp_term_ast terms)) *) | Reduce (_, kind, 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 %s" (if pos = `Left then "left" else "right") (pp_term_ast t) -- 2.39.2