From 185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42 Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Thu, 14 Mar 2019 10:31:01 +0100 Subject: [PATCH] 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 --- matita/components/grafite/grafiteAst.ml | 2 ++ matita/components/grafite/grafiteAstPp.ml | 2 ++ matita/components/grafite_engine/grafiteEngine.ml | 1 + matita/components/grafite_parser/grafiteParser.ml | 4 +++- matita/components/ng_tactics/declarative.ml | 4 ++++ matita/components/ng_tactics/declarative.mli | 1 + matita/matita/matita.lang | 5 +++++ 7 files changed, 18 insertions(+), 1 deletion(-) 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 @@ lapply destruct assume + suppose + that + is + equivalent + to alias -- 2.39.2