58 if b = a then noatoms else |
58 if b = a then noatoms else |
59 HOLogic.mk_binop @{const_name minus} (a, b); |
59 HOLogic.mk_binop @{const_name minus} (a, b); |
60 *} |
60 *} |
61 |
61 |
62 ML {* |
62 ML {* |
63 fun atoms thy t = |
63 fun is_atom_list (Type (@{type_name list}, [T])) = true |
|
64 | is_atom_list _ = false |
|
65 *} |
|
66 |
|
67 ML {* |
|
68 fun dest_listT (Type (@{type_name list}, [T])) = T |
|
69 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) |
|
70 *} |
|
71 |
|
72 ML {* |
|
73 fun mk_atom_list t = |
|
74 let |
|
75 val ty = fastype_of t; |
|
76 val atom_ty = dest_listT ty --> @{typ atom}; |
|
77 val map_ty = atom_ty --> ty --> @{typ "atom list"}; |
|
78 in |
|
79 (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t) |
|
80 end; |
|
81 *} |
|
82 |
|
83 ML {* |
|
84 fun setify thy t = |
64 let |
85 let |
65 val ty = fastype_of t; |
86 val ty = fastype_of t; |
66 in |
87 in |
67 if is_atom thy ty |
88 if is_atom thy ty |
68 then mk_singleton_atom t |
89 then mk_singleton_atom t |
69 else if is_atom_set thy ty |
90 else if is_atom_set thy ty |
70 then mk_atom_set t |
91 then mk_atom_set t |
71 else if is_atom_fset thy ty |
92 else if is_atom_fset thy ty |
72 then mk_atom_fset t |
93 then mk_atom_fset t |
73 else noatoms |
94 else error ("setify" ^ (PolyML.makestring (t, ty))) |
74 end |
95 end |
75 *} |
96 *} |
76 |
97 |
77 ML {* |
98 ML {* |
78 fun setify x = |
99 fun listify thy t = |
|
100 let |
|
101 val ty = fastype_of t; |
|
102 in |
|
103 if is_atom thy ty |
|
104 then HOLogic.mk_list @{typ atom} [mk_atom t] |
|
105 else if is_atom_list ty |
|
106 then mk_atom_set t |
|
107 else error "listify" |
|
108 end |
|
109 *} |
|
110 |
|
111 ML {* |
|
112 fun set x = |
79 if fastype_of x = @{typ "atom list"} |
113 if fastype_of x = @{typ "atom list"} |
80 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
114 then @{term "set::atom list \<Rightarrow> atom set"} $ x |
81 else x |
115 else x |
82 *} |
116 *} |
83 |
117 |
87 val x = nth args i; |
121 val x = nth args i; |
88 val dt = nth dts i; |
122 val dt = nth dts i; |
89 in |
123 in |
90 if Datatype_Aux.is_rec_type dt |
124 if Datatype_Aux.is_rec_type dt |
91 then nth fv_frees (Datatype_Aux.body_index dt) $ x |
125 then nth fv_frees (Datatype_Aux.body_index dt) $ x |
92 else (if supp then mk_supp x else atoms thy x) |
126 else (if supp then mk_supp x else setify thy x) |
93 end |
127 end |
94 *} |
128 *} |
95 |
129 |
96 ML {* |
130 ML {* |
97 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
131 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
98 let |
132 let |
99 val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) |
133 val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) |
100 val bound_vars = |
134 val bound_vars = |
101 case binds of |
135 case binds of |
102 [(SOME bn, i)] => setify (bn $ nth args i) |
136 [(SOME bn, i)] => set (bn $ nth args i) |
103 | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds)); |
137 | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds)); |
104 val non_rec_vars = |
138 val non_rec_vars = |
105 case binds of |
139 case binds of |
106 [(SOME bn, i)] => |
140 [(SOME bn, i)] => |
107 if i mem bodys |
141 if i mem bodys |