author | wenzelm |
Fri, 21 Mar 2014 20:33:56 +0100 | |
changeset 56245 | 84fc7dfa3cd4 |
parent 55890 | bd7927cca152 |
child 59058 | a78612c67ec0 |
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 |
|
55889 | 100 |
|
33192 | 101 |
fun is_Opt (Opt _) = true |
102 |
| is_Opt _ = false |
|
55889 | 103 |
|
33192 | 104 |
fun is_opt_rep (Func (_, R2)) = is_opt_rep R2 |
105 |
| is_opt_rep (Opt _) = true |
|
106 |
| is_opt_rep _ = false |
|
107 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
108 |
fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any]) |
33192 | 109 |
| card_of_rep (Formula _) = 2 |
110 |
| card_of_rep (Atom (k, _)) = k |
|
111 |
| card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs) |
|
112 |
| card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k |
|
113 |
| card_of_rep (Func (R1, R2)) = |
|
114 |
reasonable_power (card_of_rep R2) (card_of_rep R1) |
|
115 |
| card_of_rep (Opt R) = card_of_rep R |
|
55889 | 116 |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
117 |
fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any]) |
33192 | 118 |
| arity_of_rep (Formula _) = 0 |
119 |
| arity_of_rep (Atom _) = 1 |
|
120 |
| arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs) |
|
121 |
| arity_of_rep (Vect (k, R)) = k * arity_of_rep R |
|
122 |
| arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2 |
|
123 |
| arity_of_rep (Opt R) = arity_of_rep R |
|
55889 | 124 |
|
33192 | 125 |
fun min_univ_card_of_rep Any = |
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
126 |
raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any]) |
33192 | 127 |
| min_univ_card_of_rep (Formula _) = 0 |
128 |
| min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1 |
|
129 |
| min_univ_card_of_rep (Struct Rs) = |
|
130 |
fold Integer.max (map min_univ_card_of_rep Rs) 0 |
|
131 |
| min_univ_card_of_rep (Vect (_, R)) = min_univ_card_of_rep R |
|
132 |
| min_univ_card_of_rep (Func (R1, R2)) = |
|
133 |
Int.max (min_univ_card_of_rep R1, min_univ_card_of_rep R2) |
|
134 |
| min_univ_card_of_rep (Opt R) = min_univ_card_of_rep R |
|
135 |
||
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
136 |
fun is_one_rep (Atom _) = true |
33192 | 137 |
| is_one_rep (Struct _) = true |
138 |
| is_one_rep (Vect _) = true |
|
139 |
| is_one_rep _ = false |
|
55889 | 140 |
|
33192 | 141 |
fun is_lone_rep (Opt R) = is_one_rep R |
142 |
| is_lone_rep R = is_one_rep R |
|
143 |
||
144 |
fun dest_Func (Func z) = z |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
145 |
| dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) |
55889 | 146 |
|
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
147 |
fun lazy_range_rep _ _ _ (Vect (_, R)) = R |
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
148 |
| lazy_range_rep _ _ _ (Func (_, R2)) = R2 |
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
149 |
| lazy_range_rep ofs T ran_card (Opt R) = |
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
150 |
Opt (lazy_range_rep ofs T ran_card R) |
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
151 |
| lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) = |
33192 | 152 |
Atom (1, offset_of_type ofs T2) |
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
153 |
| lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) = |
33192 | 154 |
Atom (ran_card (), offset_of_type ofs T2) |
36128
a3d8d5329438
make Nitpick output everything to tracing in debug mode;
blanchet
parents:
35665
diff
changeset
|
155 |
| lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R]) |
33192 | 156 |
|
157 |
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
|
158 |
| binder_reps _ = [] |
55889 | 159 |
|
33192 | 160 |
fun body_rep (Func (_, R2)) = body_rep R2 |
161 |
| body_rep R = R |
|
162 |
||
163 |
fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar) |
|
164 |
| flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2) |
|
165 |
| flip_rep_polarity R = R |
|
166 |
||
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
167 |
fun one_rep _ _ Any = raise REP ("Nitpick_Rep.one_rep", [Any]) |
33192 | 168 |
| one_rep _ _ (Atom x) = Atom x |
169 |
| one_rep _ _ (Struct Rs) = Struct Rs |
|
170 |
| one_rep _ _ (Vect z) = Vect z |
|
171 |
| one_rep ofs T (Opt R) = one_rep ofs T R |
|
172 |
| one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T) |
|
55889 | 173 |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
174 |
fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
33192 | 175 |
Func (R1, optable_rep ofs T2 R2) |
46083 | 176 |
| optable_rep ofs (Type (@{type_name set}, [T'])) R = |
177 |
optable_rep ofs (T' --> bool_T) R |
|
33192 | 178 |
| optable_rep ofs T R = one_rep ofs T R |
55889 | 179 |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
180 |
fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
33192 | 181 |
Func (R1, opt_rep ofs T2 R2) |
46083 | 182 |
| opt_rep ofs (Type (@{type_name set}, [T'])) R = |
183 |
opt_rep ofs (T' --> bool_T) R |
|
33192 | 184 |
| opt_rep ofs T R = Opt (optable_rep ofs T R) |
55889 | 185 |
|
33192 | 186 |
fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2) |
187 |
| unopt_rep (Opt R) = R |
|
188 |
| unopt_rep R = R |
|
189 |
||
190 |
fun min_polarity polar1 polar2 = |
|
191 |
if polar1 = polar2 then |
|
192 |
polar1 |
|
193 |
else if polar1 = Neut then |
|
194 |
polar2 |
|
195 |
else if polar2 = Neut then |
|
196 |
polar1 |
|
197 |
else |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
198 |
raise ARG ("Nitpick_Rep.min_polarity", |
33192 | 199 |
commas (map (quote o string_for_polarity) [polar1, polar2])) |
200 |
||
201 |
(* It's important that Func is before Vect, because if the range is Opt we |
|
202 |
could lose information by converting a Func to a Vect. *) |
|
203 |
fun min_rep (Opt R1) (Opt R2) = Opt (min_rep R1 R2) |
|
204 |
| min_rep (Opt R) _ = Opt R |
|
205 |
| min_rep _ (Opt R) = Opt R |
|
206 |
| min_rep (Formula polar1) (Formula polar2) = |
|
207 |
Formula (min_polarity polar1 polar2) |
|
208 |
| min_rep (Formula polar) _ = Formula polar |
|
209 |
| min_rep _ (Formula polar) = Formula polar |
|
210 |
| min_rep (Atom x) _ = Atom x |
|
211 |
| min_rep _ (Atom x) = Atom x |
|
212 |
| min_rep (Struct Rs1) (Struct Rs2) = Struct (min_reps Rs1 Rs2) |
|
213 |
| min_rep (Struct Rs) _ = Struct Rs |
|
214 |
| min_rep _ (Struct Rs) = Struct Rs |
|
215 |
| min_rep (R1 as Func (R11, R12)) (R2 as Func (R21, R22)) = |
|
216 |
(case pairself is_opt_rep (R12, R22) of |
|
217 |
(true, false) => R1 |
|
218 |
| (false, true) => R2 |
|
219 |
| _ => if R11 = R21 then Func (R11, min_rep R12 R22) |
|
220 |
else if min_rep R11 R21 = R11 then R1 |
|
221 |
else R2) |
|
222 |
| min_rep (Func z) _ = Func z |
|
223 |
| min_rep _ (Func z) = Func z |
|
224 |
| min_rep (Vect (k1, R1)) (Vect (k2, R2)) = |
|
225 |
if k1 < k2 then Vect (k1, R1) |
|
226 |
else if k1 > k2 then Vect (k2, R2) |
|
227 |
else Vect (k1, min_rep R1 R2) |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
228 |
| min_rep R1 R2 = raise REP ("Nitpick_Rep.min_rep", [R1, R2]) |
33192 | 229 |
and min_reps [] _ = [] |
230 |
| min_reps _ [] = [] |
|
231 |
| min_reps (R1 :: Rs1) (R2 :: Rs2) = |
|
232 |
if R1 = R2 then R1 :: min_reps Rs1 Rs2 |
|
233 |
else if min_rep R1 R2 = R1 then R1 :: Rs1 |
|
234 |
else R2 :: Rs2 |
|
235 |
||
236 |
fun card_of_domain_from_rep ran_card R = |
|
237 |
case R of |
|
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet
parents:
37678
diff
changeset
|
238 |
Atom (k, _) => exact_log ran_card k |
33192 | 239 |
| Vect (k, _) => k |
240 |
| Func (R1, _) => card_of_rep R1 |
|
241 |
| 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
|
242 |
| _ => raise REP ("Nitpick_Rep.card_of_domain_from_rep", [R]) |
33192 | 243 |
|
244 |
fun rep_to_binary_rel_rep ofs T R = |
|
245 |
let |
|
246 |
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
|
247 |
val j0 = |
447cda88adfe
fixed a few more bugs in \Nitpick's new "set" support
blanchet
parents:
46083
diff
changeset
|
248 |
offset_of_type ofs (fst (HOLogic.dest_prodT (pseudo_domain_type T))) |
33192 | 249 |
in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end |
250 |
||
251 |
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
|
252 |
(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
|
253 |
Vect (card_of_type card_assigns T1, (best_one_rep_for_type scope T2)) |
46083 | 254 |
| best_one_rep_for_type scope (Type (@{type_name set}, [T'])) = |
255 |
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
|
256 |
| 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
|
257 |
Struct (map (best_one_rep_for_type scope) Ts) |
39345 | 258 |
| 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
|
259 |
Atom (card_of_type card_assigns T, offset_of_type ofs T) |
33192 | 260 |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35385
diff
changeset
|
261 |
fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = |
33192 | 262 |
Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2) |
46083 | 263 |
| best_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
264 |
best_opt_set_rep_for_type scope (T' --> bool_T) |
|
33192 | 265 |
| best_opt_set_rep_for_type (scope as {ofs, ...}) T = |
266 |
opt_rep ofs T (best_one_rep_for_type scope T) |
|
55889 | 267 |
|
39345 | 268 |
fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = |
33192 | 269 |
(case (best_one_rep_for_type scope T1, |
270 |
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
|
271 |
(R1, Atom (2, _)) => Func (R1, Formula Neut) |
33192 | 272 |
| z => Func z) |
46083 | 273 |
| best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
274 |
best_non_opt_set_rep_for_type scope (T' --> bool_T) |
|
33192 | 275 |
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T |
55889 | 276 |
|
55890 | 277 |
fun best_set_rep_for_type (scope as {data_types, ...}) T = |
278 |
(if is_exact_type data_types true T then best_non_opt_set_rep_for_type |
|
33192 | 279 |
else best_opt_set_rep_for_type) scope T |
55889 | 280 |
|
33192 | 281 |
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
|
282 |
(Type (@{type_name fun}, [T1, T2])) = |
33192 | 283 |
(optable_rep ofs T1 (best_one_rep_for_type scope T1), |
284 |
optable_rep ofs T2 (best_one_rep_for_type scope T2)) |
|
285 |
| 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
|
286 |
raise TYPE ("Nitpick_Rep.best_non_opt_symmetric_reps_for_fun_type", [T], []) |
33192 | 287 |
|
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset
|
288 |
fun atom_schema_of_rep Any = raise REP ("Nitpick_Rep.atom_schema_of_rep", [Any]) |
33192 | 289 |
| atom_schema_of_rep (Formula _) = [] |
290 |
| atom_schema_of_rep (Atom x) = [x] |
|
291 |
| atom_schema_of_rep (Struct Rs) = atom_schema_of_reps Rs |
|
292 |
| atom_schema_of_rep (Vect (k, R)) = replicate_list k (atom_schema_of_rep R) |
|
293 |
| atom_schema_of_rep (Func (R1, R2)) = |
|
294 |
atom_schema_of_rep R1 @ atom_schema_of_rep R2 |
|
295 |
| atom_schema_of_rep (Opt R) = atom_schema_of_rep R |
|
296 |
and atom_schema_of_reps Rs = maps atom_schema_of_rep Rs |
|
297 |
||
298 |
fun type_schema_of_rep _ (Formula _) = [] |
|
299 |
| 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
|
300 |
| type_schema_of_rep (Type (@{type_name prod}, [T1, T2])) (Struct [R1, R2]) = |
33192 | 301 |
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
|
302 |
| type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) = |
33192 | 303 |
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
|
304 |
| type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) = |
33192 | 305 |
type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2 |
46083 | 306 |
| type_schema_of_rep (Type (@{type_name set}, [T'])) R = |
307 |
type_schema_of_rep (T' --> bool_T) R |
|
33192 | 308 |
| 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
|
309 |
| type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R]) |
33192 | 310 |
and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs) |
311 |
||
312 |
val all_combinations_for_rep = all_combinations o atom_schema_of_rep |
|
313 |
val all_combinations_for_reps = all_combinations o atom_schema_of_reps |
|
314 |
||
315 |
end; |