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 908ad007f79cc5fd8a863c09e7dfe84e9f0c9a7f..056e595e7ed8b8fc5eaf3867a47a1072e53058f9 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -107,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 ->
@@ -125,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;