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
[ "Prop" -> `Prop
| "Set" -> `Set
| "Type" -> `Type (CicUniv.fresh ())
- | "CProp" -> `CProp
+ | "CProp" -> `CProp (CicUniv.fresh ())
]
];
explicit_subst: [
]
];
match_pattern: [
- [ id = IDENT -> id, None, []
+ [ id = IDENT -> Ast.Pattern (id, None, [])
| LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
- id, None, vars
- | id = IDENT; vars = LIST1 possibly_typed_name -> 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;
[ "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 *)