X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=4a21e10b5a9e6334ce022bbb430b6ba6739fb08f;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=fae3df93d4eb3eea3005a63646ddf68e437af6f3;hpb=08ecc780b3b0a4cac7ed72cf68c310e4eeffa2c1;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index fae3df93d..4a21e10b5 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: [
@@ -348,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: [
@@ -393,14 +397,14 @@ EXTEND
     ]
   ];
   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: [
@@ -417,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))
@@ -448,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 ->