1144 else |
1144 else |
1145 case (rty, qty) of |
1145 case (rty, qty) of |
1146 (Type (s, tys), Type (s', tys')) => |
1146 (Type (s, tys), Type (s', tys')) => |
1147 if s = s' |
1147 if s = s' |
1148 then let |
1148 then let |
1149 val _ = tracing ("maps lookup for " ^ s) |
|
1150 val _ = tracing (Syntax.string_of_typ lthy rty) |
|
1151 val _ = tracing (Syntax.string_of_typ lthy qty) |
|
1152 val SOME map_info = maps_lookup thy s |
1149 val SOME map_info = maps_lookup thy s |
1153 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
1150 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
1154 in |
1151 in |
1155 list_comb (Const (#relfun map_info, dummyT), args) |
1152 list_comb (Const (#relfun map_info, dummyT), args) |
1156 end |
1153 end |
1157 else let |
1154 else let |
1158 val SOME qinfo = quotdata_lookup_thy thy s' |
1155 val SOME qinfo = quotdata_lookup_thy thy s' |
1159 (* FIXME: check in this case that the rty and qty *) |
1156 (* FIXME: check in this case that the rty and qty *) |
1160 (* FIXME: correspond to each other *) |
1157 (* FIXME: correspond to each other *) |
|
1158 val (s, _) = dest_Const (#rel qinfo) |
|
1159 (* FIXME: the relation should only be the string *) |
|
1160 (* FIXME: and the type needs to be calculated as below *) |
1161 in |
1161 in |
1162 #rel qinfo |
1162 Const (s, rty --> rty --> @{typ bool}) |
1163 end |
1163 end |
1164 | _ => HOLogic.eq_const dummyT |
1164 | _ => HOLogic.eq_const dummyT |
1165 (* FIXME: check that the types correspond to each other? *) |
1165 (* FIXME: check that the types correspond to each other? *) |
1166 end |
1166 end |
1167 *} |
1167 *} |
1236 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1236 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
1237 end |
1237 end |
1238 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1238 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
1239 let |
1239 let |
1240 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1240 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1241 val _ = tracing "quantor types All" |
|
1242 val _ = tracing (Syntax.string_of_typ lthy ty) |
|
1243 val _ = tracing (Syntax.string_of_typ lthy ty') |
|
1244 in |
1241 in |
1245 if ty = ty' |
1242 if ty = ty' |
1246 then Const (@{const_name "All"}, ty) $ subtrm |
1243 then Const (@{const_name "All"}, ty) $ subtrm |
1247 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1244 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1248 end |
1245 end |
1249 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
1246 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
1250 let |
1247 let |
1251 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1248 val subtrm = apply_subt (REGULARIZE_trm lthy) t t' |
1252 val _ = tracing "quantor types Ex" |
|
1253 val _ = tracing (Syntax.string_of_typ lthy ty) |
|
1254 val _ = tracing (Syntax.string_of_typ lthy ty') |
|
1255 in |
1249 in |
1256 if ty = ty' |
1250 if ty = ty' |
1257 then Const (@{const_name "Ex"}, ty) $ subtrm |
1251 then Const (@{const_name "Ex"}, ty) $ subtrm |
1258 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1252 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
1259 end |
1253 end |