274 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = |
274 fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = |
275 let |
275 let |
276 (* new parsing with proper declaration *) |
276 (* new parsing with proper declaration *) |
277 val rty = Syntax.read_typ lthy rty_str |
277 val rty = Syntax.read_typ lthy rty_str |
278 val lthy1 = Variable.declare_typ rty lthy |
278 val lthy1 = Variable.declare_typ rty lthy |
279 val pre_rel = Syntax.parse_term lthy1 rel_str |
279 val rel = |
280 val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel |
280 Syntax.parse_term lthy1 rel_str |
281 val rel = Syntax.check_term lthy1 pre_rel' |
281 |> Syntax.type_constraint (rty --> rty --> @{typ bool}) |
|
282 |> Syntax.check_term lthy1 |
282 val lthy2 = Variable.declare_term rel lthy1 |
283 val lthy2 = Variable.declare_term rel lthy1 |
283 |
|
284 (* old parsing *) |
|
285 (* val rty = Syntax.read_typ lthy rty_str |
|
286 val rel = Syntax.read_term lthy rel_str *) |
|
287 in |
284 in |
288 (((vs, qty_name, mx), (rty, rel)), lthy2) |
285 (((vs, qty_name, mx), (rty, rel)), lthy2) |
289 end |
286 end |
290 |
287 |
291 val (spec', lthy') = fold_map parse_spec specs lthy |
288 val (spec', lthy') = fold_map parse_spec specs lthy |
292 in |
289 in |
293 quotient_type spec' lthy' |
290 quotient_type spec' lthy' |
294 end |
291 end |
295 |
292 |
|
293 local |
|
294 structure P = OuterParse; |
|
295 in |
|
296 |
296 val quotspec_parser = |
297 val quotspec_parser = |
297 OuterParse.and_list1 |
298 P.and_list1 ((P.type_args -- P.binding) -- P.opt_infix -- |
298 ((OuterParse.type_args -- OuterParse.binding) -- |
299 (P.$$$ "=" |-- P.typ) -- (P.$$$ "/" |-- P.term)) |
299 OuterParse.opt_infix -- (OuterParse.$$$ "=" |-- OuterParse.typ) -- |
300 end |
300 (OuterParse.$$$ "/" |-- OuterParse.term)) |
|
301 |
301 |
302 val _ = OuterKeyword.keyword "/" |
302 val _ = OuterKeyword.keyword "/" |
303 |
303 |
304 val _ = |
304 val _ = |
305 OuterSyntax.local_theory_to_proof "quotient_type" |
305 OuterSyntax.local_theory_to_proof "quotient_type" |