equal
deleted
inserted
replaced
94 fun double_lookup rtyenv qtyenv v = |
94 fun double_lookup rtyenv qtyenv v = |
95 let |
95 let |
96 val v' = fst (dest_TVar v) |
96 val v' = fst (dest_TVar v) |
97 in |
97 in |
98 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
98 (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
|
99 end |
|
100 |
|
101 (* matches a type pattern with a type *) |
|
102 fun match ctxt err ty_pat ty = |
|
103 let |
|
104 val thy = ProofContext.theory_of ctxt |
|
105 in |
|
106 Sign.typ_match thy (ty_pat, ty) Vartab.empty |
|
107 handle MATCH_TYPE => err ctxt ty_pat ty |
99 end |
108 end |
100 |
109 |
101 (* produces the rep or abs constant for a qty *) |
110 (* produces the rep or abs constant for a qty *) |
102 fun absrep_const flag ctxt qty_str = |
111 fun absrep_const flag ctxt qty_str = |
103 let |
112 let |
168 then |
177 then |
169 let |
178 let |
170 val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
179 val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
171 in |
180 in |
172 list_comb (get_mapfun ctxt s, args) |
181 list_comb (get_mapfun ctxt s, args) |
173 end |
182 end |
174 else |
183 else |
175 let |
184 let |
176 val thy = ProofContext.theory_of ctxt |
|
177 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
185 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
178 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
186 val rtyenv = match ctxt absrep_match_err rty_pat rty |
179 handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty |
187 val qtyenv = match ctxt absrep_match_err qty_pat qty |
180 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
|
181 handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty |
|
182 val args_aux = map (double_lookup rtyenv qtyenv) vs |
188 val args_aux = map (double_lookup rtyenv qtyenv) vs |
183 val args = map (absrep_fun flag ctxt) args_aux |
189 val args = map (absrep_fun flag ctxt) args_aux |
184 val map_fun = mk_mapfun ctxt vs rty_pat |
190 val map_fun = mk_mapfun ctxt vs rty_pat |
185 val result = list_comb (map_fun, args) |
191 val result = list_comb (map_fun, args) |
186 in |
192 in |
273 in |
279 in |
274 list_comb (get_relmap ctxt s, args) |
280 list_comb (get_relmap ctxt s, args) |
275 end |
281 end |
276 else |
282 else |
277 let |
283 let |
278 val thy = ProofContext.theory_of ctxt |
|
279 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
284 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' |
280 val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty |
285 val rtyenv = match ctxt equiv_match_err rty_pat rty |
281 handle MATCH_TYPE => equiv_match_err ctxt rty_pat rty |
286 val qtyenv = match ctxt equiv_match_err qty_pat qty |
282 val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty |
|
283 handle MATCH_TYPE => equiv_match_err ctxt qty_pat qty |
|
284 val args_aux = map (double_lookup rtyenv qtyenv) vs |
287 val args_aux = map (double_lookup rtyenv qtyenv) vs |
285 val args = map (equiv_relation ctxt) args_aux |
288 val args = map (equiv_relation ctxt) args_aux |
286 val rel_map = mk_relmap ctxt vs rty_pat |
289 val rel_map = mk_relmap ctxt vs rty_pat |
287 val result = list_comb (rel_map, args) |
290 val result = list_comb (rel_map, args) |
288 val eqv_rel = get_equiv_rel ctxt s' |
291 val eqv_rel = get_equiv_rel ctxt s' |