24 val get_codetypes_arities: theory -> (string * bool) list -> sort |
24 val get_codetypes_arities: theory -> (string * bool) list -> sort |
25 -> (string * (arity * term list)) list option |
25 -> (string * (arity * term list)) list option |
26 val prove_codetypes_arities: tactic -> (string * bool) list -> sort |
26 val prove_codetypes_arities: tactic -> (string * bool) list -> sort |
27 -> (arity list -> (string * term list) list -> theory |
27 -> (arity list -> (string * term list) list -> theory |
28 -> ((bstring * Attrib.src list) * term) list * theory) |
28 -> ((bstring * Attrib.src list) * term) list * theory) |
29 -> (arity list -> (string * term list) list -> theory -> theory) |
29 -> (arity list -> (string * term list) list -> thm list -> theory -> theory) |
30 -> theory -> theory |
30 -> theory -> theory |
31 |
31 |
32 val setup: theory -> theory |
32 val setup: theory -> theory |
33 val setup_hooks: theory -> theory |
33 val setup_hooks: theory -> theory |
34 end; |
34 end; |
535 in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end; |
535 in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end; |
536 |
536 |
537 |
537 |
538 (* registering code types in code generator *) |
538 (* registering code types in code generator *) |
539 |
539 |
540 fun codetype_hook dtspecs = |
540 fun add_datatype_spec (tyco, (vs, cos)) thy = |
541 fold (fn (dtco, (_, spec)) => Code.add_datatype (dtco, spec)) dtspecs; |
541 let |
|
542 val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos; |
|
543 in try (Code.add_datatype cs) thy |> the_default thy end; |
|
544 |
|
545 val codetype_hook = |
|
546 fold (fn (dtco, (_, spec)) => add_datatype_spec (dtco, spec)); |
542 |
547 |
543 |
548 |
544 (* instrumentalizing the sort algebra *) |
549 (* instrumentalizing the sort algebra *) |
545 |
550 |
546 fun get_codetypes_arities thy tycos sort = |
551 fun get_codetypes_arities thy tycos sort = |
584 thy |
589 thy |
585 |> not (null arities) ? ( |
590 |> not (null arities) ? ( |
586 f arities css |
591 f arities css |
587 #-> (fn defs => |
592 #-> (fn defs => |
588 Class.prove_instance_arity tac arities defs |
593 Class.prove_instance_arity tac arities defs |
589 #> after_qed arities css)) |
594 #-> (fn defs => |
|
595 after_qed arities css defs))) |
590 end; |
596 end; |
591 |
597 |
592 |
598 |
593 (* operational equality *) |
599 (* operational equality *) |
594 |
600 |
595 fun eq_hook specs = |
601 fun eq_hook specs = |
596 let |
602 let |
597 fun add_eq_thms (dtco, (_, (vs, cs))) thy = |
603 fun add_eq_thms (dtco, (_, (vs, cs))) thy = |
598 let |
604 let |
599 val thy_ref = Theory.check_thy thy; |
605 val thy_ref = Theory.check_thy thy; |
600 val const = ("op =", SOME dtco); |
606 val const = Class.inst_const thy ("op =", dtco); |
601 val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev); |
607 val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev); |
602 in |
608 in |
603 Code.add_funcl (const, Susp.delay get_thms) thy |
609 Code.add_funcl (const, Susp.delay get_thms) thy |
604 end; |
610 end; |
605 in |
611 in |
606 prove_codetypes_arities (Class.intro_classes_tac []) |
612 prove_codetypes_arities (Class.intro_classes_tac []) |
607 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
613 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
608 [HOLogic.class_eq] ((K o K o pair) []) ((K o K) (fold add_eq_thms specs)) |
614 [HOLogic.class_eq] ((K o K o pair) []) ((K o K o K) (fold add_eq_thms specs)) |
609 end; |
615 end; |
610 |
616 |
611 |
617 |
612 |
618 |
613 (** theory setup **) |
619 (** theory setup **) |