213 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
213 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
214 let |
214 let |
215 val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy2) = |
215 val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy2) = |
216 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
216 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
217 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
217 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); |
|
218 val descr = #descr dtinfo; |
|
219 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
|
220 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; |
|
221 val inject = flat (map #inject dtinfos); |
|
222 val distinct = flat (map #distinct dtinfos); |
|
223 val inducts = #inducts dtinfo; |
218 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
224 val ((raw_perm_def, raw_perm_simps, perms), lthy3) = |
219 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
225 Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2; |
220 val raw_binds_flat = map (map flat) raw_binds; |
226 val raw_binds_flat = map (map flat) raw_binds; |
221 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; |
227 val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat lthy3; |
222 |
228 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
223 in |
229 val _ = tracing (PolyML.makestring dts_names); |
224 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4) |
230 val bn_tys = map (domain_type o fastype_of) raw_bn_funs; |
|
231 val _ = tracing (PolyML.makestring bn_tys); |
|
232 val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys; |
|
233 val _ = tracing (PolyML.makestring bn_nos); |
|
234 val bns = raw_bn_funs ~~ bn_nos; |
|
235 val alpha_intros = #intrs alpha; |
|
236 val alpha_cases = #elims alpha |
|
237 val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4 |
|
238 val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4; |
|
239 |
|
240 in |
|
241 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5) |
225 end |
242 end |
226 *} |
243 *} |
227 |
244 |
228 ML {* |
245 ML {* |
229 (* parsing the datatypes and declaring *) |
246 (* parsing the datatypes and declaring *) |