use uniform naming for referencing cicNotation* modules

[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 c138fce2787ff3baced04c691c3a1e865b98eac2..ae7e5229d1941d2809023f51863295cace796659 100644 (file)
--- 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) ] ];
@@ -63,12 +65,12 @@ EXTEND
       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
+          None -> Ast.UserInput
         | Some goal_path -> goal_path
       in
        hyp_paths,goal_path
@@ -86,12 +88,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: [
@@ -349,10 +351,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: [
@@ -394,14 +396,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: [
@@ -418,26 +420,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))
@@ -449,9 +451,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 ->