146 |
146 |
147 ML {* |
147 ML {* |
148 fun non_rec_binds l = |
148 fun non_rec_binds l = |
149 let |
149 let |
150 fun is_non_rec (SOME (f, false), _, _) = SOME f |
150 fun is_non_rec (SOME (f, false), _, _) = SOME f |
|
151 | is_non_rec _ = NONE |
|
152 in |
|
153 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
|
154 end |
|
155 *} |
|
156 |
|
157 ML {* |
|
158 fun all_binds l = |
|
159 let |
|
160 fun is_non_rec (SOME (f, _), _, _) = SOME f |
151 | is_non_rec _ = NONE |
161 | is_non_rec _ = NONE |
152 in |
162 in |
153 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
163 distinct (op =) (map_filter is_non_rec (flat (flat l))) |
154 end |
164 end |
155 *} |
165 *} |
242 ML {* |
252 ML {* |
243 fun bns_same l = |
253 fun bns_same l = |
244 length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1 |
254 length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1 |
245 *} |
255 *} |
246 |
256 |
247 ML {* fn x => split_list(flat x) *} |
|
248 ML {* fn x => apsnd flat (split_list (map split_list x)) *} |
|
249 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
257 (* TODO: Notice datatypes without bindings and replace alpha with equality *) |
250 ML {* |
258 ML {* |
251 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
259 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy = |
252 let |
260 let |
253 val thy = ProofContext.theory_of lthy; |
261 val thy = ProofContext.theory_of lthy; |
255 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
263 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
256 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
264 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
257 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
265 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
258 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
266 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
259 val fv_frees = map Free (fv_names ~~ fv_types); |
267 val fv_frees = map Free (fv_names ~~ fv_types); |
|
268 val all_bns = all_binds bindsall; |
260 val nr_bns = non_rec_binds bindsall; |
269 val nr_bns = non_rec_binds bindsall; |
261 val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns; |
270 val rel_bns = filter (fn (bn, _, _) => bn mem all_bns) bns; |
262 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
271 val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns); |
263 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
272 val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs; |
264 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
273 val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
265 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
274 "alpha_" ^ name_of_typ (nth_dtyp i)) descr); |
266 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
275 val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr; |
295 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
304 if ((is_atom_set thy) o fastype_of) (nth args i) then mk_atoms (nth args i) else |
296 (* TODO we do not know what to do with non-atomizable things *) |
305 (* TODO we do not know what to do with non-atomizable things *) |
297 @{term "{} :: atom set"} |
306 @{term "{} :: atom set"} |
298 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
307 | fv_bind args (SOME (f, _), i, _) = f $ (nth args i); |
299 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
308 fun fv_binds args relevant = mk_union (map (fv_bind args) relevant) |
300 fun find_nonrec_binder j (SOME (f, false), i, _) = if i = j then SOME f else NONE |
309 fun find_compound_binder j (SOME (f, r), i, _) = if i = j then SOME (f, r) else NONE |
301 | find_nonrec_binder _ _ = NONE |
310 | find_compound_binder _ _ = NONE |
302 fun fv_arg ((dt, x), arg_no) = |
311 fun fv_arg ((dt, x), arg_no) = |
303 case get_first (find_nonrec_binder arg_no) bindcs of |
312 case get_first (find_compound_binder arg_no) bindcs of |
304 SOME f => |
313 SOME (f, is_rec) => |
305 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
314 (case get_first (fn (x, y) => if x = f then SOME y else NONE) bn_fv_bns of |
306 SOME fv_bn => fv_bn $ x |
315 SOME fv_bn => |
|
316 if is_rec then |
|
317 let |
|
318 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
|
319 val sub = fv_binds args relevant |
|
320 in |
|
321 mk_diff (fv_bn $ x) sub |
|
322 end |
|
323 else fv_bn $ x |
307 | NONE => error "bn specified in a non-rec binding but not in bn list") |
324 | NONE => error "bn specified in a non-rec binding but not in bn list") |
308 | NONE => |
325 | NONE => |
309 let |
326 let |
310 val arg = |
327 val arg = |
311 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
328 if is_rec_type dt then nth fv_frees (body_index dt) $ x else |
312 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
329 if ((is_atom thy) o fastype_of) x then mk_single_atom x else |
313 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else |
330 if ((is_atom_set thy) o fastype_of) x then mk_atoms x else |
314 (* TODO we do not know what to do with non-atomizable things *) |
331 (* TODO we do not know what to do with non-atomizable things *) |
315 @{term "{} :: atom set"} |
332 @{term "{} :: atom set"}; |
316 (* If i = j then we generate it only once *) |
333 (* If i = j then we generate it only once *) |
317 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
334 val relevant = filter (fn (_, i, j) => ((i = arg_no) orelse (j = arg_no))) bindcs; |
318 val sub = fv_binds args relevant |
335 val sub = fv_binds args relevant |
319 in |
336 in |
320 mk_diff arg sub |
337 mk_diff arg sub |