It is now possible to pass a ${ident x} to another previously defined

notation that expects an ${ident y}.

diff --git a/matita/components/content/notationEnv.ml b/matita/components/content/notationEnv.ml
index e95b3ab51d8c29729840ebbf9a5b5702d9252e63..be9171a8d9318a714e16fd5ceffbc2a069099278 100644 (file)
--- a/matita/components/content/notationEnv.ml
+++ b/matita/components/content/notationEnv.ml
@@ -27,9 +27,13 @@
 
 module Ast = NotationPt
 
+type ident_or_var =
+   Ident of string
+ | Var of string
+
 type value =
   | TermValue of Ast.term
-  | StringValue of string
+  | StringValue of ident_or_var
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
@@ -103,12 +107,12 @@ let declaration_of_var = function
 
 let value_of_term = function
   | Ast.Num (s, _) -> NumValue s
-  | Ast.Ident (s, None) -> StringValue s
+  | Ast.Ident (s, None) -> StringValue (Var s)
   | t -> TermValue t
 
 let term_of_value = function
   | NumValue s -> Ast.Num (s, 0)
-  | StringValue s -> Ast.Ident (s, None)
+  | StringValue (Ident s) -> Ast.Ident (s, None)
   | TermValue t -> t
   | _ -> assert false (* TO BE UNDERSTOOD *)
 

diff --git a/matita/components/content/notationEnv.mli b/matita/components/content/notationEnv.mli
index 858af233c45a2345e05ad7944ea041daca012a5b..372bc15e821b4aec68045a062c3cb8683aa131e7 100644 (file)
--- a/matita/components/content/notationEnv.mli
+++ b/matita/components/content/notationEnv.mli
@@ -25,9 +25,13 @@
 
 (** {2 Types} *)
 
+type ident_or_var =
+   Ident of string
+ | Var of string
+
 type value =
   | TermValue of NotationPt.term
-  | StringValue of string
+  | StringValue of ident_or_var
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
@@ -66,7 +70,7 @@ val lookup_value:   t -> string -> value  (** @raise Value_not_found *)
 (** lookup_* functions below may raise Value_not_found and Type_mismatch *)
 
 val lookup_term:    t -> string -> NotationPt.term
-val lookup_string:  t -> string -> string
+val lookup_string:  t -> string -> ident_or_var
 val lookup_num:     t -> string -> string
 val lookup_opt:     t -> string -> value option
 val lookup_list:    t -> string -> value list

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index e9209d5154e1faf27474ed193f7120472ebf022f..b75192460135beeb4d2286c89ded2d0577af51c7 100644 (file)
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -325,7 +325,8 @@ let pp_obj pp_term = function
 
 let rec pp_value = function
   | Env.TermValue t -> sprintf "$%s$" (pp_term t)
-  | Env.StringValue s -> sprintf "\"%s\"" s
+  | Env.StringValue (Env.Ident s) -> sprintf "\"%s\"" s
+  | Env.StringValue (Env.Var s) -> sprintf "\"${ident %s}\"" s
   | Env.NumValue n -> n
   | Env.OptValue (Some v) -> "Some " ^ pp_value v
   | Env.OptValue None -> "None"

diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index 7379dd693e128b5c480298d7249b704047d322d2..a9b558968829d8692683a63c09b9f4910545bd3a 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
@@ -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 =
@@ -556,9 +560,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 +640,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;
@@ -779,6 +797,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 +805,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;
@@ -823,7 +843,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 = 

diff --git a/matita/components/content_pres/content2presMatcher.ml b/matita/components/content_pres/content2presMatcher.ml
index 2a432d33255eb35d94e7f59a91361ac2cda62c11..5316c92ee437eee8e6cae0f169e0506b1891ad57 100644 (file)
--- a/matita/components/content_pres/content2presMatcher.ml
+++ b/matita/components/content_pres/content2presMatcher.ml
@@ -101,7 +101,7 @@ struct
           | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
               name, (Env.NumType, Env.NumValue s)
           | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
-              name, (Env.StringType, Env.StringValue s)
+              name, (Env.StringType, Env.StringValue (Env.Ident s))
           | _ -> assert false)
         pl tl
     with Invalid_argument _ -> assert false

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index 6b0d9d0c8595c4ade106306369efb9acc20e9389..b9abb44183389782a7e463eaeacf0801751010f5 100644 (file)
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -575,6 +575,7 @@ let tail_names names env =
 
 let instantiate_level2 env term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
+prerr_endline ("istanzio: " ^ NotationPp.pp_term term);
   let fresh_env = ref [] in
   let lookup_fresh_name n =
     try
@@ -584,8 +585,9 @@ let instantiate_level2 env term =
       fresh_env := (n, new_name) :: !fresh_env;
       new_name
   in
+prerr_endline ("ENV " ^ NotationPp.pp_env env);
   let rec aux env term =
-(*    prerr_endline ("ENV " ^ NotationPp.pp_env env); *)
+prerr_endline ("istanzio_deep: " ^ NotationPp.pp_term term);
     match term with
     | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
@@ -637,7 +639,10 @@ let instantiate_level2 env term =
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
-    | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
+    | Ast.IdentVar name ->
+       (match Env.lookup_string env name with
+           Env.Ident x -> Ast.Ident (x, None)
+         | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)