43 |
43 |
44 fun get_map ctxt ty_str = |
44 fun get_map ctxt ty_str = |
45 let |
45 let |
46 val thy = ProofContext.theory_of ctxt |
46 val thy = ProofContext.theory_of ctxt |
47 val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."]) |
47 val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."]) |
48 val info = maps_lookup thy ty_str handle NotFound => raise exc |
48 val mapfun = #mapfun (maps_lookup thy ty_str) handle NotFound => raise exc |
49 in |
49 in |
50 Const (#mapfun info, dummyT) |
50 Const (mapfun, dummyT) |
51 end |
51 end |
52 |
52 |
53 fun get_absrep_const flag ctxt _ qty = |
53 fun get_absrep_const flag ctxt _ qty = |
54 (* FIXME: check here that the type-constructors of _ and qty are related *) |
54 (* FIXME: check here that the type-constructors of _ and qty are related *) |
55 let |
55 let |
143 case (rty, qty) of |
143 case (rty, qty) of |
144 (Type (s, tys), Type (s', tys')) => |
144 (Type (s, tys), Type (s', tys')) => |
145 if s = s' |
145 if s = s' |
146 then |
146 then |
147 let |
147 let |
148 val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s) |
148 val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") |
149 val map_info = maps_lookup thy s handle NotFound => raise exc |
149 val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc |
150 val args = map (mk_resp_arg ctxt) (tys ~~ tys') |
150 val args = map (mk_resp_arg ctxt) (tys ~~ tys') |
151 in |
151 in |
152 list_comb (Const (#relfun map_info, dummyT), args) |
152 list_comb (Const (relmap, dummyT), args) |
153 end |
153 end |
154 else |
154 else |
155 let |
155 let |
156 val SOME qinfo = quotdata_lookup_thy thy s' |
156 val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") |
|
157 val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc |
157 (* FIXME: check in this case that the rty and qty *) |
158 (* FIXME: check in this case that the rty and qty *) |
158 (* FIXME: correspond to each other *) |
159 (* FIXME: correspond to each other *) |
159 |
160 |
160 (* we need to instantiate the TVars in the relation *) |
161 (* we need to instantiate the TVars in the relation *) |
161 val thy = ProofContext.theory_of ctxt |
162 val thy = ProofContext.theory_of ctxt |
162 val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool}) |
163 val forced_equiv_rel = force_typ thy equiv_rel (rty --> rty --> @{typ bool}) |
163 in |
164 in |
164 forced_rel |
165 forced_equiv_rel |
165 end |
166 end |
166 | _ => HOLogic.eq_const rty |
167 | _ => HOLogic.eq_const rty |
167 (* FIXME: check that the types correspond to each other? *) |
168 (* FIXME: check that the types correspond to each other? *) |
168 end |
169 end |
169 |
170 |