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 5d6dac77108bbc9da550cf495a5193c08c613800..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: [
@@ -236,12 +242,27 @@ EXTEND
         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 -> Some t' | SYMBOL "_" -> None];
+    | 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
-           None -> GrafiteAst.Bydone (loc, t) 
-        | Some (ty,id,t1) ->
-           GrafiteAst.By_term_we_proved(loc, t, ty, id, t1))
+           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 ->  
@@ -253,19 +274,27 @@ EXTEND
     | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ;
         SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] ->
         GrafiteAst.Case(loc,id,params)
-    | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term ->
-        GrafiteAst.Let1 (loc, id, t, t1)
-    | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ->
-       GrafiteAst.Bywehave (loc, t, t1, id, t2, id1)
-    | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ->
-     GrafiteAst.RewritingStep(loc, Some termine, t1, t2)
-    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ->
-     GrafiteAst.RewritingStep(loc, None, t1, t2)
+    | 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] -> Some (ty,id,t1)
-    | IDENT "done" -> None
+    [ 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: