249 |
249 |
250 ML {* |
250 ML {* |
251 (* for testing porposes - to exit the procedure early *) |
251 (* for testing porposes - to exit the procedure early *) |
252 exception TEST of Proof.context |
252 exception TEST of Proof.context |
253 |
253 |
254 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0); |
254 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 100); |
255 |
255 |
256 fun get_STEPS ctxt = Config.get ctxt STEPS |
256 fun get_STEPS ctxt = Config.get ctxt STEPS |
257 *} |
257 *} |
258 |
258 |
259 setup STEPS_setup |
259 setup STEPS_setup |
260 |
260 |
261 ML {* |
261 ML {* |
262 fun nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses lthy = |
262 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
263 let |
263 let |
264 (* definition of the raw datatypes *) |
264 (* definition of the raw datatypes *) |
265 val _ = warning "Definition of raw datatypes"; |
265 val _ = warning "Definition of raw datatypes"; |
266 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
266 val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) = |
267 if get_STEPS lthy > 0 |
267 if get_STEPS lthy > 0 |
435 |
435 |
436 val qtys = map #qtyp qty_infos |
436 val qtys = map #qtyp qty_infos |
437 val qty_full_names = map (fst o dest_Type) qtys |
437 val qty_full_names = map (fst o dest_Type) qtys |
438 val qty_names = map Long_Name.base_name qty_full_names |
438 val qty_names = map Long_Name.base_name qty_full_names |
439 |
439 |
440 |
|
441 (* defining of quotient term-constructors, binding functions, free vars functions *) |
440 (* defining of quotient term-constructors, binding functions, free vars functions *) |
442 val _ = warning "Defining the quotient constants" |
441 val _ = warning "Defining the quotient constants" |
443 val qconstrs_descr = |
442 val qconstrs_descr = |
444 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
443 flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts) |
445 |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs |
444 |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs |
515 |> lift_thms qtys [] raw_size_eqvt |
514 |> lift_thms qtys [] raw_size_eqvt |
516 ||>> lift_thms qtys [] [raw_induct_thm] |
515 ||>> lift_thms qtys [] [raw_induct_thm] |
517 ||>> lift_thms qtys [] raw_exhaust_thms |
516 ||>> lift_thms qtys [] raw_exhaust_thms |
518 else raise TEST lthyA |
517 else raise TEST lthyA |
519 |
518 |
520 |
519 (* noting the theorems *) |
521 (* temporary theorem bindings *) |
520 |
|
521 (* generating the prefix for the theorem names *) |
|
522 val thms_name = |
|
523 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
|
524 fun thms_suffix s = Binding.qualified true s thms_name |
|
525 |
522 val (_, lthy9') = lthyB |
526 val (_, lthy9') = lthyB |
523 |> Local_Theory.note ((@{binding "distinct"}, []), qdistincts) |
527 |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) |
524 ||>> Local_Theory.note ((@{binding "eq_iff"}, []), qeq_iffs) |
528 ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs) |
525 ||>> Local_Theory.note ((@{binding "fv_defs"}, []), qfv_defs) |
529 ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) |
526 ||>> Local_Theory.note ((@{binding "bn_defs"}, []), qbn_defs) |
530 ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) |
527 ||>> Local_Theory.note ((@{binding "perm_simps"}, []), qperm_simps) |
531 ||>> Local_Theory.note ((thms_suffix "perm_simps", []), qperm_simps) |
528 ||>> Local_Theory.note ((@{binding "fv_bn_eqvt"}, []), qfv_qbn_eqvts) |
532 ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) |
529 ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), qsize_eqvt) |
533 ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt) |
530 ||>> Local_Theory.note ((@{binding "induct"}, []), [qinduct]) |
534 ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) |
531 ||>> Local_Theory.note ((@{binding "exhaust"}, []), qexhausts) |
535 ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts) |
532 |
536 |
533 |
|
534 val _ = |
|
535 if get_STEPS lthy > 21 |
|
536 then true else raise TEST lthy9' |
|
537 |
|
538 in |
537 in |
539 (0, lthy9') |
538 (0, lthy9') |
540 end handle TEST ctxt => (0, ctxt) |
539 end handle TEST ctxt => (0, ctxt) |
541 *} |
540 *} |
542 |
541 |
690 map2 (map2 complt) args bclauses |
689 map2 (map2 complt) args bclauses |
691 end |
690 end |
692 *} |
691 *} |
693 |
692 |
694 ML {* |
693 ML {* |
695 fun nominal_datatype2_cmd (opt_thm_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
694 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
696 let |
695 let |
697 val (pre_typ_names, pre_typs) = split_list |
696 val pre_typs = |
698 (map (fn (tvs, tname, mx, _) => |
697 map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs |
699 (Binding.name_of tname, (tname, length tvs, mx))) dt_strs) |
|
700 |
698 |
701 (* this theory is used just for parsing *) |
699 (* this theory is used just for parsing *) |
702 val thy = ProofContext.theory_of lthy |
700 val thy = ProofContext.theory_of lthy |
703 val tmp_thy = Theory.copy thy |
701 val tmp_thy = Theory.copy thy |
704 |
702 |
708 |> prepare_dts dt_strs |
706 |> prepare_dts dt_strs |
709 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
707 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
710 ||>> prepare_bclauses dt_strs |
708 ||>> prepare_bclauses dt_strs |
711 |
709 |
712 val bclauses' = complete dt_strs bclauses |
710 val bclauses' = complete dt_strs bclauses |
713 val thm_name = |
711 in |
714 the_default (Binding.name (space_implode "_" pre_typ_names)) opt_thm_name |
712 timeit (fn () => nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy |> snd) |
715 in |
|
716 timeit (fn () => nominal_datatype2 thm_name dts bn_funs bn_eqs bclauses' lthy |> snd) |
|
717 end |
713 end |
718 *} |
714 *} |
719 |
715 |
720 ML {* |
716 ML {* |
721 (* nominal datatype parser *) |
717 (* nominal datatype parser *) |