equal
deleted
inserted
replaced
98 |
98 |
99 (* looks up the (varified) rty and qty for |
99 (* looks up the (varified) rty and qty for |
100 a quotient definition |
100 a quotient definition |
101 *) |
101 *) |
102 fun get_rty_qty ctxt s = |
102 fun get_rty_qty ctxt s = |
103 let |
103 case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of |
104 val thy = Proof_Context.theory_of ctxt |
104 SOME qdata => (#rtyp qdata, #qtyp qdata) |
105 val qdata = Quotient_Info.quotdata_lookup thy s handle Quotient_Info.NotFound => |
105 | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."); |
106 raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") |
|
107 in |
|
108 (#rtyp qdata, #qtyp qdata) |
|
109 end |
|
110 |
106 |
111 (* takes two type-environments and looks |
107 (* takes two type-environments and looks |
112 up in both of them the variable v, which |
108 up in both of them the variable v, which |
113 must be listed in the environment |
109 must be listed in the environment |
114 *) |
110 *) |
300 in |
296 in |
301 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
297 fold_rev Term.lambda vs' (mk_relmap_aux rty) |
302 end |
298 end |
303 |
299 |
304 fun get_equiv_rel ctxt s = |
300 fun get_equiv_rel ctxt s = |
305 let |
301 case Quotient_Info.quotdata_lookup (Proof_Context.theory_of ctxt) s of |
306 val thy = Proof_Context.theory_of ctxt |
302 SOME qdata => #equiv_rel qdata |
307 in |
303 | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
308 #equiv_rel (Quotient_Info.quotdata_lookup thy s) handle Quotient_Info.NotFound => |
|
309 raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
|
310 end |
|
311 |
304 |
312 fun equiv_match_err ctxt ty_pat ty = |
305 fun equiv_match_err ctxt ty_pat ty = |
313 let |
306 let |
314 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
307 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
315 val ty_str = Syntax.string_of_typ ctxt ty |
308 val ty_str = Syntax.string_of_typ ctxt ty |
440 (Type (rs, rtys), Type (qs, qtys)) => |
433 (Type (rs, rtys), Type (qs, qtys)) => |
441 if rs = qs then |
434 if rs = qs then |
442 if length rtys <> length qtys then false |
435 if length rtys <> length qtys then false |
443 else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) |
436 else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys) |
444 else |
437 else |
445 (case Quotient_Info.quotdata_lookup_raw thy qs of |
438 (case Quotient_Info.quotdata_lookup thy qs of |
446 SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
439 SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
447 | NONE => false) |
440 | NONE => false) |
448 | _ => false) |
441 | _ => false) |
449 |
442 |
450 |
443 |