X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=c138fce2787ff3baced04c691c3a1e865b98eac2;hb=f981a524748846acc29b76b6e616af110b4ee13d;hp=984635ec60cc44433df2b847ee3f877f1ff9edc6;hpb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 984635ec6..c138fce27 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -30,8 +30,10 @@ let grammar = CicNotationParser.level2_ast_grammar
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
 
-let add_raw_attribute ?context ~text term =
-  CicNotationPt.AttributedTerm (`Raw (text, context), term)
+let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+
+let default_precedence = 50
+let default_associativity = Gramext.NonA
 
 EXTEND
   GLOBAL: term statement;
@@ -50,10 +52,11 @@ EXTEND
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
   reduction_kind: [
-    [ IDENT "reduce" -> `Reduce
+    [ IDENT "normalize" -> `Normalize
+    | IDENT "reduce" -> `Reduce
     | IDENT "simplify" -> `Simpl
-    | IDENT "whd" -> `Whd 
-    | IDENT "normalize" -> `Normalize ]
+    | IDENT "unfold"; t = OPT term -> `Unfold t
+    | IDENT "whd" -> `Whd ]
   ];
   sequent_pattern_spec: [
    [ hyp_paths =
@@ -105,8 +108,9 @@ EXTEND
         GrafiteAst.Assumption loc
     | IDENT "auto";
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
-      width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ] -> 
-          GrafiteAst.Auto (loc,depth,width)
+      width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
+      paramodulation = OPT [ IDENT "paramodulation" ] ->  (* ALB *)
+          GrafiteAst.Auto (loc,depth,width,paramodulation)
     | IDENT "clear"; id = IDENT ->
         GrafiteAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->
@@ -123,8 +127,13 @@ EXTEND
         GrafiteAst.Cut (loc, ident, t)
     | IDENT "decide"; IDENT "equality" ->
         GrafiteAst.DecideEquality loc
-    | IDENT "decompose"; where = tactic_term ->
-        GrafiteAst.Decompose (loc, where)
+    | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
+      OPT "names"; num = OPT [num = int -> num];
+      idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in   
+        let types = match types with None -> [] | Some types -> types in
+	let to_spec id = GrafiteAst.Ident id in
+	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "discriminate"; t = tactic_term ->
         GrafiteAst.Discriminate (loc, t)
     | IDENT "elim"; what = tactic_term;
@@ -356,20 +365,32 @@ EXTEND
     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
   ];
   notation: [
-    [ s = QSTRING;
+    [ dir = OPT direction; s = QSTRING;
       assoc = OPT associativity; prec = OPT precedence;
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            add_raw_attribute ~context:`Ast ~text:blob
+            add_raw_attribute ~text:(sprintf "@{%s}" blob)
               (CicNotationParser.parse_level2_ast (Stream.of_string blob))
         | blob = UNPARSED_META ->
-            add_raw_attribute ~context:`Meta ~text:blob
+            add_raw_attribute ~text:(sprintf "${%s}" blob)
               (CicNotationParser.parse_level2_meta (Stream.of_string blob))
         ] ->
-          (add_raw_attribute ~text:s
-            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
-           assoc, prec, p2)
+          let assoc =
+            match assoc with
+            | 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 (Stream.of_string s))
+          in
+          (dir, p1, assoc, prec, p2)
     ]
   ];
   level3_term: [
@@ -384,7 +405,7 @@ EXTEND
     ]
   ];
   interpretation: [
-    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+    [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
         (s, args, t)
     ]
   ];
@@ -440,8 +461,8 @@ EXTEND
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
-    | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
-        GrafiteAst.Notation (loc, l1, assoc, prec, l2)
+    | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
+        GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)