1793 in Thm.implies_elim thm' thm end; |
1793 in Thm.implies_elim thm' thm end; |
1794 |
1794 |
1795 |
1795 |
1796 (* code generation *) |
1796 (* code generation *) |
1797 |
1797 |
1798 fun instantiate_random_record tyco vs extN Ts thy = |
1798 fun mk_random_eq tyco vs extN Ts = |
1799 let |
1799 let |
1800 val size = @{term "i::code_numeral"}; |
1800 val size = @{term "i::code_numeral"}; |
1801 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
1801 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
1802 val T = Type (tyco, map TFree vs); |
1802 val T = Type (tyco, map TFree vs); |
1803 val Tm = termifyT T; |
1803 val Tm = termifyT T; |
1808 val rhs = |
1808 val rhs = |
1809 HOLogic.mk_ST |
1809 HOLogic.mk_ST |
1810 (map (fn (v, T') => |
1810 (map (fn (v, T') => |
1811 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params) |
1811 ((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, termifyT T'))) params) |
1812 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed}); |
1812 tc @{typ Random.seed} (SOME Tm, @{typ Random.seed}); |
1813 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
1813 in |
|
1814 (lhs, rhs) |
|
1815 end |
|
1816 |
|
1817 fun mk_full_exhaustive_eq tyco vs extN Ts = |
|
1818 let |
|
1819 val size = @{term "i::code_numeral"}; |
|
1820 fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}); |
|
1821 val T = Type (tyco, map TFree vs); |
|
1822 val test_function = Free ("f", termifyT T --> @{typ "term list option"}); |
|
1823 val params = Name.names Name.context "x" Ts; |
|
1824 fun full_exhaustiveT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) |
|
1825 --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} |
|
1826 fun mk_full_exhaustive T = |
|
1827 Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, |
|
1828 full_exhaustiveT T) |
|
1829 val lhs = mk_full_exhaustive T $ test_function $ size; |
|
1830 val tc = test_function $ (HOLogic.mk_valtermify_app extN params T); |
|
1831 val rhs = fold_rev (fn (v, T) => fn cont => |
|
1832 mk_full_exhaustive T $ (lambda (Free (v, termifyT T)) cont) $ size) params tc |
|
1833 in |
|
1834 (lhs, rhs) |
|
1835 end |
|
1836 |
|
1837 fun instantiate_sort_record (sort, mk_eq) tyco vs extN Ts thy = |
|
1838 let |
|
1839 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_eq tyco vs extN Ts)); |
1814 in |
1840 in |
1815 thy |
1841 thy |
1816 |> Class.instantiation ([tyco], vs, @{sort random}) |
1842 |> Class.instantiation ([tyco], vs, sort) |
1817 |> `(fn lthy => Syntax.check_term lthy eq) |
1843 |> `(fn lthy => Syntax.check_term lthy eq) |
1818 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq))) |
1844 |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq))) |
1819 |> snd |
1845 |> snd |
1820 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
1846 |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) |
1821 end; |
1847 end |
1822 |
1848 |
1823 fun ensure_random_record ext_tyco vs extN Ts thy = |
1849 fun ensure_sort_record (sort, mk_eq) ext_tyco vs extN Ts thy = |
1824 let |
1850 let |
1825 val algebra = Sign.classes_of thy; |
1851 val algebra = Sign.classes_of thy; |
1826 val has_inst = can (Sorts.mg_domain algebra ext_tyco) @{sort random}; |
1852 val has_inst = can (Sorts.mg_domain algebra ext_tyco) sort; |
1827 in |
1853 in |
1828 if has_inst then thy |
1854 if has_inst then thy |
1829 else |
1855 else |
1830 (case Quickcheck_Common.perhaps_constrain thy (map (rpair @{sort random}) Ts) vs of |
1856 (case Quickcheck_Common.perhaps_constrain thy (map (rpair sort) Ts) vs of |
1831 SOME constrain => |
1857 SOME constrain => |
1832 instantiate_random_record ext_tyco (map constrain vs) extN |
1858 instantiate_sort_record (sort, mk_eq) ext_tyco (map constrain vs) extN |
1833 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy |
1859 ((map o map_atyps) (fn TFree v => TFree (constrain v)) Ts) thy |
1834 | NONE => thy) |
1860 | NONE => thy) |
1835 end; |
1861 end; |
1836 |
1862 |
1837 fun add_code ext_tyco vs extT ext simps inject thy = |
1863 fun add_code ext_tyco vs extT ext simps inject thy = |
1849 fun mk_eq_refl thy = |
1875 fun mk_eq_refl thy = |
1850 @{thm equal_refl} |
1876 @{thm equal_refl} |
1851 |> Thm.instantiate |
1877 |> Thm.instantiate |
1852 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) |
1878 ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) |
1853 |> AxClass.unoverload thy; |
1879 |> AxClass.unoverload thy; |
|
1880 val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq) |
|
1881 val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq) |
1854 in |
1882 in |
1855 thy |
1883 thy |
1856 |> Code.add_datatype [ext] |
1884 |> Code.add_datatype [ext] |
1857 |> fold Code.add_default_eqn simps |
1885 |> fold Code.add_default_eqn simps |
1858 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal]) |
1886 |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal]) |