Keeping track of locations of disambiguated ids and symbols.

[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 451d03a101de6273a20d566dc0e1103e06abb6e3..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)
@@ -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 ]
@@ -612,11 +609,18 @@ 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, `Ambiguous)) names, Some ty
-    | name = IDENT -> [Ast.Ident (name, `Ambiguous)], 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
@@ -626,7 +630,7 @@ EXTEND
    ]
   ];
   single_arg: [
-    [ name = IDENT -> Ast.Ident (name, `Ambiguous)
+    [ (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
@@ -649,6 +653,9 @@ EXTEND
         | _ -> failwith ("Invalid index name: " ^ blob)
     ]
   ];
+  located: [
+    [ s = SYMBOL -> loc ]
+  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -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,`Ambiguous), 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,10 +752,7 @@ EXTEND
     ];
   term: LEVEL "90"
     [
-      [ id = IDENT -> return_term loc (Ast.Ident (id, `Ambiguous))
-      | id = IDENT; s = explicit_subst -> (* XXX: no more explicit subst? *)
-          assert false
-          (* return_term loc (Ast.Ident (id, Some s))*)
+      [ (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))
@@ -798,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
@@ -807,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;
@@ -845,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))