src/HOL/Library/Code_Integer.thy
author haftmann
Sat Jul 24 18:08:41 2010 +0200 (2010-07-24)
changeset 37958 9728342bcd56
parent 37947 844977c7abeb
child 37968 52fdcb76c0af
permissions -rw-r--r--
another refinement chapter in the neverending numeral story
     1 (*  Title:      HOL/Library/Code_Integer.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Pretty integer literals for code generation *}
     6 
     7 theory Code_Integer
     8 imports Main
     9 begin
    10 
    11 text {*
    12   HOL numeral expressions are mapped to integer literals
    13   in target languages, using predefined target language
    14   operations for abstract integer operations.
    15 *}
    16 
    17 text {*
    18   Preliminary: alternative representation of @{typ code_numeral}
    19   for @{text Haskell} and @{text Scala}.
    20 *}
    21 
    22 code_include Haskell "Natural" {*
    23 newtype Natural = Natural Integer deriving (Eq, Show, Read);
    24 
    25 instance Num Natural where {
    26   fromInteger k = Natural (if k >= 0 then k else 0);
    27   Natural n + Natural m = Natural (n + m);
    28   Natural n - Natural m = fromInteger (n - m);
    29   Natural n * Natural m = Natural (n * m);
    30   abs n = n;
    31   signum _ = 1;
    32   negate n = error "negate Natural";
    33 };
    34 
    35 instance Ord Natural where {
    36   Natural n <= Natural m = n <= m;
    37   Natural n < Natural m = n < m;
    38 };
    39 
    40 instance Real Natural where {
    41   toRational (Natural n) = toRational n;
    42 };
    43 
    44 instance Enum Natural where {
    45   toEnum k = fromInteger (toEnum k);
    46   fromEnum (Natural n) = fromEnum n;
    47 };
    48 
    49 instance Integral Natural where {
    50   toInteger (Natural n) = n;
    51   divMod n m = quotRem n m;
    52   quotRem (Natural n) (Natural m)
    53     | (m == 0) = (0, Natural n)
    54     | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m;
    55 };
    56 *}
    57 
    58 code_reserved Haskell Natural
    59 
    60 code_include Scala "Natural" {*
    61 import scala.Math
    62 
    63 object Natural {
    64 
    65   def apply(numeral: BigInt): Natural = new Natural(numeral max 0)
    66   def apply(numeral: Int): Natural = Natural(BigInt(numeral))
    67   def apply(numeral: String): Natural = Natural(BigInt(numeral))
    68 
    69 }
    70 
    71 class Natural private(private val value: BigInt) {
    72 
    73   override def hashCode(): Int = this.value.hashCode()
    74 
    75   override def equals(that: Any): Boolean = that match {
    76     case that: Natural => this equals that
    77     case _ => false
    78   }
    79 
    80   override def toString(): String = this.value.toString
    81 
    82   def equals(that: Natural): Boolean = this.value == that.value
    83 
    84   def as_BigInt: BigInt = this.value
    85   def as_Int: Int = if (this.value >= Int.MinValue && this.value <= Int.MaxValue)
    86       this.value.intValue
    87     else this.value.intValue
    88 
    89   def +(that: Natural): Natural = new Natural(this.value + that.value)
    90   def -(that: Natural): Natural = Natural(this.value - that.value)
    91   def *(that: Natural): Natural = new Natural(this.value * that.value)
    92 
    93   def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this)
    94     else {
    95       val (k, l) = this.value /% that.value
    96       (new Natural(k), new Natural(l))
    97     }
    98 
    99   def <=(that: Natural): Boolean = this.value <= that.value
   100 
   101   def <(that: Natural): Boolean = this.value < that.value
   102 
   103 }
   104 *}
   105 
   106 code_reserved Scala Natural
   107 
   108 code_type code_numeral
   109   (Haskell "Natural.Natural")
   110   (Scala "Natural")
   111 
   112 setup {*
   113   fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
   114     false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
   115 *}
   116 
   117 code_instance code_numeral :: eq
   118   (Haskell -)
   119 
   120 code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   121   (Haskell infixl 6 "+")
   122   (Scala infixl 7 "+")
   123 
   124 code_const "op - \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   125   (Haskell infixl 6 "-")
   126   (Scala infixl 7 "-")
   127 
   128 code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   129   (Haskell infixl 7 "*")
   130   (Scala infixl 8 "*")
   131 
   132 code_const div_mod_code_numeral
   133   (Haskell "divMod")
   134   (Scala infixl 8 "/%")
   135 
   136 code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   137   (Haskell infixl 4 "==")
   138   (Scala infixl 5 "==")
   139 
   140 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   141   (Haskell infix 4 "<=")
   142   (Scala infixl 4 "<=")
   143 
   144 code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   145   (Haskell infix 4 "<")
   146   (Scala infixl 4 "<")
   147 
   148 text {*
   149   Setup for @{typ int} proper.
   150 *}
   151 
   152 
   153 code_type int
   154   (SML "IntInf.int")
   155   (OCaml "Big'_int.big'_int")
   156   (Haskell "Integer")
   157   (Scala "BigInt")
   158 
   159 code_instance int :: eq
   160   (Haskell -)
   161 
   162 setup {*
   163   fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
   164     true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
   165 *}
   166 
   167 code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
   168   (SML "raise/ Fail/ \"Pls\""
   169      and "raise/ Fail/ \"Min\""
   170      and "!((_);/ raise/ Fail/ \"Bit0\")"
   171      and "!((_);/ raise/ Fail/ \"Bit1\")")
   172   (OCaml "failwith/ \"Pls\""
   173      and "failwith/ \"Min\""
   174      and "!((_);/ failwith/ \"Bit0\")"
   175      and "!((_);/ failwith/ \"Bit1\")")
   176   (Haskell "error/ \"Pls\""
   177      and "error/ \"Min\""
   178      and "error/ \"Bit0\""
   179      and "error/ \"Bit1\"")
   180   (Scala "!error(\"Pls\")"
   181      and "!error(\"Min\")"
   182      and "!error(\"Bit0\")"
   183      and "!error(\"Bit1\")")
   184 
   185 code_const Int.pred
   186   (SML "IntInf.- ((_), 1)")
   187   (OCaml "Big'_int.pred'_big'_int")
   188   (Haskell "!(_/ -/ 1)")
   189   (Scala "!(_/ -/ 1)")
   190   (Eval "!(_/ -/ 1)")
   191 
   192 code_const Int.succ
   193   (SML "IntInf.+ ((_), 1)")
   194   (OCaml "Big'_int.succ'_big'_int")
   195   (Haskell "!(_/ +/ 1)")
   196   (Scala "!(_/ +/ 1)")
   197   (Eval "!(_/ +/ 1)")
   198 
   199 code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   200   (SML "IntInf.+ ((_), (_))")
   201   (OCaml "Big'_int.add'_big'_int")
   202   (Haskell infixl 6 "+")
   203   (Scala infixl 7 "+")
   204   (Eval infixl 8 "+")
   205 
   206 code_const "uminus \<Colon> int \<Rightarrow> int"
   207   (SML "IntInf.~")
   208   (OCaml "Big'_int.minus'_big'_int")
   209   (Haskell "negate")
   210   (Scala "!(- _)")
   211   (Eval "~/ _")
   212 
   213 code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   214   (SML "IntInf.- ((_), (_))")
   215   (OCaml "Big'_int.sub'_big'_int")
   216   (Haskell infixl 6 "-")
   217   (Scala infixl 7 "-")
   218   (Eval infixl 8 "-")
   219 
   220 code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   221   (SML "IntInf.* ((_), (_))")
   222   (OCaml "Big'_int.mult'_big'_int")
   223   (Haskell infixl 7 "*")
   224   (Scala infixl 8 "*")
   225   (Eval infixl 9 "*")
   226 
   227 code_const pdivmod
   228   (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
   229   (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   230   (Haskell "divMod/ (abs _)/ (abs _)")
   231   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   232   (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   233 
   234 code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   235   (SML "!((_ : IntInf.int) = _)")
   236   (OCaml "Big'_int.eq'_big'_int")
   237   (Haskell infixl 4 "==")
   238   (Scala infixl 5 "==")
   239   (Eval infixl 6 "=")
   240 
   241 code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   242   (SML "IntInf.<= ((_), (_))")
   243   (OCaml "Big'_int.le'_big'_int")
   244   (Haskell infix 4 "<=")
   245   (Scala infixl 4 "<=")
   246   (Eval infixl 6 "<=")
   247 
   248 code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   249   (SML "IntInf.< ((_), (_))")
   250   (OCaml "Big'_int.lt'_big'_int")
   251   (Haskell infix 4 "<")
   252   (Scala infixl 4 "<")
   253   (Eval infixl 6 "<")
   254 
   255 code_const Code_Numeral.int_of
   256   (SML "IntInf.fromInt")
   257   (OCaml "_")
   258   (Haskell "toInteger")
   259   (Scala "!_.as'_BigInt")
   260   (Eval "_")
   261 
   262 text {* Evaluation *}
   263 
   264 code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
   265   (Eval "HOLogic.mk'_number/ HOLogic.intT")
   266 
   267 end