author | blanchet |
Fri, 26 Feb 2010 16:49:46 +0100 | |
changeset 35386 | 45a4e19d3ebd |
parent 35385 | 29f81babefd7 |
child 35665 | ff2bf50505ab |
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 |
|
35384 | 5 |
Monotonicity inference for higher-order logic. |
33192 | 6 |
*) |
7 |
||
8 |
signature NITPICK_MONO = |
|
9 |
sig |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset
|
10 |
type hol_context = Nitpick_HOL.hol_context |
33192 | 11 |
|
12 |
val formulas_monotonic : |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
13 |
hol_context -> bool -> typ -> term list * term list -> bool |
33192 | 14 |
end; |
15 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
16 |
structure Nitpick_Mono : NITPICK_MONO = |
33192 | 17 |
struct |
18 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
19 |
open Nitpick_Util |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
20 |
open Nitpick_HOL |
33192 | 21 |
|
22 |
type var = int |
|
23 |
||
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
|
24 |
datatype sign = Plus | Minus |
33192 | 25 |
datatype sign_atom = S of sign | V of var |
26 |
||
27 |
type literal = var * sign |
|
28 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
29 |
datatype mtyp = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
30 |
MAlpha | |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
31 |
MFun of mtyp * sign_atom * mtyp | |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
32 |
MPair of mtyp * mtyp | |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
33 |
MType of string * mtyp list | |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
34 |
MRec of string * typ list |
33192 | 35 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
36 |
datatype mterm = |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
37 |
MRaw of term * mtyp | |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
38 |
MAbs of string * typ * mtyp * sign_atom * mterm | |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
39 |
MApp of mterm * mterm |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
40 |
|
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
41 |
type mdata = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34998
diff
changeset
|
42 |
{hol_ctxt: hol_context, |
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset
|
43 |
binarize: bool, |
33192 | 44 |
alpha_T: typ, |
45 |
max_fresh: int Unsynchronized.ref, |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
46 |
datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
47 |
constr_cache: (styp * mtyp) list Unsynchronized.ref} |
33192 | 48 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
49 |
exception MTYPE of string * mtyp list |
33192 | 50 |
|
51 |
(* string -> unit *) |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
52 |
fun print_g (_ : string) = () |
33192 | 53 |
|
54 |
(* var -> string *) |
|
55 |
val string_for_var = signed_string_of_int |
|
56 |
(* string -> var list -> string *) |
|
57 |
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>" |
|
58 |
| string_for_vars sep xs = space_implode sep (map string_for_var xs) |
|
59 |
fun subscript_string_for_vars sep xs = |
|
60 |
if null xs then "" else "\<^bsub>" ^ string_for_vars sep xs ^ "\<^esub>" |
|
61 |
||
62 |
(* 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
|
63 |
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
|
64 |
| string_for_sign Minus = "-" |
33192 | 65 |
|
66 |
(* 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
|
67 |
fun xor sn1 sn2 = if sn1 = sn2 then Plus else Minus |
33192 | 68 |
(* 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
|
69 |
val negate = xor Minus |
33192 | 70 |
|
71 |
(* sign_atom -> string *) |
|
72 |
fun string_for_sign_atom (S sn) = string_for_sign sn |
|
73 |
| string_for_sign_atom (V j) = string_for_var j |
|
74 |
||
75 |
(* literal -> string *) |
|
76 |
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn |
|
77 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
78 |
val bool_M = MType (@{type_name bool}, []) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
79 |
val dummy_M = MType (nitpick_prefix ^ "dummy", []) |
33192 | 80 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
81 |
(* mtyp -> bool *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
82 |
fun is_MRec (MRec _) = true |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
83 |
| is_MRec _ = false |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
84 |
(* mtyp -> mtyp * sign_atom * mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
85 |
fun dest_MFun (MFun z) = z |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
86 |
| dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M]) |
33192 | 87 |
|
88 |
val no_prec = 100 |
|
89 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
90 |
(* mtyp -> int *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
91 |
fun precedence_of_mtype (MFun _) = 1 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
92 |
| precedence_of_mtype (MPair _) = 2 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
93 |
| precedence_of_mtype _ = no_prec |
33192 | 94 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
95 |
(* mtyp -> string *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
96 |
val string_for_mtype = |
33192 | 97 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
98 |
(* int -> mtyp -> string *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
99 |
fun aux outer_prec M = |
33192 | 100 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
101 |
val prec = precedence_of_mtype M |
33192 | 102 |
val need_parens = (prec < outer_prec) |
103 |
in |
|
104 |
(if need_parens then "(" else "") ^ |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
105 |
(if M = dummy_M then |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
106 |
"_" |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
107 |
else case M of |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
108 |
MAlpha => "\<alpha>" |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
109 |
| MFun (M1, a, M2) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
110 |
aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^ |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
111 |
string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
112 |
| MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
113 |
| MType (s, []) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
114 |
if s = @{type_name prop} orelse s = @{type_name bool} then "o" |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
115 |
else s |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
116 |
| MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
117 |
| MRec (s, _) => "[" ^ s ^ "]") ^ |
33192 | 118 |
(if need_parens then ")" else "") |
119 |
end |
|
120 |
in aux 0 end |
|
121 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
122 |
(* mtyp -> mtyp list *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
123 |
fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
124 |
| flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
125 |
| flatten_mtype M = [M] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
126 |
|
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
127 |
(* mterm -> bool *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
128 |
fun precedence_of_mterm (MRaw _) = no_prec |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
129 |
| precedence_of_mterm (MAbs _) = 1 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
130 |
| precedence_of_mterm (MApp _) = 2 |
33192 | 131 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
132 |
(* Proof.context -> mterm -> string *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
133 |
fun string_for_mterm ctxt = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
134 |
let |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
135 |
(* mtype -> string *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
136 |
fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>" |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
137 |
(* int -> mterm -> string *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
138 |
fun aux outer_prec m = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
139 |
let |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
140 |
val prec = precedence_of_mterm m |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
141 |
val need_parens = (prec < outer_prec) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
142 |
in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
143 |
(if need_parens then "(" else "") ^ |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
144 |
(case m of |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
145 |
MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
146 |
| MAbs (s, _, M, a, m) => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
147 |
"\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^ |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
148 |
string_for_sign_atom a ^ "\<^esup> " ^ aux prec m |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
149 |
| MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^ |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
150 |
(if need_parens then ")" else "") |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
151 |
end |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
152 |
in aux 0 end |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
153 |
|
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
154 |
(* mterm -> mtyp *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
155 |
fun mtype_of_mterm (MRaw (_, M)) = M |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
156 |
| mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
157 |
| mtype_of_mterm (MApp (m1, _)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
158 |
case mtype_of_mterm m1 of |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
159 |
MFun (_, _, M12) => M12 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
160 |
| M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1]) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
161 |
|
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
162 |
(* hol_context -> bool -> typ -> mdata *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
163 |
fun initial_mdata hol_ctxt binarize alpha_T = |
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset
|
164 |
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T, |
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset
|
165 |
max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [], |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
166 |
constr_cache = Unsynchronized.ref []} : mdata) |
33192 | 167 |
|
168 |
(* typ -> typ -> bool *) |
|
169 |
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
|
170 |
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
|
171 |
exists (could_exist_alpha_subtype alpha_T) Ts) |
33192 | 172 |
| could_exist_alpha_subtype alpha_T T = (T = alpha_T) |
173 |
(* theory -> typ -> typ -> bool *) |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
174 |
fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T = |
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
175 |
could_exist_alpha_subtype alpha_T T |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
176 |
| could_exist_alpha_sub_mtype thy alpha_T T = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
177 |
(T = alpha_T orelse is_datatype thy [(NONE, true)] T) |
33192 | 178 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
179 |
(* mtyp -> bool *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
180 |
fun exists_alpha_sub_mtype MAlpha = true |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
181 |
| exists_alpha_sub_mtype (MFun (M1, _, M2)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
182 |
exists exists_alpha_sub_mtype [M1, M2] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
183 |
| exists_alpha_sub_mtype (MPair (M1, M2)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
184 |
exists exists_alpha_sub_mtype [M1, M2] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
185 |
| exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
186 |
| exists_alpha_sub_mtype (MRec _) = true |
33192 | 187 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
188 |
(* mtyp -> bool *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
189 |
fun exists_alpha_sub_mtype_fresh MAlpha = true |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
190 |
| exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
191 |
| exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
192 |
exists_alpha_sub_mtype_fresh M2 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
193 |
| exists_alpha_sub_mtype_fresh (MPair (M1, M2)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
194 |
exists exists_alpha_sub_mtype_fresh [M1, M2] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
195 |
| exists_alpha_sub_mtype_fresh (MType (_, Ms)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
196 |
exists exists_alpha_sub_mtype_fresh Ms |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
197 |
| exists_alpha_sub_mtype_fresh (MRec _) = true |
33192 | 198 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
199 |
(* string * typ list -> mtyp list -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
200 |
fun constr_mtype_for_binders z Ms = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
201 |
fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z) |
33192 | 202 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
203 |
(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
204 |
fun repair_mtype _ _ MAlpha = MAlpha |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
205 |
| repair_mtype cache seen (MFun (M1, a, M2)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
206 |
MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
207 |
| repair_mtype cache seen (MPair Mp) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
208 |
MPair (pairself (repair_mtype cache seen) Mp) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
209 |
| repair_mtype cache seen (MType (s, Ms)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
210 |
MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
211 |
| repair_mtype cache seen (MRec (z as (s, _))) = |
33192 | 212 |
case AList.lookup (op =) cache z |> the of |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
213 |
MRec _ => MType (s, []) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
214 |
| M => if member (op =) seen M then MType (s, []) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
215 |
else repair_mtype cache (M :: seen) M |
33192 | 216 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
217 |
(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *) |
33192 | 218 |
fun repair_datatype_cache cache = |
219 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
220 |
(* (string * typ list) * mtyp -> unit *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
221 |
fun repair_one (z, M) = |
33192 | 222 |
Unsynchronized.change cache |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
223 |
(AList.update (op =) (z, repair_mtype (!cache) [] M)) |
33192 | 224 |
in List.app repair_one (rev (!cache)) end |
225 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
226 |
(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *) |
33192 | 227 |
fun repair_constr_cache dtype_cache constr_cache = |
228 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
229 |
(* styp * mtyp -> unit *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
230 |
fun repair_one (x, M) = |
33192 | 231 |
Unsynchronized.change constr_cache |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
232 |
(AList.update (op =) (x, repair_mtype dtype_cache [] M)) |
33192 | 233 |
in List.app repair_one (!constr_cache) end |
234 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
235 |
(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
236 |
fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 = |
33192 | 237 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
238 |
val M1 = fresh_mtype_for_type mdata T1 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
239 |
val M2 = fresh_mtype_for_type mdata T2 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
240 |
val a = if is_boolean_type (body_type T2) andalso |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
241 |
exists_alpha_sub_mtype_fresh M1 then |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
242 |
V (Unsynchronized.inc max_fresh) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
243 |
else |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
244 |
S Minus |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
245 |
in (M1, a, M2) end |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
246 |
(* mdata -> typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
247 |
and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
248 |
datatype_cache, constr_cache, ...}) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
249 |
let |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
250 |
(* typ -> typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
251 |
val do_fun = MFun oo fresh_mfun_for_fun_type mdata |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
252 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
253 |
fun do_type T = |
33192 | 254 |
if T = alpha_T then |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
255 |
MAlpha |
33192 | 256 |
else case T of |
257 |
Type ("fun", [T1, T2]) => do_fun T1 T2 |
|
258 |
| Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
259 |
| Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2)) |
33192 | 260 |
| Type (z as (s, _)) => |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
261 |
if could_exist_alpha_sub_mtype thy alpha_T T then |
33192 | 262 |
case AList.lookup (op =) (!datatype_cache) z of |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
263 |
SOME M => M |
33192 | 264 |
| NONE => |
265 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
266 |
val _ = Unsynchronized.change datatype_cache (cons (z, MRec z)) |
35219
15a5f213ef5b
fix bug in Nitpick's monotonicity code w.r.t. binary integers
blanchet
parents:
35190
diff
changeset
|
267 |
val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
268 |
val (all_Ms, constr_Ms) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
269 |
fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) => |
33192 | 270 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
271 |
val binder_Ms = map do_type (binder_types T') |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
272 |
val new_Ms = filter exists_alpha_sub_mtype_fresh |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
273 |
binder_Ms |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
274 |
val constr_M = constr_mtype_for_binders z |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
275 |
binder_Ms |
33192 | 276 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
277 |
(union (op =) new_Ms all_Ms, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
278 |
constr_M :: constr_Ms) |
33192 | 279 |
end) |
280 |
xs ([], []) |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
281 |
val M = MType (s, all_Ms) |
33192 | 282 |
val _ = Unsynchronized.change datatype_cache |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
283 |
(AList.update (op =) (z, M)) |
33192 | 284 |
val _ = Unsynchronized.change constr_cache |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
285 |
(append (xs ~~ constr_Ms)) |
33192 | 286 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
287 |
if forall (not o is_MRec o snd) (!datatype_cache) then |
33192 | 288 |
(repair_datatype_cache datatype_cache; |
289 |
repair_constr_cache (!datatype_cache) constr_cache; |
|
290 |
AList.lookup (op =) (!datatype_cache) z |> the) |
|
291 |
else |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
292 |
M |
33192 | 293 |
end |
294 |
else |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
295 |
MType (s, []) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
296 |
| _ => MType (Refute.string_of_typ T, []) |
33192 | 297 |
in do_type end |
298 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
299 |
(* mtyp -> mtyp list *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
300 |
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
301 |
| prodM_factors M = [M] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
302 |
(* mtyp -> mtyp list * mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
303 |
fun curried_strip_mtype (MFun (M1, S Minus, M2)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
304 |
curried_strip_mtype M2 |>> append (prodM_factors M1) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
305 |
| curried_strip_mtype M = ([], M) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
306 |
(* string -> mtyp -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
307 |
fun sel_mtype_from_constr_mtype s M = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
308 |
let val (arg_Ms, dataM) = curried_strip_mtype M in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
309 |
MFun (dataM, S Minus, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
310 |
case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n) |
33192 | 311 |
end |
312 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
313 |
(* mdata -> styp -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
314 |
fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache, |
33192 | 315 |
...}) (x as (_, T)) = |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
316 |
if could_exist_alpha_sub_mtype thy alpha_T T then |
33192 | 317 |
case AList.lookup (op =) (!constr_cache) x of |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
318 |
SOME M => M |
35384 | 319 |
| NONE => if T = alpha_T then |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
320 |
let val M = fresh_mtype_for_type mdata T in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
321 |
(Unsynchronized.change constr_cache (cons (x, M)); M) |
35384 | 322 |
end |
323 |
else |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
324 |
(fresh_mtype_for_type mdata (body_type T); |
35384 | 325 |
AList.lookup (op =) (!constr_cache) x |> the) |
33192 | 326 |
else |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
327 |
fresh_mtype_for_type mdata T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
328 |
fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = |
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35079
diff
changeset
|
329 |
x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
330 |
|> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s |
33192 | 331 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
332 |
(* literal list -> mtyp -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
333 |
fun instantiate_mtype lits = |
33192 | 334 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
335 |
(* mtyp -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
336 |
fun aux MAlpha = MAlpha |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
337 |
| aux (MFun (M1, V x, M2)) = |
33192 | 338 |
let |
339 |
val a = case AList.lookup (op =) lits x of |
|
340 |
SOME sn => S sn |
|
341 |
| NONE => V x |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
342 |
in MFun (aux M1, a, aux M2) end |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
343 |
| aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
344 |
| aux (MPair Mp) = MPair (pairself aux Mp) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
345 |
| aux (MType (s, Ms)) = MType (s, map aux Ms) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
346 |
| aux (MRec z) = MRec z |
33192 | 347 |
in aux end |
348 |
||
349 |
datatype comp_op = Eq | Leq |
|
350 |
||
351 |
type comp = sign_atom * sign_atom * comp_op * var list |
|
352 |
type sign_expr = literal list |
|
353 |
||
354 |
datatype constraint_set = |
|
355 |
UnsolvableCSet | |
|
356 |
CSet of literal list * comp list * sign_expr list |
|
357 |
||
358 |
(* comp_op -> string *) |
|
359 |
fun string_for_comp_op Eq = "=" |
|
360 |
| string_for_comp_op Leq = "\<le>" |
|
361 |
||
362 |
(* sign_expr -> string *) |
|
363 |
fun string_for_sign_expr [] = "\<bot>" |
|
364 |
| string_for_sign_expr lits = |
|
365 |
space_implode " \<or> " (map string_for_literal lits) |
|
366 |
||
367 |
(* constraint_set *) |
|
368 |
val slack = CSet ([], [], []) |
|
369 |
||
370 |
(* literal -> literal list option -> literal list option *) |
|
371 |
fun do_literal _ NONE = NONE |
|
372 |
| do_literal (x, sn) (SOME lits) = |
|
373 |
case AList.lookup (op =) lits x of |
|
374 |
SOME sn' => if sn = sn' then SOME lits else NONE |
|
375 |
| NONE => SOME ((x, sn) :: lits) |
|
376 |
||
377 |
(* comp_op -> var list -> sign_atom -> sign_atom -> literal list * comp list |
|
378 |
-> (literal list * comp list) option *) |
|
379 |
fun do_sign_atom_comp Eq [] a1 a2 (accum as (lits, comps)) = |
|
380 |
(case (a1, a2) of |
|
381 |
(S sn1, S sn2) => if sn1 = sn2 then SOME accum else NONE |
|
382 |
| (V x1, S sn2) => |
|
383 |
Option.map (rpair comps) (do_literal (x1, sn2) (SOME lits)) |
|
384 |
| (V _, V _) => SOME (lits, insert (op =) (a1, a2, Eq, []) comps) |
|
385 |
| _ => do_sign_atom_comp Eq [] a2 a1 accum) |
|
386 |
| do_sign_atom_comp Leq [] a1 a2 (accum as (lits, comps)) = |
|
387 |
(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
|
388 |
(_, 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
|
389 |
| (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
|
390 |
| (S Minus, S Plus) => NONE |
33192 | 391 |
| (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps) |
392 |
| _ => do_sign_atom_comp Eq [] a1 a2 accum) |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
393 |
| do_sign_atom_comp cmp xs a1 a2 (lits, comps) = |
33192 | 394 |
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) |
395 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
396 |
(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option |
33192 | 397 |
-> (literal list * comp list) option *) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
398 |
fun do_mtype_comp _ _ _ _ NONE = NONE |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
399 |
| do_mtype_comp _ _ MAlpha MAlpha accum = accum |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
400 |
| do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) |
33192 | 401 |
(SOME accum) = |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
402 |
accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
403 |
|> do_mtype_comp Eq xs M12 M22 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
404 |
| do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) |
33192 | 405 |
(SOME accum) = |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
406 |
(if exists_alpha_sub_mtype M11 then |
33192 | 407 |
accum |> do_sign_atom_comp Leq xs a1 a2 |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
408 |
|> do_mtype_comp Leq xs M21 M11 |
33192 | 409 |
|> (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
|
410 |
S Minus => I |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
411 |
| S Plus => do_mtype_comp Leq xs M11 M21 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
412 |
| V x => do_mtype_comp Leq (x :: xs) M11 M21) |
33192 | 413 |
else |
414 |
SOME accum) |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
415 |
|> do_mtype_comp Leq xs M12 M22 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
416 |
| do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22)) |
33192 | 417 |
accum = |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
418 |
(accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)] |
33192 | 419 |
handle Library.UnequalLengths => |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
420 |
raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
421 |
| do_mtype_comp _ _ (MType _) (MType _) accum = |
33192 | 422 |
accum (* no need to compare them thanks to the cache *) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
423 |
| do_mtype_comp _ _ M1 M2 _ = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
424 |
raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]) |
33192 | 425 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
426 |
(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
427 |
fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
428 |
| add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
429 |
(print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^ |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
430 |
" " ^ string_for_mtype M2); |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
431 |
case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of |
33192 | 432 |
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
433 |
| SOME (lits, comps) => CSet (lits, comps, sexps)) |
|
434 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
435 |
(* mtyp -> mtyp -> constraint_set -> constraint_set *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
436 |
val add_mtypes_equal = add_mtype_comp Eq |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
437 |
val add_is_sub_mtype = add_mtype_comp Leq |
33192 | 438 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
439 |
(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option |
33192 | 440 |
-> (literal list * sign_expr list) option *) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
441 |
fun do_notin_mtype_fv _ _ _ NONE = NONE |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
442 |
| do_notin_mtype_fv Minus _ MAlpha accum = accum |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
443 |
| do_notin_mtype_fv Plus [] MAlpha _ = NONE |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
444 |
| do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) = |
33192 | 445 |
SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
446 |
| do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) = |
33192 | 447 |
SOME (lits, insert (op =) sexp sexps) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
448 |
| do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) 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
|
449 |
accum |> (if sn' = Plus andalso sn = Plus then |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
450 |
do_notin_mtype_fv Plus sexp M1 |
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
|
451 |
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
|
452 |
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
|
453 |
|> (if sn' = Minus orelse sn = Plus then |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
454 |
do_notin_mtype_fv Minus sexp M1 |
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
|
455 |
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
|
456 |
I) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
457 |
|> do_notin_mtype_fv sn sexp M2 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
458 |
| do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) 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
|
459 |
accum |> (case do_literal (x, Minus) (SOME sexp) of |
33192 | 460 |
NONE => I |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
461 |
| SOME sexp' => do_notin_mtype_fv Plus sexp' M1) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
462 |
|> do_notin_mtype_fv Minus sexp M1 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
463 |
|> do_notin_mtype_fv Plus sexp M2 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
464 |
| do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) 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
|
465 |
accum |> (case do_literal (x, Plus) (SOME sexp) of |
33192 | 466 |
NONE => I |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
467 |
| SOME sexp' => do_notin_mtype_fv Plus sexp' M1) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
468 |
|> do_notin_mtype_fv Minus sexp M2 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
469 |
| do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
470 |
accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2] |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
471 |
| do_notin_mtype_fv sn sexp (MType (_, Ms)) accum = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
472 |
accum |> fold (do_notin_mtype_fv sn sexp) Ms |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
473 |
| do_notin_mtype_fv _ _ M _ = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
474 |
raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M]) |
33192 | 475 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
476 |
(* sign -> mtyp -> constraint_set -> constraint_set *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
477 |
fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
478 |
| add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
479 |
(print_g ("*** Add " ^ string_for_mtype M ^ " 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
|
480 |
(case sn of Minus => "unique" | Plus => "total") ^ "."); |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
481 |
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of |
33192 | 482 |
NONE => (print_g "**** Unsolvable"; UnsolvableCSet) |
483 |
| SOME (lits, sexps) => CSet (lits, comps, sexps)) |
|
484 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
485 |
(* mtyp -> constraint_set -> constraint_set *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
486 |
val add_mtype_is_right_unique = add_notin_mtype_fv Minus |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
487 |
val add_mtype_is_right_total = add_notin_mtype_fv Plus |
33192 | 488 |
|
35384 | 489 |
val bool_from_minus = true |
490 |
||
33192 | 491 |
(* sign -> bool *) |
35384 | 492 |
fun bool_from_sign Plus = not bool_from_minus |
493 |
| bool_from_sign Minus = bool_from_minus |
|
33192 | 494 |
(* bool -> sign *) |
35384 | 495 |
fun sign_from_bool b = if b = bool_from_minus then Minus else Plus |
33192 | 496 |
|
497 |
(* literal -> PropLogic.prop_formula *) |
|
498 |
fun prop_for_literal (x, sn) = |
|
499 |
(not (bool_from_sign sn) ? PropLogic.Not) (PropLogic.BoolVar x) |
|
500 |
(* sign_atom -> PropLogic.prop_formula *) |
|
501 |
fun prop_for_sign_atom_eq (S sn', sn) = |
|
502 |
if sn = sn' then PropLogic.True else PropLogic.False |
|
503 |
| prop_for_sign_atom_eq (V x, sn) = prop_for_literal (x, sn) |
|
504 |
(* sign_expr -> PropLogic.prop_formula *) |
|
505 |
fun prop_for_sign_expr xs = PropLogic.exists (map prop_for_literal xs) |
|
506 |
(* var list -> sign -> PropLogic.prop_formula *) |
|
507 |
fun prop_for_exists_eq xs sn = |
|
508 |
PropLogic.exists (map (fn x => prop_for_literal (x, sn)) xs) |
|
509 |
(* comp -> PropLogic.prop_formula *) |
|
510 |
fun prop_for_comp (a1, a2, Eq, []) = |
|
511 |
PropLogic.SAnd (prop_for_comp (a1, a2, Leq, []), |
|
512 |
prop_for_comp (a2, a1, Leq, [])) |
|
513 |
| 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
|
514 |
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
|
515 |
prop_for_sign_atom_eq (a2, Minus)) |
33192 | 516 |
| 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
|
517 |
PropLogic.SOr (prop_for_exists_eq xs Minus, prop_for_comp (a1, a2, cmp, [])) |
33192 | 518 |
|
519 |
(* 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
|
520 |
fun literals_from_assignments max_var assigns lits = |
33192 | 521 |
fold (fn x => fn accum => |
522 |
if AList.defined (op =) lits x then |
|
523 |
accum |
|
34123
c4988215a691
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
blanchet
parents:
34121
diff
changeset
|
524 |
else case assigns x of |
33192 | 525 |
SOME b => (x, sign_from_bool b) :: accum |
526 |
| NONE => accum) (max_var downto 1) lits |
|
527 |
||
528 |
(* comp -> string *) |
|
529 |
fun string_for_comp (a1, a2, cmp, xs) = |
|
530 |
string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^ |
|
531 |
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2 |
|
532 |
||
533 |
(* literal list -> comp list -> sign_expr list -> unit *) |
|
534 |
fun print_problem lits comps sexps = |
|
535 |
print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @ |
|
536 |
map string_for_comp comps @ |
|
537 |
map string_for_sign_expr sexps)) |
|
538 |
||
539 |
(* literal list -> unit *) |
|
540 |
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
|
541 |
let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in |
33192 | 542 |
print_g ("*** Solution:\n" ^ |
543 |
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^ |
|
544 |
"-: " ^ commas (map (string_for_var o fst) neg)) |
|
545 |
end |
|
546 |
||
35384 | 547 |
(* var -> constraint_set -> literal list option *) |
33192 | 548 |
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE) |
549 |
| solve max_var (CSet (lits, comps, sexps)) = |
|
550 |
let |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
551 |
(* (int -> bool option) -> literal list option *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
552 |
fun do_assigns assigns = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
553 |
SOME (literals_from_assignments max_var assigns lits |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
554 |
|> tap print_solution) |
33192 | 555 |
val _ = print_problem lits comps sexps |
556 |
val prop = PropLogic.all (map prop_for_literal lits @ |
|
557 |
map prop_for_comp comps @ |
|
558 |
map prop_for_sign_expr sexps) |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
559 |
val default_val = bool_from_sign Minus |
33192 | 560 |
in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
561 |
if PropLogic.eval (K default_val) prop then |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
562 |
do_assigns (K (SOME default_val)) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
563 |
else |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
564 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
565 |
(* use the first ML solver (to avoid startup overhead) *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
566 |
val solvers = !SatSolver.solvers |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
567 |
|> filter (member (op =) ["dptsat", "dpll"] o fst) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
568 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
569 |
case snd (hd solvers) prop of |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
570 |
SatSolver.SATISFIABLE assigns => do_assigns assigns |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
571 |
| _ => NONE |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
572 |
end |
33192 | 573 |
end |
574 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
575 |
type mtype_schema = mtyp * constraint_set |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
576 |
type mtype_context = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
577 |
{bounds: mtyp list, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
578 |
frees: (styp * mtyp) list, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
579 |
consts: (styp * mtyp) list} |
33192 | 580 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
581 |
type accumulator = mtype_context * constraint_set |
33192 | 582 |
|
583 |
val initial_gamma = {bounds = [], frees = [], consts = []} |
|
584 |
val unsolvable_accum = (initial_gamma, UnsolvableCSet) |
|
585 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
586 |
(* mtyp -> mtype_context -> mtype_context *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
587 |
fun push_bound M {bounds, frees, consts} = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
588 |
{bounds = M :: bounds, frees = frees, consts = consts} |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
589 |
(* mtype_context -> mtype_context *) |
33192 | 590 |
fun pop_bound {bounds, frees, consts} = |
591 |
{bounds = tl bounds, frees = frees, consts = consts} |
|
592 |
handle List.Empty => initial_gamma |
|
593 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
594 |
(* mdata -> term -> accumulator -> mterm * accumulator *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
595 |
fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs, |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
596 |
def_table, ...}, |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
597 |
alpha_T, max_fresh, ...}) = |
33192 | 598 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
599 |
(* typ -> typ -> mtyp * sign_atom * mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
600 |
val mfun_for = fresh_mfun_for_fun_type mdata |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
601 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
602 |
val mtype_for = fresh_mtype_for_type mdata |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
603 |
(* mtyp -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
604 |
fun pos_set_mtype_for_dom M = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
605 |
MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
606 |
(* typ -> accumulator -> mterm * accumulator *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
607 |
fun do_all T (gamma, cset) = |
33192 | 608 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
609 |
val abs_M = mtype_for (domain_type (domain_type T)) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
610 |
val body_M = mtype_for (body_type T) |
33192 | 611 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
612 |
(MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M), |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
613 |
(gamma, cset |> add_mtype_is_right_total abs_M)) |
33192 | 614 |
end |
615 |
fun do_equals T (gamma, cset) = |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
616 |
let val M = mtype_for (domain_type T) in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
617 |
(MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh), |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
618 |
mtype_for (nth_range_type 2 T))), |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
619 |
(gamma, cset |> add_mtype_is_right_unique M)) |
33192 | 620 |
end |
621 |
fun do_robust_set_operation T (gamma, cset) = |
|
622 |
let |
|
623 |
val set_T = domain_type T |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
624 |
val M1 = mtype_for set_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
625 |
val M2 = mtype_for set_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
626 |
val M3 = mtype_for set_T |
33192 | 627 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
628 |
(MFun (M1, S Minus, MFun (M2, S Minus, M3)), |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
629 |
(gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3)) |
33192 | 630 |
end |
631 |
fun do_fragile_set_operation T (gamma, cset) = |
|
632 |
let |
|
633 |
val set_T = domain_type T |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
634 |
val set_M = mtype_for set_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
635 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
636 |
fun custom_mtype_for (T as Type ("fun", [T1, T2])) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
637 |
if T = set_T then set_M |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
638 |
else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
639 |
| custom_mtype_for T = mtype_for T |
33192 | 640 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
641 |
(custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M)) |
33192 | 642 |
end |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
643 |
(* typ -> accumulator -> mtyp * accumulator *) |
33192 | 644 |
fun do_pair_constr T accum = |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
645 |
case mtype_for (nth_range_type 2 T) of |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
646 |
M as MPair (a_M, b_M) => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
647 |
(MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
648 |
| M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M]) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
649 |
(* int -> typ -> accumulator -> mtyp * accumulator *) |
33192 | 650 |
fun do_nth_pair_sel n T = |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
651 |
case mtype_for (domain_type T) of |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
652 |
M as MPair (a_M, b_M) => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
653 |
pair (MFun (M, S Minus, if n = 0 then a_M else b_M)) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
654 |
| M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M]) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
655 |
(* mtyp * accumulator *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
656 |
val mtype_unsolvable = (dummy_M, unsolvable_accum) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
657 |
(* term -> mterm * accumulator *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
658 |
fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
659 |
(* term -> string -> typ -> term -> term -> term -> accumulator |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
660 |
-> mterm * accumulator *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
661 |
fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum = |
33192 | 662 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
663 |
val abs_M = mtype_for abs_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
664 |
val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
665 |
val expected_bound_M = pos_set_mtype_for_dom abs_M |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
666 |
val (body_m, accum) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
667 |
accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
668 |
|> do_term body_t ||> apfst pop_bound |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
669 |
val bound_M = mtype_of_mterm bound_m |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
670 |
val (M1, a, M2) = dest_MFun bound_M |
33192 | 671 |
in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
672 |
(MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)), |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
673 |
MAbs (abs_s, abs_T, M1, a, |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
674 |
MApp (MApp (MRaw (connective_t, |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
675 |
mtype_for (fastype_of connective_t)), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
676 |
MApp (bound_m, MRaw (Bound 0, M1))), |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
677 |
body_m))), accum) |
33192 | 678 |
end |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
679 |
(* term -> accumulator -> mterm * accumulator *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
680 |
and do_term t (_, UnsolvableCSet) = mterm_unsolvable t |
33192 | 681 |
| do_term t (accum as (gamma as {bounds, frees, consts}, cset)) = |
682 |
(case t of |
|
683 |
Const (x as (s, T)) => |
|
684 |
(case AList.lookup (op =) consts x of |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
685 |
SOME M => (M, accum) |
33192 | 686 |
| NONE => |
687 |
if not (could_exist_alpha_subtype alpha_T T) then |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
688 |
(mtype_for T, accum) |
33192 | 689 |
else case s of |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
690 |
@{const_name all} => do_all T accum |
33192 | 691 |
| @{const_name "=="} => do_equals T accum |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
692 |
| @{const_name All} => do_all T accum |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
693 |
| @{const_name Ex} => |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
694 |
let val set_T = domain_type T in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
695 |
do_term (Abs (Name.uu, set_T, |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
696 |
@{const Not} $ (HOLogic.mk_eq |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
697 |
(Abs (Name.uu, domain_type set_T, |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
698 |
@{const False}), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
699 |
Bound 0)))) accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
700 |
|>> mtype_of_mterm |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
701 |
end |
33192 | 702 |
| @{const_name "op ="} => do_equals T accum |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
703 |
| @{const_name The} => (print_g "*** The"; mtype_unsolvable) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
704 |
| @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable) |
33192 | 705 |
| @{const_name If} => |
706 |
do_robust_set_operation (range_type T) accum |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
707 |
|>> curry3 MFun bool_M (S Minus) |
33192 | 708 |
| @{const_name Pair} => do_pair_constr T accum |
709 |
| @{const_name fst} => do_nth_pair_sel 0 T accum |
|
710 |
| @{const_name snd} => do_nth_pair_sel 1 T accum |
|
711 |
| @{const_name Id} => |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
712 |
(MFun (mtype_for (domain_type T), S Minus, bool_M), accum) |
33192 | 713 |
| @{const_name insert} => |
714 |
let |
|
715 |
val set_T = domain_type (range_type T) |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
716 |
val M1 = mtype_for (domain_type set_T) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
717 |
val M1' = pos_set_mtype_for_dom M1 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
718 |
val M2 = mtype_for set_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
719 |
val M3 = mtype_for set_T |
33192 | 720 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
721 |
(MFun (M1, S Minus, MFun (M2, S Minus, M3)), |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
722 |
(gamma, cset |> add_mtype_is_right_unique M1 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
723 |
|> add_is_sub_mtype M1' M3 |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
724 |
|> add_is_sub_mtype M2 M3)) |
33192 | 725 |
end |
726 |
| @{const_name converse} => |
|
727 |
let |
|
728 |
val x = Unsynchronized.inc max_fresh |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
729 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
730 |
fun mtype_for_set T = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
731 |
MFun (mtype_for (domain_type T), V x, bool_M) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
732 |
val ab_set_M = domain_type T |> mtype_for_set |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
733 |
val ba_set_M = range_type T |> mtype_for_set |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
734 |
in (MFun (ab_set_M, S Minus, ba_set_M), accum) end |
33192 | 735 |
| @{const_name trancl} => do_fragile_set_operation T accum |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
736 |
| @{const_name rtrancl} => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
737 |
(print_g "*** rtrancl"; mtype_unsolvable) |
33192 | 738 |
| @{const_name finite} => |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
739 |
if is_finite_type hol_ctxt T then |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
740 |
let val M1 = mtype_for (domain_type (domain_type T)) in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
741 |
(MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
742 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
743 |
else |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
744 |
(print_g "*** finite"; mtype_unsolvable) |
33192 | 745 |
| @{const_name rel_comp} => |
746 |
let |
|
747 |
val x = Unsynchronized.inc max_fresh |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
748 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
749 |
fun mtype_for_set T = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
750 |
MFun (mtype_for (domain_type T), V x, bool_M) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
751 |
val bc_set_M = domain_type T |> mtype_for_set |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
752 |
val ab_set_M = domain_type (range_type T) |> mtype_for_set |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
753 |
val ac_set_M = nth_range_type 2 T |> mtype_for_set |
33192 | 754 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
755 |
(MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)), |
33192 | 756 |
accum) |
757 |
end |
|
758 |
| @{const_name image} => |
|
759 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
760 |
val a_M = mtype_for (domain_type (domain_type T)) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
761 |
val b_M = mtype_for (range_type (domain_type T)) |
33192 | 762 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
763 |
(MFun (MFun (a_M, S Minus, b_M), S Minus, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
764 |
MFun (pos_set_mtype_for_dom a_M, S Minus, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
765 |
pos_set_mtype_for_dom b_M)), accum) |
33192 | 766 |
end |
767 |
| @{const_name Sigma} => |
|
768 |
let |
|
769 |
val x = Unsynchronized.inc max_fresh |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
770 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
771 |
fun mtype_for_set T = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
772 |
MFun (mtype_for (domain_type T), V x, bool_M) |
33192 | 773 |
val a_set_T = domain_type T |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
774 |
val a_M = mtype_for (domain_type a_set_T) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
775 |
val b_set_M = mtype_for_set (range_type (domain_type |
33192 | 776 |
(range_type T))) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
777 |
val a_set_M = mtype_for_set a_set_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
778 |
val a_to_b_set_M = MFun (a_M, S Minus, b_set_M) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
779 |
val ab_set_M = mtype_for_set (nth_range_type 2 T) |
33192 | 780 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
781 |
(MFun (a_set_M, S Minus, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
782 |
MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) |
33192 | 783 |
end |
784 |
| @{const_name Tha} => |
|
785 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
786 |
val a_M = mtype_for (domain_type (domain_type T)) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
787 |
val a_set_M = pos_set_mtype_for_dom a_M |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
788 |
in (MFun (a_set_M, S Minus, a_M), accum) end |
33192 | 789 |
| @{const_name FunBox} => |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
790 |
let val dom_M = mtype_for (domain_type T) in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
791 |
(MFun (dom_M, S Minus, dom_M), accum) |
33192 | 792 |
end |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
793 |
| _ => |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
794 |
if s = @{const_name minus_class.minus} andalso |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
795 |
is_set_type (domain_type T) then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
796 |
let |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
797 |
val set_T = domain_type T |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
798 |
val left_set_M = mtype_for set_T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
799 |
val right_set_M = mtype_for set_T |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
800 |
in |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
801 |
(MFun (left_set_M, S Minus, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
802 |
MFun (right_set_M, S Minus, left_set_M)), |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
803 |
(gamma, cset |> add_mtype_is_right_unique right_set_M |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
804 |
|> add_is_sub_mtype right_set_M left_set_M)) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
805 |
end |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
806 |
else if s = @{const_name ord_class.less_eq} andalso |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
807 |
is_set_type (domain_type T) then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
808 |
do_fragile_set_operation T accum |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
809 |
else if (s = @{const_name semilattice_inf_class.inf} orelse |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
810 |
s = @{const_name semilattice_sup_class.sup}) andalso |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
811 |
is_set_type (domain_type T) then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
812 |
do_robust_set_operation T accum |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
813 |
else if is_sel s then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
814 |
if constr_name_for_sel_like s = @{const_name FunBox} then |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
815 |
let val dom_M = mtype_for (domain_type T) in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
816 |
(MFun (dom_M, S Minus, dom_M), accum) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
817 |
end |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
818 |
else |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
819 |
(mtype_for_sel mdata x, accum) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
820 |
else if is_constr thy stds x then |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
821 |
(mtype_for_constr mdata x, accum) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
822 |
else if is_built_in_const thy stds fast_descrs x then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
823 |
case def_of_const thy def_table x of |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
824 |
SOME t' => do_term t' accum |>> mtype_of_mterm |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
825 |
| NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
826 |
else |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
827 |
let val M = mtype_for T in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
828 |
(M, ({bounds = bounds, frees = frees, |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
829 |
consts = (x, M) :: consts}, cset)) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
830 |
end) |>> curry MRaw t |
33192 | 831 |
| Free (x as (_, T)) => |
832 |
(case AList.lookup (op =) frees x of |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
833 |
SOME M => (M, accum) |
33192 | 834 |
| NONE => |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
835 |
let val M = mtype_for T in |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
836 |
(M, ({bounds = bounds, frees = (x, M) :: frees, |
33192 | 837 |
consts = consts}, cset)) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
838 |
end) |>> curry MRaw t |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
839 |
| Var _ => (print_g "*** Var"; mterm_unsolvable t) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
840 |
| Bound j => (MRaw (t, nth bounds j), accum) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
841 |
| Abs (s, T, t' as @{const False}) => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
842 |
let val (M1, a, M2) = mfun_for T bool_T in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
843 |
(MAbs (s, T, M1, a, MRaw (t', M2)), accum) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
844 |
end |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
845 |
| Abs (s, T, t') => |
34998 | 846 |
((case t' of |
847 |
t1' $ Bound 0 => |
|
848 |
if not (loose_bvar1 (t1', 0)) then |
|
849 |
do_term (incr_boundvars ~1 t1') accum |
|
850 |
else |
|
851 |
raise SAME () |
|
852 |
| _ => raise SAME ()) |
|
853 |
handle SAME () => |
|
854 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
855 |
val M = mtype_for T |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
856 |
val (m', accum) = do_term t' (accum |>> push_bound M) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
857 |
in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
858 |
| (t0 as Const (@{const_name All}, _)) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
859 |
$ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
860 |
do_bounded_quantifier t0 s' T' t10 t11 t12 accum |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
861 |
| (t0 as Const (@{const_name Ex}, _)) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
862 |
$ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) => |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
863 |
do_bounded_quantifier t0 s' T' t10 t11 t12 accum |
33192 | 864 |
| Const (@{const_name Let}, _) $ t1 $ t2 => |
865 |
do_term (betapply (t2, t1)) accum |
|
866 |
| t1 $ t2 => |
|
867 |
let |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
868 |
val (m1, accum) = do_term t1 accum |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
869 |
val (m2, accum) = do_term t2 accum |
33192 | 870 |
in |
871 |
case accum of |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
872 |
(_, UnsolvableCSet) => mterm_unsolvable t |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
873 |
| _ => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
874 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
875 |
val M11 = mtype_of_mterm m1 |> dest_MFun |> #1 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
876 |
val M2 = mtype_of_mterm m2 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
877 |
in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end |
33192 | 878 |
end) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
879 |
|> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^ |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
880 |
string_for_mterm ctxt m)) |
33192 | 881 |
in do_term end |
882 |
||
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
883 |
(* mdata -> styp -> term -> term -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
884 |
fun consider_general_equals mdata (x as (_, T)) t1 t2 accum = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
885 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
886 |
val (m1, accum) = consider_term mdata t1 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
887 |
val (m2, accum) = consider_term mdata t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
888 |
val M1 = mtype_of_mterm m1 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
889 |
val M2 = mtype_of_mterm m2 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
890 |
val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
891 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
892 |
(MApp (MApp (MRaw (Const x, |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
893 |
MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
894 |
accum ||> add_mtypes_equal M1 M2) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
895 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
896 |
|
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
897 |
(* mdata -> sign -> term -> accumulator -> mterm * accumulator *) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
898 |
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) = |
33192 | 899 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
900 |
(* typ -> mtyp *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
901 |
val mtype_for = fresh_mtype_for_type mdata |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
902 |
(* term -> accumulator -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
903 |
val do_term = consider_term mdata |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
904 |
(* sign -> term -> accumulator -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
905 |
fun do_formula _ t (_, UnsolvableCSet) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
906 |
(MRaw (t, dummy_M), unsolvable_accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
907 |
| do_formula sn t accum = |
33192 | 908 |
let |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
909 |
(* styp -> string -> typ -> term -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
910 |
fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t = |
33192 | 911 |
let |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
912 |
val abs_M = mtype_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
|
913 |
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
914 |
val (body_m, accum) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
915 |
accum ||> side_cond ? add_mtype_is_right_total abs_M |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
916 |
|>> push_bound abs_M |> do_formula sn body_t |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
917 |
val body_M = mtype_of_mterm body_m |
33192 | 918 |
in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
919 |
(MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
920 |
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
921 |
accum |>> pop_bound) |
33192 | 922 |
end |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
923 |
(* styp -> term -> term -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
924 |
fun do_equals x t1 t2 = |
33192 | 925 |
case sn of |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
926 |
Plus => do_term t accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
927 |
| Minus => consider_general_equals mdata x t1 t2 accum |
33192 | 928 |
in |
929 |
case t of |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
930 |
Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
931 |
do_quantifier x s1 T1 t1 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
932 |
| Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
933 |
| @{const Trueprop} $ t1 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
934 |
let val (m1, accum) = do_formula sn t1 accum in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
935 |
(MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
936 |
m1), accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
937 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
938 |
| @{const Not} $ t1 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
939 |
let val (m1, accum) = do_formula (negate sn) t1 accum in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
940 |
(MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
941 |
accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
942 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
943 |
| Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
944 |
do_quantifier x s1 T1 t1 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
945 |
| Const (x0 as (s0 as @{const_name Ex}, T0)) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
946 |
$ (t1 as Abs (s1, T1, t1')) => |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
947 |
(case sn of |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
948 |
Plus => do_quantifier x0 s1 T1 t1' |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
949 |
| Minus => |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
950 |
(* ### do elsewhere *) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
951 |
do_term (@{const Not} |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
952 |
$ (HOLogic.eq_const (domain_type T0) $ t1 |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
953 |
$ Abs (Name.uu, T1, @{const False}))) accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
954 |
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
955 |
do_equals x t1 t2 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
956 |
| (t0 as Const (s0, _)) $ t1 $ t2 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
957 |
if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
958 |
s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
959 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
960 |
val impl = (s0 = @{const_name "==>"} orelse |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
961 |
s0 = @{const_name "op -->"}) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
962 |
val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
963 |
val (m2, accum) = do_formula sn t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
964 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
965 |
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
966 |
accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
967 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
968 |
else |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
969 |
do_term t accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
970 |
| _ => do_term t accum |
33192 | 971 |
end |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
972 |
|> tap (fn (m, _) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
973 |
print_g ("\<Gamma> \<turnstile> " ^ |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
974 |
string_for_mterm ctxt m ^ " : o\<^sup>" ^ |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
975 |
string_for_sign sn)) |
33192 | 976 |
in do_formula end |
977 |
||
978 |
(* The harmless axiom optimization below is somewhat too aggressive in the face |
|
979 |
of (rather peculiar) user-defined axioms. *) |
|
980 |
val harmless_consts = |
|
981 |
[@{const_name ord_class.less}, @{const_name ord_class.less_eq}] |
|
982 |
val bounteous_consts = [@{const_name bisim}] |
|
983 |
||
984 |
(* term -> bool *) |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
985 |
fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
986 |
Term.add_consts t [] |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
987 |
|> filter_out (is_built_in_const thy stds fast_descrs) |
33192 | 988 |
|> (forall (member (op =) harmless_consts o original_name o fst) |
989 |
orf exists (member (op =) bounteous_consts o fst)) |
|
990 |
||
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
991 |
(* mdata -> term -> accumulator -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
992 |
fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
993 |
if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M)) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
994 |
else consider_general_formula mdata Plus t |
33192 | 995 |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
996 |
(* mdata -> term -> accumulator -> mterm * accumulator *) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
997 |
fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t = |
33192 | 998 |
if not (is_constr_pattern_formula thy t) then |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
999 |
consider_nondefinitional_axiom mdata t |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35219
diff
changeset
|
1000 |
else if is_harmless_axiom hol_ctxt t then |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1001 |
pair (MRaw (t, dummy_M)) |
33192 | 1002 |
else |
1003 |
let |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1004 |
(* typ -> mtyp *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1005 |
val mtype_for = fresh_mtype_for_type mdata |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1006 |
(* term -> accumulator -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1007 |
val do_term = consider_term mdata |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1008 |
(* term -> string -> typ -> term -> accumulator -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1009 |
fun do_all quant_t abs_s abs_T body_t accum = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1010 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1011 |
val abs_M = mtype_for abs_T |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1012 |
val (body_m, accum) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1013 |
accum |>> push_bound abs_M |> do_formula body_t |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1014 |
val body_M = mtype_of_mterm body_m |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1015 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1016 |
(MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1017 |
MAbs (abs_s, abs_T, abs_M, S Minus, body_m)), |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1018 |
accum |>> pop_bound) |
33192 | 1019 |
end |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1020 |
(* term -> term -> term -> accumulator -> mterm * accumulator *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1021 |
and do_conjunction t0 t1 t2 accum = |
33192 | 1022 |
let |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1023 |
val (m1, accum) = do_formula t1 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1024 |
val (m2, accum) = do_formula t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1025 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1026 |
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1027 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1028 |
and do_implies t0 t1 t2 accum = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1029 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1030 |
val (m1, accum) = do_term t1 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1031 |
val (m2, accum) = do_formula t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1032 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1033 |
(MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1034 |
end |
33192 | 1035 |
(* term -> accumulator -> accumulator *) |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1036 |
and do_formula t (_, UnsolvableCSet) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1037 |
(MRaw (t, dummy_M), unsolvable_accum) |
33192 | 1038 |
| do_formula t accum = |
1039 |
case t of |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1040 |
(t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1041 |
do_all t0 s1 T1 t1 accum |
33192 | 1042 |
| @{const Trueprop} $ t1 => do_formula t1 accum |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1043 |
| Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1044 |
consider_general_equals mdata x t1 t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1045 |
| (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1046 |
| (t0 as @{const Pure.conjunction}) $ t1 $ t2 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1047 |
do_conjunction t0 t1 t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1048 |
| (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1049 |
do_all t0 s0 T1 t1 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1050 |
| Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 => |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1051 |
consider_general_equals mdata x t1 t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1052 |
| (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1053 |
| (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum |
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
1054 |
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\ |
33192 | 1055 |
\do_formula", [t]) |
1056 |
in do_formula t end |
|
1057 |
||
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1058 |
(* Proof.context -> literal list -> term -> mtyp -> string *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1059 |
fun string_for_mtype_of_term ctxt lits t M = |
33192 | 1060 |
Syntax.string_of_term ctxt t ^ " : " ^ |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1061 |
string_for_mtype (instantiate_mtype lits M) |
33192 | 1062 |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1063 |
(* theory -> literal list -> mtype_context -> unit *) |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1064 |
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1065 |
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @ |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1066 |
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts |
33192 | 1067 |
|> cat_lines |> print_g |
1068 |
||
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1069 |
(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1070 |
fun gather f t (ms, accum) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1071 |
let val (m, accum) = f t accum in (m :: ms, accum) end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1072 |
|
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1073 |
(* hol_context -> bool -> typ -> term list * term list -> bool *) |
35384 | 1074 |
fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1075 |
(nondef_ts, def_ts) = |
33192 | 1076 |
let |
35384 | 1077 |
val _ = print_g ("****** Monotonicity analysis: " ^ |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1078 |
string_for_mtype MAlpha ^ " is " ^ |
33192 | 1079 |
Syntax.string_of_typ ctxt alpha_T) |
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1080 |
val mdata as {max_fresh, constr_cache, ...} = |
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1081 |
initial_mdata hol_ctxt binarize alpha_T |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1082 |
|
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1083 |
val accum = (initial_gamma, slack) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1084 |
val (nondef_ms, accum) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1085 |
([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1086 |
|> fold (gather (consider_nondefinitional_axiom mdata)) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1087 |
(tl nondef_ts) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1088 |
val (def_ms, (gamma, cset)) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1089 |
([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts |
33192 | 1090 |
in |
1091 |
case solve (!max_fresh) cset of |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1092 |
SOME lits => (print_mtype_context ctxt lits gamma; true) |
33192 | 1093 |
| _ => false |
1094 |
end |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35384
diff
changeset
|
1095 |
handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms)) |
33192 | 1096 |
|
1097 |
end; |