121 in |
121 in |
122 case (AList.lookup (op=) fv_map ty) of |
122 case (AList.lookup (op=) fv_map ty) of |
123 NONE => mk_supp arg |
123 NONE => mk_supp arg |
124 | SOME fv => fv $ arg |
124 | SOME fv => fv $ arg |
125 end |
125 end |
|
126 handle Option => error "fv_map lookup " |
|
127 |
|
128 fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = |
|
129 let |
|
130 val arg = nth args i |
|
131 in |
|
132 case bn_option of |
|
133 NONE => (setify lthy arg, @{term "{}::atom set"}) |
|
134 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
|
135 end |
|
136 handle Option => error "fv_bn_map lookup " |
126 |
137 |
127 fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = |
138 fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = |
128 let |
139 let |
129 val arg = nth args i |
140 val arg = nth args i |
130 val ty = fastype_of arg |
141 val ty = fastype_of arg |
134 NONE => mk_supp arg |
145 NONE => mk_supp arg |
135 | SOME fv => fv $ arg) |
146 | SOME fv => fv $ arg) |
136 | SOME (NONE) => @{term "{}::atom set"} |
147 | SOME (NONE) => @{term "{}::atom set"} |
137 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
148 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
138 end |
149 end |
139 |
150 handle Option => error "fv_map/fv_bn_map lookup " |
140 fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = |
|
141 let |
|
142 val arg = nth args i |
|
143 in |
|
144 case bn_option of |
|
145 NONE => (setify lthy arg, @{term "{}::atom set"}) |
|
146 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
|
147 end |
|
148 |
151 |
149 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
152 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
150 let |
153 let |
151 val t1 = map (mk_fv_body fv_map args) bodies |
154 val t1 = map (mk_fv_body fv_map args) bodies |
152 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
155 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
153 in |
156 in |
154 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
157 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
155 end |
158 end |
156 |
159 |
|
160 (* in case of fv_bn we have to treat the case special, where an |
|
161 "empty" binding clause is given *) |
157 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
162 fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = |
158 case bclause of |
163 case bclause of |
159 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
164 BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) |
160 | BC (_, binders, bodies) => |
165 | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause |
161 let |
166 |
162 val t1 = map (mk_fv_body fv_map args) bodies |
|
163 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
|
164 in |
|
165 fold_union (mk_diff (fold_union t1, fold_union t2)::t3) |
|
166 end |
|
167 |
167 |
168 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
168 fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = |
169 let |
169 let |
170 val arg_names = Datatype_Prop.make_tnames arg_tys |
170 val arg_names = Datatype_Prop.make_tnames arg_tys |
171 val args = map Free (arg_names ~~ arg_tys) |
171 val args = map Free (arg_names ~~ arg_tys) |
221 val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2) |
221 val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2) |
222 val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3) |
222 val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3) |
223 |
223 |
224 val constrs_info = all_dtyp_constrs_types dt_descr sorts |
224 val constrs_info = all_dtyp_constrs_types dt_descr sorts |
225 |
225 |
226 val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss |
226 val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map3)) constrs_info bclausesss |
227 val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 |
227 val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 |
228 |
228 |
229 val _ = tracing ("functions to be defined\n " ^ @{make_string} (fv_names @ fv_bn_names2)) |
229 val _ = tracing ("functions to be defined\n " ^ @{make_string} (t1 @ fv_names @ fv_bn_names2)) |
230 val _ = tracing ("equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_eqs2 @ flat fv_bn_eqs2))) |
230 val _ = tracing ("equations\n " ^ |
231 |
231 cat_lines (map (Syntax.string_of_term lthy) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2))) |
232 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) |
232 |
233 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) |
233 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (t1 @ fv_names @ fv_bn_names2) |
|
234 val all_fv_eqs = map (pair Attrib.empty_binding) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2) |
234 |
235 |
235 fun pat_completeness_auto lthy = |
236 fun pat_completeness_auto lthy = |
236 Pat_Completeness.pat_completeness_tac lthy 1 |
237 Pat_Completeness.pat_completeness_tac lthy 1 |
237 THEN auto_tac (clasimpset_of lthy) |
238 THEN auto_tac (clasimpset_of lthy) |
238 |
239 |