716 val more' = mk_ext rest; |
716 val more' = mk_ext rest; |
717 in |
717 in |
718 list_comb |
718 list_comb |
719 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more']) |
719 (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more']) |
720 end |
720 end |
721 | NONE => err ("no fields defined for " ^ ext)) |
721 | NONE => err ("no fields defined for " ^ quote ext)) |
722 | NONE => err (name ^ " is no proper field")) |
722 | NONE => err (quote name ^ " is no proper field")) |
723 | mk_ext [] = more; |
723 | mk_ext [] = more; |
724 in |
724 in |
725 mk_ext (field_types_tr t) |
725 mk_ext (field_types_tr t) |
726 end; |
726 end; |
727 |
727 |
751 let |
751 let |
752 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs |
752 val (args, rest) = split_args (map fst (fst (split_last fields))) fargs |
753 handle Fail msg => err msg; |
753 handle Fail msg => err msg; |
754 val more' = mk_ext rest; |
754 val more' = mk_ext rest; |
755 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end |
755 in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end |
756 | NONE => err ("no fields defined for " ^ ext)) |
756 | NONE => err ("no fields defined for " ^ quote ext)) |
757 | NONE => err (name ^ " is no proper field")) |
757 | NONE => err (quote name ^ " is no proper field")) |
758 | mk_ext [] = more; |
758 | mk_ext [] = more; |
759 in mk_ext (fields_tr t) end; |
759 in mk_ext (fields_tr t) end; |
760 |
760 |
761 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t |
761 fun record_tr ctxt [t] = record_fields_tr (Syntax.const @{const_syntax Unity}) ctxt t |
762 | record_tr _ ts = raise TERM ("record_tr", ts); |
762 | record_tr _ ts = raise TERM ("record_tr", ts); |
764 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t |
764 fun record_scheme_tr ctxt [t, more] = record_fields_tr more ctxt t |
765 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); |
765 | record_scheme_tr _ ts = raise TERM ("record_scheme_tr", ts); |
766 |
766 |
767 |
767 |
768 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) = |
768 fun field_update_tr (Const (@{syntax_const "_field_update"}, _) $ Const (name, _) $ arg) = |
769 Syntax.const (suffix updateN name) $ Abs ("_", dummyT, arg) |
769 Syntax.const (suffix updateN name) $ Abs (Name.uu_, dummyT, arg) |
770 | field_update_tr t = raise TERM ("field_update_tr", [t]); |
770 | field_update_tr t = raise TERM ("field_update_tr", [t]); |
771 |
771 |
772 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) = |
772 fun field_updates_tr (Const (@{syntax_const "_field_updates"}, _) $ t $ u) = |
773 field_update_tr t :: field_updates_tr u |
773 field_update_tr t :: field_updates_tr u |
774 | field_updates_tr t = [field_update_tr t]; |
774 | field_updates_tr t = [field_update_tr t]; |
1656 val variants = map (fn Free (x, _) => x) vars_more; |
1656 val variants = map (fn Free (x, _) => x) vars_more; |
1657 val ext = mk_ext vars_more; |
1657 val ext = mk_ext vars_more; |
1658 val s = Free (rN, extT); |
1658 val s = Free (rN, extT); |
1659 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT); |
1659 val P = Free (singleton (Name.variant_list variants) "P", extT --> HOLogic.boolT); |
1660 |
1660 |
1661 val inject_prop = |
1661 val inject_prop = (* FIXME local x x' *) |
1662 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in |
1662 let val vars_more' = map (fn (Free (x, T)) => Free (x ^ "'", T)) vars_more in |
1663 HOLogic.mk_conj (HOLogic.eq_const extT $ |
1663 HOLogic.mk_conj (HOLogic.eq_const extT $ |
1664 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const) |
1664 mk_ext vars_more $ mk_ext vars_more', HOLogic.true_const) |
1665 === |
1665 === |
1666 foldr1 HOLogic.mk_conj |
1666 foldr1 HOLogic.mk_conj |
1668 end; |
1668 end; |
1669 |
1669 |
1670 val induct_prop = |
1670 val induct_prop = |
1671 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s)); |
1671 (All (map dest_Free vars_more) (Trueprop (P $ ext)), Trueprop (P $ s)); |
1672 |
1672 |
1673 val split_meta_prop = |
1673 val split_meta_prop = (* FIXME local P *) |
1674 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in |
1674 let val P = Free (singleton (Name.variant_list variants) "P", extT --> Term.propT) in |
1675 Logic.mk_equals |
1675 Logic.mk_equals |
1676 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) |
1676 (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext)) |
1677 end; |
1677 end; |
1678 |
1678 |
1789 |
1789 |
1790 (* code generation *) |
1790 (* code generation *) |
1791 |
1791 |
1792 fun mk_random_eq tyco vs extN Ts = |
1792 fun mk_random_eq tyco vs extN Ts = |
1793 let |
1793 let |
|
1794 (* FIXME local i etc. *) |
1794 val size = @{term "i::code_numeral"}; |
1795 val size = @{term "i::code_numeral"}; |
1795 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
1796 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
1796 val T = Type (tyco, map TFree vs); |
1797 val T = Type (tyco, map TFree vs); |
1797 val Tm = termifyT T; |
1798 val Tm = termifyT T; |
1798 val params = Name.invent_names Name.context "x" Ts; |
1799 val params = Name.invent_names Name.context "x" Ts; |
1808 (lhs, rhs) |
1809 (lhs, rhs) |
1809 end |
1810 end |
1810 |
1811 |
1811 fun mk_full_exhaustive_eq tyco vs extN Ts = |
1812 fun mk_full_exhaustive_eq tyco vs extN Ts = |
1812 let |
1813 let |
|
1814 (* FIXME local i etc. *) |
1813 val size = @{term "i::code_numeral"}; |
1815 val size = @{term "i::code_numeral"}; |
1814 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
1816 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
1815 val T = Type (tyco, map TFree vs); |
1817 val T = Type (tyco, map TFree vs); |
1816 val test_function = Free ("f", termifyT T --> @{typ "term list option"}); |
1818 val test_function = Free ("f", termifyT T --> @{typ "term list option"}); |
1817 val params = Name.invent_names Name.context "x" Ts; |
1819 val params = Name.invent_names Name.context "x" Ts; |
1818 fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) |
1820 fun full_exhaustiveT T = |
1819 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} |
1821 (termifyT T --> @{typ "Code_Evaluation.term list option"}) --> |
|
1822 @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}; |
1820 fun mk_full_exhaustive T = |
1823 fun mk_full_exhaustive T = |
1821 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, |
1824 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, |
1822 full_exhaustiveT T) |
1825 full_exhaustiveT T); |
1823 val lhs = mk_full_exhaustive T $ test_function $ size; |
1826 val lhs = mk_full_exhaustive T $ test_function $ size; |
1824 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T); |
1827 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T); |
1825 val rhs = fold_rev (fn (v, T) => fn cont => |
1828 val rhs = fold_rev (fn (v, T) => fn cont => |
1826 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc |
1829 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc; |
1827 in |
1830 in |
1828 (lhs, rhs) |
1831 (lhs, rhs) |
1829 end |
1832 end; |
1830 |
1833 |
1831 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy = |
1834 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy = |
1832 let |
1835 let |
1833 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts)); |
1836 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts)); |
1834 in |
1837 in |
1836 |> Class.instantiation ([tyco], vs, sort) |
1839 |> Class.instantiation ([tyco], vs, sort) |
1837 |> `(fn lthy => Syntax.check_term lthy eq) |
1840 |> `(fn lthy => Syntax.check_term lthy eq) |
1838 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq))) |
1841 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq))) |
1839 |> snd |
1842 |> snd |
1840 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
1843 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
1841 end |
1844 end; |
1842 |
1845 |
1843 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy = |
1846 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy = |
1844 let |
1847 let |
1845 val algebra = Sign.classes_of thy; |
1848 val algebra = Sign.classes_of thy; |
1846 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort; |
1849 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort; |