Declarative tactics for rewriting steps, elimination of the existential

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 1a11ec62f0d788e06a15c55d3c3f3453ccb73e7d..1eb2a495d4624bed0709830af6386c4a25e5ec10 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -53,6 +53,12 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 let default_precedence = 50
 let default_associativity = Gramext.NonA
 
+type by_continuation =
+   BYC_done
+ | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
+ | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
+
 EXTEND
   GLOBAL: term statement;
   arg: [
@@ -231,8 +237,66 @@ EXTEND
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
         GrafiteAst.Transitivity (loc, t)
+     (* Produzioni Aggiunte *)
+    | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ->
+        GrafiteAst.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']->
+        GrafiteAst.Suppose (loc, t, id, t1)
+    | IDENT "by" ; t = [t' = tactic_term -> LSome t' | SYMBOL "_" -> LNone loc];
+      cont=by_continuation ->
+       let t' = match t with LNone _ -> None | LSome t -> Some t in
+       (match cont with
+           BYC_done -> GrafiteAst.Bydone (loc, t')
+        | BYC_weproved (ty,id,t1) ->
+           GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
+        | BYC_letsuchthat (id1,t1,id2,t2) ->
+           (match t with
+               LNone floc ->
+                 raise (HExtlib.Localized
+                 (floc,CicNotationParser.Parse_error
+                   "tactic_term expected here"))
+              | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+        | BYC_wehaveand (id1,t1,id2,t2) ->
+           (match t with
+               LNone floc ->
+                 raise (HExtlib.Localized
+                 (floc,CicNotationParser.Parse_error
+                   "tactic_term expected here"))
+              | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2)))
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']->
+        GrafiteAst.We_need_to_prove (loc, t, id, t1)
+    | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term ->  
+        GrafiteAst.We_proceed_by_induction_on (loc, t, t1)
+    | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN ->
+        GrafiteAst.Byinduction(loc, t, id)
+    | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term ->
+        GrafiteAst.Thesisbecomes(loc, t)
+    | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
+        SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
+        GrafiteAst.Case(loc,id,params)
+    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ; cont=rewriting_step_continuation ->
+     GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont)
+    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ; cont=rewriting_step_continuation  ->
+     GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+  ]
+];
+  by_continuation: [
+    [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,id,t1)
+    | IDENT "done" -> BYC_done
+    | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
+      IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ;
+      RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
+    | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;
+      "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
+       BYC_wehaveand (id1,t1,id2,t2)
     ]
-  ];
+];
+  rewriting_step_continuation : [
+    [ IDENT "done" -> None
+    | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
+    | -> Some Cic.Anonymous
+    ]
+];
   atomic_tactical:
     [ "sequence" LEFTA
       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
@@ -332,13 +396,7 @@ EXTEND
   ] ];
   
   macro: [
-    [ [ IDENT "quit"  ] -> GrafiteAst.Quit loc
-(*     | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
-(*     | [ IDENT "undo"   ]; steps = OPT NUMBER ->
-        GrafiteAst.Undo (loc, int_opt steps)
-    | [ IDENT "redo"   ]; steps = OPT NUMBER ->
-        GrafiteAst.Redo (loc, int_opt steps) *)
-    | [ IDENT "check"   ]; t = term ->
+    [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
@@ -351,7 +409,6 @@ EXTEND
         GrafiteAst.WElim (loc, t)
     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
         GrafiteAst.WHint (loc,t)
-    | [ IDENT "print" ]; name = QSTRING -> GrafiteAst.Print (loc, name)
     ]
   ];
   alias_spec: [
@@ -463,6 +520,7 @@ EXTEND
       IDENT "set"; n = QSTRING; v = QSTRING ->
         GrafiteAst.Set (loc, n, v)
     | IDENT "drop" -> GrafiteAst.Drop loc
+    | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s)
     | IDENT "qed" -> GrafiteAst.Qed loc
     | IDENT "variant" ; name = IDENT; SYMBOL ":"; 
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->