added optional "paramodulation" parameter to auto to turn on paramodulation

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 8bd5cc04e3e976c62dcc2f07e4cecbdfc36ec0a7..056e595e7ed8b8fc5eaf3867a47a1072e53058f9 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -30,6 +30,11 @@ let grammar = CicNotationParser.level2_ast_grammar
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
 
+let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+
+let default_precedence = 50
+let default_associativity = Gramext.NonA
+
 EXTEND
   GLOBAL: term statement;
   arg: [
@@ -102,8 +107,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 ->
@@ -120,8 +126,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;
@@ -358,11 +369,25 @@ EXTEND
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
-            CicNotationParser.parse_level2_ast (Stream.of_string blob)
+            add_raw_attribute ~text:(sprintf "@{%s}" blob)
+              (CicNotationParser.parse_level2_ast (Stream.of_string blob))
         | blob = UNPARSED_META ->
-            CicNotationParser.parse_level2_meta (Stream.of_string blob) ]
-      ->
-        (CicNotationParser.parse_level1_pattern (Stream.of_string s), assoc, prec, p2)
+            add_raw_attribute ~text:(sprintf "${%s}" blob)
+              (CicNotationParser.parse_level2_meta (Stream.of_string blob))
+        ] ->
+          let assoc =
+            match assoc with
+            | None -> default_associativity
+            | Some assoc -> assoc
+          in
+          let prec =
+            match prec with
+            | None -> default_precedence
+            | Some prec -> prec
+          in
+          (add_raw_attribute ~text:s
+            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
+           assoc, prec, p2)
     ]
   ];
   level3_term: [