247 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
247 val exc = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")") |
248 in |
248 in |
249 #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc |
249 #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exc |
250 end |
250 end |
251 |
251 |
|
252 fun equiv_match_err ctxt ty_pat ty = |
|
253 let |
|
254 val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
255 val ty_str = Syntax.string_of_typ ctxt ty |
|
256 in |
|
257 raise LIFT_MATCH (space_implode " " |
|
258 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
259 end |
|
260 |
252 (* builds the aggregate equivalence relation *) |
261 (* builds the aggregate equivalence relation *) |
253 (* that will be the argument of Respects *) |
262 (* that will be the argument of Respects *) |
254 |
|
255 (* FIXME: check that the types correspond to each other *) |
|
256 fun new_equiv_relation ctxt (rty, qty) = |
263 fun new_equiv_relation ctxt (rty, qty) = |
257 if rty = qty |
264 if rty = qty |
258 then HOLogic.eq_const rty |
265 then HOLogic.eq_const rty |
259 else |
266 else |
260 case (rty, qty) of |
267 case (rty, qty) of |
269 else |
276 else |
270 let |
277 let |
271 val thy = ProofContext.theory_of ctxt |
278 val thy = ProofContext.theory_of ctxt |
272 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
279 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
273 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
280 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
274 handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty |
281 handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty |
275 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
282 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
276 handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty |
283 handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty |
277 val args_aux = map (double_lookup rtyenv qtyenv) vs |
284 val args_aux = map (double_lookup rtyenv qtyenv) vs |
278 val args = map (new_equiv_relation ctxt) args_aux |
285 val args = map (new_equiv_relation ctxt) args_aux |
279 val rel_map = mk_relmap ctxt vs rty_pat |
286 val rel_map = mk_relmap ctxt vs rty_pat |
280 val result = list_comb (rel_map, args) |
287 val result = list_comb (rel_map, args) |
281 val eqv_rel = get_equiv_rel ctxt s' |
288 val eqv_rel = get_equiv_rel ctxt s' |