+ (fun (id : string) (loc : Lexing.position * Lexing.position) ->
+ (Ast.TermVar id : 'l2_variable));
+ [Gramext.Stoken ("", "anonymous")],
+ Gramext.action
+ (fun _ (loc : Lexing.position * Lexing.position) ->
+ (Ast.TermVar "_" : 'l2_variable));
+ [Gramext.Stoken ("", "fresh"); Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+ (Ast.FreshVar id : 'l2_variable));
+ [Gramext.Stoken ("", "ident"); Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+ (Ast.IdentVar id : 'l2_variable));
+ [Gramext.Stoken ("", "number"); Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+ (Ast.NumVar id : 'l2_variable));
+ [Gramext.Stoken ("", "term"); Gramext.Stoken ("IDENT", "")],
+ Gramext.action
+ (fun (id : string) _ (loc : Lexing.position * Lexing.position) ->
+ (Ast.TermVar id : 'l2_variable))]];
+ Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e), None,
+ [None, None,
+ [[Gramext.Stoken ("", "fail")],
+ Gramext.action
+ (fun _ (loc : Lexing.position * Lexing.position) ->
+ (Ast.Fail : 'l2_magic));
+ [Gramext.Stoken ("", "if");
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+ Gramext.Stoken ("", "then");
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+ Gramext.Stoken ("", "else");
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
+ Gramext.action
+ (fun (p_false : 'level2_meta) _ (p_true : 'level2_meta) _
+ (p_test : 'level2_meta) _
+ (loc : Lexing.position * Lexing.position) ->
+ (Ast.If (p_test, p_true, p_false) : 'l2_magic));
+ [Gramext.Stoken ("", "default");
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
+ Gramext.action
+ (fun (none : 'level2_meta) (some : 'level2_meta) _
+ (loc : Lexing.position * Lexing.position) ->
+ (Ast.Default (some, none) : 'l2_magic));
+ [Gramext.Stoken ("", "fold");
+ Gramext.srules
+ [[Gramext.Stoken ("", "right")],
+ Gramext.action
+ (fun _ (loc : Lexing.position * Lexing.position) ->
+ (`Right : 'e__1));
+ [Gramext.Stoken ("", "left")],
+ Gramext.action
+ (fun _ (loc : Lexing.position * Lexing.position) ->
+ (`Left : 'e__1))];
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e));
+ Gramext.Stoken ("", "rec"); Gramext.Stoken ("IDENT", "");
+ Gramext.Snterm
+ (Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e))],
+ Gramext.action
+ (fun (recursive : 'level2_meta) (id : string) _
+ (base : 'level2_meta) (kind : 'e__1) _
+ (loc : Lexing.position * Lexing.position) ->
+ (Ast.Fold (kind, base, [id], recursive) : 'l2_magic))]];
+ Grammar.Entry.obj (level2_meta : 'level2_meta Grammar.Entry.e), None,
+ [None, None,
+ [[Gramext.Stoken ("UNPARSED_AST", "")],
+ Gramext.action
+ (fun (blob : string) (loc : Lexing.position * Lexing.position) ->
+ (!parse_level2_ast_ref (Ulexing.from_utf8_string blob) :
+ 'level2_meta));
+ [Gramext.Snterm
+ (Grammar.Entry.obj (l2_variable : 'l2_variable Grammar.Entry.e))],
+ Gramext.action
+ (fun (var : 'l2_variable)
+ (loc : Lexing.position * Lexing.position) ->
+ (Ast.Variable var : 'level2_meta));
+ [Gramext.Snterm
+ (Grammar.Entry.obj (l2_magic : 'l2_magic Grammar.Entry.e))],
+ Gramext.action
+ (fun (magic : 'l2_magic)
+ (loc : Lexing.position * Lexing.position) ->
+ (Ast.Magic magic : 'level2_meta))]]])
+(* }}} *)
+
+(* {{{ Grammar for ast patterns, notation level 2 *)
+let _ =
+ Grammar.extend
+ (let _ = (level2_ast : 'level2_ast Grammar.Entry.e)
+ and _ = (term : 'term Grammar.Entry.e)
+ and _ = (let_defs : 'let_defs Grammar.Entry.e) in
+ let grammar_entry_create s =
+ Grammar.Entry.create (Grammar.of_entry level2_ast) s
+ in
+ let sort : 'sort Grammar.Entry.e = grammar_entry_create "sort"
+ and explicit_subst : 'explicit_subst Grammar.Entry.e =
+ grammar_entry_create "explicit_subst"
+ and meta_subst : 'meta_subst Grammar.Entry.e =
+ grammar_entry_create "meta_subst"
+ and meta_substs : 'meta_substs Grammar.Entry.e =
+ grammar_entry_create "meta_substs"
+ and possibly_typed_name : 'possibly_typed_name Grammar.Entry.e =
+ grammar_entry_create "possibly_typed_name"
+ and match_pattern : 'match_pattern Grammar.Entry.e =
+ grammar_entry_create "match_pattern"
+ and binder : 'binder Grammar.Entry.e = grammar_entry_create "binder"
+ and arg : 'arg Grammar.Entry.e = grammar_entry_create "arg"
+ and single_arg : 'single_arg Grammar.Entry.e =
+ grammar_entry_create "single_arg"
+ and induction_kind : 'induction_kind Grammar.Entry.e =
+ grammar_entry_create "induction_kind"
+ and binder_vars : 'binder_vars Grammar.Entry.e =
+ grammar_entry_create "binder_vars"
+ in
+ [Grammar.Entry.obj (level2_ast : 'level2_ast Grammar.Entry.e), None,
+ [None, None,
+ [[Gramext.Snterm (Grammar.Entry.obj (term : 'term Grammar.Entry.e))],
+ Gramext.action
+ (fun (p : 'term) (loc : Lexing.position * Lexing.position) ->
+ (p : 'level2_ast))]];