(no commit message)

[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 dc4534c845f332fdc0679113bf520a6badc2a015..6736211d4e67fbf5b88990b1bf93535f74b2d5e9 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -30,6 +30,8 @@ open Printf
 module Ast = NotationPt
 module Env = NotationEnv
 
+let prerr_endline _ = () 
+
 exception Parse_error of string
 exception Level_not_found of int
 
@@ -45,6 +47,7 @@ type ('a,'b,'c,'d,'e) grammars = {
   sym_attributes: (string option * string option) Grammar.Entry.e;
   sym_table: (string * Stdpp.location Grammar.Entry.e) list;
   let_defs: 'c Grammar.Entry.e;
+  let_codefs: 'c Grammar.Entry.e;
   protected_binder_vars: 'd Grammar.Entry.e;
   level2_meta: 'b Grammar.Entry.e;
 }
@@ -103,12 +106,12 @@ let add_symbol_to_grammar_explicit level2_ast_grammar
           (Gramext.action (fun _ loc -> None, loc))
         ; [Gramext.Stoken ("ATAG","")
           ;Gramext.Snterm (Grammar.Entry.obj sym_attributes)
-          ;Gramext.Stoken ("SYMBOL",">")
+          ;Gramext.Stoken ("SYMBOL","\005")
           ;Gramext.Stoken ("SYMBOL",s)
           ;Gramext.Stoken ("ATAGEND","")],
           (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc))
         ]]];
-  prerr_endline ("adding to grammar symbol " ^ s);
+(*  prerr_endline ("adding to grammar symbol " ^ s); *)
   (s,entry)::sym_table
  
 
@@ -157,9 +160,9 @@ let gram_term status = function
 
 let gram_of_literal status =
   function
-  | `Symbol s -> gram_symbol status s
-  | `Keyword s -> gram_keyword s
-  | `Number s -> gram_number s
+  | `Symbol (s,_) -> gram_symbol status s
+  | `Keyword (s,_) -> gram_keyword s
+  | `Number (s,_) -> gram_number s
 
 let make_action status action bindings =
   let rec aux (vl : NotationEnv.t) =
@@ -226,9 +229,9 @@ let update_sym_grammar status pattern =
         assert false
   and aux_literal status =
     function
-    | `Symbol s -> add_symbol_to_grammar status s
-    | `Keyword s -> status
-    | `Number s -> status
+    | `Symbol (s,_) -> add_symbol_to_grammar status s
+    | `Keyword _ -> status
+    | `Number _ -> status
   and aux_layout status = function
     | Ast.Sub (p1, p2) -> aux (aux status p1) p2
     | Ast.Sup (p1, p2) -> aux (aux status p1) p2
@@ -273,11 +276,11 @@ let extract_term_production status pattern =
         assert false
   and aux_literal =
     function
-    | `Symbol s -> [NoBinding, gram_symbol status s]
-    | `Keyword s ->
+    | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
+    | `Keyword (s,_) ->
         (* assumption: s will be registered as a keyword with the lexer *)
         [NoBinding, gram_keyword s]
-    | `Number s -> [NoBinding, gram_number s]
+    | `Number (s,_) -> [NoBinding, gram_number s]
   and aux_layout = function
     | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
     | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
@@ -321,9 +324,9 @@ let extract_term_production status pattern =
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
           | Ast.List0 (_, Some l) -> 
-              Gramext.Slist0sep (s, gram_of_literal status l)
+              Gramext.Slist0sep (s, gram_of_literal status l,true)
           | Ast.List1 (_, Some l) -> 
-              Gramext.Slist1sep (s, gram_of_literal status l)
+              Gramext.Slist1sep (s, gram_of_literal status l,true)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -528,9 +531,9 @@ EXTEND
         fun l -> List.map (fun x -> x l) p ] 
   ];
   literal: [
-    [ s = SYMBOL -> `Symbol s
-    | k = QKEYWORD -> `Keyword k
-    | n = NUMBER -> `Number n
+    [ s = SYMBOL -> `Symbol (s, (None,None))
+    | k = QKEYWORD -> `Keyword (k, (None,None))
+    | n = NUMBER -> `Number (n,(None,None))
     ]
   ];
   sep:       [ [ "sep";      sep = literal -> sep ] ];
@@ -672,10 +675,11 @@ END
   let term = grammars.term in
   let atag_attributes = grammars.sym_attributes in
   let let_defs = grammars.let_defs in
+  let let_codefs = grammars.let_codefs in
   let ident = grammars.ident in
   let protected_binder_vars = grammars.protected_binder_vars in
 EXTEND
-  GLOBAL: level2_ast term let_defs protected_binder_vars ident atag_attributes;
+  GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident atag_attributes;
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
@@ -724,10 +728,24 @@ EXTEND
          let uri,_ = CicNotationLexer.LocalizeEnv.find loc 
            !loctable in
          match uri with
-         | Some u -> id, `Uri u
-         | None -> id, `Ambiguous
+         | Some u -> 
+            prerr_endline ("trovata interpretazione per " ^ id ^ ": " ^ u);
+                         id, `Uri u
+         | None ->
+            prerr_endline ("identificatore ambiguo: " ^ id);
+                         id, `Ambiguous
+       with
+       | Not_found -> 
+            prerr_endline ("identificatore non trovato: " ^ id);
+                       id, `Ambiguous ]];
+  gnum: [
+    [ n = NUMBER ->
+       try
+         match CicNotationLexer.LocalizeEnv.find loc !loctable with
+         | _uri, Some interpr -> n, Some (Some "cic:/fakeuri.def(1)",interpr)
+         | _ -> n,None 
        with
-       | Not_found -> id, `Ambiguous ]];
+       | Not_found -> n,None ]];
   arg: [
     [ LPAREN; names = LIST1 gident SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN ->
@@ -782,7 +800,7 @@ EXTEND
                 (* CSC: new NCicPp.status is the best I can do here
                    without changing the return type *)
                 Ast.fail loc (sprintf "Argument %s not found"
-                  (NotationPp.pp_term (new NCicPp.status) name))
+                  (NotationPp.pp_term (new NCicPp.status None) name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -866,7 +884,7 @@ EXTEND
       | 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, None))
+      | (n,interpr) = gnum -> return_term loc (Ast.Num (n, interpr))
       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
       | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
@@ -924,6 +942,7 @@ let initial_grammars loctable keywords =
       [] initial_symbols
   in
   let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs" in
+  let let_codefs = Grammar.Entry.create level2_ast_grammar "let_codefs" in
   let protected_binder_vars = 
     Grammar.Entry.create level2_ast_grammar "protected_binder_vars" in
   let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in
@@ -935,6 +954,7 @@ let initial_grammars loctable keywords =
     sym_table=sym_table;
     sym_attributes=sym_attributes;
     let_defs=let_defs;
+    let_codefs=let_codefs;
     protected_binder_vars=protected_binder_vars;
     level2_meta=level2_meta;
     level2_ast_grammar=level2_ast_grammar;
@@ -961,9 +981,9 @@ class status0 ~keywords:kwds =
     db.loctable := CicNotationLexer.LocalizeEnv.empty
  end
 
-class virtual status ~keywords:kwds =
+class virtual status uid ~keywords:kwds =
  object
-  inherit NCic.status
+  inherit NCic.status uid
   inherit status0 kwds
  end
 
@@ -1011,6 +1031,7 @@ let level2_ast_grammar status =
   status#notation_parser_db.grammars.level2_ast_grammar
 let term status = status#notation_parser_db.grammars.term
 let let_defs status = status#notation_parser_db.grammars.let_defs
+let let_codefs status = status#notation_parser_db.grammars.let_codefs
 let protected_binder_vars status = 
   status#notation_parser_db.grammars.protected_binder_vars