else
uri
+let mk_binder_ast binder typ vars body =
+ List.fold_right
+ (fun var body ->
+ let name = name_of_string var in
+ CicAst.Binder (binder, (name, typ), body))
+ vars body
+
EXTEND
GLOBAL: term term0 tactic tactical tactical0 command script;
int: [
[ s = SYMBOL "_" -> None
| t = term -> Some t ]
];
- binder: [
- [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
- | SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
+ binder_low: [
+ [ SYMBOL <:unicode<Pi>> (* Π *) -> `Pi
| SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
| SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
];
+ binder_high: [ [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda ] ];
sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
] SEP "and" -> defs
]];
constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
+ binder_vars: [
+ [ vars = LIST1 IDENT SEP SYMBOL ",";
+ typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
+ | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
+ typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+ ]
+ ];
term0: [ [ t = term; EOI -> return_term loc t ] ];
term:
[ "letin" NONA
defs = let_defs; "in"; body = term ->
return_term loc (CicAst.LetRec (ind_kind, defs, body))
]
- | "apply" LEFTA
- [ t1 = term; t2 = term ->
- let rec aux = function
- | CicAst.Appl (hd :: tl) -> aux hd @ tl
- | term -> [term]
- in
- CicAst.Appl (aux t1 @ [t2])
- ]
| "binder" RIGHTA
[
- b = binder;
- (vars, typ) =
- [ vars = LIST1 IDENT SEP SYMBOL ",";
- typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
- | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
- typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
- ];
- SYMBOL "."; body = term ->
- let binder =
- List.fold_right
- (fun var body ->
- let name = name_of_string var in
- CicAst.Binder (b, (name, typ), body))
- vars body
- in
+ b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ let binder = mk_binder_ast b typ vars body in
return_term loc binder
| t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
- return_term loc
- (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
+ return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
| "logic_add" LEFTA [ (* nothing here by default *) ]
| "logic_mult" LEFTA [ (* nothing here by default *) ]
| "mult" LEFTA [ (* nothing here by default *) ]
| "power" LEFTA [ (* nothing here by default *) ]
| "inv" NONA [ (* nothing here by default *) ]
+ | "apply" LEFTA
+ [ t1 = term; t2 = term ->
+ let rec aux = function
+ | CicAst.Appl (hd :: tl) -> aux hd @ tl
+ | term -> [term]
+ in
+ CicAst.Appl (aux t1 @ [t2])
+ ]
+ | "binder" RIGHTA
+ [
+ b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ let binder = mk_binder_ast b typ vars body in
+ return_term loc binder
+ ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
| n = substituted_name -> return_term loc n