857 "neg" ("(_ < 0)") |
857 "neg" ("(_ < 0)") |
858 |
858 |
859 ML {* |
859 ML {* |
860 fun number_of_codegen thy gr s b (Const ("Numeral.number_of", |
860 fun number_of_codegen thy gr s b (Const ("Numeral.number_of", |
861 Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) = |
861 Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) = |
862 (Some (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin))) |
862 (SOME (gr, Pretty.str (string_of_int (HOLogic.dest_binum bin))) |
863 handle TERM _ => None) |
863 handle TERM _ => NONE) |
864 | number_of_codegen thy gr s b (Const ("Numeral.number_of", |
864 | number_of_codegen thy gr s b (Const ("Numeral.number_of", |
865 Type ("fun", [_, Type ("nat", [])])) $ bin) = |
865 Type ("fun", [_, Type ("nat", [])])) $ bin) = |
866 Some (Codegen.invoke_codegen thy s b (gr, |
866 SOME (Codegen.invoke_codegen thy s b (gr, |
867 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ |
867 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ |
868 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
868 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) |
869 | number_of_codegen _ _ _ _ _ = None; |
869 | number_of_codegen _ _ _ _ _ = NONE; |
870 *} |
870 *} |
871 |
871 |
872 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} |
872 setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *} |
873 |
873 |
874 end |
874 end |