+
+
+EXTEND
+ GLOBAL: level2_meta;
+ l2_variable: [
+ [ "term"; id = IDENT -> TermVar id
+ | "number"; id = IDENT -> NumVar id
+ | "ident"; id = IDENT -> IdentVar id
+ | "fresh"; id = IDENT -> FreshVar id
+ | "anonymous" -> TermVar "_"
+ | id = IDENT -> TermVar id
+ ]
+ ];
+ l2_magic: [
+ [ "fold"; kind = [ "left" -> `Left | "right" -> `Right ];
+ base = level2_meta; "rec"; id = IDENT; recursive = level2_meta ->
+ Fold (kind, base, [id], recursive)
+ | "default"; some = level2_meta; none = level2_meta -> Default (some, none)
+ | "if"; p_test = level2_meta;
+ "then"; p_true = level2_meta;
+ "else"; p_false = level2_meta ->
+ If (p_test, p_true, p_false)
+ | "fail" -> Fail
+ ]
+ ];
+ level2_meta: [
+ [ magic = l2_magic -> Magic magic
+ | var = l2_variable -> Variable var
+ | blob = UNPARSED_AST -> !parse_level2_ast_ref (Stream.of_string blob)
+ ]
+ ];
+END
+
+EXTEND
+ GLOBAL: level2_ast term
+ level3_term
+ notation interpretation
+ phrase;