X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=65df218d4f4bf22a1f8d519bcad35f2846c839bf;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=cceeaf10dfb4b717f82e59c6e1d3154221607255;hpb=cb473667ca89549ed0ca6dd2bfb03a5fe9eeaa82;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index cceeaf10d..65df218d4 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -25,12 +25,14 @@
 
 open Printf
 
+module Ast = CicNotationPt
+
 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 add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 
 let default_precedence = 50
 let default_associativity = Gramext.NonA
@@ -40,7 +42,7 @@ EXTEND
   arg: [
    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN -> names,ty
-   | name = IDENT -> [name],CicNotationPt.Implicit
+   | name = IDENT -> [name],Ast.Implicit
    ]
   ];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
@@ -52,23 +54,25 @@ 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 =
       LIST0
        [ id = IDENT ;
          path = OPT [SYMBOL ":" ; path = term -> path ] ->
-         (id,match path with Some p -> p | None -> CicNotationPt.UserInput) ]
+         (id,match path with Some p -> p | None -> Ast.UserInput) ]
        SEP SYMBOL ";";
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
       let goal_path =
-       match goal_path with
-          None -> CicNotationPt.UserInput
-        | Some goal_path -> goal_path
+       match goal_path, hyp_paths with
+          None, [] -> Ast.UserInput
+        | None, _::_ -> Ast.Implicit
+        | Some goal_path, _ -> goal_path
       in
        hyp_paths,goal_path
    ]
@@ -85,12 +89,12 @@ EXTEND
         ] ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
-             wanted,None -> wanted, [], CicNotationPt.UserInput
+             wanted,None -> wanted, [], Ast.UserInput
            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
          in
           wanted, hyp_paths, goal_path ] ->
       match res with
-         None -> None,[],CicNotationPt.UserInput
+         None -> None,[],Ast.UserInput
        | Some ps -> ps]
   ];
   direction: [
@@ -107,8 +111,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 ->
@@ -347,10 +352,10 @@ EXTEND
     ]
   ];
   argument: [
-    [ id = IDENT -> CicNotationPt.IdentArg (0, id)
+    [ id = IDENT -> Ast.IdentArg (0, id)
     | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
       SYMBOL "."; id = IDENT ->
-        CicNotationPt.IdentArg (List.length l, id)
+        Ast.IdentArg (List.length l, id)
     ]
   ];
   associativity: [
@@ -363,7 +368,7 @@ 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 = 
@@ -384,24 +389,26 @@ EXTEND
             | None -> default_precedence
             | Some prec -> prec
           in
-          (add_raw_attribute ~text:s
-            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
-           assoc, prec, p2)
+          let p1 =
+            add_raw_attribute ~text:s
+              (CicNotationParser.parse_level1_pattern (Stream.of_string s))
+          in
+          (dir, p1, assoc, prec, p2)
     ]
   ];
   level3_term: [
-    [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
-    | id = IDENT -> CicNotationPt.VarPattern id
-    | SYMBOL "_" -> CicNotationPt.ImplicitPattern
+    [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
+    | id = IDENT -> Ast.VarPattern id
+    | SYMBOL "_" -> Ast.ImplicitPattern
     | LPAREN; terms = LIST1 SELF; RPAREN ->
         (match terms with
         | [] -> assert false
         | [term] -> term
-        | terms -> CicNotationPt.ApplPattern terms)
+        | terms -> Ast.ApplPattern terms)
     ]
   ];
   interpretation: [
-    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+    [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
         (s, args, t)
     ]
   ];
@@ -414,26 +421,26 @@ EXTEND
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
         GrafiteAst.Obj (loc, 
           GrafiteAst.Theorem 
-            (`Variant,name,typ,Some (CicNotationPt.Ident (newname, None))))
+            (`Variant,name,typ,Some (Ast.Ident (newname, None))))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body))
     | flavour = theorem_flavour; name = IDENT;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc,
-          GrafiteAst.Theorem (flavour, name, CicNotationPt.Implicit, body))
+          GrafiteAst.Theorem (flavour, name, Ast.Implicit, body))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
             match defs with
-            | ((CicNotationPt.Ident (name, None), Some ty),_,_) :: _ -> name,ty
-            | ((CicNotationPt.Ident (name, None), None),_,_) :: _ ->
-                name, CicNotationPt.Implicit
+            | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
+            | ((Ast.Ident (name, None), None),_,_) :: _ ->
+                name, Ast.Implicit
             | _ -> assert false 
           in
-          let body = CicNotationPt.Ident (name,None) in
+          let body = Ast.Ident (name,None) in
           GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty,
-            Some (CicNotationPt.LetRec (ind_kind, defs, body))))
+            Some (Ast.LetRec (ind_kind, defs, body))))
     | [ IDENT "inductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
@@ -445,9 +452,9 @@ EXTEND
         in
         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
     | IDENT "coercion" ; name = IDENT -> 
-        GrafiteAst.Coercion (loc, CicNotationPt.Ident (name,Some []))
+        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []))
     | IDENT "coercion" ; name = URI -> 
-        GrafiteAst.Coercion (loc, CicNotationPt.Uri (name,Some []))
+        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []))
     | IDENT "alias" ; spec = alias_spec ->
         GrafiteAst.Alias (loc, spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
@@ -457,8 +464,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)
@@ -501,3 +508,19 @@ let exc_located_wrapper f =
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
 
+let parse_dependencies stream = 
+  let tok_stream,_ = CicNotationLexer.level2_ast_lexer.Token.tok_func stream in
+  let rec parse acc = 
+    (parser
+    | [< '("URI", u) >] ->
+        parse (GrafiteAst.UriDep (UriManager.uri_of_string u) :: acc)
+    | [< '("IDENT", "include"); '("QSTRING", fname) >] ->
+        parse (GrafiteAst.IncludeDep fname :: acc)
+    | [< '("IDENT", "set"); '("QSTRING", "baseuri"); '("QSTRING", baseuri) >] ->
+        parse (GrafiteAst.BaseuriDep baseuri :: acc)
+    | [< '("EOI", _) >] -> acc
+    | [< 'tok >] -> parse acc
+    | [<  >] -> acc) tok_stream
+  in
+  List.rev (parse [])
+