160 T = alpha_T orelse (not (is_fp_iterator_type T) andalso |
160 T = alpha_T orelse (not (is_fp_iterator_type T) andalso |
161 exists (could_exist_alpha_subtype alpha_T) Ts) |
161 exists (could_exist_alpha_subtype alpha_T) Ts) |
162 | could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
162 | could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
163 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T = |
163 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T = |
164 could_exist_alpha_subtype alpha_T T |
164 could_exist_alpha_subtype alpha_T T |
165 | could_exist_alpha_sub_mtype thy alpha_T T = |
165 | could_exist_alpha_sub_mtype ctxt alpha_T T = |
166 (T = alpha_T orelse is_datatype thy [(NONE, true)] T) |
166 (T = alpha_T orelse is_datatype ctxt [(NONE, true)] T) |
167 |
167 |
168 fun exists_alpha_sub_mtype MAlpha = true |
168 fun exists_alpha_sub_mtype MAlpha = true |
169 | exists_alpha_sub_mtype (MFun (M1, _, M2)) = |
169 | exists_alpha_sub_mtype (MFun (M1, _, M2)) = |
170 exists exists_alpha_sub_mtype [M1, M2] |
170 exists exists_alpha_sub_mtype [M1, M2] |
171 | exists_alpha_sub_mtype (MPair (M1, M2)) = |
171 | exists_alpha_sub_mtype (MPair (M1, M2)) = |
241 is_fin_fun_supported_type (body_type T2) then |
241 is_fin_fun_supported_type (body_type T2) then |
242 V (Unsynchronized.inc max_fresh) |
242 V (Unsynchronized.inc max_fresh) |
243 else |
243 else |
244 S Minus |
244 S Minus |
245 in (M1, a, M2) end |
245 in (M1, a, M2) end |
246 and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, |
246 and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T, |
247 datatype_mcache, constr_mcache, ...}) |
247 datatype_mcache, constr_mcache, ...}) |
248 all_minus = |
248 all_minus = |
249 let |
249 let |
250 fun do_type T = |
250 fun do_type T = |
251 if T = alpha_T then |
251 if T = alpha_T then |
253 else case T of |
253 else case T of |
254 Type (@{type_name fun}, [T1, T2]) => |
254 Type (@{type_name fun}, [T1, T2]) => |
255 MFun (fresh_mfun_for_fun_type mdata false T1 T2) |
255 MFun (fresh_mfun_for_fun_type mdata false T1 T2) |
256 | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2)) |
256 | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2)) |
257 | Type (z as (s, _)) => |
257 | Type (z as (s, _)) => |
258 if could_exist_alpha_sub_mtype thy alpha_T T then |
258 if could_exist_alpha_sub_mtype ctxt alpha_T T then |
259 case AList.lookup (op =) (!datatype_mcache) z of |
259 case AList.lookup (op =) (!datatype_mcache) z of |
260 SOME M => M |
260 SOME M => M |
261 | NONE => |
261 | NONE => |
262 let |
262 let |
263 val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z)) |
263 val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z)) |
302 let val (arg_Ms, dataM) = curried_strip_mtype M in |
302 let val (arg_Ms, dataM) = curried_strip_mtype M in |
303 MFun (dataM, S Minus, |
303 MFun (dataM, S Minus, |
304 case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n) |
304 case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n) |
305 end |
305 end |
306 |
306 |
307 fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache, |
307 fun mtype_for_constr (mdata as {hol_ctxt = {ctxt, ...}, alpha_T, constr_mcache, |
308 ...}) (x as (_, T)) = |
308 ...}) (x as (_, T)) = |
309 if could_exist_alpha_sub_mtype thy alpha_T T then |
309 if could_exist_alpha_sub_mtype ctxt alpha_T T then |
310 case AList.lookup (op =) (!constr_mcache) x of |
310 case AList.lookup (op =) (!constr_mcache) x of |
311 SOME M => M |
311 SOME M => M |
312 | NONE => if T = alpha_T then |
312 | NONE => if T = alpha_T then |
313 let val M = fresh_mtype_for_type mdata false T in |
313 let val M = fresh_mtype_for_type mdata false T in |
314 (Unsynchronized.change constr_mcache (cons (x, M)); M) |
314 (Unsynchronized.change constr_mcache (cons (x, M)); M) |
739 s = @{const_name semilattice_sup_class.sup}) andalso |
739 s = @{const_name semilattice_sup_class.sup}) andalso |
740 is_set_type (domain_type T) then |
740 is_set_type (domain_type T) then |
741 do_robust_set_operation T accum |
741 do_robust_set_operation T accum |
742 else if is_sel s then |
742 else if is_sel s then |
743 (mtype_for_sel mdata x, accum) |
743 (mtype_for_sel mdata x, accum) |
744 else if is_constr thy stds x then |
744 else if is_constr ctxt stds x then |
745 (mtype_for_constr mdata x, accum) |
745 (mtype_for_constr mdata x, accum) |
746 else if is_built_in_const thy stds fast_descrs x then |
746 else if is_built_in_const thy stds fast_descrs x then |
747 (fresh_mtype_for_type mdata true T, accum) |
747 (fresh_mtype_for_type mdata true T, accum) |
748 else |
748 else |
749 let val M = mtype_for T in |
749 let val M = mtype_for T in |
922 |
922 |
923 fun consider_nondefinitional_axiom mdata t = |
923 fun consider_nondefinitional_axiom mdata t = |
924 if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M)) |
924 if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M)) |
925 else consider_general_formula mdata Plus t |
925 else consider_general_formula mdata Plus t |
926 |
926 |
927 fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t = |
927 fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t = |
928 if not (is_constr_pattern_formula thy t) then |
928 if not (is_constr_pattern_formula ctxt t) then |
929 consider_nondefinitional_axiom mdata t |
929 consider_nondefinitional_axiom mdata t |
930 else if is_harmless_axiom mdata t then |
930 else if is_harmless_axiom mdata t then |
931 pair (MRaw (t, dummy_M)) |
931 pair (MRaw (t, dummy_M)) |
932 else |
932 else |
933 let |
933 let |
1025 val formulas_monotonic = is_some oooo infer "Monotonicity" false |
1025 val formulas_monotonic = is_some oooo infer "Monotonicity" false |
1026 |
1026 |
1027 fun fin_fun_constr T1 T2 = |
1027 fun fin_fun_constr T1 T2 = |
1028 (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2])) |
1028 (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2])) |
1029 |
1029 |
1030 fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...}) |
1030 fun finitize_funs (hol_ctxt as {thy, ctxt, stds, fast_descrs, constr_cache, |
|
1031 ...}) |
1031 binarize finitizes alpha_T tsp = |
1032 binarize finitizes alpha_T tsp = |
1032 case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of |
1033 case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of |
1033 SOME (lits, msp, constr_mtypes) => |
1034 SOME (lits, msp, constr_mtypes) => |
1034 if forall (curry (op =) Minus o snd) lits then |
1035 if forall (curry (op =) Minus o snd) lits then |
1035 tsp |
1036 tsp |
1083 else if s = @{const_name "=="} orelse |
1084 else if s = @{const_name "=="} orelse |
1084 s = @{const_name "op ="} then |
1085 s = @{const_name "op ="} then |
1085 Const (s, T') |
1086 Const (s, T') |
1086 else if is_built_in_const thy stds fast_descrs x then |
1087 else if is_built_in_const thy stds fast_descrs x then |
1087 coerce_term hol_ctxt Ts T' T t |
1088 coerce_term hol_ctxt Ts T' T t |
1088 else if is_constr thy stds x then |
1089 else if is_constr ctxt stds x then |
1089 Const (finitize_constr x) |
1090 Const (finitize_constr x) |
1090 else if is_sel s then |
1091 else if is_sel s then |
1091 let |
1092 let |
1092 val n = sel_no_from_name s |
1093 val n = sel_no_from_name s |
1093 val x' = |
1094 val x' = |
1110 val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) |
1111 val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2) |
1111 val (t1', T2') = |
1112 val (t1', T2') = |
1112 case T1 of |
1113 case T1 of |
1113 Type (s, [T11, T12]) => |
1114 Type (s, [T11, T12]) => |
1114 (if s = @{type_name fin_fun} then |
1115 (if s = @{type_name fin_fun} then |
1115 select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 |
1116 select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1 |
1116 0 (T11 --> T12) |
1117 0 (T11 --> T12) |
1117 else |
1118 else |
1118 t1, T11) |
1119 t1, T11) |
1119 | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", |
1120 | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", |
1120 [T1], []) |
1121 [T1], []) |
1125 val t' = term_from_mterm (T :: Ts) m' |
1126 val t' = term_from_mterm (T :: Ts) m' |
1126 val T' = fastype_of1 (T :: Ts, t') |
1127 val T' = fastype_of1 (T :: Ts, t') |
1127 in |
1128 in |
1128 Abs (s, T, t') |
1129 Abs (s, T, t') |
1129 |> should_finitize (T --> T') a |
1130 |> should_finitize (T --> T') a |
1130 ? construct_value thy stds (fin_fun_constr T T') o single |
1131 ? construct_value ctxt stds (fin_fun_constr T T') o single |
1131 end |
1132 end |
1132 in |
1133 in |
1133 Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); |
1134 Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); |
1134 pairself (map (term_from_mterm [])) msp |
1135 pairself (map (term_from_mterm [])) msp |
1135 end |
1136 end |