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 ML {* |
899 ML {* |
900 fun number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of", |
900 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", |
901 Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) = |
901 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = |
902 (SOME (gr, Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) |
902 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), |
903 handle TERM _ => NONE) |
903 Pretty.str (IntInf.toString (HOLogic.dest_binum bin))) handle TERM _ => NONE) |
904 | number_of_codegen thy defs gr s thyname b (Const ("Numeral.number_of", |
|
905 Type ("fun", [_, Type ("nat", [])])) $ bin) = |
|
906 SOME (Codegen.invoke_codegen thy defs s thyname b (gr, |
|
907 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ |
|
908 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
|
909 | number_of_codegen _ _ _ _ _ _ _ = NONE; |
904 | number_of_codegen _ _ _ _ _ _ _ = NONE; |
910 *} |
905 *} |
911 |
906 |
912 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} |
907 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} |
913 |
908 |