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 41c3fd054bb411936e8289f386addbfe93933e5e..056e595e7ed8b8fc5eaf3867a47a1072e53058f9 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -29,10 +29,14 @@ let grammar = CicNotationParser.level2_ast_grammar
 
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
-let statements = Grammar.Entry.create grammar "statements"
+
+let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+
+let default_precedence = 50
+let default_associativity = Gramext.NonA
 
 EXTEND
-  GLOBAL: term statement statements;
+  GLOBAL: term statement;
   arg: [
    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN -> names,ty
@@ -103,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 ->
@@ -121,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;
@@ -338,10 +348,10 @@ EXTEND
     ]
   ];
   argument: [
-    [ id = IDENT -> GrafiteAst.IdentArg (0, id)
+    [ id = IDENT -> CicNotationPt.IdentArg (0, id)
     | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
       SYMBOL "."; id = IDENT ->
-        GrafiteAst.IdentArg (List.length l, id)
+        CicNotationPt.IdentArg (List.length l, id)
     ]
   ];
   associativity: [
@@ -359,21 +369,36 @@ 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: [
-    [ u = URI -> GrafiteAst.UriPattern (UriManager.uri_of_string u)
-    | id = IDENT -> GrafiteAst.VarPattern id
+    [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
+    | id = IDENT -> CicNotationPt.VarPattern id
+    | SYMBOL "_" -> CicNotationPt.ImplicitPattern
     | LPAREN; terms = LIST1 SELF; RPAREN ->
         (match terms with
         | [] -> assert false
         | [term] -> term
-        | terms -> GrafiteAst.ApplPattern terms)
+        | terms -> CicNotationPt.ApplPattern terms)
     ]
   ];
   interpretation: [
@@ -435,11 +460,13 @@ EXTEND
         GrafiteAst.Default (loc,what,uris)
     | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
         GrafiteAst.Notation (loc, l1, assoc, prec, l2)
-    | IDENT "interpretation"; (symbol, args, l3) = interpretation ->
-        GrafiteAst.Interpretation (loc, (symbol, args), l3)
+    | IDENT "interpretation"; id = QSTRING;
+      (symbol, args, l3) = interpretation ->
+        GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
 
     | IDENT "dump" -> GrafiteAst.Dump loc
-    | IDENT "render"; u = URI -> GrafiteAst.Render (loc, UriManager.uri_of_string u)
+    | IDENT "render"; u = URI ->
+        GrafiteAst.Render (loc, UriManager.uri_of_string u)
   ]];
   executable: [
     [ cmd = command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
@@ -457,18 +484,16 @@ EXTEND
   statement: [
     [ ex = executable -> GrafiteAst.Executable (loc,ex)
     | com = comment -> GrafiteAst.Comment (loc, com)
+    | EOI -> raise End_of_file
     ]
   ];
-  statements: [
-    [ l = LIST0 statement ; EOI -> l 
-    ]  
-  ];
 END
 
 let exc_located_wrapper f =
   try
     f ()
   with
+  | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
       raise (CicNotationParser.Parse_error (floc, msg))
   | Stdpp.Exc_located (floc, exn) ->
@@ -476,6 +501,4 @@ let exc_located_wrapper f =
 
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
-let parse_statements stream =
-  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))