+ level2_pattern: [ [ p = l2_pattern -> p ] ];
+ sort: [
+ [ SYMBOL "\\PROP" -> `Prop
+ | SYMBOL "\\SET" -> `Set
+ | SYMBOL "\\TYPE" -> `Type
+ ]
+ ];
+ explicit_subst: [
+ [ SYMBOL "\\subst"; (* to avoid catching frequent "a [1]" cases *)
+ SYMBOL "[";
+ substs = LIST1 [
+ i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = l2_pattern -> (i, t)
+ ] SEP SYMBOL ";";
+ SYMBOL "]" ->
+ substs
+ ]
+ ];
+ meta_subst: [
+ [ s = SYMBOL "_" -> None
+ | p = l2_pattern -> Some p ]
+ ];
+ meta_substs: [
+ [ SYMBOL "["; substs = LIST0 meta_subst; SYMBOL "]" -> substs ]
+ ];
+ possibly_typed_name: [
+ [ SYMBOL "("; id = bound_name; SYMBOL ":"; typ = l2_pattern; SYMBOL ")" ->
+ id, Some typ
+ | id = bound_name -> id, None
+ ]
+ ];
+ match_pattern: [
+ [ id = IDENT -> id, []
+ | SYMBOL "("; id = IDENT; vars = LIST1 possibly_typed_name; SYMBOL ")" ->
+ id, vars
+ ]
+ ];
+ binder: [
+ [ SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
+ | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
+ | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall
+ | SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
+ ]
+ ];
+ bound_name: [
+ [ i = IDENT -> Ident (i, None)
+ | SYMBOL "\\FRESH"; i = IDENT -> Variable (FreshVar i)
+ ]
+ ];
+ bound_names: [
+ [ vars = LIST1 bound_name SEP SYMBOL ",";
+ ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ] ->
+ [ vars, ty ]
+ | clusters = LIST1 [
+ SYMBOL "(";
+ vars = LIST1 bound_name SEP SYMBOL ",";
+ ty = OPT [ SYMBOL ":"; p = l2_pattern -> p ];
+ SYMBOL ")" ->
+ vars, ty
+ ] ->
+ clusters
+ ]
+ ];
+ induction_kind: [
+ [ IDENT "rec" -> `Inductive
+ | IDENT "corec" -> `CoInductive
+ ]
+ ];
+ let_defs: [
+ [ defs = LIST1 [
+ name = bound_name; args = bound_names;
+ index_name = OPT [ IDENT "on"; id = bound_name -> id ];
+ ty = OPT [ SYMBOL ":" ; p = l2_pattern -> p ];
+ SYMBOL <:unicode<def>> (* ≝ *); body = l2_pattern ->
+ let body = fold_binder `Lambda args body in
+ let ty =
+ match ty with
+ | None -> None
+ | Some ty -> Some (fold_binder `Pi args ty)
+ in
+ let rec position_of name p = function
+ | [] -> None, p
+ | n :: _ when n = name -> Some p, p
+ | _ :: tl -> position_of name (p + 1) tl
+ in
+ let rec find_arg name n = function
+ | [] ->
+ fail loc (sprintf "Argument %s not found"
+ (CicNotationPp.pp_term name))
+ | (l,_) :: tl ->
+ (match position_of name 0 l with
+ | None, len -> find_arg name (n + len) tl
+ | Some where, len -> n + where)
+ in
+ let index =
+ match index_name with
+ | None -> 0
+ | Some name -> find_arg name 0 args
+ in
+ (name, ty), body, index
+ ] SEP IDENT "and" ->
+ defs
+ ]
+ ];
+ l2_pattern_variable: [
+ [ SYMBOL "\\TERM"; id = IDENT -> TermVar id
+ | SYMBOL "\\NUM"; id = IDENT -> NumVar id
+ | SYMBOL "\\IDENT"; id = IDENT -> IdentVar id
+ | SYMBOL "\\FRESH"; id = IDENT -> FreshVar id
+ ]
+ ];
+ l2_magic_pattern: [
+ [ SYMBOL "\\FOLD";
+ kind = [ IDENT "left" -> `Left | IDENT "right" -> `Right ];
+ DELIM "\\["; base = l2_pattern; DELIM "\\]";
+ SYMBOL "\\LAMBDA"; id = IDENT;
+ DELIM "\\["; recursive = l2_pattern; DELIM "\\]" ->
+ Fold (kind, base, [id], recursive)
+ | SYMBOL "\\DEFAULT";
+ DELIM "\\["; some = l2_pattern; DELIM "\\]";
+ DELIM "\\["; none = l2_pattern; DELIM "\\]" ->
+ Default (some, none)
+ ]
+ ];
+ l2_pattern: LEVEL "10" (* let in *)
+ [ "10" NONA
+ [ IDENT "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+ p1 = l2_pattern; "in"; p2 = l2_pattern ->
+ return_term loc (LetIn (var, p1, p2))
+ | IDENT "let"; k = induction_kind; defs = let_defs; IDENT "in";
+ body = l2_pattern ->
+ return_term loc (LetRec (k, defs, body))
+ ]
+ ];
+ l2_pattern: LEVEL "20" (* binder *)
+ [ "20" RIGHTA
+ [ b = binder; names = bound_names; SYMBOL "."; body = l2_pattern ->
+ return_term loc (fold_binder b names body)
+ ]
+ ];
+ l2_pattern: LEVEL "70" (* apply *)
+ [ "70" LEFTA
+ [ p1 = l2_pattern; p2 = l2_pattern ->
+ let rec aux = function
+ | Appl (hd :: tl)
+ | AttributedTerm (_, Appl (hd :: tl)) ->
+ aux hd @ tl
+ | term -> [term]
+ in
+ return_term loc (Appl (aux p1 @ [p2]))
+ ]
+ ];
+ l2_pattern: LEVEL "90" (* simple *)
+ [ "90" NONA
+ [ id = IDENT -> return_term loc (Ident (id, None))
+ | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
+ | s = CSYMBOL -> return_term loc (Symbol (s, 0))
+ | u = URI -> return_term loc (Uri (u, None))
+ | n = NUMBER -> return_term loc (Num (n, 0))
+ | IMPLICIT -> return_term loc (Implicit)
+ | m = META -> return_term loc (Meta (int_of_string m, []))
+ | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
+ | s = sort -> return_term loc (Sort s)
+ | outtyp = OPT [ SYMBOL "["; ty = l2_pattern; SYMBOL "]" -> ty ];
+ IDENT "match"; t = l2_pattern;
+ indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+ IDENT "with"; SYMBOL "[";
+ patterns = LIST0 [
+ lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);
+ rhs = l2_pattern ->
+ lhs, rhs
+ ] SEP SYMBOL "|";
+ SYMBOL "]" ->
+ return_term loc (Case (t, indty_ident, outtyp, patterns))
+ | SYMBOL "("; p1 = l2_pattern; SYMBOL ":"; p2 = l2_pattern; SYMBOL ")" ->
+ return_term loc (Appl [ Symbol ("cast", 0); p1; p2 ])
+ | SYMBOL "("; p = l2_pattern; SYMBOL ")" -> p
+ | v = l2_pattern_variable -> return_term loc (Variable v)
+ | m = l2_magic_pattern -> return_term loc (Magic m)
+ ]
+ ];
+(* }}} *)
+(* {{{ Grammar for interpretation, notation level 3 *)
+ argument: [
+ [ id = IDENT -> IdentArg (0, id)
+ | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
+ SYMBOL "."; id = IDENT ->
+ IdentArg (List.length l, id)
+ ]
+ ];
+ level3_term: [
+ [ u = URI -> UriPattern (UriManager.uri_of_string u)
+ | id = IDENT -> VarPattern id
+ | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
+ (match terms with
+ | [] -> assert false
+ | [term] -> term
+ | terms -> ApplPattern terms)
+ ]
+ ];
+(* }}} *)
+(* {{{ Notation glues *)
+ associativity: [
+ [ IDENT "left"; IDENT "associative" -> Gramext.LeftA
+ | IDENT "right"; IDENT "associative" -> Gramext.RightA
+ | IDENT "non"; IDENT "associative" -> Gramext.NonA
+ ]
+ ];
+ precedence: [
+ [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
+ ];
+ notation: [
+ [ p1 = level1_pattern;
+ assoc = OPT associativity; prec = OPT precedence;
+ IDENT "for"; p2 = level2_pattern ->
+ (p1, assoc, prec, p2)
+ ]
+ ];
+ interpretation: [
+ [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+ (s, args, t)
+ ]
+ ];
+(* }}} *)
+(* {{{ Top-level phrases *)
+ phrase: [
+ [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2
+ | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." ->
+ Notation (l1, assoc, prec, l2)
+ | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." ->
+ Interpretation ((symbol, args), l3)
+ | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u)
+ ]
+ ];