positivity check fixed, some subterms were erroneously skipped

[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 6ce615091a5203602f6195221d48e2b0b62f4911..26dd9b9e050ddb2707997ee69ea7cfb43978d3f0 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -55,7 +55,6 @@ let statement = Grammar.Entry.create grammar "statement"
 
 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 
-let default_precedence = 50
 let default_associativity = Gramext.NonA
         
 let mk_rec_corec ind_kind defs loc = 
@@ -96,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 ]
@@ -170,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" ->
@@ -575,7 +576,7 @@ EXTEND
   ];
   notation: [
     [ dir = OPT direction; s = QSTRING;
-      assoc = OPT associativity; prec = OPT precedence;
+      assoc = OPT associativity; prec = precedence;
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
@@ -592,14 +593,9 @@ EXTEND
             | None -> default_associativity
             | Some assoc -> assoc
           in
-          let prec =
-            match prec with
-            | None -> default_precedence
-            | Some prec -> prec
-          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)
@@ -663,13 +659,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 ->
@@ -717,6 +715,7 @@ EXTEND
     | com = comment ->
        fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
+       !out fname;       
        fun ?(never_include=false) ~include_paths status ->
         let _root, buri, fullpath, _rrelpath = 
           Librarian.baseuri_of_script ~include_paths fname 
@@ -726,7 +725,6 @@ EXTEND
          else LexiconEngine.eval_command status 
                 (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
-         !out fname;
          status,
           LSome
           (GrafiteAst.Executable