equal
deleted
inserted
replaced
197 val args_aux = map (double_lookup rtyenv qtyenv) vs |
197 val args_aux = map (double_lookup rtyenv qtyenv) vs |
198 val args = map (absrep_fun flag ctxt) args_aux |
198 val args = map (absrep_fun flag ctxt) args_aux |
199 val map_fun = mk_mapfun ctxt vs rty_pat |
199 val map_fun = mk_mapfun ctxt vs rty_pat |
200 val result = list_comb (map_fun, args) |
200 val result = list_comb (map_fun, args) |
201 in |
201 in |
202 (*if tys' = [] orelse tys' = tys |
202 mk_fun_compose flag (absrep_const flag ctxt s', result) |
203 then absrep_const flag ctxt s' |
|
204 else*) mk_fun_compose flag (absrep_const flag ctxt s', result) |
|
205 end |
203 end |
206 | (TFree x, TFree x') => |
204 | (TFree x, TFree x') => |
207 if x = x' |
205 if x = x' |
208 then mk_identity rty |
206 then mk_identity rty |
209 else raise (LIFT_MATCH "absrep_fun (frees)") |
207 else raise (LIFT_MATCH "absrep_fun (frees)") |
298 val rel_map = mk_relmap ctxt vs rty_pat |
296 val rel_map = mk_relmap ctxt vs rty_pat |
299 val result = list_comb (rel_map, args) |
297 val result = list_comb (rel_map, args) |
300 val eqv_rel = get_equiv_rel ctxt s' |
298 val eqv_rel = get_equiv_rel ctxt s' |
301 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
299 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
302 in |
300 in |
303 (*if tys' = [] orelse tys' = tys |
301 mk_rel_compose (result, eqv_rel') |
304 then eqv_rel' |
|
305 else*) mk_rel_compose (result, eqv_rel') |
|
306 end |
302 end |
307 | _ => HOLogic.eq_const rty |
303 | _ => HOLogic.eq_const rty |
308 |
304 |
309 fun equiv_relation_chk ctxt (rty, qty) = |
305 fun equiv_relation_chk ctxt (rty, qty) = |
310 equiv_relation ctxt (rty, qty) |
306 equiv_relation ctxt (rty, qty) |
400 else equiv_relation ctxt (domain_type ty, domain_type ty') |
396 else equiv_relation ctxt (domain_type ty, domain_type ty') |
401 |
397 |
402 | (* in this case we just check whether the given equivalence relation is correct *) |
398 | (* in this case we just check whether the given equivalence relation is correct *) |
403 (rel, Const (@{const_name "op ="}, ty')) => |
399 (rel, Const (@{const_name "op ="}, ty')) => |
404 let |
400 let |
|
401 (* FIXME: better exception handling *) |
405 fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
402 fun exc rel rel' = LIFT_MATCH ("regularise (relation mismatch)\n[" ^ |
406 Syntax.string_of_term ctxt rel ^ " :: " ^ |
403 Syntax.string_of_term ctxt rel ^ " :: " ^ |
407 Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^ |
404 Syntax.string_of_typ ctxt (fastype_of rel) ^ "]\n[" ^ |
408 Syntax.string_of_term ctxt rel' ^ " :: " ^ |
405 Syntax.string_of_term ctxt rel' ^ " :: " ^ |
409 Syntax.string_of_typ ctxt (fastype_of rel') ^ "]") |
406 Syntax.string_of_typ ctxt (fastype_of rel') ^ "]") |