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