149 |
149 |
150 |
150 |
151 |
151 |
152 (** functions that construct the equations for fv and fv_bn **) |
152 (** functions that construct the equations for fv and fv_bn **) |
153 |
153 |
154 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
154 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |
155 let |
155 let |
156 fun mk_fv_body fv_map args i = |
156 fun mk_fv_body fv_map args i = |
157 let |
157 let |
158 val arg = nth args i |
158 val arg = nth args i |
159 val ty = fastype_of arg |
159 val ty = fastype_of arg |
161 case AList.lookup (op=) fv_map ty of |
161 case AList.lookup (op=) fv_map ty of |
162 NONE => mk_supp arg |
162 NONE => mk_supp arg |
163 | SOME fv => fv $ arg |
163 | SOME fv => fv $ arg |
164 end |
164 end |
165 |
165 |
166 fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = |
166 fun mk_fv_binder lthy fv_bn_map args binders = |
167 let |
167 let |
168 val arg = nth args i |
168 fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"}) |
|
169 | bind_set _ args (SOME bn, i) = (bn $ (nth args i), |
|
170 if member (op=) bodies i then @{term "{}::atom set"} |
|
171 else lookup fv_bn_map bn $ (nth args i)) |
|
172 fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"}) |
|
173 | bind_lst _ args (SOME bn, i) = (bn $ (nth args i), |
|
174 if member (op=) bodies i then @{term "[]::atom list"} |
|
175 else lookup fv_bn_map bn $ (nth args i)) |
|
176 |
|
177 val (combine_fn, bind_fn) = |
|
178 case bmode of |
|
179 Lst => (fold_append, bind_lst) |
|
180 | Set => (fold_union, bind_set) |
|
181 | Res => (fold_union, bind_set) |
169 in |
182 in |
170 case bn_option of |
183 binders |
171 NONE => (setify lthy arg, @{term "{}::atom set"}) |
184 |> map (bind_fn lthy args) |
172 | SOME bn => (to_set (bn $ arg), |
185 |> split_list |
173 if member (op=) bodies i then @{term "{}::atom set"} |
186 |> pairself combine_fn |
174 else lookup fv_bn_map bn $ arg) |
|
175 end |
187 end |
176 |
188 |
177 val t1 = map (mk_fv_body fv_map args) bodies |
189 val t1 = map (mk_fv_body fv_map args) bodies |
178 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
190 val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders |
179 in |
191 in |
180 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
192 mk_union (mk_diff (fold_union t1, to_set t2), to_set t3) |
181 end |
193 end |
182 |
194 |
183 (* in case of fv_bn we have to treat the case special, where an |
195 (* in case of fv_bn we have to treat the case special, where an |
184 "empty" binding clause is given *) |
196 "empty" binding clause is given *) |
185 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
197 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |