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
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)
-let grammars = ref (initial_grammars ());;
+type binding =
+ | NoBinding
+ | Binding of string * Env.value_type
+ | Env of (string * Env.value_type) list
+
+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
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)
;;
| `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)
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
(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)
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
| 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
and aux_magic magic =
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 _p_bindings, p_atoms, p_names, p_action = inner_pattern p in
+ 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
| 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)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
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
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
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))
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
+ | Ploc.Exc (floc, Stream.Error msg) ->
+ raise (HExtlib.Localized (floc, Parse_error msg))
+ | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
+ raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
+ | Ploc.Exc (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")
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 ->
| "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 ->
(* }}} *)
(* {{{ 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: [
[ 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
(* }}} *)
(* {{{ 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: [
];
arg: [
[ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
- SYMBOL ":"; ty = term; RPAREN ->
+ typ = OPT [ SYMBOL ":"; typ = term -> typ] ; RPAREN -> (* FG: now type is optional *)
+ let ty = match typ with Some ty -> ty | None -> Ast.Implicit `JustOne in
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
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
| _ -> 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;
args = LIST1 arg;
index_name = OPT [ "on"; id = single_arg -> id ];
ty = OPT [ SYMBOL ":" ; p = term -> p ];
- SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
let rec position_of name p = function
| [] -> None, p
| n :: _ when n = name -> Some p, p
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
defs
]
];
+ let_codefs: [
+ [ defs = LIST1 [
+ name = single_arg;
+ args = LIST0 arg;
+ ty = OPT [ SYMBOL ":" ; p = term -> p ];
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
+ 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
SYMBOL <:unicode<def>> (* ≝ *);
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"
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
projects / helm.git / blobdiff