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