author | blanchet |
Tue, 03 Jan 2012 18:33:17 +0100 | |
changeset 46085 | 447cda88adfe |
parent 46083 | efeaa79f021b |
child 55889 | 6bfbec3dff62 |
permissions | -rw-r--r-- |
33982 | 1 |
(* Title: HOL/Tools/Nitpick/nitpick_rep.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 2008, 2009, 2010 |
33192 | 4 |
|
5 |
Kodkod representations of Nitpick terms. |
|
6 |
*) |
|
7 |
||
8 |
signature NITPICK_REP = |
|
9 |
sig |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
10 |
type polarity = Nitpick_Util.polarity |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
11 |
type scope = Nitpick_Scope.scope |
33192 | 12 |
|
13 |
datatype rep = |
|
14 |
Any | |
|
15 |
Formula of polarity | |
|
16 |
Atom of int * int | |
|
17 |
Struct of rep list | |
|
18 |
Vect of int * rep | |
|
19 |
Func of rep * rep | |
|
20 |
Opt of rep |
|
21 |
||
22 |
exception REP of string * rep list |
|
23 |
||
24 |
val string_for_polarity : polarity -> string |
|
25 |
val string_for_rep : rep -> string |
|
26 |
val is_Func : rep -> bool |
|
27 |
val is_Opt : rep -> bool |
|
28 |
val is_opt_rep : rep -> bool |
|
29 |
val flip_rep_polarity : rep -> rep |
|
30 |
val card_of_rep : rep -> int |
|
31 |
val arity_of_rep : rep -> int |
|
32 |
val min_univ_card_of_rep : rep -> int |
|
33 |
val is_one_rep : rep -> bool |
|
34 |
val is_lone_rep : rep -> bool |
|
35 |
val dest_Func : rep -> rep * rep |
|
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
36 |
val lazy_range_rep : int Typtab.table -> typ -> (unit -> int) -> rep -> rep |
33192 | 37 |
val binder_reps : rep -> rep list |
38 |
val body_rep : rep -> rep |
|
39 |
val one_rep : int Typtab.table -> typ -> rep -> rep |
|
40 |
val optable_rep : int Typtab.table -> typ -> rep -> rep |
|
41 |
val opt_rep : int Typtab.table -> typ -> rep -> rep |
|
42 |
val unopt_rep : rep -> rep |
|
43 |
val min_rep : rep -> rep -> rep |
|
44 |
val min_reps : rep list -> rep list -> rep list |
|
45 |
val card_of_domain_from_rep : int -> rep -> int |
|
46 |
val rep_to_binary_rel_rep : int Typtab.table -> typ -> rep -> rep |
|
47 |
val best_one_rep_for_type : scope -> typ -> rep |
|
48 |
val best_opt_set_rep_for_type : scope -> typ -> rep |
|
49 |
val best_non_opt_set_rep_for_type : scope -> typ -> rep |
|
50 |
val best_set_rep_for_type : scope -> typ -> rep |
|
51 |
val best_non_opt_symmetric_reps_for_fun_type : scope -> typ -> rep * rep |
|
52 |
val atom_schema_of_rep : rep -> (int * int) list |
|
53 |
val atom_schema_of_reps : rep list -> (int * int) list |
|
54 |
val type_schema_of_rep : typ -> rep -> typ list |
|
55 |
val type_schema_of_reps : typ list -> rep list -> typ list |
|
56 |
val all_combinations_for_rep : rep -> int list list |
|
57 |
val all_combinations_for_reps : rep list -> int list list |
|
58 |
end; |
|
59 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
60 |
structure Nitpick_Rep : NITPICK_REP = |
33192 | 61 |
struct |
62 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
63 |
open Nitpick_Util |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
64 |
open Nitpick_HOL |
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
65 |
open Nitpick_Scope |
33192 | 66 |
|
67 |
datatype rep = |
|
68 |
Any | |
|
69 |
Formula of polarity | |
|
70 |
Atom of int * int | |
|
71 |
Struct of rep list | |
|
72 |
Vect of int * rep | |
|
73 |
Func of rep * rep | |
|
74 |
Opt of rep |
|
75 |
||
76 |
exception REP of string * rep list |
|
77 |
||
78 |
fun string_for_polarity Pos = "+" |
|
79 |
| string_for_polarity Neg = "-" |
|
80 |
| string_for_polarity Neut = "=" |
|
81 |
||
82 |
fun atomic_string_for_rep rep = |
|
83 |
let val s = string_for_rep rep in |
|
84 |
if String.isPrefix "[" s orelse not (is_substring_of " " s) then s |
|
85 |
else "(" ^ s ^ ")" |
|
86 |
end |
|
87 |
and string_for_rep Any = "X" |
|
88 |
| string_for_rep (Formula polar) = "F" ^ string_for_polarity polar |
|
89 |
| string_for_rep (Atom (k, j0)) = |
|
90 |
"A" ^ string_of_int k ^ (if j0 = 0 then "" else "@" ^ string_of_int j0) |
|
91 |
| string_for_rep (Struct rs) = "[" ^ commas (map string_for_rep rs) ^ "]" |
|
92 |
| string_for_rep (Vect (k, R)) = |
|
93 |
string_of_int k ^ " x " ^ atomic_string_for_rep R |
|
94 |
| string_for_rep (Func (R1, R2)) = |
|
95 |
atomic_string_for_rep R1 ^ " => " ^ string_for_rep R2 |
|
96 |
| string_for_rep (Opt R) = atomic_string_for_rep R ^ "?" |
|
97 |
||
98 |
fun is_Func (Func _) = true |
|
99 |
| is_Func _ = false |
|
100 |
fun is_Opt (Opt _) = true |
|
101 |
| is_Opt _ = false |
|
102 |
fun is_opt_rep (Func (_, R2)) = is_opt_rep R2 |
|
103 |
| is_opt_rep (Opt _) = true |
|
104 |
| is_opt_rep _ = false |
|
105 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
106 |
fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any]) |
33192 | 107 |
| card_of_rep (Formula _) = 2 |
108 |
| card_of_rep (Atom (k, _)) = k |
|
109 |
| card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs) |
|
110 |
| card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k |
|
111 |
| card_of_rep (Func (R1, R2)) = |
|
112 |
reasonable_power (card_of_rep R2) (card_of_rep R1) |
|
113 |
| card_of_rep (Opt R) = card_of_rep R |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
114 |
fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any]) |
33192 | 115 |
| arity_of_rep (Formula _) = 0 |
116 |
| arity_of_rep (Atom _) = 1 |
|
117 |
| arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs) |
|
118 |
| arity_of_rep (Vect (k, R)) = k * arity_of_rep R |
|
119 |
| arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2 |
|
120 |
| arity_of_rep (Opt R) = arity_of_rep R |
|
121 |
fun min_univ_card_of_rep Any = |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
122 |
raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any]) |
33192 | 123 |
| min_univ_card_of_rep (Formula _) = 0 |
124 |
| min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1 |
|
125 |
| min_univ_card_of_rep (Struct Rs) = |
|
126 |
fold Integer.max (map min_univ_card_of_rep Rs) 0 |
|
127 |
| min_univ_card_of_rep (Vect (_, R)) = min_univ_card_of_rep R |
|
128 |
| min_univ_card_of_rep (Func (R1, R2)) = |
|
129 |
Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2) |
|
130 |
| min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R |
|
131 |
||
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
132 |
fun is_one_rep (Atom _) = true |
33192 | 133 |
| is_one_rep (Struct _) = true |
134 |
| is_one_rep (Vect _) = true |
|
135 |
| is_one_rep _ = false |
|
136 |
fun is_lone_rep (Opt R) = is_one_rep R |
|
137 |
| is_lone_rep R = is_one_rep R |
|
138 |
||
139 |
fun dest_Func (Func z) = z |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
140 |
| dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) |
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
141 |
fun lazy_range_rep _ _ _ (Vect (_, R)) = R |
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
142 |
| lazy_range_rep _ _ _ (Func (_, R2)) = R2 |
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
143 |
| lazy_range_rep ofs T ran_card (Opt R) = |
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
144 |
Opt (lazy_range_rep ofs T ran_card R) |
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
145 |
| lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) = |
33192 | 146 |
Atom (1, offset_of_type ofs T2) |
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
147 |
| lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) = |
33192 | 148 |
Atom (ran_card (), offset_of_type ofs T2) |
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
149 |
| lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R]) |
33192 | 150 |
|
151 |
fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
34982
diff
changeset
|
152 |
| binder_reps _ = [] |
33192 | 153 |
fun body_rep (Func (_, R2)) = body_rep R2 |
154 |
| body_rep R = R |
|
155 |
||
156 |
fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar) |
|
157 |
| flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2) |
|
158 |
| flip_rep_polarity R = R |
|
159 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
160 |
fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any]) |
33192 | 161 |
| one_rep _ _ (Atom x) = Atom x |
162 |
| one_rep _ _ (Struct Rs) = Struct Rs |
|
163 |
| one_rep _ _ (Vect z) = Vect z |
|
164 |
| one_rep ofs T (Opt R) = one_rep ofs T R |
|
165 |
| one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T) |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
166 |
fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
33192 | 167 |
Func (R1, optable_rep ofs T2 R2) |
46083 | 168 |
| optable_rep ofs (Type (@{type_name set}, [T'])) R = |
169 |
optable_rep ofs (T' --> bool_T) R |
|
33192 | 170 |
| optable_rep ofs T R = one_rep ofs T R |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
171 |
fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
33192 | 172 |
Func (R1, opt_rep ofs T2 R2) |
46083 | 173 |
| opt_rep ofs (Type (@{type_name set}, [T'])) R = |
174 |
opt_rep ofs (T' --> bool_T) R |
|
33192 | 175 |
| opt_rep ofs T R = Opt (optable_rep ofs T R) |
176 |
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2) |
|
177 |
| unopt_rep (Opt R) = R |
|
178 |
| unopt_rep R = R |
|
179 |
||
180 |
fun min_polarity polar1 polar2 = |
|
181 |
if polar1 = polar2 then |
|
182 |
polar1 |
|
183 |
else if polar1 = Neut then |
|
184 |
polar2 |
|
185 |
else if polar2 = Neut then |
|
186 |
polar1 |
|
187 |
else |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
188 |
raise ARG ("Nitpick_Rep.min_polarity", |
33192 | 189 |
commas (map (quote o string_for_polarity) [polar1, polar2])) |
190 |
||
191 |
(* It's important that Func is before Vect, because if the range is Opt we |
|
192 |
could lose information by converting a Func to a Vect. *) |
|
193 |
fun min_rep (Opt R1) (Opt R2) = Opt (min_rep R1 R2) |
|
194 |
| min_rep (Opt R) _ = Opt R |
|
195 |
| min_rep _ (Opt R) = Opt R |
|
196 |
| min_rep (Formula polar1) (Formula polar2) = |
|
197 |
Formula (min_polarity polar1 polar2) |
|
198 |
| min_rep (Formula polar) _ = Formula polar |
|
199 |
| min_rep _ (Formula polar) = Formula polar |
|
200 |
| min_rep (Atom x) _ = Atom x |
|
201 |
| min_rep _ (Atom x) = Atom x |
|
202 |
| min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2) |
|
203 |
| min_rep (Struct Rs) _ = Struct Rs |
|
204 |
| min_rep _ (Struct Rs) = Struct Rs |
|
205 |
| min_rep (R1 as Func (R11, R12)) (R2 as Func (R21, R22)) = |
|
206 |
(case pairself is_opt_rep (R12, R22) of |
|
207 |
(true, false) => R1 |
|
208 |
| (false, true) => R2 |
|
209 |
| _ => if R11 = R21 then Func (R11, min_rep R12 R22) |
|
210 |
else if min_rep R11 R21 = R11 then R1 |
|
211 |
else R2) |
|
212 |
| min_rep (Func z) _ = Func z |
|
213 |
| min_rep _ (Func z) = Func z |
|
214 |
| min_rep (Vect (k1, R1)) (Vect (k2, R2)) = |
|
215 |
if k1 < k2 then Vect (k1, R1) |
|
216 |
else if k1 > k2 then Vect (k2, R2) |
|
217 |
else Vect (k1, min_rep R1 R2) |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
218 |
| min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2]) |
33192 | 219 |
and min_reps [] _ = [] |
220 |
| min_reps _ [] = [] |
|
221 |
| min_reps (R1 :: Rs1) (R2 :: Rs2) = |
|
222 |
if R1 = R2 then R1 :: min_reps Rs1 Rs2 |
|
223 |
else if min_rep R1 R2 = R1 then R1 :: Rs1 |
|
224 |
else R2 :: Rs2 |
|
225 |
||
226 |
fun card_of_domain_from_rep ran_card R = |
|
227 |
case R of |
|
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
228 |
Atom (k, _) => exact_log ran_card k |
33192 | 229 |
| Vect (k, _) => k |
230 |
| Func (R1, _) => card_of_rep R1 |
|
231 |
| Opt R => card_of_domain_from_rep ran_card R |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
232 |
| _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R]) |
33192 | 233 |
|
234 |
fun rep_to_binary_rel_rep ofs T R = |
|
235 |
let |
|
236 |
val k = exact_root 2 (card_of_domain_from_rep 2 R) |
|
46085
447cda88adfe
fixed a few more bugs in \Nitpick's new "set" support
blanchet
parents:
46083
diff
changeset
|
237 |
val j0 = |
447cda88adfe
fixed a few more bugs in \Nitpick's new "set" support
blanchet
parents:
46083
diff
changeset
|
238 |
offset_of_type ofs (fst (HOLogic.dest_prodT (pseudo_domain_type T))) |
33192 | 239 |
in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end |
240 |
||
241 |
fun best_one_rep_for_type (scope as {card_assigns, ...} : scope) |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
242 |
(Type (@{type_name fun}, [T1, T2])) = |
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
243 |
Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2)) |
46083 | 244 |
| best_one_rep_for_type scope (Type (@{type_name set}, [T'])) = |
245 |
best_one_rep_for_type scope (T' --> bool_T) |
|
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
246 |
| best_one_rep_for_type scope (Type (@{type_name prod}, Ts)) = |
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
247 |
Struct (map (best_one_rep_for_type scope) Ts) |
39345 | 248 |
| best_one_rep_for_type {card_assigns, ofs, ...} T = |
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
249 |
Atom (card_of_type card_assigns T, offset_of_type ofs T) |
33192 | 250 |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
251 |
fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = |
33192 | 252 |
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2) |
46083 | 253 |
| best_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
254 |
best_opt_set_rep_for_type scope (T' --> bool_T) |
|
33192 | 255 |
| best_opt_set_rep_for_type (scope as {ofs, ...}) T = |
256 |
opt_rep ofs T (best_one_rep_for_type scope T) |
|
39345 | 257 |
fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = |
33192 | 258 |
(case (best_one_rep_for_type scope T1, |
259 |
best_non_opt_set_rep_for_type scope T2) of |
|
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
260 |
(R1, Atom (2, _)) => Func (R1, Formula Neut) |
33192 | 261 |
| z => Func z) |
46083 | 262 |
| best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
263 |
best_non_opt_set_rep_for_type scope (T' --> bool_T) |
|
33192 | 264 |
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T |
265 |
fun best_set_rep_for_type (scope as {datatypes, ...}) T = |
|
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35280
diff
changeset
|
266 |
(if is_exact_type datatypes true T then best_non_opt_set_rep_for_type |
33192 | 267 |
else best_opt_set_rep_for_type) scope T |
268 |
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...}) |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
269 |
(Type (@{type_name fun}, [T1, T2])) = |
33192 | 270 |
(optable_rep ofs T1 (best_one_rep_for_type scope T1), |
271 |
optable_rep ofs T2 (best_one_rep_for_type scope T2)) |
|
272 |
| best_non_opt_symmetric_reps_for_fun_type _ T = |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
273 |
raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], []) |
33192 | 274 |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
275 |
fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any]) |
33192 | 276 |
| atom_schema_of_rep (Formula _) = [] |
277 |
| atom_schema_of_rep (Atom x) = [x] |
|
278 |
| atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs |
|
279 |
| atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R) |
|
280 |
| atom_schema_of_rep (Func (R1, R2)) = |
|
281 |
atom_schema_of_rep R1 @ atom_schema_of_rep R2 |
|
282 |
| atom_schema_of_rep (Opt R) = atom_schema_of_rep R |
|
283 |
and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs |
|
284 |
||
285 |
fun type_schema_of_rep _ (Formula _) = [] |
|
286 |
| type_schema_of_rep T (Atom _) = [T] |
|
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
287 |
| type_schema_of_rep (Type (@{type_name prod}, [T1, T2])) (Struct [R1, R2]) = |
33192 | 288 |
type_schema_of_reps [T1, T2] [R1, R2] |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
289 |
| type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) = |
33192 | 290 |
replicate_list k (type_schema_of_rep T2 R) |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
291 |
| type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) = |
33192 | 292 |
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2 |
46083 | 293 |
| type_schema_of_rep (Type (@{type_name set}, [T'])) R = |
294 |
type_schema_of_rep (T' --> bool_T) R |
|
33192 | 295 |
| type_schema_of_rep T (Opt R) = type_schema_of_rep T R |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
34982
diff
changeset
|
296 |
| type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R]) |
33192 | 297 |
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs) |
298 |
||
299 |
val all_combinations_for_rep = all_combinations o atom_schema_of_rep |
|
300 |
val all_combinations_for_reps = all_combinations o atom_schema_of_reps |
|
301 |
||
302 |
end; |