HUGE COMMIT:

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

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 7379dd693e128b5c480298d7249b704047d322d2..53c60820c78632bd58f3b8527d697897537c92ff 100644 (file)
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -36,11 +36,12 @@ exception Level_not_found of int
 let min_precedence = 0
 let max_precedence = 100
 
-type ('a,'b,'c,'d) grammars = {
+type ('a,'b,'c,'d,'e) grammars = {
   level1_pattern: 'a Grammar.Entry.e;
   level2_ast: 'b Grammar.Entry.e;
   level2_ast_grammar : Grammar.g;
   term: 'b Grammar.Entry.e;
+  ident: 'e Grammar.Entry.e;
   let_defs: 'c Grammar.Entry.e;
   protected_binder_vars: 'd Grammar.Entry.e;
   level2_meta: 'b Grammar.Entry.e;
@@ -65,7 +66,7 @@ type db = {
     Ast.term,
     (Ast.term Ast.capture_variable list *
       Ast.term Ast.capture_variable * Ast.term * int) list, 
-    Ast.term list * Ast.term option) grammars;
+    Ast.term list * Ast.term option, Env.ident_or_var) grammars;
   keywords: string list;
   items: (string * Ast.term * (NotationEnv.t -> Ast.location -> Ast.term)) list
 }
@@ -84,7 +85,10 @@ let level_of precedence =
   string_of_int precedence 
 
 let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
-let gram_ident s = Gramext.Stoken ("IDENT", s)
+let gram_ident status =
+ Gramext.Snterm (Grammar.Entry.obj
+  (status#notation_parser_db.grammars.ident : 'a Grammar.Entry.e))
+  (*Gramext.Stoken ("IDENT", s)*)
 let gram_number s = Gramext.Stoken ("NUMBER", s)
 let gram_keyword s = Gramext.Stoken ("", s)
 let gram_term status = function
@@ -114,7 +118,7 @@ let make_action action bindings =
             aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
     | Binding (name, Env.StringType) :: tl ->
         Gramext.action
-          (fun (v:string) ->
+          (fun (v:Env.ident_or_var) ->
             aux ((name, (Env.StringType, Env.StringValue v)) :: vl) tl)
     | Binding (name, Env.NumType) :: tl ->
         Gramext.action
@@ -153,7 +157,7 @@ let extract_term_production status pattern =
     | Ast.Magic m -> aux_magic m
     | Ast.Variable v -> aux_variable v
     | t ->
-        prerr_endline (NotationPp.pp_term t);
+        prerr_endline (NotationPp.pp_term status t);
         assert false
   and aux_literal =
     function
@@ -218,7 +222,7 @@ let extract_term_production status pattern =
     | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
     | Ast.TermVar (s,(Ast.Self level|Ast.Level level as lv)) -> 
         [Binding (s, Env.TermType level), gram_term status lv]
-    | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
+    | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident status]
     | Ast.Ascription (p, s) -> assert false (* TODO *)
     | Ast.FreshVar _ -> assert false
   and inner_pattern p =
@@ -371,10 +375,6 @@ let parse_level2_meta grammars lexbuf =
   exc_located_wrapper
     (fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf))
 
-let parse_term grammars lexbuf =
-  exc_located_wrapper
-    (fun () -> (Grammar.Entry.parse grammars.term (Obj.magic lexbuf)))
-
   (* create empty precedence level for "term" *)
 let initialize_grammars grammars =
   let dummy_action =
@@ -556,9 +556,10 @@ END
   let level2_ast = grammars.level2_ast in
   let term = grammars.term in
   let let_defs = grammars.let_defs 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;
+  GLOBAL: level2_ast term let_defs protected_binder_vars ident;
   level2_ast: [ [ p = term -> p ] ];
   sort: [
     [ "Prop" -> `Prop
@@ -635,6 +636,19 @@ EXTEND
         | _ -> failwith "Invalid index name."
     ]
   ];
+  ident: [
+    [ name = IDENT -> Env.Ident name
+    | blob = UNPARSED_META ->
+        let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
+        match meta with
+        | Ast.Variable (Ast.FreshVar _) ->
+           (* it makes sense: extend Env.ident_or_var *)
+            assert false
+        | Ast.Variable (Ast.IdentVar name) -> Env.Var name
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Env.Var "_"
+        | _ -> failwith ("Invalid index name: " ^ blob)
+    ]
+  ];
   let_defs: [
     [ defs = LIST1 [
         name = single_arg;
@@ -649,8 +663,10 @@ EXTEND
           in
           let rec find_arg name n = function 
             | [] ->
+                (* 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 name))
+                  (NotationPp.pp_term (new NCicPp.status) name))
             | (l,_) :: tl -> 
                 (match position_of name 0 l with
                 | None, len -> find_arg name (n + len) tl
@@ -779,6 +795,7 @@ let initial_grammars keywords =
     Grammar.Entry.create level1_pattern_grammar "level1_pattern" in
   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 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
@@ -786,6 +803,7 @@ let initial_grammars keywords =
   initialize_grammars { level1_pattern=level1_pattern;
     level2_ast=level2_ast;
     term=term;
+    ident=ident;
     let_defs=let_defs;
     protected_binder_vars=protected_binder_vars;
     level2_meta=level2_meta;
@@ -798,7 +816,7 @@ class type g_status =
   method notation_parser_db: db
  end
 
-class status ~keywords:kwds =
+class status0 ~keywords:kwds =
  object
   val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] }
   method notation_parser_db = db
@@ -808,6 +826,12 @@ class status ~keywords:kwds =
    = fun o -> {< db = o#notation_parser_db >}
  end
 
+class virtual status ~keywords:kwds =
+ object
+  inherit NCic.status
+  inherit status0 kwds
+ end
+
 let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         (* move inside constructor XXX *)
   let add1item status (level, level1_pattern, action) =
@@ -823,7 +847,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
             (make_action
               (fun (env: NotationEnv.t) (loc: Ast.location) ->
                 (action env loc))
-            p_bindings) ]]];
+              p_bindings) ]]];
     status
   in
   let current_item = 
@@ -832,7 +856,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
   let keywords = NotationUtil.keywords_of_term level1_pattern @
     status#notation_parser_db.keywords in
   let items = current_item :: status#notation_parser_db.items in 
-  let status = status#set_notation_parser_status (new status ~keywords) in
+  let status = status#set_notation_parser_status (new status0 ~keywords) in
   let status = status#set_notation_parser_db 
     {status#notation_parser_db with items = items} in
   List.fold_left add1item status items
@@ -845,8 +869,6 @@ let parse_level2_ast status =
   parse_level2_ast status#notation_parser_db.grammars 
 let parse_level2_meta status =
   parse_level2_meta status#notation_parser_db.grammars
-let parse_term status =
-  parse_term status#notation_parser_db.grammars
 
 let level2_ast_grammar status = 
   status#notation_parser_db.grammars.level2_ast_grammar