From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 13:45:36 +0000 (+0000) Subject: New argument (the hypothesis name) for cut. X-Git-Tag: INDEXING_NO_PROOFS~45 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=60033ee6d57f253ce1b90e3758a69b85d13f6a41;p=helm.git New argument (the hypothesis name) for cut. --- diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index d2b6280b7..735d79922 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -35,8 +35,10 @@ rec record with - - + and + to + as + using diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 5b5a76a7d..650dbc9aa 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -29,7 +29,9 @@ let tactic_of_ast = function | TacticAst.Contradiction _ -> Tactics.contradiction | TacticAst.Compare (_, term) -> Tactics.compare term | TacticAst.Constructor (_, n) -> Tactics.constructor n - | TacticAst.Cut (_, term) -> Tactics.cut term + | TacticAst.Cut (_, ident, term) -> + let names = match ident with None -> [] | Some id -> [id] in + Tactics.cut ~mk_fresh_name_callback:(namer_of names) term | TacticAst.DecideEquality _ -> Tactics.decide_equality | TacticAst.Decompose (_,term) -> Tactics.decompose term | TacticAst.Discriminate (_,term) -> Tactics.discriminate term @@ -394,9 +396,9 @@ let disambiguate_tactic status = function status, TacticAst.Constructor (loc,n) | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc - | TacticAst.Cut (loc, term) -> + | TacticAst.Cut (loc, ident, term) -> let status, cic = disambiguate_term status term in - status, TacticAst.Cut (loc, cic) + status, TacticAst.Cut (loc, ident, cic) | TacticAst.DecideEquality loc -> status, TacticAst.DecideEquality loc | TacticAst.Decompose (loc,term) -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 8eec3244d..e2b4d4682 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -167,7 +167,7 @@ class gui () = connect_button tbar#transitivityButton (tac_w_term (A.Transitivity (loc, hole))); connect_button tbar#assumptionButton (tac (A.Assumption loc)); - connect_button tbar#cutButton (tac_w_term (A.Cut (loc, hole))); + connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); connect_button tbar#autoButton (tac (A.Auto (loc,None,None))); MatitaGtkMisc.toggle_widget_visibility ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget) diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index d5a06db88..e67613091 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"; "to" ] + "in"; "and"; "to"; "as" ] 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 1b67821c1..efacfccd7 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -361,8 +361,8 @@ EXTEND TacticAst.Constructor (loc,int_of_string n) | IDENT "contradiction" -> TacticAst.Contradiction loc - | IDENT "cut"; t = tactic_term -> - TacticAst.Cut (loc, t) + | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> + TacticAst.Cut (loc, ident, t) | IDENT "decide"; IDENT "equality" -> TacticAst.DecideEquality loc | IDENT "decompose"; where = term -> diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 8983490ea..8b66ca0e6 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -40,7 +40,7 @@ type ('term, 'ident) tactic = | Compare of loc * 'term | Constructor of loc * int | Contradiction of loc - | Cut of loc * 'term + | Cut of loc * 'ident option * 'term | DecideEquality of loc | Decompose of loc * 'term | Discriminate of loc * 'term diff --git a/helm/ocaml/cic_transformations/tacticAst2Box.ml b/helm/ocaml/cic_transformations/tacticAst2Box.ml index 0eb2fbde1..f0626c772 100644 --- a/helm/ocaml/cic_transformations/tacticAst2Box.ml +++ b/helm/ocaml/cic_transformations/tacticAst2Box.ml @@ -46,7 +46,13 @@ let rec count_tactic current_size tac = | Compare (_, term) -> countterm (current_size + 7) term | Constructor (_, n) -> current_size + 12 | Contradiction _ -> current_size + 13 - | Cut (_, term) -> countterm (current_size + 4) term + | Cut (_, ident, term) -> + let id_size = + match ident with + None -> 0 + | Some id -> String.length id + 4 + in + countterm (current_size + 4 + id_size) term | DecideEquality _ -> current_size + 15 | Decompose (_, term) -> countterm (current_size + 11) term @@ -131,9 +137,6 @@ and big_tactic2box = function 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"); diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index eeaa500cd..bbb2c935b 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -70,7 +70,9 @@ let rec pp_tactic = function | Compare (_,term) -> "compare " ^ pp_term_ast term | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" - | Cut (_, term) -> "cut " ^ pp_term_ast term + | Cut (_, ident, term) -> + "cut " ^ pp_term_ast term ^ + (match ident with None -> "" | Some id -> " as " ^ id) | DecideEquality _ -> "decide equality" | Decompose (_, term) -> sprintf "decompose %s" (pp_term_ast term)