68 | string_for_sign_atom (V j) = string_for_var j |
73 | string_for_sign_atom (V j) = string_for_var j |
69 |
74 |
70 (* literal -> string *) |
75 (* literal -> string *) |
71 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn |
76 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn |
72 |
77 |
73 val bool_C = CType (@{type_name bool}, []) |
78 val bool_M = MType (@{type_name bool}, []) |
74 |
79 val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", []) |
75 (* ctype -> bool *) |
80 |
76 fun is_CRec (CRec _) = true |
81 (* mtyp -> bool *) |
77 | is_CRec _ = false |
82 fun is_MRec (MRec _) = true |
|
83 | is_MRec _ = false |
|
84 (* mtyp -> mtyp * sign_atom * mtyp *) |
|
85 fun dest_MFun (MFun z) = z |
|
86 | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M]) |
78 |
87 |
79 val no_prec = 100 |
88 val no_prec = 100 |
80 val prec_CFun = 1 |
89 |
81 val prec_CPair = 2 |
90 (* mtyp -> int *) |
82 |
91 fun precedence_of_mtype (MFun _) = 1 |
83 (* tuple_set -> int *) |
92 | precedence_of_mtype (MPair _) = 2 |
84 fun precedence_of_ctype (CFun _) = prec_CFun |
93 | precedence_of_mtype _ = no_prec |
85 | precedence_of_ctype (CPair _) = prec_CPair |
94 |
86 | precedence_of_ctype _ = no_prec |
95 (* mtyp -> string *) |
87 |
96 val string_for_mtype = |
88 (* ctype -> string *) |
|
89 val string_for_ctype = |
|
90 let |
97 let |
91 (* int -> ctype -> string *) |
98 (* int -> mtyp -> string *) |
92 fun aux outer_prec C = |
99 fun aux outer_prec M = |
93 let |
100 let |
94 val prec = precedence_of_ctype C |
101 val prec = precedence_of_mtype M |
95 val need_parens = (prec < outer_prec) |
102 val need_parens = (prec < outer_prec) |
96 in |
103 in |
97 (if need_parens then "(" else "") ^ |
104 (if need_parens then "(" else "") ^ |
98 (case C of |
105 (case M of |
99 CAlpha => "\<alpha>" |
106 MAlpha => "\<alpha>" |
100 | CFun (C1, a, C2) => |
107 | MFun (M1, a, M2) => |
101 aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^ |
108 aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^ |
102 string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2 |
109 string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2 |
103 | CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2 |
110 | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2 |
104 | CType (s, []) => |
111 | MType (s, []) => |
105 if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s |
112 if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s |
106 | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s |
113 | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s |
107 | CRec (s, _) => "[" ^ s ^ "]") ^ |
114 | MRec (s, _) => "[" ^ s ^ "]") ^ |
108 (if need_parens then ")" else "") |
115 (if need_parens then ")" else "") |
109 end |
116 end |
110 in aux 0 end |
117 in aux 0 end |
111 |
118 |
112 (* ctype -> ctype list *) |
119 (* mtyp -> mtyp list *) |
113 fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2] |
120 fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2] |
114 | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs |
121 | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms |
115 | flatten_ctype C = [C] |
122 | flatten_mtype M = [M] |
116 |
123 |
117 (* hol_context -> bool -> typ -> cdata *) |
124 (* mterm -> bool *) |
118 fun initial_cdata hol_ctxt binarize alpha_T = |
125 fun precedence_of_mterm (MAtom _) = no_prec |
|
126 | precedence_of_mterm (MAbs _) = 1 |
|
127 | precedence_of_mterm (MApp _) = 2 |
|
128 |
|
129 (* Proof.context -> mterm -> string *) |
|
130 fun string_for_mterm ctxt = |
|
131 let |
|
132 (* mtype -> string *) |
|
133 fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>" |
|
134 (* int -> mterm -> string *) |
|
135 fun aux outer_prec m = |
|
136 let |
|
137 val prec = precedence_of_mterm m |
|
138 val need_parens = (prec < outer_prec) |
|
139 in |
|
140 (if need_parens then "(" else "") ^ |
|
141 (case m of |
|
142 MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M |
|
143 | MAbs (s, _, M, a, m) => |
|
144 "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^ |
|
145 string_for_sign_atom a ^ "\<^esup> " ^ aux prec m |
|
146 | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^ |
|
147 (if need_parens then ")" else "") |
|
148 end |
|
149 in aux 0 end |
|
150 |
|
151 (* mterm -> mtyp *) |
|
152 fun mtype_of_mterm (MAtom (_, M)) = M |
|
153 | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m) |
|
154 | mtype_of_mterm (MApp (m1, _)) = |
|
155 case mtype_of_mterm m1 of |
|
156 MFun (_, _, M12) => M12 |
|
157 | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1]) |
|
158 |
|
159 (* hol_context -> bool -> typ -> mdata *) |
|
160 fun initial_mdata hol_ctxt binarize alpha_T = |
119 ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T, |
161 ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T, |
120 max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [], |
162 max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [], |
121 constr_cache = Unsynchronized.ref []} : cdata) |
163 constr_cache = Unsynchronized.ref []} : mdata) |
122 |
164 |
123 (* typ -> typ -> bool *) |
165 (* typ -> typ -> bool *) |
124 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = |
166 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = |
125 T = alpha_T orelse (not (is_fp_iterator_type T) andalso |
167 T = alpha_T orelse (not (is_fp_iterator_type T) andalso |
126 exists (could_exist_alpha_subtype alpha_T) Ts) |
168 exists (could_exist_alpha_subtype alpha_T) Ts) |
127 | could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
169 | could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
128 (* theory -> typ -> typ -> bool *) |
170 (* theory -> typ -> typ -> bool *) |
129 fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T = |
171 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T = |
130 could_exist_alpha_subtype alpha_T T |
172 could_exist_alpha_subtype alpha_T T |
131 | could_exist_alpha_sub_ctype thy alpha_T T = |
173 | could_exist_alpha_sub_mtype thy alpha_T T = |
132 (T = alpha_T orelse is_datatype thy [(NONE, true)] T) |
174 (T = alpha_T orelse is_datatype thy [(NONE, true)] T) |
133 |
175 |
134 (* ctype -> bool *) |
176 (* mtyp -> bool *) |
135 fun exists_alpha_sub_ctype CAlpha = true |
177 fun exists_alpha_sub_mtype MAlpha = true |
136 | exists_alpha_sub_ctype (CFun (C1, _, C2)) = |
178 | exists_alpha_sub_mtype (MFun (M1, _, M2)) = |
137 exists exists_alpha_sub_ctype [C1, C2] |
179 exists exists_alpha_sub_mtype [M1, M2] |
138 | exists_alpha_sub_ctype (CPair (C1, C2)) = |
180 | exists_alpha_sub_mtype (MPair (M1, M2)) = |
139 exists exists_alpha_sub_ctype [C1, C2] |
181 exists exists_alpha_sub_mtype [M1, M2] |
140 | exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs |
182 | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms |
141 | exists_alpha_sub_ctype (CRec _) = true |
183 | exists_alpha_sub_mtype (MRec _) = true |
142 |
184 |
143 (* ctype -> bool *) |
185 (* mtyp -> bool *) |
144 fun exists_alpha_sub_ctype_fresh CAlpha = true |
186 fun exists_alpha_sub_mtype_fresh MAlpha = true |
145 | exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true |
187 | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true |
146 | exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) = |
188 | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) = |
147 exists_alpha_sub_ctype_fresh C2 |
189 exists_alpha_sub_mtype_fresh M2 |
148 | exists_alpha_sub_ctype_fresh (CPair (C1, C2)) = |
190 | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) = |
149 exists exists_alpha_sub_ctype_fresh [C1, C2] |
191 exists exists_alpha_sub_mtype_fresh [M1, M2] |
150 | exists_alpha_sub_ctype_fresh (CType (_, Cs)) = |
192 | exists_alpha_sub_mtype_fresh (MType (_, Ms)) = |
151 exists exists_alpha_sub_ctype_fresh Cs |
193 exists exists_alpha_sub_mtype_fresh Ms |
152 | exists_alpha_sub_ctype_fresh (CRec _) = true |
194 | exists_alpha_sub_mtype_fresh (MRec _) = true |
153 |
195 |
154 (* string * typ list -> ctype list -> ctype *) |
196 (* string * typ list -> mtyp list -> mtyp *) |
155 fun constr_ctype_for_binders z Cs = |
197 fun constr_mtype_for_binders z Ms = |
156 fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z) |
198 fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z) |
157 |
199 |
158 (* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *) |
200 (* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *) |
159 fun repair_ctype _ _ CAlpha = CAlpha |
201 fun repair_mtype _ _ MAlpha = MAlpha |
160 | repair_ctype cache seen (CFun (C1, a, C2)) = |
202 | repair_mtype cache seen (MFun (M1, a, M2)) = |
161 CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2) |
203 MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2) |
162 | repair_ctype cache seen (CPair Cp) = |
204 | repair_mtype cache seen (MPair Mp) = |
163 CPair (pairself (repair_ctype cache seen) Cp) |
205 MPair (pairself (repair_mtype cache seen) Mp) |
164 | repair_ctype cache seen (CType (s, Cs)) = |
206 | repair_mtype cache seen (MType (s, Ms)) = |
165 CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs) |
207 MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms) |
166 | repair_ctype cache seen (CRec (z as (s, _))) = |
208 | repair_mtype cache seen (MRec (z as (s, _))) = |
167 case AList.lookup (op =) cache z |> the of |
209 case AList.lookup (op =) cache z |> the of |
168 CRec _ => CType (s, []) |
210 MRec _ => MType (s, []) |
169 | C => if member (op =) seen C then CType (s, []) |
211 | M => if member (op =) seen M then MType (s, []) |
170 else repair_ctype cache (C :: seen) C |
212 else repair_mtype cache (M :: seen) M |
171 |
213 |
172 (* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *) |
214 (* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *) |
173 fun repair_datatype_cache cache = |
215 fun repair_datatype_cache cache = |
174 let |
216 let |
175 (* (string * typ list) * ctype -> unit *) |
217 (* (string * typ list) * mtyp -> unit *) |
176 fun repair_one (z, C) = |
218 fun repair_one (z, M) = |
177 Unsynchronized.change cache |
219 Unsynchronized.change cache |
178 (AList.update (op =) (z, repair_ctype (!cache) [] C)) |
220 (AList.update (op =) (z, repair_mtype (!cache) [] M)) |
179 in List.app repair_one (rev (!cache)) end |
221 in List.app repair_one (rev (!cache)) end |
180 |
222 |
181 (* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *) |
223 (* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *) |
182 fun repair_constr_cache dtype_cache constr_cache = |
224 fun repair_constr_cache dtype_cache constr_cache = |
183 let |
225 let |
184 (* styp * ctype -> unit *) |
226 (* styp * mtyp -> unit *) |
185 fun repair_one (x, C) = |
227 fun repair_one (x, M) = |
186 Unsynchronized.change constr_cache |
228 Unsynchronized.change constr_cache |
187 (AList.update (op =) (x, repair_ctype dtype_cache [] C)) |
229 (AList.update (op =) (x, repair_mtype dtype_cache [] M)) |
188 in List.app repair_one (!constr_cache) end |
230 in List.app repair_one (!constr_cache) end |
189 |
231 |
190 (* cdata -> typ -> ctype *) |
232 (* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *) |
191 fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh, |
233 fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 = |
192 datatype_cache, constr_cache, ...} : cdata) = |
|
193 let |
234 let |
194 (* typ -> typ -> ctype *) |
235 val M1 = fresh_mtype_for_type mdata T1 |
195 fun do_fun T1 T2 = |
236 val M2 = fresh_mtype_for_type mdata T2 |
196 let |
237 val a = if is_boolean_type (body_type T2) andalso |
197 val C1 = do_type T1 |
238 exists_alpha_sub_mtype_fresh M1 then |
198 val C2 = do_type T2 |
239 V (Unsynchronized.inc max_fresh) |
199 val a = if is_boolean_type (body_type T2) andalso |
240 else |
200 exists_alpha_sub_ctype_fresh C1 then |
241 S Minus |
201 V (Unsynchronized.inc max_fresh) |
242 in (M1, a, M2) end |
202 else |
243 (* mdata -> typ -> mtyp *) |
203 S Minus |
244 and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, |
204 in CFun (C1, a, C2) end |
245 datatype_cache, constr_cache, ...}) = |
205 (* typ -> ctype *) |
246 let |
206 and do_type T = |
247 (* typ -> typ -> mtyp *) |
|
248 val do_fun = MFun oo fresh_mfun_for_fun_type mdata |
|
249 (* typ -> mtyp *) |
|
250 fun do_type T = |
207 if T = alpha_T then |
251 if T = alpha_T then |
208 CAlpha |
252 MAlpha |
209 else case T of |
253 else case T of |
210 Type ("fun", [T1, T2]) => do_fun T1 T2 |
254 Type ("fun", [T1, T2]) => do_fun T1 T2 |
211 | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2 |
255 | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2 |
212 | Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2)) |
256 | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2)) |
213 | Type (z as (s, _)) => |
257 | Type (z as (s, _)) => |
214 if could_exist_alpha_sub_ctype thy alpha_T T then |
258 if could_exist_alpha_sub_mtype thy alpha_T T then |
215 case AList.lookup (op =) (!datatype_cache) z of |
259 case AList.lookup (op =) (!datatype_cache) z of |
216 SOME C => C |
260 SOME M => M |
217 | NONE => |
261 | NONE => |
218 let |
262 let |
219 val _ = Unsynchronized.change datatype_cache (cons (z, CRec z)) |
263 val _ = Unsynchronized.change datatype_cache (cons (z, MRec z)) |
220 val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T |
264 val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T |
221 val (all_Cs, constr_Cs) = |
265 val (all_Ms, constr_Ms) = |
222 fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) => |
266 fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) => |
223 let |
267 let |
224 val binder_Cs = map do_type (binder_types T') |
268 val binder_Ms = map do_type (binder_types T') |
225 val new_Cs = filter exists_alpha_sub_ctype_fresh |
269 val new_Ms = filter exists_alpha_sub_mtype_fresh |
226 binder_Cs |
270 binder_Ms |
227 val constr_C = constr_ctype_for_binders z |
271 val constr_M = constr_mtype_for_binders z |
228 binder_Cs |
272 binder_Ms |
229 in |
273 in |
230 (union (op =) new_Cs all_Cs, |
274 (union (op =) new_Ms all_Ms, |
231 constr_C :: constr_Cs) |
275 constr_M :: constr_Ms) |
232 end) |
276 end) |
233 xs ([], []) |
277 xs ([], []) |
234 val C = CType (s, all_Cs) |
278 val M = MType (s, all_Ms) |
235 val _ = Unsynchronized.change datatype_cache |
279 val _ = Unsynchronized.change datatype_cache |
236 (AList.update (op =) (z, C)) |
280 (AList.update (op =) (z, M)) |
237 val _ = Unsynchronized.change constr_cache |
281 val _ = Unsynchronized.change constr_cache |
238 (append (xs ~~ constr_Cs)) |
282 (append (xs ~~ constr_Ms)) |
239 in |
283 in |
240 if forall (not o is_CRec o snd) (!datatype_cache) then |
284 if forall (not o is_MRec o snd) (!datatype_cache) then |
241 (repair_datatype_cache datatype_cache; |
285 (repair_datatype_cache datatype_cache; |
242 repair_constr_cache (!datatype_cache) constr_cache; |
286 repair_constr_cache (!datatype_cache) constr_cache; |
243 AList.lookup (op =) (!datatype_cache) z |> the) |
287 AList.lookup (op =) (!datatype_cache) z |> the) |
244 else |
288 else |
245 C |
289 M |
246 end |
290 end |
247 else |
291 else |
248 CType (s, []) |
292 MType (s, []) |
249 | _ => CType (Refute.string_of_typ T, []) |
293 | _ => MType (Refute.string_of_typ T, []) |
250 in do_type end |
294 in do_type end |
251 |
295 |
252 (* ctype -> ctype list *) |
296 (* mtyp -> mtyp list *) |
253 fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2] |
297 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2] |
254 | prodC_factors C = [C] |
298 | prodM_factors M = [M] |
255 (* ctype -> ctype list * ctype *) |
299 (* mtyp -> mtyp list * mtyp *) |
256 fun curried_strip_ctype (CFun (C1, S Minus, C2)) = |
300 fun curried_strip_mtype (MFun (M1, S Minus, M2)) = |
257 curried_strip_ctype C2 |>> append (prodC_factors C1) |
301 curried_strip_mtype M2 |>> append (prodM_factors M1) |
258 | curried_strip_ctype C = ([], C) |
302 | curried_strip_mtype M = ([], M) |
259 (* string -> ctype -> ctype *) |
303 (* string -> mtyp -> mtyp *) |
260 fun sel_ctype_from_constr_ctype s C = |
304 fun sel_mtype_from_constr_mtype s M = |
261 let val (arg_Cs, dataC) = curried_strip_ctype C in |
305 let val (arg_Ms, dataM) = curried_strip_mtype M in |
262 CFun (dataC, S Minus, |
306 MFun (dataM, S Minus, |
263 case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n) |
307 case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n) |
264 end |
308 end |
265 |
309 |
266 (* cdata -> styp -> ctype *) |
310 (* mdata -> styp -> mtyp *) |
267 fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache, |
311 fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache, |
268 ...}) (x as (_, T)) = |
312 ...}) (x as (_, T)) = |
269 if could_exist_alpha_sub_ctype thy alpha_T T then |
313 if could_exist_alpha_sub_mtype thy alpha_T T then |
270 case AList.lookup (op =) (!constr_cache) x of |
314 case AList.lookup (op =) (!constr_cache) x of |
271 SOME C => C |
315 SOME M => M |
272 | NONE => if T = alpha_T then |
316 | NONE => if T = alpha_T then |
273 let val C = fresh_ctype_for_type cdata T in |
317 let val M = fresh_mtype_for_type mdata T in |
274 (Unsynchronized.change constr_cache (cons (x, C)); C) |
318 (Unsynchronized.change constr_cache (cons (x, M)); M) |
275 end |
319 end |
276 else |
320 else |
277 (fresh_ctype_for_type cdata (body_type T); |
321 (fresh_mtype_for_type mdata (body_type T); |
278 AList.lookup (op =) (!constr_cache) x |> the) |
322 AList.lookup (op =) (!constr_cache) x |> the) |
279 else |
323 else |
280 fresh_ctype_for_type cdata T |
324 fresh_mtype_for_type mdata T |
281 fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = |
325 fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = |
282 x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize |
326 x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize |
283 |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s |
327 |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s |
284 |
328 |
285 (* literal list -> ctype -> ctype *) |
329 (* literal list -> mtyp -> mtyp *) |
286 fun instantiate_ctype lits = |
330 fun instantiate_mtype lits = |
287 let |
331 let |
288 (* ctype -> ctype *) |
332 (* mtyp -> mtyp *) |
289 fun aux CAlpha = CAlpha |
333 fun aux MAlpha = MAlpha |
290 | aux (CFun (C1, V x, C2)) = |
334 | aux (MFun (M1, V x, M2)) = |
291 let |
335 let |
292 val a = case AList.lookup (op =) lits x of |
336 val a = case AList.lookup (op =) lits x of |
293 SOME sn => S sn |
337 SOME sn => S sn |
294 | NONE => V x |
338 | NONE => V x |
295 in CFun (aux C1, a, aux C2) end |
339 in MFun (aux M1, a, aux M2) end |
296 | aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2) |
340 | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2) |
297 | aux (CPair Cp) = CPair (pairself aux Cp) |
341 | aux (MPair Mp) = MPair (pairself aux Mp) |
298 | aux (CType (s, Cs)) = CType (s, map aux Cs) |
342 | aux (MType (s, Ms)) = MType (s, map aux Ms) |
299 | aux (CRec z) = CRec z |
343 | aux (MRec z) = MRec z |
300 in aux end |
344 in aux end |
301 |
345 |
302 datatype comp_op = Eq | Leq |
346 datatype comp_op = Eq | Leq |
303 |
347 |
304 type comp = sign_atom * sign_atom * comp_op * var list |
348 type comp = sign_atom * sign_atom * comp_op * var list |
344 | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps) |
388 | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps) |
345 | _ => do_sign_atom_comp Eq [] a1 a2 accum) |
389 | _ => do_sign_atom_comp Eq [] a1 a2 accum) |
346 | do_sign_atom_comp cmp xs a1 a2 (lits, comps) = |
390 | do_sign_atom_comp cmp xs a1 a2 (lits, comps) = |
347 SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) |
391 SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) |
348 |
392 |
349 (* comp -> var list -> ctype -> ctype -> (literal list * comp list) option |
393 (* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option |
350 -> (literal list * comp list) option *) |
394 -> (literal list * comp list) option *) |
351 fun do_ctype_comp _ _ _ _ NONE = NONE |
395 fun do_mtype_comp _ _ _ _ NONE = NONE |
352 | do_ctype_comp _ _ CAlpha CAlpha accum = accum |
396 | do_mtype_comp _ _ MAlpha MAlpha accum = accum |
353 | do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22)) |
397 | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) |
354 (SOME accum) = |
398 (SOME accum) = |
355 accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21 |
399 accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21 |
356 |> do_ctype_comp Eq xs C12 C22 |
400 |> do_mtype_comp Eq xs M12 M22 |
357 | do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22)) |
401 | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) |
358 (SOME accum) = |
402 (SOME accum) = |
359 (if exists_alpha_sub_ctype C11 then |
403 (if exists_alpha_sub_mtype M11 then |
360 accum |> do_sign_atom_comp Leq xs a1 a2 |
404 accum |> do_sign_atom_comp Leq xs a1 a2 |
361 |> do_ctype_comp Leq xs C21 C11 |
405 |> do_mtype_comp Leq xs M21 M11 |
362 |> (case a2 of |
406 |> (case a2 of |
363 S Minus => I |
407 S Minus => I |
364 | S Plus => do_ctype_comp Leq xs C11 C21 |
408 | S Plus => do_mtype_comp Leq xs M11 M21 |
365 | V x => do_ctype_comp Leq (x :: xs) C11 C21) |
409 | V x => do_mtype_comp Leq (x :: xs) M11 M21) |
366 else |
410 else |
367 SOME accum) |
411 SOME accum) |
368 |> do_ctype_comp Leq xs C12 C22 |
412 |> do_mtype_comp Leq xs M12 M22 |
369 | do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22)) |
413 | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22)) |
370 accum = |
414 accum = |
371 (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)] |
415 (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)] |
372 handle Library.UnequalLengths => |
416 handle Library.UnequalLengths => |
373 raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])) |
417 raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])) |
374 | do_ctype_comp _ _ (CType _) (CType _) accum = |
418 | do_mtype_comp _ _ (MType _) (MType _) accum = |
375 accum (* no need to compare them thanks to the cache *) |
419 accum (* no need to compare them thanks to the cache *) |
376 | do_ctype_comp _ _ C1 C2 _ = |
420 | do_mtype_comp _ _ M1 M2 _ = |
377 raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]) |
421 raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]) |
378 |
422 |
379 (* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *) |
423 (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *) |
380 fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet |
424 fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet |
381 | add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) = |
425 | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) = |
382 (print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^ |
426 (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^ |
383 " " ^ string_for_ctype C2); |
427 " " ^ string_for_mtype M2); |
384 case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of |
428 case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of |
385 NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
429 NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
386 | SOME (lits, comps) => CSet (lits, comps, sexps)) |
430 | SOME (lits, comps) => CSet (lits, comps, sexps)) |
387 |
431 |
388 (* ctype -> ctype -> constraint_set -> constraint_set *) |
432 (* mtyp -> mtyp -> constraint_set -> constraint_set *) |
389 val add_ctypes_equal = add_ctype_comp Eq |
433 val add_mtypes_equal = add_mtype_comp Eq |
390 val add_is_sub_ctype = add_ctype_comp Leq |
434 val add_is_sub_mtype = add_mtype_comp Leq |
391 |
435 |
392 (* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option |
436 (* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option |
393 -> (literal list * sign_expr list) option *) |
437 -> (literal list * sign_expr list) option *) |
394 fun do_notin_ctype_fv _ _ _ NONE = NONE |
438 fun do_notin_mtype_fv _ _ _ NONE = NONE |
395 | do_notin_ctype_fv Minus _ CAlpha accum = accum |
439 | do_notin_mtype_fv Minus _ MAlpha accum = accum |
396 | do_notin_ctype_fv Plus [] CAlpha _ = NONE |
440 | do_notin_mtype_fv Plus [] MAlpha _ = NONE |
397 | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) = |
441 | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) = |
398 SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps) |
442 SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps) |
399 | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) = |
443 | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) = |
400 SOME (lits, insert (op =) sexp sexps) |
444 SOME (lits, insert (op =) sexp sexps) |
401 | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum = |
445 | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum = |
402 accum |> (if sn' = Plus andalso sn = Plus then |
446 accum |> (if sn' = Plus andalso sn = Plus then |
403 do_notin_ctype_fv Plus sexp C1 |
447 do_notin_mtype_fv Plus sexp M1 |
404 else |
448 else |
405 I) |
449 I) |
406 |> (if sn' = Minus orelse sn = Plus then |
450 |> (if sn' = Minus orelse sn = Plus then |
407 do_notin_ctype_fv Minus sexp C1 |
451 do_notin_mtype_fv Minus sexp M1 |
408 else |
452 else |
409 I) |
453 I) |
410 |> do_notin_ctype_fv sn sexp C2 |
454 |> do_notin_mtype_fv sn sexp M2 |
411 | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum = |
455 | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum = |
412 accum |> (case do_literal (x, Minus) (SOME sexp) of |
456 accum |> (case do_literal (x, Minus) (SOME sexp) of |
413 NONE => I |
457 NONE => I |
414 | SOME sexp' => do_notin_ctype_fv Plus sexp' C1) |
458 | SOME sexp' => do_notin_mtype_fv Plus sexp' M1) |
415 |> do_notin_ctype_fv Minus sexp C1 |
459 |> do_notin_mtype_fv Minus sexp M1 |
416 |> do_notin_ctype_fv Plus sexp C2 |
460 |> do_notin_mtype_fv Plus sexp M2 |
417 | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum = |
461 | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum = |
418 accum |> (case do_literal (x, Plus) (SOME sexp) of |
462 accum |> (case do_literal (x, Plus) (SOME sexp) of |
419 NONE => I |
463 NONE => I |
420 | SOME sexp' => do_notin_ctype_fv Plus sexp' C1) |
464 | SOME sexp' => do_notin_mtype_fv Plus sexp' M1) |
421 |> do_notin_ctype_fv Minus sexp C2 |
465 |> do_notin_mtype_fv Minus sexp M2 |
422 | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum = |
466 | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum = |
423 accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2] |
467 accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2] |
424 | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum = |
468 | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum = |
425 accum |> fold (do_notin_ctype_fv sn sexp) Cs |
469 accum |> fold (do_notin_mtype_fv sn sexp) Ms |
426 | do_notin_ctype_fv _ _ C _ = |
470 | do_notin_mtype_fv _ _ M _ = |
427 raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C]) |
471 raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M]) |
428 |
472 |
429 (* sign -> ctype -> constraint_set -> constraint_set *) |
473 (* sign -> mtyp -> constraint_set -> constraint_set *) |
430 fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet |
474 fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet |
431 | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) = |
475 | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) = |
432 (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^ |
476 (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^ |
433 (case sn of Minus => "unique" | Plus => "total") ^ "."); |
477 (case sn of Minus => "unique" | Plus => "total") ^ "."); |
434 case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of |
478 case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of |
435 NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
479 NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
436 | SOME (lits, sexps) => CSet (lits, comps, sexps)) |
480 | SOME (lits, sexps) => CSet (lits, comps, sexps)) |
437 |
481 |
438 (* ctype -> constraint_set -> constraint_set *) |
482 (* mtyp -> constraint_set -> constraint_set *) |
439 val add_ctype_is_right_unique = add_notin_ctype_fv Minus |
483 val add_mtype_is_right_unique = add_notin_mtype_fv Minus |
440 val add_ctype_is_right_total = add_notin_ctype_fv Plus |
484 val add_mtype_is_right_total = add_notin_mtype_fv Plus |
441 |
485 |
442 val bool_from_minus = true |
486 val bool_from_minus = true |
443 |
487 |
444 (* sign -> bool *) |
488 (* sign -> bool *) |
445 fun bool_from_sign Plus = not bool_from_minus |
489 fun bool_from_sign Plus = not bool_from_minus |
514 SOME (literals_from_assignments max_var assigns lits |
558 SOME (literals_from_assignments max_var assigns lits |
515 |> tap print_solution) |
559 |> tap print_solution) |
516 | _ => NONE |
560 | _ => NONE |
517 end |
561 end |
518 |
562 |
519 type ctype_schema = ctype * constraint_set |
563 type mtype_schema = mtyp * constraint_set |
520 type ctype_context = |
564 type mtype_context = |
521 {bounds: ctype list, |
565 {bounds: mtyp list, |
522 frees: (styp * ctype) list, |
566 frees: (styp * mtyp) list, |
523 consts: (styp * ctype) list} |
567 consts: (styp * mtyp) list} |
524 |
568 |
525 type accumulator = ctype_context * constraint_set |
569 type accumulator = mtype_context * constraint_set |
526 |
570 |
527 val initial_gamma = {bounds = [], frees = [], consts = []} |
571 val initial_gamma = {bounds = [], frees = [], consts = []} |
528 val unsolvable_accum = (initial_gamma, UnsolvableCSet) |
572 val unsolvable_accum = (initial_gamma, UnsolvableCSet) |
529 |
573 |
530 (* ctype -> ctype_context -> ctype_context *) |
574 (* mtyp -> mtype_context -> mtype_context *) |
531 fun push_bound C {bounds, frees, consts} = |
575 fun push_bound M {bounds, frees, consts} = |
532 {bounds = C :: bounds, frees = frees, consts = consts} |
576 {bounds = M :: bounds, frees = frees, consts = consts} |
533 (* ctype_context -> ctype_context *) |
577 (* mtype_context -> mtype_context *) |
534 fun pop_bound {bounds, frees, consts} = |
578 fun pop_bound {bounds, frees, consts} = |
535 {bounds = tl bounds, frees = frees, consts = consts} |
579 {bounds = tl bounds, frees = frees, consts = consts} |
536 handle List.Empty => initial_gamma |
580 handle List.Empty => initial_gamma |
537 |
581 |
538 (* cdata -> term -> accumulator -> ctype * accumulator *) |
582 (* mdata -> term -> accumulator -> mterm * accumulator *) |
539 fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, |
583 fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, |
540 def_table, ...}, |
584 def_table, ...}, |
541 alpha_T, max_fresh, ...}) = |
585 alpha_T, max_fresh, ...}) = |
542 let |
586 let |
543 (* typ -> ctype *) |
587 (* typ -> typ -> mtyp * sign_atom * mtyp *) |
544 val ctype_for = fresh_ctype_for_type cdata |
588 val mfun_for = fresh_mfun_for_fun_type mdata |
545 (* ctype -> ctype *) |
589 (* typ -> mtyp *) |
546 fun pos_set_ctype_for_dom C = |
590 val mtype_for = fresh_mtype_for_type mdata |
547 CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C) |
591 (* mtyp -> mtyp *) |
548 (* typ -> accumulator -> ctype * accumulator *) |
592 fun pos_set_mtype_for_dom M = |
549 fun do_quantifier T (gamma, cset) = |
593 MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M) |
|
594 (* typ -> accumulator -> mterm * accumulator *) |
|
595 fun do_all T (gamma, cset) = |
550 let |
596 let |
551 val abs_C = ctype_for (domain_type (domain_type T)) |
597 val abs_M = mtype_for (domain_type (domain_type T)) |
552 val body_C = ctype_for (range_type T) |
598 val body_M = mtype_for (range_type T) |
553 in |
599 in |
554 (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C), |
600 (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M), |
555 (gamma, cset |> add_ctype_is_right_total abs_C)) |
601 (gamma, cset |> add_mtype_is_right_total abs_M)) |
556 end |
602 end |
557 fun do_equals T (gamma, cset) = |
603 fun do_equals T (gamma, cset) = |
558 let val C = ctype_for (domain_type T) in |
604 let val M = mtype_for (domain_type T) in |
559 (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh), |
605 (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh), |
560 ctype_for (nth_range_type 2 T))), |
606 mtype_for (nth_range_type 2 T))), |
561 (gamma, cset |> add_ctype_is_right_unique C)) |
607 (gamma, cset |> add_mtype_is_right_unique M)) |
562 end |
608 end |
563 fun do_robust_set_operation T (gamma, cset) = |
609 fun do_robust_set_operation T (gamma, cset) = |
564 let |
610 let |
565 val set_T = domain_type T |
611 val set_T = domain_type T |
566 val C1 = ctype_for set_T |
612 val M1 = mtype_for set_T |
567 val C2 = ctype_for set_T |
613 val M2 = mtype_for set_T |
568 val C3 = ctype_for set_T |
614 val M3 = mtype_for set_T |
569 in |
615 in |
570 (CFun (C1, S Minus, CFun (C2, S Minus, C3)), |
616 (MFun (M1, S Minus, MFun (M2, S Minus, M3)), |
571 (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3)) |
617 (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3)) |
572 end |
618 end |
573 fun do_fragile_set_operation T (gamma, cset) = |
619 fun do_fragile_set_operation T (gamma, cset) = |
574 let |
620 let |
575 val set_T = domain_type T |
621 val set_T = domain_type T |
576 val set_C = ctype_for set_T |
622 val set_M = mtype_for set_T |
577 (* typ -> ctype *) |
623 (* typ -> mtyp *) |
578 fun custom_ctype_for (T as Type ("fun", [T1, T2])) = |
624 fun custom_mtype_for (T as Type ("fun", [T1, T2])) = |
579 if T = set_T then set_C |
625 if T = set_T then set_M |
580 else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2) |
626 else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2) |
581 | custom_ctype_for T = ctype_for T |
627 | custom_mtype_for T = mtype_for T |
582 in |
628 in |
583 (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C)) |
629 (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M)) |
584 end |
630 end |
585 (* typ -> accumulator -> ctype * accumulator *) |
631 (* typ -> accumulator -> mtyp * accumulator *) |
586 fun do_pair_constr T accum = |
632 fun do_pair_constr T accum = |
587 case ctype_for (nth_range_type 2 T) of |
633 case mtype_for (nth_range_type 2 T) of |
588 C as CPair (a_C, b_C) => |
634 M as MPair (a_M, b_M) => |
589 (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum) |
635 (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum) |
590 | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C]) |
636 | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M]) |
591 (* int -> typ -> accumulator -> ctype * accumulator *) |
637 (* int -> typ -> accumulator -> mtyp * accumulator *) |
592 fun do_nth_pair_sel n T = |
638 fun do_nth_pair_sel n T = |
593 case ctype_for (domain_type T) of |
639 case mtype_for (domain_type T) of |
594 C as CPair (a_C, b_C) => |
640 M as MPair (a_M, b_M) => |
595 pair (CFun (C, S Minus, if n = 0 then a_C else b_C)) |
641 pair (MFun (M, S Minus, if n = 0 then a_M else b_M)) |
596 | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C]) |
642 | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M]) |
597 val unsolvable = (CType ("unsolvable", []), unsolvable_accum) |
643 (* mtyp * accumulator *) |
598 (* typ -> term -> accumulator -> ctype * accumulator *) |
644 val mtype_unsolvable = (irrelevant_M, unsolvable_accum) |
599 fun do_bounded_quantifier abs_T bound_t body_t accum = |
645 (* term -> mterm * accumulator *) |
|
646 fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum) |
|
647 (* term -> string -> typ -> term -> term -> term -> accumulator |
|
648 -> mterm * accumulator *) |
|
649 fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum = |
600 let |
650 let |
601 val abs_C = ctype_for abs_T |
651 val abs_M = mtype_for abs_T |
602 val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t |
652 val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t |
603 val expected_bound_C = pos_set_ctype_for_dom abs_C |
653 val expected_bound_M = pos_set_mtype_for_dom abs_M |
|
654 val (body_m, accum) = |
|
655 accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m) |
|
656 |> do_term body_t ||> apfst pop_bound |
|
657 val bound_M = mtype_of_mterm bound_m |
|
658 val (M1, a, M2) = dest_MFun bound_M |
604 in |
659 in |
605 accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t |
660 (MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)), |
606 ||> apfst pop_bound |
661 MAbs (abs_s, abs_T, M1, a, |
|
662 MApp (MApp (MAtom (connective_t, irrelevant_M), |
|
663 MApp (bound_m, MAtom (Bound 0, M1))), |
|
664 body_m))), accum) |
607 end |
665 end |
608 (* term -> accumulator -> ctype * accumulator *) |
666 (* term -> accumulator -> mterm * accumulator *) |
609 and do_term _ (_, UnsolvableCSet) = unsolvable |
667 and do_term t (_, UnsolvableCSet) = mterm_unsolvable t |
610 | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) = |
668 | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) = |
611 (case t of |
669 (case t of |
612 Const (x as (s, T)) => |
670 Const (x as (s, T)) => |
613 (case AList.lookup (op =) consts x of |
671 (case AList.lookup (op =) consts x of |
614 SOME C => (C, accum) |
672 SOME M => (M, accum) |
615 | NONE => |
673 | NONE => |
616 if not (could_exist_alpha_subtype alpha_T T) then |
674 if not (could_exist_alpha_subtype alpha_T T) then |
617 (ctype_for T, accum) |
675 (mtype_for T, accum) |
618 else case s of |
676 else case s of |
619 @{const_name all} => do_quantifier T accum |
677 @{const_name all} => do_all T accum |
620 | @{const_name "=="} => do_equals T accum |
678 | @{const_name "=="} => do_equals T accum |
621 | @{const_name All} => do_quantifier T accum |
679 | @{const_name All} => do_all T accum |
622 | @{const_name Ex} => do_quantifier T accum |
680 | @{const_name Ex} => |
|
681 do_term (@{const Not} |
|
682 $ (HOLogic.eq_const (domain_type T) |
|
683 $ Abs (Name.uu, T, @{const False}))) accum |
|
684 |>> mtype_of_mterm |
623 | @{const_name "op ="} => do_equals T accum |
685 | @{const_name "op ="} => do_equals T accum |
624 | @{const_name The} => (print_g "*** The"; unsolvable) |
686 | @{const_name The} => (print_g "*** The"; mtype_unsolvable) |
625 | @{const_name Eps} => (print_g "*** Eps"; unsolvable) |
687 | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable) |
626 | @{const_name If} => |
688 | @{const_name If} => |
627 do_robust_set_operation (range_type T) accum |
689 do_robust_set_operation (range_type T) accum |
628 |>> curry3 CFun bool_C (S Minus) |
690 |>> curry3 MFun bool_M (S Minus) |
629 | @{const_name Pair} => do_pair_constr T accum |
691 | @{const_name Pair} => do_pair_constr T accum |
630 | @{const_name fst} => do_nth_pair_sel 0 T accum |
692 | @{const_name fst} => do_nth_pair_sel 0 T accum |
631 | @{const_name snd} => do_nth_pair_sel 1 T accum |
693 | @{const_name snd} => do_nth_pair_sel 1 T accum |
632 | @{const_name Id} => |
694 | @{const_name Id} => |
633 (CFun (ctype_for (domain_type T), S Minus, bool_C), accum) |
695 (MFun (mtype_for (domain_type T), S Minus, bool_M), accum) |
634 | @{const_name insert} => |
696 | @{const_name insert} => |
635 let |
697 let |
636 val set_T = domain_type (range_type T) |
698 val set_T = domain_type (range_type T) |
637 val C1 = ctype_for (domain_type set_T) |
699 val M1 = mtype_for (domain_type set_T) |
638 val C1' = pos_set_ctype_for_dom C1 |
700 val M1' = pos_set_mtype_for_dom M1 |
639 val C2 = ctype_for set_T |
701 val M2 = mtype_for set_T |
640 val C3 = ctype_for set_T |
702 val M3 = mtype_for set_T |
641 in |
703 in |
642 (CFun (C1, S Minus, CFun (C2, S Minus, C3)), |
704 (MFun (M1, S Minus, MFun (M2, S Minus, M3)), |
643 (gamma, cset |> add_ctype_is_right_unique C1 |
705 (gamma, cset |> add_mtype_is_right_unique M1 |
644 |> add_is_sub_ctype C1' C3 |
706 |> add_is_sub_mtype M1' M3 |
645 |> add_is_sub_ctype C2 C3)) |
707 |> add_is_sub_mtype M2 M3)) |
646 end |
708 end |
647 | @{const_name converse} => |
709 | @{const_name converse} => |
648 let |
710 let |
649 val x = Unsynchronized.inc max_fresh |
711 val x = Unsynchronized.inc max_fresh |
650 (* typ -> ctype *) |
712 (* typ -> mtyp *) |
651 fun ctype_for_set T = |
713 fun mtype_for_set T = |
652 CFun (ctype_for (domain_type T), V x, bool_C) |
714 MFun (mtype_for (domain_type T), V x, bool_M) |
653 val ab_set_C = domain_type T |> ctype_for_set |
715 val ab_set_M = domain_type T |> mtype_for_set |
654 val ba_set_C = range_type T |> ctype_for_set |
716 val ba_set_M = range_type T |> mtype_for_set |
655 in (CFun (ab_set_C, S Minus, ba_set_C), accum) end |
717 in (MFun (ab_set_M, S Minus, ba_set_M), accum) end |
656 | @{const_name trancl} => do_fragile_set_operation T accum |
718 | @{const_name trancl} => do_fragile_set_operation T accum |
657 | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable) |
719 | @{const_name rtrancl} => |
|
720 (print_g "*** rtrancl"; mtype_unsolvable) |
658 | @{const_name finite} => |
721 | @{const_name finite} => |
659 let val C1 = ctype_for (domain_type (domain_type T)) in |
722 let val M1 = mtype_for (domain_type (domain_type T)) in |
660 (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum) |
723 (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum) |
661 end |
724 end |
662 | @{const_name rel_comp} => |
725 | @{const_name rel_comp} => |
663 let |
726 let |
664 val x = Unsynchronized.inc max_fresh |
727 val x = Unsynchronized.inc max_fresh |
665 (* typ -> ctype *) |
728 (* typ -> mtyp *) |
666 fun ctype_for_set T = |
729 fun mtype_for_set T = |
667 CFun (ctype_for (domain_type T), V x, bool_C) |
730 MFun (mtype_for (domain_type T), V x, bool_M) |
668 val bc_set_C = domain_type T |> ctype_for_set |
731 val bc_set_M = domain_type T |> mtype_for_set |
669 val ab_set_C = domain_type (range_type T) |> ctype_for_set |
732 val ab_set_M = domain_type (range_type T) |> mtype_for_set |
670 val ac_set_C = nth_range_type 2 T |> ctype_for_set |
733 val ac_set_M = nth_range_type 2 T |> mtype_for_set |
671 in |
734 in |
672 (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)), |
735 (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)), |
673 accum) |
736 accum) |
674 end |
737 end |
675 | @{const_name image} => |
738 | @{const_name image} => |
676 let |
739 let |
677 val a_C = ctype_for (domain_type (domain_type T)) |
740 val a_M = mtype_for (domain_type (domain_type T)) |
678 val b_C = ctype_for (range_type (domain_type T)) |
741 val b_M = mtype_for (range_type (domain_type T)) |
679 in |
742 in |
680 (CFun (CFun (a_C, S Minus, b_C), S Minus, |
743 (MFun (MFun (a_M, S Minus, b_M), S Minus, |
681 CFun (pos_set_ctype_for_dom a_C, S Minus, |
744 MFun (pos_set_mtype_for_dom a_M, S Minus, |
682 pos_set_ctype_for_dom b_C)), accum) |
745 pos_set_mtype_for_dom b_M)), accum) |
683 end |
746 end |
684 | @{const_name Sigma} => |
747 | @{const_name Sigma} => |
685 let |
748 let |
686 val x = Unsynchronized.inc max_fresh |
749 val x = Unsynchronized.inc max_fresh |
687 (* typ -> ctype *) |
750 (* typ -> mtyp *) |
688 fun ctype_for_set T = |
751 fun mtype_for_set T = |
689 CFun (ctype_for (domain_type T), V x, bool_C) |
752 MFun (mtype_for (domain_type T), V x, bool_M) |
690 val a_set_T = domain_type T |
753 val a_set_T = domain_type T |
691 val a_C = ctype_for (domain_type a_set_T) |
754 val a_M = mtype_for (domain_type a_set_T) |
692 val b_set_C = ctype_for_set (range_type (domain_type |
755 val b_set_M = mtype_for_set (range_type (domain_type |
693 (range_type T))) |
756 (range_type T))) |
694 val a_set_C = ctype_for_set a_set_T |
757 val a_set_M = mtype_for_set a_set_T |
695 val a_to_b_set_C = CFun (a_C, S Minus, b_set_C) |
758 val a_to_b_set_M = MFun (a_M, S Minus, b_set_M) |
696 val ab_set_C = ctype_for_set (nth_range_type 2 T) |
759 val ab_set_M = mtype_for_set (nth_range_type 2 T) |
697 in |
760 in |
698 (CFun (a_set_C, S Minus, |
761 (MFun (a_set_M, S Minus, |
699 CFun (a_to_b_set_C, S Minus, ab_set_C)), accum) |
762 MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) |
700 end |
763 end |
701 | @{const_name Tha} => |
764 | @{const_name Tha} => |
702 let |
765 let |
703 val a_C = ctype_for (domain_type (domain_type T)) |
766 val a_M = mtype_for (domain_type (domain_type T)) |
704 val a_set_C = pos_set_ctype_for_dom a_C |
767 val a_set_M = pos_set_mtype_for_dom a_M |
705 in (CFun (a_set_C, S Minus, a_C), accum) end |
768 in (MFun (a_set_M, S Minus, a_M), accum) end |
706 | @{const_name FunBox} => |
769 | @{const_name FunBox} => |
707 let val dom_C = ctype_for (domain_type T) in |
770 let val dom_M = mtype_for (domain_type T) in |
708 (CFun (dom_C, S Minus, dom_C), accum) |
771 (MFun (dom_M, S Minus, dom_M), accum) |
709 end |
772 end |
710 | _ => |
773 | _ => |
711 if s = @{const_name minus_class.minus} andalso |
774 if s = @{const_name minus_class.minus} andalso |
712 is_set_type (domain_type T) then |
775 is_set_type (domain_type T) then |
713 let |
776 let |
714 val set_T = domain_type T |
777 val set_T = domain_type T |
715 val left_set_C = ctype_for set_T |
778 val left_set_M = mtype_for set_T |
716 val right_set_C = ctype_for set_T |
779 val right_set_M = mtype_for set_T |
717 in |
780 in |
718 (CFun (left_set_C, S Minus, |
781 (MFun (left_set_M, S Minus, |
719 CFun (right_set_C, S Minus, left_set_C)), |
782 MFun (right_set_M, S Minus, left_set_M)), |
720 (gamma, cset |> add_ctype_is_right_unique right_set_C |
783 (gamma, cset |> add_mtype_is_right_unique right_set_M |
721 |> add_is_sub_ctype right_set_C left_set_C)) |
784 |> add_is_sub_mtype right_set_M left_set_M)) |
722 end |
785 end |
723 else if s = @{const_name ord_class.less_eq} andalso |
786 else if s = @{const_name ord_class.less_eq} andalso |
724 is_set_type (domain_type T) then |
787 is_set_type (domain_type T) then |
725 do_fragile_set_operation T accum |
788 do_fragile_set_operation T accum |
726 else if (s = @{const_name semilattice_inf_class.inf} orelse |
789 else if (s = @{const_name semilattice_inf_class.inf} orelse |
727 s = @{const_name semilattice_sup_class.sup}) andalso |
790 s = @{const_name semilattice_sup_class.sup}) andalso |
728 is_set_type (domain_type T) then |
791 is_set_type (domain_type T) then |
729 do_robust_set_operation T accum |
792 do_robust_set_operation T accum |
730 else if is_sel s then |
793 else if is_sel s then |
731 if constr_name_for_sel_like s = @{const_name FunBox} then |
794 if constr_name_for_sel_like s = @{const_name FunBox} then |
732 let val dom_C = ctype_for (domain_type T) in |
795 let val dom_M = mtype_for (domain_type T) in |
733 (CFun (dom_C, S Minus, dom_C), accum) |
796 (MFun (dom_M, S Minus, dom_M), accum) |
734 end |
797 end |
735 else |
798 else |
736 (ctype_for_sel cdata x, accum) |
799 (mtype_for_sel mdata x, accum) |
737 else if is_constr thy stds x then |
800 else if is_constr thy stds x then |
738 (ctype_for_constr cdata x, accum) |
801 (mtype_for_constr mdata x, accum) |
739 else if is_built_in_const thy stds fast_descrs x then |
802 else if is_built_in_const thy stds fast_descrs x then |
740 case def_of_const thy def_table x of |
803 case def_of_const thy def_table x of |
741 SOME t' => do_term t' accum |
804 SOME t' => do_term t' accum |>> mtype_of_mterm |
742 | NONE => (print_g ("*** built-in " ^ s); unsolvable) |
805 | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable) |
743 else |
806 else |
744 let val C = ctype_for T in |
807 let val M = mtype_for T in |
745 (C, ({bounds = bounds, frees = frees, |
808 (M, ({bounds = bounds, frees = frees, |
746 consts = (x, C) :: consts}, cset)) |
809 consts = (x, M) :: consts}, cset)) |
747 end) |
810 end) |>> curry MAtom t |
748 | Free (x as (_, T)) => |
811 | Free (x as (_, T)) => |
749 (case AList.lookup (op =) frees x of |
812 (case AList.lookup (op =) frees x of |
750 SOME C => (C, accum) |
813 SOME M => (M, accum) |
751 | NONE => |
814 | NONE => |
752 let val C = ctype_for T in |
815 let val M = mtype_for T in |
753 (C, ({bounds = bounds, frees = (x, C) :: frees, |
816 (M, ({bounds = bounds, frees = (x, M) :: frees, |
754 consts = consts}, cset)) |
817 consts = consts}, cset)) |
755 end) |
818 end) |>> curry MAtom t |
756 | Var _ => (print_g "*** Var"; unsolvable) |
819 | Var _ => (print_g "*** Var"; mterm_unsolvable t) |
757 | Bound j => (nth bounds j, accum) |
820 | Bound j => (MAtom (t, nth bounds j), accum) |
758 | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum) |
821 | Abs (s, T, t' as @{const False}) => |
759 | Abs (_, T, t') => |
822 let val (M1, a, M2) = mfun_for T bool_T in |
|
823 (MAbs (s, T, M1, a, MAtom (t', M2)), accum) |
|
824 end |
|
825 | Abs (s, T, t') => |
760 ((case t' of |
826 ((case t' of |
761 t1' $ Bound 0 => |
827 t1' $ Bound 0 => |
762 if not (loose_bvar1 (t1', 0)) then |
828 if not (loose_bvar1 (t1', 0)) then |
763 do_term (incr_boundvars ~1 t1') accum |
829 do_term (incr_boundvars ~1 t1') accum |
764 else |
830 else |
765 raise SAME () |
831 raise SAME () |
766 | _ => raise SAME ()) |
832 | _ => raise SAME ()) |
767 handle SAME () => |
833 handle SAME () => |
768 let |
834 let |
769 val C = ctype_for T |
835 val M = mtype_for T |
770 val (C', accum) = do_term t' (accum |>> push_bound C) |
836 val (m', accum) = do_term t' (accum |>> push_bound M) |
771 in (CFun (C, S Minus, C'), accum |>> pop_bound) end) |
837 in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end) |
772 | Const (@{const_name All}, _) |
838 | (t0 as Const (@{const_name All}, _)) |
773 $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) => |
839 $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) => |
774 do_bounded_quantifier T' t1 t2 accum |
840 do_bounded_quantifier t0 s' T' t10 t11 t12 accum |
775 | Const (@{const_name Ex}, _) |
841 | (t0 as Const (@{const_name Ex}, _)) |
776 $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) => |
842 $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) => |
777 do_bounded_quantifier T' t1 t2 accum |
843 do_bounded_quantifier t0 s' T' t10 t11 t12 accum |
778 | Const (@{const_name Let}, _) $ t1 $ t2 => |
844 | Const (@{const_name Let}, _) $ t1 $ t2 => |
779 do_term (betapply (t2, t1)) accum |
845 do_term (betapply (t2, t1)) accum |
780 | t1 $ t2 => |
846 | t1 $ t2 => |
781 let |
847 let |
782 val (C1, accum) = do_term t1 accum |
848 val (m1, accum) = do_term t1 accum |
783 val (C2, accum) = do_term t2 accum |
849 val (m2, accum) = do_term t2 accum |
784 in |
850 in |
785 case accum of |
851 case accum of |
786 (_, UnsolvableCSet) => unsolvable |
852 (_, UnsolvableCSet) => mterm_unsolvable t |
787 | _ => case C1 of |
853 | _ => (MApp (m1, m2), accum) |
788 CFun (C11, _, C12) => |
|
789 (C12, accum ||> add_is_sub_ctype C2 C11) |
|
790 | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \ |
|
791 \(op $)", [C1]) |
|
792 end) |
854 end) |
793 |> tap (fn (C, _) => |
855 |> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^ |
794 print_g (" \<Gamma> \<turnstile> " ^ |
856 string_for_mterm ctxt m)) |
795 Syntax.string_of_term ctxt t ^ " : " ^ |
|
796 string_for_ctype C)) |
|
797 in do_term end |
857 in do_term end |
798 |
858 |
799 (* cdata -> sign -> term -> accumulator -> accumulator *) |
859 (* mdata -> sign -> term -> accumulator -> accumulator *) |
800 fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) = |
860 fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) = |
801 let |
861 let |
802 (* typ -> ctype *) |
862 (* typ -> mtyp *) |
803 val ctype_for = fresh_ctype_for_type cdata |
863 val mtype_for = fresh_mtype_for_type mdata |
804 (* term -> accumulator -> ctype * accumulator *) |
864 (* term -> accumulator -> mtyp * accumulator *) |
805 val do_term = consider_term cdata |
865 val do_term = apfst mtype_of_mterm oo consider_term mdata |
806 (* sign -> term -> accumulator -> accumulator *) |
866 (* sign -> term -> accumulator -> accumulator *) |
807 fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum |
867 fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum |
808 | do_formula sn t (accum as (gamma, cset)) = |
868 | do_formula sn t (accum as (gamma, cset)) = |
809 let |
869 let |
810 (* term -> accumulator -> accumulator *) |
870 (* term -> accumulator -> accumulator *) |
811 val do_co_formula = do_formula sn |
871 val do_co_formula = do_formula sn |
812 val do_contra_formula = do_formula (negate sn) |
872 val do_contra_formula = do_formula (negate sn) |
813 (* string -> typ -> term -> accumulator *) |
873 (* string -> typ -> term -> accumulator *) |
814 fun do_quantifier quant_s abs_T body_t = |
874 fun do_quantifier quant_s abs_T body_t = |
815 let |
875 let |
816 val abs_C = ctype_for abs_T |
876 val abs_M = mtype_for abs_T |
817 val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) |
877 val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) |
818 val cset = cset |> side_cond ? add_ctype_is_right_total abs_C |
878 val cset = cset |> side_cond ? add_mtype_is_right_total abs_M |
819 in |
879 in |
820 (gamma |> push_bound abs_C, cset) |
880 (gamma |> push_bound abs_M, cset) |
821 |> do_co_formula body_t |>> pop_bound |
881 |> do_co_formula body_t |>> pop_bound |
822 end |
882 end |
823 (* typ -> term -> accumulator *) |
883 (* typ -> term -> accumulator *) |
824 fun do_bounded_quantifier abs_T body_t = |
884 fun do_bounded_quantifier abs_T body_t = |
825 accum |>> push_bound (ctype_for abs_T) |> do_co_formula body_t |
885 accum |>> push_bound (mtype_for abs_T) |> do_co_formula body_t |
826 |>> pop_bound |
886 |>> pop_bound |
827 (* term -> term -> accumulator *) |
887 (* term -> term -> accumulator *) |
828 fun do_equals t1 t2 = |
888 fun do_equals t1 t2 = |
829 case sn of |
889 case sn of |
830 Plus => do_term t accum |> snd |
890 Plus => do_term t accum |> snd |
831 | Minus => let |
891 | Minus => let |
832 val (C1, accum) = do_term t1 accum |
892 val (M1, accum) = do_term t1 accum |
833 val (C2, accum) = do_term t2 accum |
893 val (M2, accum) = do_term t2 accum |
834 in accum ||> add_ctypes_equal C1 C2 end |
894 in accum ||> add_mtypes_equal M1 M2 end |
835 in |
895 in |
836 case t of |
896 case t of |
837 Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) => |
897 Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) => |
838 do_quantifier s0 T1 t1 |
898 do_quantifier s0 T1 t1 |
839 | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 |
899 | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 |