+ l1_simple_pattern:
+ [ "layout" LEFTA
+ [ p1 = SELF; SYMBOL "\\SUB"; p2 = SELF ->
+ return_term loc (Layout (Sub (p1, p2)))
+ | p1 = SELF; SYMBOL "\\SUP"; p2 = SELF ->
+ return_term loc (Layout (Sup (p1, p2)))
+ | p1 = SELF; SYMBOL "\\BELOW"; p2 = SELF ->
+ return_term loc (Layout (Below (p1, p2)))
+ | p1 = SELF; SYMBOL "\\ABOVE"; p2 = SELF ->
+ return_term loc (Layout (Above (p1, p2)))
+ | p1 = SELF; SYMBOL "\\OVER"; p2 = SELF ->
+ return_term loc (Layout (Over (p1, p2)))
+ | p1 = SELF; SYMBOL "\\ATOP"; p2 = SELF ->
+ return_term loc (Layout (Atop (p1, p2)))
+(* | SYMBOL "\\ARRAY"; p = SELF; csep = OPT field_sep; rsep = OPT row_sep ->
+ return_term loc (Array (p, csep, rsep)) *)
+ | SYMBOL "\\FRAC"; p1 = SELF; p2 = SELF ->
+ return_term loc (Layout (Frac (p1, p2)))
+ | SYMBOL "\\SQRT"; p = SELF -> return_term loc (Layout (Sqrt p))
+ | SYMBOL "\\ROOT"; index = SELF; SYMBOL "\\OF"; arg = SELF ->
+ return_term loc (Layout (Root (arg, index)));
+ | SYMBOL "\\HBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+ return_term loc (Layout (Box (H, p)))
+ | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+ return_term loc (Layout (Box (V, p)))
+ | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
+ | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+ return_term loc (CicNotationUtil.boxify p)
+ | p = SELF; SYMBOL "\\AS"; id = IDENT ->
+ return_term loc (Variable (Ascription (p, id)))
+ ]
+ | "simple" NONA
+ [ i = IDENT -> return_term loc (Ident (i, None))
+ | m = l1_magic_pattern -> return_term loc (Magic m)
+ | v = l1_pattern_variable -> return_term loc (Variable v)
+ | l = literal -> return_term loc (Literal l)
+ ]
+ ];
+(* }}} *)
+(* {{{ Grammar for ast patterns, notation level 2 *)
+ 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)