we proved that the union of two saturated sets is saturated

[helm.git] / matitaB / components / content_pres / cicNotationParser.ml

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 53c60820c78632bd58f3b8527d697897537c92ff..3ccd5414139bbd8886d90fc7ba12bdfc4675461d 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -43,6 +43,7 @@ type ('a,'b,'c,'d,'e) grammars = {
   term: 'b Grammar.Entry.e;
   ident: 'e Grammar.Entry.e;
   let_defs: 'c Grammar.Entry.e;
+  located: Stdpp.location Grammar.Entry.e;
   protected_binder_vars: 'd Grammar.Entry.e;
   level2_meta: 'b Grammar.Entry.e;
 }
@@ -84,7 +85,10 @@ let level_of precedence =
     raise (Level_not_found precedence);
   string_of_int precedence 
 
-let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
+let gram_symbol s = 
+  Gramext.srules 
+   [ [ Gramext.Stoken ("SYMBOL",s) ], Gramext.action (fun _ loc -> loc) ]
+ 
 let gram_ident status =
  Gramext.Snterm (Grammar.Entry.obj
   (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
@@ -110,7 +114,9 @@ let make_action action bindings =
   let rec aux (vl : NotationEnv.t) =
     function
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
-    | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
+    | NoBinding :: tl -> Gramext.action 
+                          (fun (loc: Ast.location) -> 
+                            aux (("",(Env.NoType,Env.LocValue loc))::vl) tl)
     (* LUCA: DEFCON 3 BEGIN *)
     | Binding (name, Env.TermType l) :: tl ->
         Gramext.action
@@ -134,6 +140,7 @@ let make_action action bindings =
             aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl)
     | Env _ :: tl ->
         Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl)
+    | _ (* Binding (_,NoType) *) -> assert false
     (* LUCA: DEFCON 3 END *)
   in
     aux [] (List.rev bindings)
@@ -338,7 +345,7 @@ let fold_exists terms ty body =
   List.fold_right
     (fun term body ->
       let lambda = Ast.Binder (`Lambda, (term, ty), body) in
-      Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+      Ast.Appl [ Ast.Symbol ("exists", None); lambda ])
     terms body
 
 let fold_binder binder pt_names body =
@@ -568,16 +575,6 @@ EXTEND
     | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
     ]
   ];
-  explicit_subst: [
-    [ SYMBOL "\\subst ";  (* to avoid catching frequent "a [1]" cases *)
-      SYMBOL "[";
-      substs = LIST1 [
-        i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
-      ] SEP SYMBOL ";";
-      SYMBOL "]" ->
-        substs
-    ]
-  ];
   meta_subst: [
     [ s = SYMBOL "_" -> None
     | p = term -> Some p ]
@@ -589,12 +586,12 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
-    | id = PIDENT -> Ast.Ident (id, None), None
-    | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | id = PIDENT -> Ast.Ident (id, `Ambiguous), None
+    | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None
     | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
-        Ast.Ident (id, None), Some typ
+        Ast.Ident (id, `Ambiguous), Some typ
     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
-        Ast.Ident ("_", None), Some typ
+        Ast.Ident ("_", `Ambiguous), Some typ
     ]
   ];
   match_pattern: [
@@ -612,27 +609,34 @@ EXTEND
     | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
     ]
   ];
+  tident: [
+    [ uri = HREF;
+      id = IDENT;
+      HREFEND -> (id, `Uri uri) ]];
+  gident: [
+    [ fullident = tident -> fullident;
+    | id = IDENT -> (id, `Ambiguous) ]];
   arg: [
-    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
+    [ LPAREN; names = LIST1 gident SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN ->
-        List.map (fun n -> Ast.Ident (n, None)) names, Some ty
-    | name = IDENT -> [Ast.Ident (name, None)], None
+        List.map (fun (n,u) -> Ast.Ident (n,u)) names, Some ty
+    | (name,uri) = gident -> [Ast.Ident (name,uri)], None
     | blob = UNPARSED_META ->
         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
-        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
+        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None
         | _ -> failwith "Invalid bound name."
    ]
   ];
   single_arg: [
-    [ name = IDENT -> Ast.Ident (name, None)
+    [ (name,uri) = gident -> Ast.Ident (name,uri)
     | blob = UNPARSED_META ->
         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
-        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous)
         | _ -> failwith "Invalid index name."
     ]
   ];
@@ -649,6 +653,9 @@ EXTEND
         | _ -> failwith ("Invalid index name: " ^ blob)
     ]
   ];
+  located: [
+    [ s = SYMBOL -> loc ]
+  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -692,7 +699,7 @@ EXTEND
     [ vars = [ l =
         [ l = LIST1 single_arg SEP SYMBOL "," -> l
         | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> 
-            List.map (fun x -> Ast.Ident(x,None)) l
+            List.map (fun x -> Ast.Ident(x,`Ambiguous)) l
       ] -> l ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
     ]
@@ -712,8 +719,8 @@ EXTEND
      var = 
       [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
          id, Some typ
-      | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
-         Ast.Ident(id,None), ty ];
+      | (id,uri) = gident; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
+         Ast.Ident (id,uri), ty ];
       SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
@@ -745,13 +752,12 @@ EXTEND
     ];
   term: LEVEL "90"
     [
-      [ id = IDENT -> return_term loc (Ast.Ident (id, None))
-      | id = IDENT; s = explicit_subst ->
-          return_term loc (Ast.Ident (id, Some s))
-      | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
-      | u = URI -> return_term loc (Ast.Uri (u, None))
+      [ (id,uri) = gident -> return_term loc (Ast.Ident (id,uri))
+      | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
+      | u = URI -> return_term loc (Ast.Ident 
+                     (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
-      | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+      | n = NUMBER -> return_term loc (Ast.Num (n, None))
       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
       | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
@@ -796,6 +802,7 @@ let initial_grammars keywords =
   let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast" in
   let term = Grammar.Entry.create level2_ast_grammar "term" in
   let ident = Grammar.Entry.create level2_ast_grammar "ident" in
+  let located = Grammar.Entry.create level2_ast_grammar "located" in
   let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
   let protected_binder_vars = 
     Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
@@ -805,6 +812,7 @@ let initial_grammars keywords =
     term=term;
     ident=ident;
     let_defs=let_defs;
+    located=located;
     protected_binder_vars=protected_binder_vars;
     level2_meta=level2_meta;
     level2_ast_grammar=level2_ast_grammar;
@@ -843,7 +851,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         Some (Gramext.Level level),
         [ None,
           Some (*Gramext.NonA*) Gramext.NonA,
-          [ p_atoms, 
+          [ p_atoms, (* concrete l1 syntax *) 
             (make_action
               (fun (env: NotationEnv.t) (loc: Ast.location) ->
                 (action env loc))