44 then HOLogic.eq_const rty |
44 then HOLogic.eq_const rty |
45 else |
45 else |
46 case (rty, qty) of |
46 case (rty, qty) of |
47 (Type (s, tys), Type (s', tys')) => |
47 (Type (s, tys), Type (s', tys')) => |
48 if s = s' |
48 if s = s' |
49 then let |
49 then |
50 val map_info = maps_lookup thy s |
50 let |
51 handle NotFound => |
51 val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) |
52 raise LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) |
52 val map_info = maps_lookup thy s handle NotFound => raise exc |
53 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
53 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
54 in |
54 in |
55 list_comb (Const (#relfun map_info, dummyT), args) |
55 list_comb (Const (#relfun map_info, dummyT), args) |
56 end |
56 end |
57 else let |
57 else |
58 val SOME qinfo = quotdata_lookup_thy thy s' |
58 let |
59 (* FIXME: check in this case that the rty and qty *) |
59 val SOME qinfo = quotdata_lookup_thy thy s' |
60 (* FIXME: correspond to each other *) |
60 (* FIXME: check in this case that the rty and qty *) |
61 val (s, _) = dest_Const (#rel qinfo) |
61 (* FIXME: correspond to each other *) |
62 (* FIXME: the relation should only be the string *) |
62 val (s, _) = dest_Const (#rel qinfo) |
63 (* FIXME: and the type needs to be calculated as below; *) |
63 (* FIXME: the relation should only be the string *) |
64 (* FIXME: maybe one should actually have a term *) |
64 (* FIXME: and the type needs to be calculated as below; *) |
65 (* FIXME: and one needs to force it to have this type *) |
65 (* FIXME: maybe one should actually have a term *) |
66 in |
66 (* FIXME: and one needs to force it to have this type *) |
67 Const (s, rty --> rty --> @{typ bool}) |
67 in |
68 end |
68 Const (s, rty --> rty --> @{typ bool}) |
|
69 end |
69 | _ => HOLogic.eq_const dummyT |
70 | _ => HOLogic.eq_const dummyT |
70 (* FIXME: check that the types correspond to each other? *) |
71 (* FIXME: check that the types correspond to each other? *) |
71 end |
72 end |
72 |
73 |
73 val mk_babs = Const (@{const_name Babs}, dummyT) |
74 val mk_babs = Const (@{const_name Babs}, dummyT) |