95 atomic_string_for_rep R1 ^ " => " ^ string_for_rep R2 |
95 atomic_string_for_rep R1 ^ " => " ^ string_for_rep R2 |
96 | string_for_rep (Opt R) = atomic_string_for_rep R ^ "?" |
96 | string_for_rep (Opt R) = atomic_string_for_rep R ^ "?" |
97 |
97 |
98 fun is_Func (Func _) = true |
98 fun is_Func (Func _) = true |
99 | is_Func _ = false |
99 | is_Func _ = false |
|
100 |
100 fun is_Opt (Opt _) = true |
101 fun is_Opt (Opt _) = true |
101 | is_Opt _ = false |
102 | is_Opt _ = false |
|
103 |
102 fun is_opt_rep (Func (_, R2)) = is_opt_rep R2 |
104 fun is_opt_rep (Func (_, R2)) = is_opt_rep R2 |
103 | is_opt_rep (Opt _) = true |
105 | is_opt_rep (Opt _) = true |
104 | is_opt_rep _ = false |
106 | is_opt_rep _ = false |
105 |
107 |
106 fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any]) |
108 fun card_of_rep Any = raise REP ("Nitpick_Rep.card_of_rep", [Any]) |
109 | card_of_rep (Struct rs) = Integer.prod (map card_of_rep rs) |
111 | 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 |
112 | card_of_rep (Vect (k, R)) = reasonable_power (card_of_rep R) k |
111 | card_of_rep (Func (R1, R2)) = |
113 | card_of_rep (Func (R1, R2)) = |
112 reasonable_power (card_of_rep R2) (card_of_rep R1) |
114 reasonable_power (card_of_rep R2) (card_of_rep R1) |
113 | card_of_rep (Opt R) = card_of_rep R |
115 | card_of_rep (Opt R) = card_of_rep R |
|
116 |
114 fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any]) |
117 fun arity_of_rep Any = raise REP ("Nitpick_Rep.arity_of_rep", [Any]) |
115 | arity_of_rep (Formula _) = 0 |
118 | arity_of_rep (Formula _) = 0 |
116 | arity_of_rep (Atom _) = 1 |
119 | arity_of_rep (Atom _) = 1 |
117 | arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs) |
120 | arity_of_rep (Struct Rs) = Integer.sum (map arity_of_rep Rs) |
118 | arity_of_rep (Vect (k, R)) = k * arity_of_rep R |
121 | 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 |
122 | arity_of_rep (Func (R1, R2)) = arity_of_rep R1 + arity_of_rep R2 |
120 | arity_of_rep (Opt R) = arity_of_rep R |
123 | arity_of_rep (Opt R) = arity_of_rep R |
|
124 |
121 fun min_univ_card_of_rep Any = |
125 fun min_univ_card_of_rep Any = |
122 raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any]) |
126 raise REP ("Nitpick_Rep.min_univ_card_of_rep", [Any]) |
123 | min_univ_card_of_rep (Formula _) = 0 |
127 | min_univ_card_of_rep (Formula _) = 0 |
124 | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1 |
128 | min_univ_card_of_rep (Atom (k, j0)) = k + j0 + 1 |
125 | min_univ_card_of_rep (Struct Rs) = |
129 | min_univ_card_of_rep (Struct Rs) = |
131 |
135 |
132 fun is_one_rep (Atom _) = true |
136 fun is_one_rep (Atom _) = true |
133 | is_one_rep (Struct _) = true |
137 | is_one_rep (Struct _) = true |
134 | is_one_rep (Vect _) = true |
138 | is_one_rep (Vect _) = true |
135 | is_one_rep _ = false |
139 | is_one_rep _ = false |
|
140 |
136 fun is_lone_rep (Opt R) = is_one_rep R |
141 fun is_lone_rep (Opt R) = is_one_rep R |
137 | is_lone_rep R = is_one_rep R |
142 | is_lone_rep R = is_one_rep R |
138 |
143 |
139 fun dest_Func (Func z) = z |
144 fun dest_Func (Func z) = z |
140 | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) |
145 | dest_Func R = raise REP ("Nitpick_Rep.dest_Func", [R]) |
|
146 |
141 fun lazy_range_rep _ _ _ (Vect (_, R)) = R |
147 fun lazy_range_rep _ _ _ (Vect (_, R)) = R |
142 | lazy_range_rep _ _ _ (Func (_, R2)) = R2 |
148 | lazy_range_rep _ _ _ (Func (_, R2)) = R2 |
143 | lazy_range_rep ofs T ran_card (Opt R) = |
149 | lazy_range_rep ofs T ran_card (Opt R) = |
144 Opt (lazy_range_rep ofs T ran_card R) |
150 Opt (lazy_range_rep ofs T ran_card R) |
145 | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) = |
151 | lazy_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) = |
148 Atom (ran_card (), offset_of_type ofs T2) |
154 Atom (ran_card (), offset_of_type ofs T2) |
149 | lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R]) |
155 | lazy_range_rep _ _ _ R = raise REP ("Nitpick_Rep.lazy_range_rep", [R]) |
150 |
156 |
151 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2 |
157 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2 |
152 | binder_reps _ = [] |
158 | binder_reps _ = [] |
|
159 |
153 fun body_rep (Func (_, R2)) = body_rep R2 |
160 fun body_rep (Func (_, R2)) = body_rep R2 |
154 | body_rep R = R |
161 | body_rep R = R |
155 |
162 |
156 fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar) |
163 fun flip_rep_polarity (Formula polar) = Formula (flip_polarity polar) |
157 | flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2) |
164 | flip_rep_polarity (Func (R1, R2)) = Func (R1, flip_rep_polarity R2) |
161 | one_rep _ _ (Atom x) = Atom x |
168 | one_rep _ _ (Atom x) = Atom x |
162 | one_rep _ _ (Struct Rs) = Struct Rs |
169 | one_rep _ _ (Struct Rs) = Struct Rs |
163 | one_rep _ _ (Vect z) = Vect z |
170 | one_rep _ _ (Vect z) = Vect z |
164 | one_rep ofs T (Opt R) = one_rep ofs T R |
171 | 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) |
172 | one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T) |
|
173 |
166 fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
174 fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
167 Func (R1, optable_rep ofs T2 R2) |
175 Func (R1, optable_rep ofs T2 R2) |
168 | optable_rep ofs (Type (@{type_name set}, [T'])) R = |
176 | optable_rep ofs (Type (@{type_name set}, [T'])) R = |
169 optable_rep ofs (T' --> bool_T) R |
177 optable_rep ofs (T' --> bool_T) R |
170 | optable_rep ofs T R = one_rep ofs T R |
178 | optable_rep ofs T R = one_rep ofs T R |
|
179 |
171 fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
180 fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) = |
172 Func (R1, opt_rep ofs T2 R2) |
181 Func (R1, opt_rep ofs T2 R2) |
173 | opt_rep ofs (Type (@{type_name set}, [T'])) R = |
182 | opt_rep ofs (Type (@{type_name set}, [T'])) R = |
174 opt_rep ofs (T' --> bool_T) R |
183 opt_rep ofs (T' --> bool_T) R |
175 | opt_rep ofs T R = Opt (optable_rep ofs T R) |
184 | opt_rep ofs T R = Opt (optable_rep ofs T R) |
|
185 |
176 fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2) |
186 fun unopt_rep (Func (R1, R2)) = Func (R1, unopt_rep R2) |
177 | unopt_rep (Opt R) = R |
187 | unopt_rep (Opt R) = R |
178 | unopt_rep R = R |
188 | unopt_rep R = R |
179 |
189 |
180 fun min_polarity polar1 polar2 = |
190 fun min_polarity polar1 polar2 = |
252 Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2) |
262 Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2) |
253 | best_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
263 | best_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
254 best_opt_set_rep_for_type scope (T' --> bool_T) |
264 best_opt_set_rep_for_type scope (T' --> bool_T) |
255 | best_opt_set_rep_for_type (scope as {ofs, ...}) T = |
265 | best_opt_set_rep_for_type (scope as {ofs, ...}) T = |
256 opt_rep ofs T (best_one_rep_for_type scope T) |
266 opt_rep ofs T (best_one_rep_for_type scope T) |
|
267 |
257 fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = |
268 fun best_non_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) = |
258 (case (best_one_rep_for_type scope T1, |
269 (case (best_one_rep_for_type scope T1, |
259 best_non_opt_set_rep_for_type scope T2) of |
270 best_non_opt_set_rep_for_type scope T2) of |
260 (R1, Atom (2, _)) => Func (R1, Formula Neut) |
271 (R1, Atom (2, _)) => Func (R1, Formula Neut) |
261 | z => Func z) |
272 | z => Func z) |
262 | best_non_opt_set_rep_for_type scope (Type (@{type_name set}, [T'])) = |
273 | 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) |
274 best_non_opt_set_rep_for_type scope (T' --> bool_T) |
264 | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T |
275 | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T |
|
276 |
265 fun best_set_rep_for_type (scope as {datatypes, ...}) T = |
277 fun best_set_rep_for_type (scope as {datatypes, ...}) T = |
266 (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type |
278 (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type |
267 else best_opt_set_rep_for_type) scope T |
279 else best_opt_set_rep_for_type) scope T |
|
280 |
268 fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...}) |
281 fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...}) |
269 (Type (@{type_name fun}, [T1, T2])) = |
282 (Type (@{type_name fun}, [T1, T2])) = |
270 (optable_rep ofs T1 (best_one_rep_for_type scope T1), |
283 (optable_rep ofs T1 (best_one_rep_for_type scope T1), |
271 optable_rep ofs T2 (best_one_rep_for_type scope T2)) |
284 optable_rep ofs T2 (best_one_rep_for_type scope T2)) |
272 | best_non_opt_symmetric_reps_for_fun_type _ T = |
285 | best_non_opt_symmetric_reps_for_fun_type _ T = |