22803

1 
(* Title: HOL/Library/Pretty_Int.thy


2 
ID: $Id$

22767

3 
Author: Florian Haftmann, TU Muenchen


4 
*)


5 


6 
header {* Pretty integer literals for code generation *}


7 


8 
theory Pretty_Int


9 
imports IntArith


10 
begin


11 


12 
text {*


13 
HOL numeral expressions are mapped to integer literals


14 
in target languages, using predefined target language


15 
operations for abstract integer operations.


16 
*}


17 


18 
code_type int


19 
(SML "IntInf.int")


20 
(OCaml "Big'_int.big'_int")


21 
(Haskell "Integer")


22 

22949

23 
code_instance int :: eq


24 
(Haskell )


25 

22767

26 
setup {*


27 
fold (fn target => CodegenSerializer.add_pretty_numeral target


28 
(@{const_name number_of}, @{typ "int \<Rightarrow> int"})


29 
@{const_name Numeral.B0} @{const_name Numeral.B1}


30 
@{const_name Numeral.Pls} @{const_name Numeral.Min}


31 
@{const_name Numeral.Bit}


32 
) ["SML", "OCaml", "Haskell"]


33 
*}


34 


35 
code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"


36 
(SML "raise/ Fail/ \"Pls\""


37 
and "raise/ Fail/ \"Min\""


38 
and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")


39 
(OCaml "failwith/ \"Pls\""


40 
and "failwith/ \"Min\""


41 
and "!((_);/ (_);/ failwith/ \"Bit\")")


42 
(Haskell "error/ \"Pls\""


43 
and "error/ \"Min\""


44 
and "error/ \"Bit\"")


45 


46 
code_const Numeral.pred


47 
(SML "IntInf. ((_), 1)")


48 
(OCaml "Big'_int.pred'_big'_int")


49 
(Haskell "!(_/ / 1)")


50 


51 
code_const Numeral.succ


52 
(SML "IntInf.+ ((_), 1)")


53 
(OCaml "Big'_int.succ'_big'_int")


54 
(Haskell "!(_/ +/ 1)")


55 


56 
code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"


57 
(SML "IntInf.+ ((_), (_))")


58 
(OCaml "Big'_int.add'_big'_int")


59 
(Haskell infixl 6 "+")


60 


61 
code_const "uminus \<Colon> int \<Rightarrow> int"


62 
(SML "IntInf.~")


63 
(OCaml "Big'_int.minus'_big'_int")


64 
(Haskell "negate")


65 


66 
code_const "op  \<Colon> int \<Rightarrow> int \<Rightarrow> int"


67 
(SML "IntInf. ((_), (_))")


68 
(OCaml "Big'_int.sub'_big'_int")


69 
(Haskell infixl 6 "")


70 


71 
code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"


72 
(SML "IntInf.* ((_), (_))")


73 
(OCaml "Big'_int.mult'_big'_int")


74 
(Haskell infixl 7 "*")


75 


76 
code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"


77 
(SML "!((_ : IntInf.int) = _)")


78 
(OCaml "Big'_int.eq'_big'_int")


79 
(Haskell infixl 4 "==")


80 


81 
code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"


82 
(SML "IntInf.<= ((_), (_))")


83 
(OCaml "Big'_int.le'_big'_int")


84 
(Haskell infix 4 "<=")


85 


86 
code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"


87 
(SML "IntInf.< ((_), (_))")


88 
(OCaml "Big'_int.lt'_big'_int")


89 
(Haskell infix 4 "<")


90 


91 
code_reserved SML IntInf


92 
code_reserved OCaml Big_int


93 


94 
end 