let level2_ast = Grammar.Entry.create level2_ast_grammar "level2_ast"
let term = Grammar.Entry.create level2_ast_grammar "term"
let let_defs = Grammar.Entry.create level2_ast_grammar "let_defs"
+let protected_binder_vars = Grammar.Entry.create level2_ast_grammar "protected_binder_vars"
let level2_meta = Grammar.Entry.create level2_meta_grammar "level2_meta"
let int_of_string s =
in
string_of_int precedence ^ assoc_string
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
(* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
let owned_keywords = Hashtbl.create 23
(* {{{ Grammar for ast patterns, notation level 2 *)
EXTEND
- GLOBAL: level2_ast term let_defs;
+ GLOBAL: level2_ast term let_defs protected_binder_vars;
level2_ast: [ [ p = term -> p ] ];
sort: [
[ "Prop" -> `Prop
| "Set" -> `Set
| "Type" -> `Type (CicUniv.fresh ())
- | "CProp" -> `CProp
+ | "CProp" -> `CProp (CicUniv.fresh ())
]
];
explicit_subst: [
id, Some typ
| arg = single_arg -> arg, None
| SYMBOL "_" -> Ast.Ident ("_", None), None
+ | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
+ Ast.Ident ("_", None), Some typ
]
];
match_pattern: [
- [ id = IDENT -> id, None, []
+ [ id = IDENT -> Ast.Pattern (id, None, [])
| LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
- id, None, vars
+ Ast.Pattern (id, None, vars)
+ | id = IDENT; vars = LIST1 possibly_typed_name ->
+ Ast.Pattern (id, None, vars)
+ | SYMBOL "_" -> Ast.Wildcard
]
];
binder: [
| _ -> failwith "Invalid index name."
]
];
- induction_kind: [
- [ "rec" -> `Inductive
- | "corec" -> `CoInductive
- ]
- ];
let_defs: [
[ defs = LIST1 [
name = single_arg;
index_name = OPT [ "on"; id = single_arg -> id ];
ty = OPT [ SYMBOL ":" ; p = term -> p ];
SYMBOL <:unicode<def>> (* ≝ *); body = term ->
- 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
| None -> 0
| Some index_name -> find_arg index_name 0 args
in
- (name, ty), body, index
+ let args =
+ List.concat
+ (List.map
+ (function (names,ty) -> List.map (function x -> x,ty) names
+ ) args)
+ in
+ args, (name, ty), body, index
] SEP "and" ->
defs
]
l = LIST1 single_arg SEP SYMBOL "," -> l
| SYMBOL "_" -> [Ast.Ident ("_", None)] ];
typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
- | LPAREN;
- vars = [
- l = LIST1 single_arg SEP SYMBOL "," -> l
- | SYMBOL "_" -> [Ast.Ident ("_", None)] ];
- typ = OPT [ SYMBOL ":"; t = term -> t ];
- RPAREN -> (vars, typ)
+ ]
+ ];
+ protected_binder_vars: [
+ [ LPAREN; vars = binder_vars; RPAREN -> vars
+ ]
+ ];
+ maybe_protected_binder_vars: [
+ [ vars = binder_vars -> vars
+ | vars = protected_binder_vars -> vars
]
];
term: LEVEL "10N" [ (* let in *)
[ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
p1 = term; "in"; p2 = term ->
return_term loc (Ast.LetIn (var, p1, p2))
- | "let"; k = induction_kind; defs = let_defs; "in";
+ | LETCOREC; defs = let_defs; "in";
+ body = term ->
+ return_term loc (Ast.LetRec (`CoInductive, defs, body))
+ | LETREC; defs = let_defs; "in";
body = term ->
- return_term loc (Ast.LetRec (k, defs, body))
+ return_term loc (Ast.LetRec (`Inductive, defs, body))
]
];
term: LEVEL "20R" (* binder *)
[
- [ b = binder; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ [ b = binder; (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
return_term loc (fold_cluster b vars typ body)
| SYMBOL <:unicode<exists>> (* ∃ *);
- (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+ (vars, typ) = maybe_protected_binder_vars; SYMBOL "."; body = term ->
return_term loc (fold_exists vars typ body)
]
];