894 "op *" :: "int => int => int" ("(_ */ _)") |
894 "op *" :: "int => int => int" ("(_ */ _)") |
895 "op <" :: "int => int => bool" ("(_ </ _)") |
895 "op <" :: "int => int => bool" ("(_ </ _)") |
896 "op <=" :: "int => int => bool" ("(_ <=/ _)") |
896 "op <=" :: "int => int => bool" ("(_ <=/ _)") |
897 "neg" ("(_ < 0)") |
897 "neg" ("(_ < 0)") |
898 |
898 |
|
899 code_syntax_tyco int |
|
900 ml (atom "IntInf.int") |
|
901 haskell (atom "Integer") |
|
902 |
|
903 code_syntax_const |
|
904 0 :: "int" |
|
905 ml ("0 : IntInf.int") |
|
906 haskell (atom "0") |
|
907 1 :: "int" |
|
908 ml ("1 : IntInf.int") |
|
909 haskell (atom "1") |
|
910 |
|
911 code_syntax_const |
|
912 "op +" :: "int \<Rightarrow> int \<Rightarrow> int" |
|
913 ml (infixl 8 "+") |
|
914 haskell (infixl 6 "+") |
|
915 "op *" :: "int \<Rightarrow> int \<Rightarrow> int" |
|
916 ml (infixl 9 "*") |
|
917 haskell (infixl 7 "*") |
|
918 uminus :: "int \<Rightarrow> int" |
|
919 ml (atom "~") |
|
920 haskell (atom "negate") |
|
921 "op <" :: "int \<Rightarrow> int \<Rightarrow> bool" |
|
922 ml (infix 6 "<") |
|
923 haskell (infix 4 "<") |
|
924 "op <=" :: "int \<Rightarrow> int \<Rightarrow> bool" |
|
925 ml (infix 6 "<=") |
|
926 haskell (infix 4 "<=") |
|
927 "neg" :: "int \<Rightarrow> bool" |
|
928 ml ("_ < 0") |
|
929 haskell ("_ < 0") |
|
930 |
899 ML {* |
931 ML {* |
900 fun mk_int_to_nat bin = |
932 fun mk_int_to_nat bin = |
901 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) |
933 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) |
902 $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin); |
934 $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin); |
|
935 |
|
936 fun bin_to_int bin = HOLogic.dest_binum bin |
|
937 handle TERM _ |
|
938 => error ("not a number: " ^ Sign.string_of_term thy bin); |
903 |
939 |
904 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", |
940 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", |
905 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = |
941 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = |
906 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), |
942 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), |
907 Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE) |
943 Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE) |
909 Type ("fun", [_, Type ("nat", [])])) $ bin) = |
945 Type ("fun", [_, Type ("nat", [])])) $ bin) = |
910 SOME (Codegen.invoke_codegen thy defs s thyname b (gr, |
946 SOME (Codegen.invoke_codegen thy defs s thyname b (gr, |
911 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ |
947 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ |
912 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
948 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
913 | number_of_codegen _ _ _ _ _ _ _ = NONE; |
949 | number_of_codegen _ _ _ _ _ _ _ = NONE; |
|
950 |
914 *} |
951 *} |
915 |
952 |
916 setup {*[ |
953 setup {*[ |
917 Codegen.add_codegen "number_of_codegen" number_of_codegen, |
954 Codegen.add_codegen "number_of_codegen" number_of_codegen, |
918 CodegenPackage.add_appconst |
955 CodegenPackage.add_appconst |
919 ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat)) |
956 ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")), |
|
957 CodegenPackage.set_int_tyco "IntDef.int" |
920 ]*} |
958 ]*} |
921 |
959 |
922 quickcheck_params [default_type = int] |
960 quickcheck_params [default_type = int] |
923 |
961 |
924 |
962 |