we parametrized CicNotationPt.obj on 'term

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index b41ae8ebcd8468c14415e86ca2e17c7eed149cc4..14802a629e8cd32360a33c33d1550f506fc50b84 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -35,7 +35,8 @@ type 'a localized_option =
 
 type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
-   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+   CicNotationPt.term GrafiteAst.reduction, 
+   CicNotationPt.term CicNotationPt.obj, string)
     GrafiteAst.statement
 
 type statement =
@@ -133,9 +134,7 @@ EXTEND
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
-    | IDENT "auto"; params = 
-        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
-          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+    | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
@@ -270,11 +269,24 @@ EXTEND
     | 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  ->
+    | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params  ] ; cont=rewriting_step_continuation ->
+     GrafiteAst.RewritingStep(loc, Some (start,termine), t1, t2, cont)
+    | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ;
+      cont=rewriting_step_continuation  ->
      GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
   ]
+];
+  auto_params: [
+   [ params =
+      LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+       string_of_int v | v = IDENT -> v ] -> i,v ] ->
+      params
+   ]
+];
+  auto_params': [
+   [ LPAREN; params = auto_params; RPAREN -> params
+   | -> []
+   ]
 ];
   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,Some id,t1)
@@ -288,9 +300,8 @@ EXTEND
     ]
 ];
   rewriting_step_continuation : [
-    [ IDENT "done" -> None
-    | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
-    | -> Some Cic.Anonymous
+    [ IDENT "done" -> true
+    | -> false
     ]
 ];
   atomic_tactical:
@@ -401,9 +412,15 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
-    | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
-         let prefix = match prefix with None -> "" | Some prefix -> prefix in
-        GrafiteAst.Inline (loc,suri,prefix)
+    | [ IDENT "inline"]; 
+        style = OPT [ IDENT "procedural" ];
+       suri = QSTRING; prefix = OPT QSTRING ->
+         let style = match style with 
+           | None   -> GrafiteAst.Declarative
+           | Some _ -> GrafiteAst.Procedural
+        in
+        let prefix = match prefix with None -> "" | Some prefix -> prefix in
+        GrafiteAst.Inline (loc,style,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)