From fb6fee82bb9172e15b1a7bc7e20641627f593fcc Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 3 Dec 2010 13:12:29 +0000 Subject: [PATCH] It is now possible to pass a ${ident x} to another previously defined notation that expects an ${ident y}. --- matita/components/content/notationEnv.ml | 10 ++++-- matita/components/content/notationEnv.mli | 8 +++-- matita/components/content/notationPp.ml | 3 +- .../content_pres/cicNotationParser.ml | 34 +++++++++++++++---- .../content_pres/content2presMatcher.ml | 2 +- .../content_pres/termContentPres.ml | 9 +++-- 6 files changed, 50 insertions(+), 16 deletions(-) diff --git a/matita/components/content/notationEnv.ml b/matita/components/content/notationEnv.ml index e95b3ab51..be9171a8d 100644 --- 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 858af233c..372bc15e8 100644 --- 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 e9209d515..b75192460 100644 --- 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 7379dd693..a9b558968 100644 --- 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 2a432d332..5316c92ee 100644 --- 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 6b0d9d0c8..b9abb4418 100644 --- 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) -- 2.39.2