37 [], |
37 [], |
38 [[], [], [(NONE, 0)]], |
38 [[], [], [(NONE, 0)]], |
39 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
39 [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]] |
40 *) |
40 *) |
41 |
41 |
42 ML foldr1 |
|
43 ML fold |
|
44 ML {* |
42 ML {* |
45 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
43 val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam"; |
46 val sorts = []; |
44 val sorts = []; |
47 val noatoms = @{term "{} :: atom set"} |
45 val noatoms = @{term "{} :: atom set"} |
48 val binds = [[[]], [[], []], [[], [(NONE, 0)]]]; |
46 val binds = [[[]], [[], []], [[], [(NONE, 0)]]]; |
49 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
47 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
50 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
48 val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) => |
51 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
49 "fv_" ^ name_of_typ (nth_dtyp i)) descr); |
52 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
50 val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr; |
53 val fv_frees = map Free (fv_names ~~ fv_types); |
51 val fv_frees = map Free (fv_names ~~ fv_types); |
|
52 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
54 fun mk_union sets = |
53 fun mk_union sets = |
55 fold (fn a => fn b => |
54 fold (fn a => fn b => |
56 if a = noatoms then b else |
55 if a = noatoms then b else |
57 if b = noatoms then a else |
56 if b = noatoms then a else |
58 HOLogic.mk_binop @{const_name union} (a, b)) sets noatoms; |
57 HOLogic.mk_binop @{const_name union} (a, b)) sets noatoms; |
59 fun mk_diff a b = |
58 fun mk_diff a b = |
60 if b = noatoms then a else |
59 if b = noatoms then a else |
61 HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (a, b); |
60 HOLogic.mk_binop @{const_name minus} (a, b); |
62 fun fv_eq_constr i (cname, dts) bindcs = |
61 fun fv_eq_constr i (cname, dts) bindcs = |
63 let |
62 let |
64 val Ts = map (typ_of_dtyp descr sorts) dts; |
63 val Ts = map (typ_of_dtyp descr sorts) dts; |
65 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
64 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
66 val args = map Free (names ~~ Ts); |
65 val args = map Free (names ~~ Ts); |
67 val c = Const (cname, Ts ---> (nth_dtyp i)); |
66 val c = Const (cname, Ts ---> (nth_dtyp i)); |
68 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
67 val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"}); |
69 fun fv_bind (_, i) = @{term "{} :: atom set"} |
68 (* TODO we assume that all can be 'atomized' *) |
|
69 fun fv_bind (NONE, i) = mk_single_atom (nth args i) |
|
70 | fv_bind (SOME f, i) = f $ (nth args i); |
70 fun fv_arg ((dt, x), bindxs) = |
71 fun fv_arg ((dt, x), bindxs) = |
71 let |
72 let |
72 val arg = |
73 val arg = |
73 if is_rec_type dt then nth fv_frees (body_index dt) $ x |
74 if is_rec_type dt then nth fv_frees (body_index dt) $ x |
74 (* TODO: we just assume everything is a 'name' *) |
75 (* TODO: we just assume everything can be 'atomized' *) |
75 else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
76 else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x] |
76 val sub = mk_union (map fv_bind bindxs) |
77 val sub = mk_union (map fv_bind bindxs) |
77 in |
78 in |
78 mk_diff arg sub |
79 mk_diff arg sub |
79 end; |
80 end; |