author | blanchet |
Thu, 04 Feb 2010 13:36:52 +0100 | |
changeset 34998 | 5e492a862b34 |
parent 34982 | 7b8c366e34a2 |
child 35028 | 108662d50512 |
child 35070 | 96136eb6218f |
permissions | -rw-r--r-- |
33982 | 1 |
(* Title: HOL/Tools/Nitpick/nitpick_mono.ML |
33192 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
3 |
Copyright 2009, 2010 |
33192 | 4 |
|
5 |
Monotonicity predicate for higher-order logic. |
|
6 |
*) |
|
7 |
||
8 |
signature NITPICK_MONO = |
|
9 |
sig |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
10 |
datatype sign = Plus | Minus |
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
11 |
type extended_context = Nitpick_HOL.extended_context |
33192 | 12 |
|
13 |
val formulas_monotonic : |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
14 |
extended_context -> typ -> sign -> term list -> term list -> term -> bool |
33192 | 15 |
end; |
16 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
17 |
structure Nitpick_Mono : NITPICK_MONO = |
33192 | 18 |
struct |
19 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
20 |
open Nitpick_Util |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
21 |
open Nitpick_HOL |
33192 | 22 |
|
23 |
type var = int |
|
24 |
||
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
25 |
datatype sign = Plus | Minus |
33192 | 26 |
datatype sign_atom = S of sign | V of var |
27 |
||
28 |
type literal = var * sign |
|
29 |
||
30 |
datatype ctype = |
|
31 |
CAlpha | |
|
32 |
CFun of ctype * sign_atom * ctype | |
|
33 |
CPair of ctype * ctype | |
|
34 |
CType of string * ctype list | |
|
35 |
CRec of string * typ list |
|
36 |
||
37 |
type cdata = |
|
38 |
{ext_ctxt: extended_context, |
|
39 |
alpha_T: typ, |
|
40 |
max_fresh: int Unsynchronized.ref, |
|
41 |
datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref, |
|
42 |
constr_cache: (styp * ctype) list Unsynchronized.ref} |
|
43 |
||
44 |
exception CTYPE of string * ctype list |
|
45 |
||
46 |
(* string -> unit *) |
|
47 |
fun print_g (s : string) = () |
|
48 |
||
49 |
(* var -> string *) |
|
50 |
val string_for_var = signed_string_of_int |
|
51 |
(* string -> var list -> string *) |
|
52 |
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>" |
|
53 |
| string_for_vars sep xs = space_implode sep (map string_for_var xs) |
|
54 |
fun subscript_string_for_vars sep xs = |
|
55 |
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>" |
|
56 |
||
57 |
(* sign -> string *) |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
58 |
fun string_for_sign Plus = "+" |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
59 |
| string_for_sign Minus = "-" |
33192 | 60 |
|
61 |
(* sign -> sign -> sign *) |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
62 |
fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus |
33192 | 63 |
(* sign -> sign *) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
64 |
val negate = xor Minus |
33192 | 65 |
|
66 |
(* sign_atom -> string *) |
|
67 |
fun string_for_sign_atom (S sn) = string_for_sign sn |
|
68 |
| string_for_sign_atom (V j) = string_for_var j |
|
69 |
||
70 |
(* literal -> string *) |
|
71 |
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn |
|
72 |
||
73 |
val bool_C = CType (@{type_name bool}, []) |
|
74 |
||
75 |
(* ctype -> bool *) |
|
76 |
fun is_CRec (CRec _) = true |
|
77 |
| is_CRec _ = false |
|
78 |
||
79 |
val no_prec = 100 |
|
80 |
val prec_CFun = 1 |
|
81 |
val prec_CPair = 2 |
|
82 |
||
83 |
(* tuple_set -> int *) |
|
84 |
fun precedence_of_ctype (CFun _) = prec_CFun |
|
85 |
| precedence_of_ctype (CPair _) = prec_CPair |
|
86 |
| precedence_of_ctype _ = no_prec |
|
87 |
||
88 |
(* ctype -> string *) |
|
89 |
val string_for_ctype = |
|
90 |
let |
|
91 |
(* int -> ctype -> string *) |
|
92 |
fun aux outer_prec C = |
|
93 |
let |
|
94 |
val prec = precedence_of_ctype C |
|
95 |
val need_parens = (prec < outer_prec) |
|
96 |
in |
|
97 |
(if need_parens then "(" else "") ^ |
|
98 |
(case C of |
|
99 |
CAlpha => "\<alpha>" |
|
100 |
| CFun (C1, a, C2) => |
|
101 |
aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^ |
|
102 |
string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2 |
|
103 |
| CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2 |
|
104 |
| CType (s, []) => |
|
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
105 |
if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s |
33192 | 106 |
| CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s |
107 |
| CRec (s, _) => "[" ^ s ^ "]") ^ |
|
108 |
(if need_parens then ")" else "") |
|
109 |
end |
|
110 |
in aux 0 end |
|
111 |
||
112 |
(* ctype -> ctype list *) |
|
113 |
fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2] |
|
114 |
| flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs |
|
115 |
| flatten_ctype C = [C] |
|
116 |
||
117 |
(* extended_context -> typ -> cdata *) |
|
118 |
fun initial_cdata ext_ctxt alpha_T = |
|
119 |
({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0, |
|
120 |
datatype_cache = Unsynchronized.ref [], |
|
121 |
constr_cache = Unsynchronized.ref []} : cdata) |
|
122 |
||
123 |
(* typ -> typ -> bool *) |
|
124 |
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34123
diff
changeset
|
125 |
T = alpha_T orelse (not (is_fp_iterator_type T) andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34123
diff
changeset
|
126 |
exists (could_exist_alpha_subtype alpha_T) Ts) |
33192 | 127 |
| could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
128 |
(* theory -> typ -> typ -> bool *) |
|
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
129 |
fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T = |
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
130 |
could_exist_alpha_subtype alpha_T T |
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
131 |
| could_exist_alpha_sub_ctype thy alpha_T T = |
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
132 |
(T = alpha_T orelse is_datatype thy T) |
33192 | 133 |
|
134 |
(* ctype -> bool *) |
|
135 |
fun exists_alpha_sub_ctype CAlpha = true |
|
136 |
| exists_alpha_sub_ctype (CFun (C1, _, C2)) = |
|
137 |
exists exists_alpha_sub_ctype [C1, C2] |
|
138 |
| exists_alpha_sub_ctype (CPair (C1, C2)) = |
|
139 |
exists exists_alpha_sub_ctype [C1, C2] |
|
140 |
| exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs |
|
141 |
| exists_alpha_sub_ctype (CRec _) = true |
|
142 |
||
143 |
(* ctype -> bool *) |
|
144 |
fun exists_alpha_sub_ctype_fresh CAlpha = true |
|
145 |
| exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true |
|
146 |
| exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) = |
|
147 |
exists_alpha_sub_ctype_fresh C2 |
|
148 |
| exists_alpha_sub_ctype_fresh (CPair (C1, C2)) = |
|
149 |
exists exists_alpha_sub_ctype_fresh [C1, C2] |
|
150 |
| exists_alpha_sub_ctype_fresh (CType (_, Cs)) = |
|
151 |
exists exists_alpha_sub_ctype_fresh Cs |
|
152 |
| exists_alpha_sub_ctype_fresh (CRec _) = true |
|
153 |
||
154 |
(* string * typ list -> ctype list -> ctype *) |
|
155 |
fun constr_ctype_for_binders z Cs = |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
156 |
fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z) |
33192 | 157 |
|
158 |
(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *) |
|
159 |
fun repair_ctype _ _ CAlpha = CAlpha |
|
160 |
| repair_ctype cache seen (CFun (C1, a, C2)) = |
|
161 |
CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2) |
|
162 |
| repair_ctype cache seen (CPair Cp) = |
|
163 |
CPair (pairself (repair_ctype cache seen) Cp) |
|
164 |
| repair_ctype cache seen (CType (s, Cs)) = |
|
165 |
CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs) |
|
166 |
| repair_ctype cache seen (CRec (z as (s, _))) = |
|
167 |
case AList.lookup (op =) cache z |> the of |
|
168 |
CRec _ => CType (s, []) |
|
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
169 |
| C => if member (op =) seen C then CType (s, []) |
33192 | 170 |
else repair_ctype cache (C :: seen) C |
171 |
||
172 |
(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *) |
|
173 |
fun repair_datatype_cache cache = |
|
174 |
let |
|
175 |
(* (string * typ list) * ctype -> unit *) |
|
176 |
fun repair_one (z, C) = |
|
177 |
Unsynchronized.change cache |
|
178 |
(AList.update (op =) (z, repair_ctype (!cache) [] C)) |
|
179 |
in List.app repair_one (rev (!cache)) end |
|
180 |
||
181 |
(* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *) |
|
182 |
fun repair_constr_cache dtype_cache constr_cache = |
|
183 |
let |
|
184 |
(* styp * ctype -> unit *) |
|
185 |
fun repair_one (x, C) = |
|
186 |
Unsynchronized.change constr_cache |
|
187 |
(AList.update (op =) (x, repair_ctype dtype_cache [] C)) |
|
188 |
in List.app repair_one (!constr_cache) end |
|
189 |
||
190 |
(* cdata -> typ -> ctype *) |
|
191 |
fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh, |
|
192 |
datatype_cache, constr_cache, ...} : cdata) = |
|
193 |
let |
|
194 |
(* typ -> typ -> ctype *) |
|
195 |
fun do_fun T1 T2 = |
|
196 |
let |
|
197 |
val C1 = do_type T1 |
|
198 |
val C2 = do_type T2 |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34123
diff
changeset
|
199 |
val a = if is_boolean_type (body_type T2) andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34123
diff
changeset
|
200 |
exists_alpha_sub_ctype_fresh C1 then |
33192 | 201 |
V (Unsynchronized.inc max_fresh) |
202 |
else |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
203 |
S Minus |
33192 | 204 |
in CFun (C1, a, C2) end |
205 |
(* typ -> ctype *) |
|
206 |
and do_type T = |
|
207 |
if T = alpha_T then |
|
208 |
CAlpha |
|
209 |
else case T of |
|
210 |
Type ("fun", [T1, T2]) => do_fun T1 T2 |
|
211 |
| Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2 |
|
212 |
| Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2)) |
|
213 |
| Type (z as (s, _)) => |
|
214 |
if could_exist_alpha_sub_ctype thy alpha_T T then |
|
215 |
case AList.lookup (op =) (!datatype_cache) z of |
|
216 |
SOME C => C |
|
217 |
| NONE => |
|
218 |
let |
|
219 |
val _ = Unsynchronized.change datatype_cache (cons (z, CRec z)) |
|
33580
45c33e97cb86
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet
parents:
33574
diff
changeset
|
220 |
val xs = datatype_constrs ext_ctxt T |
33192 | 221 |
val (all_Cs, constr_Cs) = |
222 |
fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) => |
|
223 |
let |
|
224 |
val binder_Cs = map do_type (binder_types T') |
|
225 |
val new_Cs = filter exists_alpha_sub_ctype_fresh |
|
226 |
binder_Cs |
|
227 |
val constr_C = constr_ctype_for_binders z |
|
228 |
binder_Cs |
|
229 |
in |
|
230 |
(union (op =) new_Cs all_Cs, |
|
231 |
constr_C :: constr_Cs) |
|
232 |
end) |
|
233 |
xs ([], []) |
|
234 |
val C = CType (s, all_Cs) |
|
235 |
val _ = Unsynchronized.change datatype_cache |
|
236 |
(AList.update (op =) (z, C)) |
|
237 |
val _ = Unsynchronized.change constr_cache |
|
238 |
(append (xs ~~ constr_Cs)) |
|
239 |
in |
|
240 |
if forall (not o is_CRec o snd) (!datatype_cache) then |
|
241 |
(repair_datatype_cache datatype_cache; |
|
242 |
repair_constr_cache (!datatype_cache) constr_cache; |
|
243 |
AList.lookup (op =) (!datatype_cache) z |> the) |
|
244 |
else |
|
245 |
C |
|
246 |
end |
|
247 |
else |
|
248 |
CType (s, []) |
|
249 |
| _ => CType (Refute.string_of_typ T, []) |
|
250 |
in do_type end |
|
251 |
||
252 |
(* ctype -> ctype list *) |
|
253 |
fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2] |
|
254 |
| prodC_factors C = [C] |
|
255 |
(* ctype -> ctype list * ctype *) |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
256 |
fun curried_strip_ctype (CFun (C1, S Minus, C2)) = |
33192 | 257 |
curried_strip_ctype C2 |>> append (prodC_factors C1) |
258 |
| curried_strip_ctype C = ([], C) |
|
259 |
(* string -> ctype -> ctype *) |
|
260 |
fun sel_ctype_from_constr_ctype s C = |
|
261 |
let val (arg_Cs, dataC) = curried_strip_ctype C in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
262 |
CFun (dataC, S Minus, |
33192 | 263 |
case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n) |
264 |
end |
|
265 |
||
266 |
(* cdata -> styp -> ctype *) |
|
267 |
fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache, |
|
268 |
...}) (x as (_, T)) = |
|
269 |
if could_exist_alpha_sub_ctype thy alpha_T T then |
|
270 |
case AList.lookup (op =) (!constr_cache) x of |
|
271 |
SOME C => C |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
272 |
| NONE => if T = alpha_T then |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
273 |
let val C = fresh_ctype_for_type cdata T in |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
274 |
(Unsynchronized.change constr_cache (cons (x, C)); C) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
275 |
end |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
276 |
else |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
277 |
(fresh_ctype_for_type cdata (body_type T); |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
278 |
AList.lookup (op =) (!constr_cache) x |> the) |
33192 | 279 |
else |
280 |
fresh_ctype_for_type cdata T |
|
281 |
fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) = |
|
282 |
x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata |
|
283 |
|> sel_ctype_from_constr_ctype s |
|
284 |
||
285 |
(* literal list -> ctype -> ctype *) |
|
286 |
fun instantiate_ctype lits = |
|
287 |
let |
|
288 |
(* ctype -> ctype *) |
|
289 |
fun aux CAlpha = CAlpha |
|
290 |
| aux (CFun (C1, V x, C2)) = |
|
291 |
let |
|
292 |
val a = case AList.lookup (op =) lits x of |
|
293 |
SOME sn => S sn |
|
294 |
| NONE => V x |
|
295 |
in CFun (aux C1, a, aux C2) end |
|
296 |
| aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2) |
|
297 |
| aux (CPair Cp) = CPair (pairself aux Cp) |
|
298 |
| aux (CType (s, Cs)) = CType (s, map aux Cs) |
|
299 |
| aux (CRec z) = CRec z |
|
300 |
in aux end |
|
301 |
||
302 |
datatype comp_op = Eq | Leq |
|
303 |
||
304 |
type comp = sign_atom * sign_atom * comp_op * var list |
|
305 |
type sign_expr = literal list |
|
306 |
||
307 |
datatype constraint_set = |
|
308 |
UnsolvableCSet | |
|
309 |
CSet of literal list * comp list * sign_expr list |
|
310 |
||
311 |
(* comp_op -> string *) |
|
312 |
fun string_for_comp_op Eq = "=" |
|
313 |
| string_for_comp_op Leq = "\<le>" |
|
314 |
||
315 |
(* sign_expr -> string *) |
|
316 |
fun string_for_sign_expr [] = "\<bot>" |
|
317 |
| string_for_sign_expr lits = |
|
318 |
space_implode " \<or> " (map string_for_literal lits) |
|
319 |
||
320 |
(* constraint_set *) |
|
321 |
val slack = CSet ([], [], []) |
|
322 |
||
323 |
(* literal -> literal list option -> literal list option *) |
|
324 |
fun do_literal _ NONE = NONE |
|
325 |
| do_literal (x, sn) (SOME lits) = |
|
326 |
case AList.lookup (op =) lits x of |
|
327 |
SOME sn' => if sn = sn' then SOME lits else NONE |
|
328 |
| NONE => SOME ((x, sn) :: lits) |
|
329 |
||
330 |
(* comp_op -> var list -> sign_atom -> sign_atom -> literal list * comp list |
|
331 |
-> (literal list * comp list) option *) |
|
332 |
fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) = |
|
333 |
(case (a1, a2) of |
|
334 |
(S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE |
|
335 |
| (V x1, S sn2) => |
|
336 |
Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits)) |
|
337 |
| (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps) |
|
338 |
| _ => do_sign_atom_comp Eq [] a2 a1 accum) |
|
339 |
| do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) = |
|
340 |
(case (a1, a2) of |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
341 |
(_, S Minus) => SOME accum |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
342 |
| (S Plus, _) => SOME accum |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
343 |
| (S Minus, S Plus) => NONE |
33192 | 344 |
| (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps) |
345 |
| _ => do_sign_atom_comp Eq [] a1 a2 accum) |
|
346 |
| do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) = |
|
347 |
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) |
|
348 |
||
349 |
(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option |
|
350 |
-> (literal list * comp list) option *) |
|
351 |
fun do_ctype_comp _ _ _ _ NONE = NONE |
|
352 |
| do_ctype_comp _ _ CAlpha CAlpha accum = accum |
|
353 |
| do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22)) |
|
354 |
(SOME accum) = |
|
355 |
accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21 |
|
356 |
|> do_ctype_comp Eq xs C12 C22 |
|
357 |
| do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22)) |
|
358 |
(SOME accum) = |
|
359 |
(if exists_alpha_sub_ctype C11 then |
|
360 |
accum |> do_sign_atom_comp Leq xs a1 a2 |
|
361 |
|> do_ctype_comp Leq xs C21 C11 |
|
362 |
|> (case a2 of |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
363 |
S Minus => I |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
364 |
| S Plus => do_ctype_comp Leq xs C11 C21 |
33192 | 365 |
| V x => do_ctype_comp Leq (x :: xs) C11 C21) |
366 |
else |
|
367 |
SOME accum) |
|
368 |
|> do_ctype_comp Leq xs C12 C22 |
|
369 |
| do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22)) |
|
370 |
accum = |
|
371 |
(accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)] |
|
372 |
handle Library.UnequalLengths => |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
373 |
raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])) |
33192 | 374 |
| do_ctype_comp cmp xs (CType _) (CType _) accum = |
375 |
accum (* no need to compare them thanks to the cache *) |
|
376 |
| do_ctype_comp _ _ C1 C2 _ = |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
377 |
raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]) |
33192 | 378 |
|
379 |
(* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *) |
|
380 |
fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet |
|
381 |
| add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) = |
|
382 |
(print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^ |
|
383 |
" " ^ string_for_ctype C2); |
|
384 |
case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of |
|
385 |
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
|
386 |
| SOME (lits, comps) => CSet (lits, comps, sexps)) |
|
387 |
||
388 |
(* ctype -> ctype -> constraint_set -> constraint_set *) |
|
389 |
val add_ctypes_equal = add_ctype_comp Eq |
|
390 |
val add_is_sub_ctype = add_ctype_comp Leq |
|
391 |
||
392 |
(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option |
|
393 |
-> (literal list * sign_expr list) option *) |
|
394 |
fun do_notin_ctype_fv _ _ _ NONE = NONE |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
395 |
| do_notin_ctype_fv Minus _ CAlpha accum = accum |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
396 |
| do_notin_ctype_fv Plus [] CAlpha _ = NONE |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
397 |
| do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) = |
33192 | 398 |
SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
399 |
| do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) = |
33192 | 400 |
SOME (lits, insert (op =) sexp sexps) |
401 |
| do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum = |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
402 |
accum |> (if sn' = Plus andalso sn = Plus then |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
403 |
do_notin_ctype_fv Plus sexp C1 |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
404 |
else |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
405 |
I) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
406 |
|> (if sn' = Minus orelse sn = Plus then |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
407 |
do_notin_ctype_fv Minus sexp C1 |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
408 |
else |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
409 |
I) |
33192 | 410 |
|> do_notin_ctype_fv sn sexp C2 |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
411 |
| do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum = |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
412 |
accum |> (case do_literal (x, Minus) (SOME sexp) of |
33192 | 413 |
NONE => I |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
414 |
| SOME sexp' => do_notin_ctype_fv Plus sexp' C1) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
415 |
|> do_notin_ctype_fv Minus sexp C1 |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
416 |
|> do_notin_ctype_fv Plus sexp C2 |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
417 |
| do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum = |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
418 |
accum |> (case do_literal (x, Plus) (SOME sexp) of |
33192 | 419 |
NONE => I |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
420 |
| SOME sexp' => do_notin_ctype_fv Plus sexp' C1) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
421 |
|> do_notin_ctype_fv Minus sexp C2 |
33192 | 422 |
| do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum = |
423 |
accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2] |
|
424 |
| do_notin_ctype_fv sn sexp (CType (_, Cs)) accum = |
|
425 |
accum |> fold (do_notin_ctype_fv sn sexp) Cs |
|
426 |
| do_notin_ctype_fv _ _ C _ = |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
427 |
raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C]) |
33192 | 428 |
|
429 |
(* sign -> ctype -> constraint_set -> constraint_set *) |
|
430 |
fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet |
|
431 |
| add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) = |
|
432 |
(print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^ |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
433 |
(case sn of Minus => "unique" | Plus => "total") ^ "."); |
33192 | 434 |
case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of |
435 |
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
|
436 |
| SOME (lits, sexps) => CSet (lits, comps, sexps)) |
|
437 |
||
438 |
(* ctype -> constraint_set -> constraint_set *) |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
439 |
val add_ctype_is_right_unique = add_notin_ctype_fv Minus |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
440 |
val add_ctype_is_right_total = add_notin_ctype_fv Plus |
33192 | 441 |
|
442 |
(* constraint_set -> constraint_set -> constraint_set *) |
|
443 |
fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) = |
|
444 |
(case SOME lits1 |> fold do_literal lits2 of |
|
445 |
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
|
446 |
| SOME lits => CSet (lits, comps1 @ comps2, sexps1 @ sexps2)) |
|
447 |
| unite _ _ = UnsolvableCSet |
|
448 |
||
449 |
(* sign -> bool *) |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
450 |
fun bool_from_sign Plus = false |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
451 |
| bool_from_sign Minus = true |
33192 | 452 |
(* bool -> sign *) |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
453 |
fun sign_from_bool false = Plus |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
454 |
| sign_from_bool true = Minus |
33192 | 455 |
|
456 |
(* literal -> PropLogic.prop_formula *) |
|
457 |
fun prop_for_literal (x, sn) = |
|
458 |
(not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x) |
|
459 |
(* sign_atom -> PropLogic.prop_formula *) |
|
460 |
fun prop_for_sign_atom_eq (S sn', sn) = |
|
461 |
if sn = sn' then PropLogic.True else PropLogic.False |
|
462 |
| prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn) |
|
463 |
(* sign_expr -> PropLogic.prop_formula *) |
|
464 |
fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs) |
|
465 |
(* var list -> sign -> PropLogic.prop_formula *) |
|
466 |
fun prop_for_exists_eq xs sn = |
|
467 |
PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs) |
|
468 |
(* comp -> PropLogic.prop_formula *) |
|
469 |
fun prop_for_comp (a1, a2, Eq, []) = |
|
470 |
PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []), |
|
471 |
prop_for_comp (a2, a1, Leq, [])) |
|
472 |
| prop_for_comp (a1, a2, Leq, []) = |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
473 |
PropLogic.SOr (prop_for_sign_atom_eq (a1, Plus), |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
474 |
prop_for_sign_atom_eq (a2, Minus)) |
33192 | 475 |
| prop_for_comp (a1, a2, cmp, xs) = |
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
476 |
PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, [])) |
33192 | 477 |
|
478 |
(* var -> (int -> bool option) -> literal list -> literal list *) |
|
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
479 |
fun literals_from_assignments max_var assigns lits = |
33192 | 480 |
fold (fn x => fn accum => |
481 |
if AList.defined (op =) lits x then |
|
482 |
accum |
|
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
483 |
else case assigns x of |
33192 | 484 |
SOME b => (x, sign_from_bool b) :: accum |
485 |
| NONE => accum) (max_var downto 1) lits |
|
486 |
||
487 |
(* literal list -> sign_atom -> sign option *) |
|
488 |
fun lookup_sign_atom _ (S sn) = SOME sn |
|
489 |
| lookup_sign_atom lit (V x) = AList.lookup (op =) lit x |
|
490 |
||
491 |
(* comp -> string *) |
|
492 |
fun string_for_comp (a1, a2, cmp, xs) = |
|
493 |
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^ |
|
494 |
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2 |
|
495 |
||
496 |
(* literal list -> comp list -> sign_expr list -> unit *) |
|
497 |
fun print_problem lits comps sexps = |
|
498 |
print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @ |
|
499 |
map string_for_comp comps @ |
|
500 |
map string_for_sign_expr sexps)) |
|
501 |
||
502 |
(* literal list -> unit *) |
|
503 |
fun print_solution lits = |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
504 |
let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in |
33192 | 505 |
print_g ("*** Solution:\n" ^ |
506 |
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^ |
|
507 |
"-: " ^ commas (map (string_for_var o fst) neg)) |
|
508 |
end |
|
509 |
||
510 |
(* var -> constraint_set -> literal list list option *) |
|
511 |
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE) |
|
512 |
| solve max_var (CSet (lits, comps, sexps)) = |
|
513 |
let |
|
514 |
val _ = print_problem lits comps sexps |
|
515 |
val prop = PropLogic.all (map prop_for_literal lits @ |
|
516 |
map prop_for_comp comps @ |
|
517 |
map prop_for_sign_expr sexps) |
|
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
518 |
(* use the first ML solver (to avoid startup overhead) *) |
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
519 |
val solvers = !SatSolver.solvers |
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
520 |
|> filter (member (op =) ["dptsat", "dpll"] o fst) |
33192 | 521 |
in |
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
522 |
case snd (hd solvers) prop of |
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
523 |
SatSolver.SATISFIABLE assigns => |
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
524 |
SOME (literals_from_assignments max_var assigns lits |
33192 | 525 |
|> tap print_solution) |
526 |
| _ => NONE |
|
527 |
end |
|
528 |
||
529 |
(* var -> constraint_set -> bool *) |
|
530 |
val is_solvable = is_some oo solve |
|
531 |
||
532 |
type ctype_schema = ctype * constraint_set |
|
533 |
type ctype_context = |
|
534 |
{bounds: ctype list, |
|
535 |
frees: (styp * ctype) list, |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
536 |
consts: (styp * ctype) list} |
33192 | 537 |
|
538 |
type accumulator = ctype_context * constraint_set |
|
539 |
||
540 |
val initial_gamma = {bounds = [], frees = [], consts = []} |
|
541 |
val unsolvable_accum = (initial_gamma, UnsolvableCSet) |
|
542 |
||
543 |
(* ctype -> ctype_context -> ctype_context *) |
|
544 |
fun push_bound C {bounds, frees, consts} = |
|
545 |
{bounds = C :: bounds, frees = frees, consts = consts} |
|
546 |
(* ctype_context -> ctype_context *) |
|
547 |
fun pop_bound {bounds, frees, consts} = |
|
548 |
{bounds = tl bounds, frees = frees, consts = consts} |
|
549 |
handle List.Empty => initial_gamma |
|
550 |
||
551 |
(* cdata -> term -> accumulator -> ctype * accumulator *) |
|
552 |
fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T, |
|
553 |
max_fresh, ...}) = |
|
554 |
let |
|
555 |
(* typ -> ctype *) |
|
556 |
val ctype_for = fresh_ctype_for_type cdata |
|
557 |
(* ctype -> ctype *) |
|
558 |
fun pos_set_ctype_for_dom C = |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
559 |
CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C) |
33192 | 560 |
(* typ -> accumulator -> ctype * accumulator *) |
561 |
fun do_quantifier T (gamma, cset) = |
|
562 |
let |
|
563 |
val abs_C = ctype_for (domain_type (domain_type T)) |
|
564 |
val body_C = ctype_for (range_type T) |
|
565 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
566 |
(CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C), |
33192 | 567 |
(gamma, cset |> add_ctype_is_right_total abs_C)) |
568 |
end |
|
569 |
fun do_equals T (gamma, cset) = |
|
570 |
let val C = ctype_for (domain_type T) in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
571 |
(CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh), |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
572 |
ctype_for (nth_range_type 2 T))), |
33192 | 573 |
(gamma, cset |> add_ctype_is_right_unique C)) |
574 |
end |
|
575 |
fun do_robust_set_operation T (gamma, cset) = |
|
576 |
let |
|
577 |
val set_T = domain_type T |
|
578 |
val C1 = ctype_for set_T |
|
579 |
val C2 = ctype_for set_T |
|
580 |
val C3 = ctype_for set_T |
|
581 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
582 |
(CFun (C1, S Minus, CFun (C2, S Minus, C3)), |
33192 | 583 |
(gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3)) |
584 |
end |
|
585 |
fun do_fragile_set_operation T (gamma, cset) = |
|
586 |
let |
|
587 |
val set_T = domain_type T |
|
588 |
val set_C = ctype_for set_T |
|
589 |
(* typ -> ctype *) |
|
590 |
fun custom_ctype_for (T as Type ("fun", [T1, T2])) = |
|
591 |
if T = set_T then set_C |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
592 |
else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2) |
33192 | 593 |
| custom_ctype_for T = ctype_for T |
594 |
in |
|
595 |
(custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C)) |
|
596 |
end |
|
597 |
(* typ -> accumulator -> ctype * accumulator *) |
|
598 |
fun do_pair_constr T accum = |
|
599 |
case ctype_for (nth_range_type 2 T) of |
|
600 |
C as CPair (a_C, b_C) => |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
601 |
(CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum) |
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
602 |
| C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C]) |
33192 | 603 |
(* int -> typ -> accumulator -> ctype * accumulator *) |
604 |
fun do_nth_pair_sel n T = |
|
605 |
case ctype_for (domain_type T) of |
|
606 |
C as CPair (a_C, b_C) => |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
607 |
pair (CFun (C, S Minus, if n = 0 then a_C else b_C)) |
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
608 |
| C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C]) |
33192 | 609 |
val unsolvable = (CType ("unsolvable", []), unsolvable_accum) |
610 |
(* typ -> term -> accumulator -> ctype * accumulator *) |
|
611 |
fun do_bounded_quantifier abs_T bound_t body_t accum = |
|
612 |
let |
|
613 |
val abs_C = ctype_for abs_T |
|
614 |
val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t |
|
615 |
val expected_bound_C = pos_set_ctype_for_dom abs_C |
|
616 |
in |
|
617 |
accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t |
|
618 |
||> apfst pop_bound |
|
619 |
end |
|
620 |
(* term -> accumulator -> ctype * accumulator *) |
|
621 |
and do_term _ (_, UnsolvableCSet) = unsolvable |
|
622 |
| do_term t (accum as (gamma as {bounds, frees, consts}, cset)) = |
|
623 |
(case t of |
|
624 |
Const (x as (s, T)) => |
|
625 |
(case AList.lookup (op =) consts x of |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
626 |
SOME C => (C, accum) |
33192 | 627 |
| NONE => |
628 |
if not (could_exist_alpha_subtype alpha_T T) then |
|
629 |
(ctype_for T, accum) |
|
630 |
else case s of |
|
631 |
@{const_name all} => do_quantifier T accum |
|
632 |
| @{const_name "=="} => do_equals T accum |
|
633 |
| @{const_name All} => do_quantifier T accum |
|
634 |
| @{const_name Ex} => do_quantifier T accum |
|
635 |
| @{const_name "op ="} => do_equals T accum |
|
636 |
| @{const_name The} => (print_g "*** The"; unsolvable) |
|
637 |
| @{const_name Eps} => (print_g "*** Eps"; unsolvable) |
|
638 |
| @{const_name If} => |
|
639 |
do_robust_set_operation (range_type T) accum |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
640 |
|>> curry3 CFun bool_C (S Minus) |
33192 | 641 |
| @{const_name Pair} => do_pair_constr T accum |
642 |
| @{const_name fst} => do_nth_pair_sel 0 T accum |
|
643 |
| @{const_name snd} => do_nth_pair_sel 1 T accum |
|
644 |
| @{const_name Id} => |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
645 |
(CFun (ctype_for (domain_type T), S Minus, bool_C), accum) |
33192 | 646 |
| @{const_name insert} => |
647 |
let |
|
648 |
val set_T = domain_type (range_type T) |
|
649 |
val C1 = ctype_for (domain_type set_T) |
|
650 |
val C1' = pos_set_ctype_for_dom C1 |
|
651 |
val C2 = ctype_for set_T |
|
652 |
val C3 = ctype_for set_T |
|
653 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
654 |
(CFun (C1, S Minus, CFun (C2, S Minus, C3)), |
33192 | 655 |
(gamma, cset |> add_ctype_is_right_unique C1 |
656 |
|> add_is_sub_ctype C1' C3 |
|
657 |
|> add_is_sub_ctype C2 C3)) |
|
658 |
end |
|
659 |
| @{const_name converse} => |
|
660 |
let |
|
661 |
val x = Unsynchronized.inc max_fresh |
|
662 |
(* typ -> ctype *) |
|
663 |
fun ctype_for_set T = |
|
664 |
CFun (ctype_for (domain_type T), V x, bool_C) |
|
665 |
val ab_set_C = domain_type T |> ctype_for_set |
|
666 |
val ba_set_C = range_type T |> ctype_for_set |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
667 |
in (CFun (ab_set_C, S Minus, ba_set_C), accum) end |
33192 | 668 |
| @{const_name trancl} => do_fragile_set_operation T accum |
669 |
| @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable) |
|
670 |
| @{const_name lower_semilattice_fun_inst.inf_fun} => |
|
671 |
do_robust_set_operation T accum |
|
672 |
| @{const_name upper_semilattice_fun_inst.sup_fun} => |
|
673 |
do_robust_set_operation T accum |
|
674 |
| @{const_name finite} => |
|
675 |
let val C1 = ctype_for (domain_type (domain_type T)) in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
676 |
(CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum) |
33192 | 677 |
end |
678 |
| @{const_name rel_comp} => |
|
679 |
let |
|
680 |
val x = Unsynchronized.inc max_fresh |
|
681 |
(* typ -> ctype *) |
|
682 |
fun ctype_for_set T = |
|
683 |
CFun (ctype_for (domain_type T), V x, bool_C) |
|
684 |
val bc_set_C = domain_type T |> ctype_for_set |
|
685 |
val ab_set_C = domain_type (range_type T) |> ctype_for_set |
|
686 |
val ac_set_C = nth_range_type 2 T |> ctype_for_set |
|
687 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
688 |
(CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)), |
33192 | 689 |
accum) |
690 |
end |
|
691 |
| @{const_name image} => |
|
692 |
let |
|
693 |
val a_C = ctype_for (domain_type (domain_type T)) |
|
694 |
val b_C = ctype_for (range_type (domain_type T)) |
|
695 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
696 |
(CFun (CFun (a_C, S Minus, b_C), S Minus, |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
697 |
CFun (pos_set_ctype_for_dom a_C, S Minus, |
33192 | 698 |
pos_set_ctype_for_dom b_C)), accum) |
699 |
end |
|
700 |
| @{const_name Sigma} => |
|
701 |
let |
|
702 |
val x = Unsynchronized.inc max_fresh |
|
703 |
(* typ -> ctype *) |
|
704 |
fun ctype_for_set T = |
|
705 |
CFun (ctype_for (domain_type T), V x, bool_C) |
|
706 |
val a_set_T = domain_type T |
|
707 |
val a_C = ctype_for (domain_type a_set_T) |
|
708 |
val b_set_C = ctype_for_set (range_type (domain_type |
|
709 |
(range_type T))) |
|
710 |
val a_set_C = ctype_for_set a_set_T |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
711 |
val a_to_b_set_C = CFun (a_C, S Minus, b_set_C) |
33192 | 712 |
val ab_set_C = ctype_for_set (nth_range_type 2 T) |
713 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
714 |
(CFun (a_set_C, S Minus, |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
715 |
CFun (a_to_b_set_C, S Minus, ab_set_C)), accum) |
33192 | 716 |
end |
717 |
| @{const_name minus_fun_inst.minus_fun} => |
|
718 |
let |
|
719 |
val set_T = domain_type T |
|
720 |
val left_set_C = ctype_for set_T |
|
721 |
val right_set_C = ctype_for set_T |
|
722 |
in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
723 |
(CFun (left_set_C, S Minus, |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
724 |
CFun (right_set_C, S Minus, left_set_C)), |
33192 | 725 |
(gamma, cset |> add_ctype_is_right_unique right_set_C |
33574
113e235e84e3
eliminate two FIXMEs in Nitpick's monotonicity check code
blanchet
parents:
33571
diff
changeset
|
726 |
|> add_is_sub_ctype right_set_C left_set_C)) |
33192 | 727 |
end |
728 |
| @{const_name ord_fun_inst.less_eq_fun} => |
|
729 |
do_fragile_set_operation T accum |
|
730 |
| @{const_name Tha} => |
|
731 |
let |
|
732 |
val a_C = ctype_for (domain_type (domain_type T)) |
|
733 |
val a_set_C = pos_set_ctype_for_dom a_C |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
734 |
in (CFun (a_set_C, S Minus, a_C), accum) end |
33192 | 735 |
| @{const_name FunBox} => |
736 |
let val dom_C = ctype_for (domain_type T) in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
737 |
(CFun (dom_C, S Minus, dom_C), accum) |
33192 | 738 |
end |
739 |
| _ => if is_sel s then |
|
740 |
if constr_name_for_sel_like s = @{const_name FunBox} then |
|
741 |
let val dom_C = ctype_for (domain_type T) in |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
742 |
(CFun (dom_C, S Minus, dom_C), accum) |
33192 | 743 |
end |
744 |
else |
|
745 |
(ctype_for_sel cdata x, accum) |
|
746 |
else if is_constr thy x then |
|
747 |
(ctype_for_constr cdata x, accum) |
|
748 |
else if is_built_in_const true x then |
|
749 |
case def_of_const thy def_table x of |
|
750 |
SOME t' => do_term t' accum |
|
751 |
| NONE => (print_g ("*** built-in " ^ s); unsolvable) |
|
752 |
else |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
753 |
let val C = ctype_for T in |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
754 |
(C, ({bounds = bounds, frees = frees, |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
755 |
consts = (x, C) :: consts}, cset)) |
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
756 |
end) |
33192 | 757 |
| Free (x as (_, T)) => |
758 |
(case AList.lookup (op =) frees x of |
|
759 |
SOME C => (C, accum) |
|
760 |
| NONE => |
|
761 |
let val C = ctype_for T in |
|
762 |
(C, ({bounds = bounds, frees = (x, C) :: frees, |
|
763 |
consts = consts}, cset)) |
|
764 |
end) |
|
765 |
| Var _ => (print_g "*** Var"; unsolvable) |
|
766 |
| Bound j => (nth bounds j, accum) |
|
767 |
| Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum) |
|
768 |
| Abs (s, T, t') => |
|
34998 | 769 |
((case t' of |
770 |
t1' $ Bound 0 => |
|
771 |
if not (loose_bvar1 (t1', 0)) then |
|
772 |
do_term (incr_boundvars ~1 t1') accum |
|
773 |
else |
|
774 |
raise SAME () |
|
775 |
| _ => raise SAME ()) |
|
776 |
handle SAME () => |
|
777 |
let |
|
778 |
val C = ctype_for T |
|
779 |
val (C', accum) = do_term t' (accum |>> push_bound C) |
|
780 |
in (CFun (C, S Minus, C'), accum |>> pop_bound) end) |
|
33192 | 781 |
| Const (@{const_name All}, _) |
782 |
$ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) => |
|
783 |
do_bounded_quantifier T' t1 t2 accum |
|
784 |
| Const (@{const_name Ex}, _) |
|
785 |
$ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) => |
|
786 |
do_bounded_quantifier T' t1 t2 accum |
|
787 |
| Const (@{const_name Let}, _) $ t1 $ t2 => |
|
788 |
do_term (betapply (t2, t1)) accum |
|
789 |
| t1 $ t2 => |
|
790 |
let |
|
791 |
val (C1, accum) = do_term t1 accum |
|
792 |
val (C2, accum) = do_term t2 accum |
|
793 |
in |
|
794 |
case accum of |
|
795 |
(_, UnsolvableCSet) => unsolvable |
|
796 |
| _ => case C1 of |
|
797 |
CFun (C11, _, C12) => |
|
798 |
(C12, accum ||> add_is_sub_ctype C2 C11) |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
799 |
| _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \ |
33192 | 800 |
\(op $)", [C1]) |
801 |
end) |
|
802 |
|> tap (fn (C, _) => |
|
803 |
print_g (" \<Gamma> \<turnstile> " ^ |
|
804 |
Syntax.string_of_term ctxt t ^ " : " ^ |
|
805 |
string_for_ctype C)) |
|
806 |
in do_term end |
|
807 |
||
808 |
(* cdata -> sign -> term -> accumulator -> accumulator *) |
|
809 |
fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) = |
|
810 |
let |
|
811 |
(* typ -> ctype *) |
|
812 |
val ctype_for = fresh_ctype_for_type cdata |
|
33732
385381514eed
added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus
blanchet
parents:
33580
diff
changeset
|
813 |
(* term -> accumulator -> ctype * accumulator *) |
385381514eed
added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus
blanchet
parents:
33580
diff
changeset
|
814 |
val do_term = consider_term cdata |
33192 | 815 |
(* sign -> term -> accumulator -> accumulator *) |
816 |
fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum |
|
817 |
| do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) = |
|
818 |
let |
|
819 |
(* term -> accumulator -> accumulator *) |
|
820 |
val do_co_formula = do_formula sn |
|
821 |
val do_contra_formula = do_formula (negate sn) |
|
822 |
(* string -> typ -> term -> accumulator *) |
|
823 |
fun do_quantifier quant_s abs_T body_t = |
|
824 |
let |
|
825 |
val abs_C = ctype_for abs_T |
|
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset
|
826 |
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) |
33192 | 827 |
val cset = cset |> side_cond ? add_ctype_is_right_total abs_C |
828 |
in |
|
829 |
(gamma |> push_bound abs_C, cset) |> do_co_formula body_t |
|
830 |
|>> pop_bound |
|
831 |
end |
|
832 |
(* typ -> term -> accumulator *) |
|
833 |
fun do_bounded_quantifier abs_T body_t = |