X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=00ac411fa51cb24cc5c6bd94da715babcbd36a4e;hb=db63f65c35efaa93d0a2cc00a194549e791975c9;hp=829e78b6d0d16476e4e73a968436c2774ec523b5;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml index 829e78b6d..00ac411fa 100644 --- a/matita/components/content_pres/cicNotationParser.ml +++ b/matita/components/content_pres/cicNotationParser.ml @@ -27,8 +27,8 @@ open Printf -module Ast = CicNotationPt -module Env = CicNotationEnv +module Ast = NotationPt +module Env = NotationEnv exception Parse_error of string exception Level_not_found of int @@ -36,42 +36,41 @@ 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; + let_codefs: 'c Grammar.Entry.e; protected_binder_vars: 'd Grammar.Entry.e; level2_meta: 'b Grammar.Entry.e; } -let initial_grammars () = - let level1_pattern_grammar = - Grammar.gcreate (CicNotationLexer.level1_pattern_lexer ()) in - let level2_ast_grammar = - Grammar.gcreate (CicNotationLexer.level2_ast_lexer ()) in - let level2_meta_grammar = - Grammar.gcreate (CicNotationLexer.level2_meta_lexer ()) in - let level1_pattern = - 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 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 - let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta" in - { level1_pattern=level1_pattern; - level2_ast=level2_ast; - term=term; - let_defs=let_defs; - protected_binder_vars=protected_binder_vars; - level2_meta=level2_meta; - level2_ast_grammar=level2_ast_grammar; -} -;; +type checked_l1_pattern = CL1P of NotationPt.term * int + +let refresh_uri_in_checked_l1_pattern ~refresh_uri_in_term + ~refresh_uri_in_reference (CL1P (t,n)) += + CL1P (NotationUtil.refresh_uri_in_term ~refresh_uri_in_term + ~refresh_uri_in_reference t, n) + +type binding = + | NoBinding + | Binding of string * Env.value_type + | Env of (string * Env.value_type) list -let grammars = ref (initial_grammars ());; +type db = { + grammars: + (int -> NotationPt.term, + Ast.term, + (Ast.term Ast.capture_variable list * + Ast.term Ast.capture_variable * Ast.term * int) list, + 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 +} let int_of_string s = try @@ -87,14 +86,18 @@ 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 = function +let gram_term status = function | Ast.Self _ -> Gramext.Sself | Ast.Level precedence -> Gramext.Snterml - (Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e), + (Grammar.Entry.obj + (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e), level_of precedence) ;; @@ -104,13 +107,8 @@ let gram_of_literal = | `Keyword s -> gram_keyword s | `Number s -> gram_number s -type binding = - | NoBinding - | Binding of string * Env.value_type - | Env of (string * Env.value_type) list - let make_action action bindings = - let rec aux (vl : CicNotationEnv.t) = + let rec aux (vl : NotationEnv.t) = function [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc) | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl) @@ -121,7 +119,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 @@ -136,7 +134,7 @@ let make_action action bindings = (fun (v:'a list) -> aux ((name, (Env.ListType t, Env.ListValue v)) :: vl) tl) | Env _ :: tl -> - Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl) + Gramext.action (fun (v:NotationEnv.t) -> aux (v @ vl) tl) (* LUCA: DEFCON 3 END *) in aux [] (List.rev bindings) @@ -152,7 +150,7 @@ let flatten_opt = aux [] (* given a level 1 pattern computes the new RHS of "term" grammar entry *) -let extract_term_production pattern = +let extract_term_production status pattern = let rec aux = function | Ast.AttributedTerm (_, t) -> aux t | Ast.Literal l -> aux_literal l @@ -160,7 +158,7 @@ let extract_term_production pattern = | Ast.Magic m -> aux_magic m | Ast.Variable v -> aux_variable v | t -> - prerr_endline (CicNotationPp.pp_term t); + prerr_endline (NotationPp.pp_term status t); assert false and aux_literal = function @@ -192,7 +190,7 @@ let extract_term_production pattern = match magic with | Ast.Opt p -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_opt : CicNotationEnv.t option) (loc : Ast.location) = + let action (env_opt : NotationEnv.t option) (loc : Ast.location) = match env_opt with | Some env -> List.map Env.opt_binding_some env | None -> List.map Env.opt_binding_of_name p_names @@ -204,13 +202,15 @@ let extract_term_production pattern = | Ast.List0 (p, _) | Ast.List1 (p, _) -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_list : CicNotationEnv.t list) (loc : Ast.location) = - CicNotationEnv.coalesce_env p_names env_list + let action (env_list : NotationEnv.t list) (loc : Ast.location) = + NotationEnv.coalesce_env p_names env_list in let gram_of_list s = match magic with | Ast.List0 (_, None) -> Gramext.Slist0 s | Ast.List1 (_, None) -> Gramext.Slist1 s +(* | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false) + | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)*) | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l) | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l) | _ -> assert false @@ -224,15 +224,15 @@ let extract_term_production pattern = function | 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 lv] - | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""] + [Binding (s, Env.TermType level), gram_term status lv] + | 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 = let p_bindings, p_atoms = List.split (aux p) in let p_names = flatten_opt p_bindings in let action = - make_action (fun (env : CicNotationEnv.t) (loc : Ast.location) -> env) + make_action (fun (env : NotationEnv.t) (loc : Ast.location) -> env) p_bindings in p_bindings, p_atoms, p_names, action @@ -252,11 +252,6 @@ let compare_rule_id x y = in aux (x,y) - (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *) -let initial_owned_keywords () = Hashtbl.create 23 -let owned_keywords = ref (initial_owned_keywords ()) - -type checked_l1_pattern = CL1P of CicNotationPt.term * int let check_l1_pattern level1_pattern pponly level associativity = let variables = ref 0 in @@ -328,50 +323,15 @@ let check_l1_pattern level1_pattern pponly level associativity = raise (Parse_error ("You can not specify an associative notation " ^ "at level "^string_of_int min_precedence ^ "; increase it")); let cp = aux level1_pattern in -(* prerr_endline ("checked_pattern: " ^ CicNotationPp.pp_term cp); *) +(* prerr_endline ("checked_pattern: " ^ NotationPp.pp_term cp); *) if !variables <> 2 && associativity <> Gramext.NonA then raise (Parse_error ("Exactly 2 variables must be specified in an "^ "associative notation")); CL1P (cp,level) ;; -let extend (CL1P (level1_pattern,precedence)) action = - let p_bindings, p_atoms = - List.split (extract_term_production level1_pattern) - in - let level = level_of precedence in - let _ = - Grammar.extend - [ Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e), - Some (Gramext.Level level), - [ None, - Some (*Gramext.NonA*) Gramext.NonA, - [ p_atoms, - (make_action - (fun (env: CicNotationEnv.t) (loc: Ast.location) -> - (action env loc)) - p_bindings) ]]] - in - let keywords = CicNotationUtil.keywords_of_term level1_pattern in - let rule_id = p_atoms in - List.iter CicNotationLexer.add_level2_ast_keyword keywords; - Hashtbl.add !owned_keywords rule_id keywords; (* keywords may be [] *) - rule_id - -let delete rule_id = - let atoms = rule_id in - (try - let keywords = Hashtbl.find !owned_keywords rule_id in - List.iter CicNotationLexer.remove_level2_ast_keyword keywords - with Not_found -> assert false); - Grammar.delete_rule !grammars.term atoms - (** {2 Grammar} *) -let parse_level1_pattern_ref = ref (fun _ _ -> assert false) -let parse_level2_ast_ref = ref (fun _ -> assert false) -let parse_level2_meta_ref = ref (fun _ -> assert false) - let fold_cluster binder terms ty body = List.fold_right (fun term body -> Ast.Binder (binder, (term, ty), body)) @@ -393,8 +353,33 @@ let return_term loc term = Ast.AttributedTerm (`Loc loc, term) let return_term_of_level loc term l = Ast.AttributedTerm (`Loc loc, term l) +(** {2 API implementation} *) + +let exc_located_wrapper f = + try + f () + with + | Stdpp.Exc_located (floc, Stream.Error msg) -> + raise (HExtlib.Localized (floc, Parse_error msg)) + | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) -> + raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) + | Stdpp.Exc_located (floc, exn) -> + raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) + +let parse_level1_pattern grammars precedence lexbuf = + exc_located_wrapper + (fun () -> Grammar.Entry.parse grammars.level1_pattern (Obj.magic lexbuf) precedence) + +let parse_level2_ast grammars lexbuf = + exc_located_wrapper + (fun () -> Grammar.Entry.parse grammars.level2_ast (Obj.magic lexbuf)) + +let parse_level2_meta grammars lexbuf = + exc_located_wrapper + (fun () -> Grammar.Entry.parse grammars.level2_meta (Obj.magic lexbuf)) + (* create empty precedence level for "term" *) -let initialize_grammars () = +let initialize_grammars grammars = let dummy_action = Gramext.action (fun _ -> failwith "internal error, lexer generated a dummy token") @@ -414,17 +399,17 @@ let initialize_grammars () = aux [] last in Grammar.extend - [ Grammar.Entry.obj (!grammars.term: 'a Grammar.Entry.e), + [ Grammar.Entry.obj (grammars.term: 'a Grammar.Entry.e), None, mk_level_list min_precedence max_precedence ]; (* {{{ Grammar for concrete syntax patterns, notation level 1 *) begin - let level1_pattern = !grammars.level1_pattern in + let level1_pattern = grammars.level1_pattern in EXTEND GLOBAL: level1_pattern; level1_pattern: [ - [ p = l1_pattern; EOI -> fun l -> CicNotationUtil.boxify (p l) ] + [ p = l1_pattern; EOI -> fun l -> NotationUtil.boxify (p l) ] ]; l1_pattern: [ [ p = LIST1 l1_simple_pattern -> @@ -513,9 +498,9 @@ EXTEND | "maction"; m = LIST1 [ LPAREN; l = l1_pattern; RPAREN -> l ] -> return_term_of_level loc (fun l -> Ast.Layout (Ast.Maction (List.map (fun x -> - CicNotationUtil.group (x l)) m))) + NotationUtil.group (x l)) m))) | LPAREN; p = l1_pattern; RPAREN -> - return_term_of_level loc (fun l -> CicNotationUtil.group (p l)) + return_term_of_level loc (fun l -> NotationUtil.group (p l)) ] | "simple" NONA [ i = IDENT -> @@ -533,7 +518,7 @@ EXTEND (* }}} *) (* {{{ Grammar for ast magics, notation level 2 *) begin - let level2_meta = !grammars.level2_meta in + let level2_meta = grammars.level2_meta in EXTEND GLOBAL: level2_meta; l2_variable: [ @@ -563,7 +548,7 @@ EXTEND [ magic = l2_magic -> Ast.Magic magic | var = l2_variable -> Ast.Variable var | blob = UNPARSED_AST -> - !parse_level2_ast_ref (Ulexing.from_utf8_string blob) + parse_level2_ast grammars (Ulexing.from_utf8_string blob) ] ]; END @@ -571,20 +556,20 @@ END (* }}} *) (* {{{ Grammar for ast patterns, notation level 2 *) begin - let level2_ast = !grammars.level2_ast in - let term = !grammars.term in - let let_defs = !grammars.let_defs in - let protected_binder_vars = !grammars.protected_binder_vars in + let level2_ast = grammars.level2_ast in + let term = grammars.term 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; + GLOBAL: level2_ast term let_defs let_codefs protected_binder_vars ident; level2_ast: [ [ p = term -> p ] ]; sort: [ [ "Prop" -> `Prop | "Set" -> `Set | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n - | "Type" -> `Type (CicUniv.fresh ()) | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n - | "CProp" -> `CProp (CicUniv.fresh ()) ] ]; explicit_subst: [ @@ -637,7 +622,7 @@ EXTEND List.map (fun n -> Ast.Ident (n, None)) names, Some ty | name = IDENT -> [Ast.Ident (name, None)], None | blob = UNPARSED_META -> - let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in + let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) -> [meta], None | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None @@ -647,7 +632,7 @@ EXTEND single_arg: [ [ name = IDENT -> Ast.Ident (name, None) | blob = UNPARSED_META -> - let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in + let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in match meta with | Ast.Variable (Ast.FreshVar _) | Ast.Variable (Ast.IdentVar _) -> meta @@ -655,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; @@ -669,8 +667,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" - (CicNotationPp.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 @@ -692,6 +692,23 @@ EXTEND defs ] ]; + let_codefs: [ + [ defs = LIST1 [ + name = single_arg; + args = LIST0 arg; + ty = OPT [ SYMBOL ":" ; p = term -> p ]; + SYMBOL <:unicode> (* ≝ *); body = term -> + let args = + List.concat + (List.map + (function (names,ty) -> List.map (function x -> x,ty) names + ) args) + in + args, (name, ty), body, 0 + ] SEP "and" -> + defs + ] + ]; binder_vars: [ [ vars = [ l = [ l = LIST1 single_arg SEP SYMBOL "," -> l @@ -721,12 +738,6 @@ EXTEND SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) - | LETCOREC; defs = let_defs; "in"; - body = term -> - return_term loc (Ast.LetRec (`CoInductive, defs, body)) - | LETREC; defs = let_defs; "in"; - body = term -> - return_term loc (Ast.LetRec (`Inductive, defs, body)) ] ]; term: LEVEL "20" @@ -778,80 +789,117 @@ EXTEND return_term loc (Ast.Cast (p1, p2)) | LPAREN; p = term; RPAREN -> p | blob = UNPARSED_META -> - !parse_level2_meta_ref (Ulexing.from_utf8_string blob) + parse_level2_meta grammars (Ulexing.from_utf8_string blob) ] ]; END - end + end; (* }}} *) + grammars ;; -let _ = initialize_grammars ();; - -let history = ref [];; - -let push () = - CicNotationLexer.push (); - history := (!owned_keywords,!grammars) :: !history; - owned_keywords := (initial_owned_keywords ()); - grammars := initial_grammars (); - initialize_grammars () +let initial_grammars keywords = + let lexers = CicNotationLexer.mk_lexers keywords in + let level1_pattern_grammar = + Grammar.gcreate lexers.CicNotationLexer.level1_pattern_lexer in + let level2_ast_grammar = + Grammar.gcreate lexers.CicNotationLexer.level2_ast_lexer in + let level2_meta_grammar = + Grammar.gcreate lexers.CicNotationLexer.level2_meta_lexer in + let level1_pattern = + 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 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 + initialize_grammars { level1_pattern=level1_pattern; + level2_ast=level2_ast; + term=term; + ident=ident; + let_defs=let_defs; + let_codefs=let_codefs; + protected_binder_vars=protected_binder_vars; + level2_meta=level2_meta; + level2_ast_grammar=level2_ast_grammar; + } ;; -let pop () = - CicNotationLexer.pop (); - match !history with - | [] -> assert false - | (kw,gram) :: old_history -> - owned_keywords := kw; - grammars := gram; - history := old_history +class type g_status = + object + method notation_parser_db: db + end + +class status0 ~keywords:kwds = + object + val db = { grammars = initial_grammars kwds; keywords = kwds; items = [] } + method notation_parser_db = db + method set_notation_parser_db v = {< db = v >} + method set_notation_parser_status + : 'status. #g_status as 'status -> 'self + = 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) = + let p_bindings, p_atoms = + List.split (extract_term_production status level1_pattern) in + Grammar.extend + [ Grammar.Entry.obj + (status#notation_parser_db.grammars.term : 'a Grammar.Entry.e), + Some (Gramext.Level level), + [ None, + Some (*Gramext.NonA*) Gramext.NonA, + [ p_atoms, + (make_action + (fun (env: NotationEnv.t) (loc: Ast.location) -> + (action env loc)) + p_bindings) ]]]; + status + in + let current_item = + let level = level_of precedence in + level, level1_pattern, action in + 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 status0 ~keywords) in + let status = status#set_notation_parser_db + {status#notation_parser_db with items = items} in + List.fold_left add1item status items ;; -(** {2 API implementation} *) - -let exc_located_wrapper f = - try - f () - with - | Stdpp.Exc_located (floc, Stream.Error msg) -> - raise (HExtlib.Localized (floc, Parse_error msg)) - | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) -> - raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) - | Stdpp.Exc_located (floc, exn) -> - raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) - -let parse_level1_pattern precedence lexbuf = - exc_located_wrapper - (fun () -> Grammar.Entry.parse !grammars.level1_pattern (Obj.magic lexbuf) precedence) - -let parse_level2_ast lexbuf = - exc_located_wrapper - (fun () -> Grammar.Entry.parse !grammars.level2_ast (Obj.magic lexbuf)) - -let parse_level2_meta lexbuf = - exc_located_wrapper - (fun () -> Grammar.Entry.parse !grammars.level2_meta (Obj.magic lexbuf)) - -let _ = - parse_level1_pattern_ref := parse_level1_pattern; - parse_level2_ast_ref := parse_level2_ast; - parse_level2_meta_ref := parse_level2_meta - -let parse_term lexbuf = - exc_located_wrapper - (fun () -> (Grammar.Entry.parse !grammars.term (Obj.magic lexbuf))) -let level2_ast_grammar () = !grammars.level2_ast_grammar -let term () = !grammars.term -let let_defs () = !grammars.let_defs -let protected_binder_vars () = !grammars.protected_binder_vars +let parse_level1_pattern status = + parse_level1_pattern status#notation_parser_db.grammars +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 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 (** {2 Debugging} *) -let print_l2_pattern () = - Grammar.print_entry Format.std_formatter (Grammar.Entry.obj !grammars.term); +let print_l2_pattern status = + Grammar.print_entry Format.std_formatter + (Grammar.Entry.obj status#notation_parser_db.grammars.term); Format.pp_print_flush Format.std_formatter (); flush stdout