252 if T = alpha_T then |
252 if T = alpha_T then |
253 MAlpha |
253 MAlpha |
254 else case T of |
254 else case T of |
255 Type (@{type_name fun}, [T1, T2]) => |
255 Type (@{type_name fun}, [T1, T2]) => |
256 MFun (fresh_mfun_for_fun_type mdata false T1 T2) |
256 MFun (fresh_mfun_for_fun_type mdata false T1 T2) |
257 | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2)) |
257 | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2)) |
258 | Type (z as (s, _)) => |
258 | Type (z as (s, _)) => |
259 if could_exist_alpha_sub_mtype ctxt alpha_T T then |
259 if could_exist_alpha_sub_mtype ctxt alpha_T T then |
260 case AList.lookup (op =) (!datatype_mcache) z of |
260 case AList.lookup (op =) (!datatype_mcache) z of |
261 SOME M => M |
261 SOME M => M |
262 | NONE => |
262 | NONE => |
1033 case (M, T) of |
1033 case (M, T) of |
1034 (MAlpha, _) => T |
1034 (MAlpha, _) => T |
1035 | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => |
1035 | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) => |
1036 Type (if should_finitize T a then @{type_name fin_fun} |
1036 Type (if should_finitize T a then @{type_name fin_fun} |
1037 else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) |
1037 else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) |
1038 | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) => |
1038 | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) => |
1039 Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2]) |
1039 Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2]) |
1040 | (MType _, _) => T |
1040 | (MType _, _) => T |
1041 | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", |
1041 | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", |
1042 [M], [T]) |
1042 [M], [T]) |
1043 fun finitize_constr (x as (s, T)) = |
1043 fun finitize_constr (x as (s, T)) = |
1044 (s, case AList.lookup (op =) constr_mtypes x of |
1044 (s, case AList.lookup (op =) constr_mtypes x of |