From: Andrea Berlingieri <andrea.berlingieri@studio.unibo.it>
Date: Thu, 14 Mar 2019 09:31:01 +0000 (+0100)
Subject: Partially restore the suppose tactic
X-Git-Tag: make_still_working~229^2~1^2~1^2~10
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42

Partially restore the suppose tactic

Add a type for the suppose tactic in GrafiteAst

Add pretty printing code for the suppose tactic

Add a parsing rule for the suppose tactic in GrafiteParser

Add a call in to the suppose tactic in GrafiteEngine

Add code for the suppose tactic in Declarative

Add syntax highlight tag for the suppose tactic
---

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 8b911a601..29dfe324b 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -76,7 +76,9 @@ type ntactic =
    | NRepeat of loc * ntactic
    | NBlock of loc * ntactic list
    (* Declarative langauge *)
+   (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
    | Assume of loc * string * nterm (* loc, identifier, term *)
+   | Suppose of loc * nterm *string * nterm option
 
 type nmacro =
   | NCheck of loc * nterm
diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml
index d56e95de0..00789961c 100644
--- a/matita/components/grafite/grafiteAstPp.ml
+++ b/matita/components/grafite/grafiteAstPp.ml
@@ -108,6 +108,8 @@ let rec pp_ntactic status ~map_unicode_to_tex =
      "(" ^ String.concat " " (List.map (pp_ntactic status ~map_unicode_to_tex) l)^ ")"
   | NRepeat (_,t) -> "nrepeat " ^ pp_ntactic status ~map_unicode_to_tex t
   | Assume (_, ident, term) -> "assume" ^ ident ^ ":" ^ NotationPp.pp_term status term
+  | Suppose (_,term,ident,term1) -> "suppose" ^ NotationPp.pp_term status term ^ "(" ^ ident ^ ")" ^ (match
+  term1 with None -> "" | Some t -> " that is equivalent to " ^ NotationPp.pp_term status t)
 ;;
 
 let pp_nmacro status = function
diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index f76b8b02a..be7154179 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -482,6 +482,7 @@ let eval_ng_tac tac =
   |GrafiteAst.NRepeat (_,tac) ->
       NTactics.repeat_tac (f f (text, prefix_len, tac))
   |GrafiteAst.Assume (_,id,t) -> Declarative.assume id t
+  |GrafiteAst.Suppose (_,t,id,t1) -> Declarative.suppose t id t1
  in
   aux aux tac (* trick for non uniform recursion call *)
 ;;
diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index c1b347071..90abc0a89 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -239,7 +239,9 @@ EXTEND
     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
     | SYMBOL "*"; "as"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
-    | IDENT "assume"; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+    | IDENT "assume" ; id = IDENT; SYMBOL ":"; t = tactic_term -> G.NTactic (loc,[G.Assume (loc,id,t)])
+    | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that"; IDENT
+    "is"; IDENT "equivalent"; "to"; t' = tactic_term -> t'] -> G.NTactic (loc,[G.Suppose (loc,t,id,t1)])
     ]
   ];
   auto_fixed_param: [
diff --git a/matita/components/ng_tactics/declarative.ml b/matita/components/ng_tactics/declarative.ml
index 532ffbb37..ae07c18ee 100644
--- a/matita/components/ng_tactics/declarative.ml
+++ b/matita/components/ng_tactics/declarative.ml
@@ -28,3 +28,7 @@ open NTactics
 
 let assume name ty =
     exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (name,None),Some ty),Ast.Implicit `JustOne)))
+
+let suppose t id t1 =
+    let t1 = match t1 with None -> t | Some t1 -> t1 in
+    exact_tac ("",0,(Ast.Binder (`Lambda,(Ast.Ident (id,None),Some t1),Ast.Implicit `JustOne)))
diff --git a/matita/components/ng_tactics/declarative.mli b/matita/components/ng_tactics/declarative.mli
index f6f0ff953..a7ec0e44d 100644
--- a/matita/components/ng_tactics/declarative.mli
+++ b/matita/components/ng_tactics/declarative.mli
@@ -24,3 +24,4 @@
  *)
 
 val assume : string -> NotationPt.term -> 's NTacStatus.tactic
+val suppose : NotationPt.term -> string -> NotationPt.term option -> 's NTacStatus.tactic
diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index 8a47418b6..6fa587de3 100644
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -107,6 +107,11 @@
          <keyword>lapply</keyword>
          <keyword>destruct</keyword>
          <keyword>assume</keyword>
+         <keyword>suppose</keyword>
+         <keyword>that</keyword>
+         <keyword>is</keyword>
+         <keyword>equivalent</keyword>
+         <keyword>to</keyword>
 
           <!-- commands -->
           <keyword>alias</keyword>