New argument (the hypothesis name) for cut.

diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index d2b6280b78847667723bc0237bfb2077278afa06..735d799220310ce0086ff9a669b9c426d0b2a713 100644 (file)
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -35,8 +35,10 @@
     <keyword>rec</keyword>
     <keyword>record</keyword>
     <keyword>with</keyword>
-<!--    <keyword>using</keyword>-->
-<!--    <keyword>at</keyword>-->
+    <keyword>and</keyword>
+    <keyword>to</keyword>
+    <keyword>as</keyword>
+    <keyword>using</keyword>
   </keyword-list>
 
   <pattern-item _name = "Command [" style = "Keyword">

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 5b5a76a7d0e6344fe0c1cdad993c9ce78b5bd696..650dbc9aab49b08b2583ccb30302026113803aaa 100644 (file)
--- 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 8eec3244d29915ff57768b0acb1f0de7961c2cc4..e2b4d4682830a4950793421987a1048d370b9521 100644 (file)
--- 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 d5a06db88ade6983a7c15c6697239e77ffd85ff5..e67613091bd2937104ef3502e07a0e2a4198aaf5 100644 (file)
--- 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 1b67821c1ec8630a3d24dd71c7ae4c3e3e2042da..efacfccd762d6ef8102c503e3761587924f417a2 100644 (file)
--- 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 8983490eac2483c198ec2cecd269cb9212208292..8b66ca0e6c008daa3399221e971d64869c421d43 100644 (file)
--- 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 0eb2fbde130bb5a50a84e48d0fc79a94b5ae1fa1..f0626c7724d3056b0e224a3cda39ecdb5c3195b9 100644 (file)
--- 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 eeaa500cde0b3d18e44bf9121d34e44321a29a02..bbb2c935b7e8233f47a4f214ad22dcc441ae244e 100644 (file)
--- 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)