121 in |
120 in |
122 case (AList.lookup (op=) fv_map ty) of |
121 case (AList.lookup (op=) fv_map ty) of |
123 NONE => mk_supp arg |
122 NONE => mk_supp arg |
124 | SOME fv => fv $ arg |
123 | SOME fv => fv $ arg |
125 end |
124 end |
126 handle Option => error "fv_map lookup " |
|
127 |
125 |
128 fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = |
126 fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = |
129 let |
127 let |
130 val arg = nth args i |
128 val arg = nth args i |
131 in |
129 in |
132 case bn_option of |
130 case bn_option of |
133 NONE => (setify lthy arg, @{term "{}::atom set"}) |
131 NONE => (setify lthy arg, @{term "{}::atom set"}) |
134 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
132 | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) |
135 end |
133 end |
136 handle Option => error "fv_bn_map lookup " |
|
137 |
134 |
138 fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = |
135 fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = |
139 let |
136 let |
140 val arg = nth args i |
137 val arg = nth args i |
141 val ty = fastype_of arg |
138 val ty = fastype_of arg |
145 NONE => mk_supp arg |
142 NONE => mk_supp arg |
146 | SOME fv => fv $ arg) |
143 | SOME fv => fv $ arg) |
147 | SOME (NONE) => @{term "{}::atom set"} |
144 | SOME (NONE) => @{term "{}::atom set"} |
148 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
145 | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg |
149 end |
146 end |
150 handle Option => error "fv_map/fv_bn_map lookup " |
|
151 |
147 |
152 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
148 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = |
153 let |
149 let |
154 val t1 = map (mk_fv_body fv_map args) bodies |
150 val t1 = map (mk_fv_body fv_map args) bodies |
155 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
151 val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) |
195 val nth_bclausess = nth bclausesss bn_n |
191 val nth_bclausess = nth bclausesss bn_n |
196 in |
192 in |
197 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
193 map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess |
198 end |
194 end |
199 |
195 |
200 fun define_raw_fvs t1 t2 dt_descr sorts bn_funs bn_funs2 bclausesss lthy = |
196 fun define_raw_fvs dt_descr sorts bn_trms bn_funs2 bclausesss lthy = |
201 let |
197 let |
202 val _ = tracing ("bn-functions to be defined\n " ^ commas t1) |
|
203 val _ = tracing ("bn-equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) t2)) |
|
204 |
|
205 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
198 val fv_names = prefix_dt_names dt_descr sorts "fv_" |
206 val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; |
199 val fv_arg_tys = map (fn (i, _) => nth_dtyp dt_descr sorts i) dt_descr; |
207 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
200 val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys; |
208 val fv_frees = map Free (fv_names ~~ fv_tys); |
201 val fv_frees = map Free (fv_names ~~ fv_tys); |
209 val fv_map = fv_arg_tys ~~ fv_frees |
202 val fv_map = fv_arg_tys ~~ fv_frees |
210 |
203 |
211 val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs) |
204 val bn_tys2 = map (fn (_, i, _) => i) bn_funs2 |
212 val (bns2, bn_tys2) = split_list (map (fn (bn, i, _) => (bn, i)) bn_funs2) |
205 val fv_bn_names2 = map (fn bn => "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bn_trms |
213 val bn_args2 = map (fn (_, _, arg) => arg) bn_funs2 |
|
214 val fv_bn_names2 = map (fn bn => "fv_" ^ (fst (dest_Free bn))) bns2 |
|
215 val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2 |
206 val fv_bn_arg_tys2 = map (fn i => nth_dtyp dt_descr sorts i) bn_tys2 |
216 val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 |
207 val fv_bn_tys2 = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys2 |
217 val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) |
208 val fv_bn_frees2 = map Free (fv_bn_names2 ~~ fv_bn_tys2) |
218 val fv_bn_map2 = bns ~~ fv_bn_frees2 |
209 val fv_bn_map = bn_trms ~~ fv_bn_frees2 |
219 val fv_bn_map3 = bns2 ~~ fv_bn_frees2 |
|
220 |
|
221 val _ = tracing ("fn_bn_map2 " ^ @{make_string} fv_bn_map2) |
|
222 val _ = tracing ("fn_bn_map3 " ^ @{make_string} fv_bn_map3) |
|
223 |
210 |
224 val constrs_info = all_dtyp_constrs_types dt_descr sorts |
211 val constrs_info = all_dtyp_constrs_types dt_descr sorts |
225 |
212 |
226 val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map3)) constrs_info bclausesss |
213 val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss |
227 val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 |
214 val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_funs2 |
228 |
215 |
229 val _ = tracing ("functions to be defined\n " ^ @{make_string} (t1 @ fv_names @ fv_bn_names2)) |
216 val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) |
230 val _ = tracing ("equations\n " ^ |
217 val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) |
231 cat_lines (map (Syntax.string_of_term lthy) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2))) |
|
232 |
|
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) |
|
235 |
218 |
236 fun pat_completeness_auto lthy = |
219 fun pat_completeness_auto lthy = |
237 Pat_Completeness.pat_completeness_tac lthy 1 |
220 Pat_Completeness.pat_completeness_tac lthy 1 |
238 THEN auto_tac (clasimpset_of lthy) |
221 THEN auto_tac (clasimpset_of lthy) |
239 |
222 |