- decompose tactic: decomposable constants are now allowed (they are unfolded)

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

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 6e108ce0447109c69dab396da7faa928f1cbac89..b41ae8ebcd8468c14415e86ca2e17c7eed149cc4 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -61,12 +61,6 @@ type by_continuation =
 
 EXTEND
   GLOBAL: term statement;
-  arg: [
-   [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
-      SYMBOL ":"; ty = term; RPAREN -> names,ty
-   | name = IDENT -> [name],Ast.Implicit
-   ]
-  ];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
   ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
@@ -133,8 +127,10 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
-    | IDENT "applyS"; t = tactic_term ->
-        GrafiteAst.ApplyS (loc, t)
+    | IDENT "applyS"; t = tactic_term ; params = 
+        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+        GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
     | IDENT "auto"; params = 
@@ -358,7 +354,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
+    fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
     tl = OPT [ "with";
@@ -380,7 +376,7 @@ EXTEND
   ] ];
   
   record_spec: [ [
-    name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+    name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
@@ -405,8 +401,9 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
-    | [ IDENT "inline"]; suri = QSTRING ->
-         GrafiteAst.Inline (loc,suri)
+    | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING ->
+         let prefix = match prefix with None -> "" | Some prefix -> prefix in
+        GrafiteAst.Inline (loc,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)
@@ -549,8 +546,14 @@ EXTEND
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
             match defs with
-            | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
-            | ((Ast.Ident (name, None), None),_,_) :: _ ->
+            | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
+                let ty =
+                 List.fold_right
+                  (fun var ty -> Ast.Binder (`Pi,var,ty)
+                  ) params ty
+                in
+                 name,ty
+            | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
                 name, Ast.Implicit
             | _ -> assert false 
           in