69 |
69 |
70 fun get_bn_fun_strs bn_funs = |
70 fun get_bn_fun_strs bn_funs = |
71 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
71 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
72 *} |
72 *} |
73 |
73 |
74 |
|
75 ML {* |
|
76 (* exports back the results *) |
|
77 fun add_primrec_wrapper funs eqs lthy = |
|
78 if null funs then ([], [], lthy) |
|
79 else |
|
80 let |
|
81 val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs |
|
82 val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs |
|
83 val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy |
|
84 val phi = ProofContext.export_morphism lthy' lthy |
|
85 in |
|
86 (map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs'', lthy') |
|
87 end |
|
88 *} |
|
89 |
74 |
90 ML {* |
75 ML {* |
91 fun add_datatype_wrapper dt_names dts = |
76 fun add_datatype_wrapper dt_names dts = |
92 let |
77 let |
93 val conf = Datatype.default_config |
78 val conf = Datatype.default_config |
448 if get_STEPS lthy > 14 |
433 if get_STEPS lthy > 14 |
449 then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
434 then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6 |
450 else raise TEST lthy6 |
435 else raise TEST lthy6 |
451 |
436 |
452 val qtys = map #qtyp qty_infos |
437 val qtys = map #qtyp qty_infos |
453 |
438 val qconstr_descrs = |
|
439 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
|
440 |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs |
|
441 |
|
442 val (qconstrs, lthy8) = |
|
443 if get_STEPS lthy > 15 |
|
444 then qconst_defs qtys qconstr_descrs lthy7 |
|
445 else raise TEST lthy7 |
|
446 |
|
447 (* HERE *) |
|
448 |
454 val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys)) |
449 val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys)) |
455 val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs)) |
450 val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs)) |
456 val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys)) |
451 val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys)) |
|
452 val _ = tracing ("qconstrs " ^ commas (map @{make_string} qconstrs)) |
457 |
453 |
458 |
|
459 |
|
460 val _ = |
454 val _ = |
461 if get_STEPS lthy > 15 |
455 if get_STEPS lthy > 16 |
462 then true else raise TEST lthy7 |
456 then true else raise TEST lthy8 |
463 |
457 |
464 (* old stuff *) |
458 (* old stuff *) |
465 |
459 |
466 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
460 val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts)); |
467 val raw_consts = |
461 val raw_consts = |
468 flat (map (fn (i, (_, _, l)) => |
462 flat (map (fn (i, (_, _, l)) => |
469 map (fn (cname, dts) => |
463 map (fn (cname, dts) => |
470 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
464 Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> |
471 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
465 Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); |
472 val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts |
466 val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts |
473 val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys dd lthy7; |
467 val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7; |
474 val _ = warning "Proving respects"; |
468 val _ = warning "Proving respects"; |
475 |
469 |
476 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
470 val bn_nos = map (fn (_, i, _) => i) raw_bn_info; |
477 val bns = raw_bn_funs ~~ bn_nos; |
471 val bns = raw_bn_funs ~~ bn_nos; |
478 |
472 |