basic support for imposed flavour in procedural object rendering

[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 20aad1cd3a19c16788264e634cb95028cca31c89..38a8667d304ae511da33b6abf47971f178922726 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -95,7 +95,7 @@ type by_continuation =
 EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
-  tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
+  tactic_term: [ [ t = term LEVEL "90" -> t ] ];
   new_name: [
     [ id = IDENT -> Some id
     | SYMBOL "_" -> None ]
@@ -169,6 +169,8 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
+    | IDENT "applyP"; t = tactic_term ->
+        GrafiteAst.ApplyP (loc, t)
     | IDENT "applyS"; t = tactic_term ; params = auto_params ->
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
@@ -450,6 +452,12 @@ EXTEND
     | [ IDENT "theorem"     ] -> `Theorem
     ]
   ];
+  inline_flavour: [
+     [ attr = theorem_flavour -> attr
+     | [ IDENT "axiom"     ]  -> `Axiom
+     | [ IDENT "mutual"    ]  -> `MutualDefinition
+     ]
+  ];
   inductive_spec: [ [
     fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
@@ -500,13 +508,14 @@ EXTEND
         GrafiteAst.Check (loc, t)
     | [ IDENT "inline"]; 
         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
-        suri = QSTRING; prefix = OPT QSTRING ->
+        suri = QSTRING; prefix = OPT QSTRING;
+       flavour = OPT [ IDENT "as"; attr = inline_flavour -> attr ]->
          let style = match style with 
             | None       -> GrafiteAst.Declarative
             | Some depth -> GrafiteAst.Procedural depth
          in
          let prefix = match prefix with None -> "" | Some prefix -> prefix in
-         GrafiteAst.Inline (loc,style,suri,prefix)
+         GrafiteAst.Inline (loc,style,suri,prefix, flavour)
     | [ IDENT "hint" ]; rew = OPT (IDENT "rewrite")  -> 
          if rew = None then GrafiteAst.Hint (loc, false) else GrafiteAst.Hint (loc,true)
     | IDENT "auto"; params = auto_params ->
@@ -593,7 +602,7 @@ EXTEND
           in
           let p1 =
             add_raw_attribute ~text:s
-              (CicNotationParser.parse_level1_pattern
+              (CicNotationParser.parse_level1_pattern prec
                 (Ulexing.from_utf8_string s))
           in
           (dir, p1, assoc, prec, p2)
@@ -657,13 +666,15 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ; arity = OPT int ; 
-      saturations = OPT int; composites = OPT (IDENT "nocomposites") ->
+    | IDENT "coercion" ; 
+      t = [ u = URI -> Ast.Uri (u,None) | t = tactic_term ; OPT "with" -> t ] ;
+      arity = OPT int ; saturations = OPT int; 
+      composites = OPT (IDENT "nocomposites") ->
         let arity = match arity with None -> 0 | Some x -> x in
         let saturations = match saturations with None -> 0 | Some x -> x in
         let composites = match composites with None -> true | Some _ -> false in
         GrafiteAst.Coercion
-         (loc, UriManager.uri_of_string suri, composites, arity, saturations)
+         (loc, t, composites, arity, saturations)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->