src/HOL/Library/Code_Integer.thy
changeset 34899 8674bb6f727b
parent 32657 5f13912245ff
child 34944 970e1466028d
     1.1 --- a/src/HOL/Library/Code_Integer.thy	Thu Jan 14 17:47:38 2010 +0100
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Thu Jan 14 17:47:39 2010 +0100
     1.3 @@ -18,13 +18,16 @@
     1.4    (SML "IntInf.int")
     1.5    (OCaml "Big'_int.big'_int")
     1.6    (Haskell "Integer")
     1.7 +  (Scala "BigInt")
     1.8  
     1.9  code_instance int :: eq
    1.10    (Haskell -)
    1.11  
    1.12  setup {*
    1.13    fold (Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.14 -    true true) ["SML", "OCaml", "Haskell"]
    1.15 +    true true Code_Printer.str) ["SML", "OCaml", "Haskell", "Scala"]
    1.16 +  #> Numeral.add_code @{const_name number_int_inst.number_of_int}
    1.17 +    true true (fn s => (Pretty.block o map Code_Printer.str) ["BigInt", s]) "Scala"
    1.18  *}
    1.19  
    1.20  code_const "Int.Pls" and "Int.Min" and "Int.Bit0" and "Int.Bit1"
    1.21 @@ -40,63 +43,80 @@
    1.22       and "error/ \"Min\""
    1.23       and "error/ \"Bit0\""
    1.24       and "error/ \"Bit1\"")
    1.25 +  (Scala "!error(\"Pls\")"
    1.26 +     and "!error(\"Min\")"
    1.27 +     and "!error(\"Bit0\")"
    1.28 +     and "!error(\"Bit1\")")
    1.29 +
    1.30  
    1.31  code_const Int.pred
    1.32    (SML "IntInf.- ((_), 1)")
    1.33    (OCaml "Big'_int.pred'_big'_int")
    1.34    (Haskell "!(_/ -/ 1)")
    1.35 +  (Scala "!(_/ -/ 1)")
    1.36  
    1.37  code_const Int.succ
    1.38    (SML "IntInf.+ ((_), 1)")
    1.39    (OCaml "Big'_int.succ'_big'_int")
    1.40    (Haskell "!(_/ +/ 1)")
    1.41 +  (Scala "!(_/ +/ 1)")
    1.42  
    1.43  code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    1.44    (SML "IntInf.+ ((_), (_))")
    1.45    (OCaml "Big'_int.add'_big'_int")
    1.46    (Haskell infixl 6 "+")
    1.47 +  (Scala infixl 7 "+")
    1.48  
    1.49  code_const "uminus \<Colon> int \<Rightarrow> int"
    1.50    (SML "IntInf.~")
    1.51    (OCaml "Big'_int.minus'_big'_int")
    1.52    (Haskell "negate")
    1.53 +  (Scala "!(- _)")
    1.54  
    1.55  code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    1.56    (SML "IntInf.- ((_), (_))")
    1.57    (OCaml "Big'_int.sub'_big'_int")
    1.58    (Haskell infixl 6 "-")
    1.59 +  (Scala infixl 7 "-")
    1.60  
    1.61  code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
    1.62    (SML "IntInf.* ((_), (_))")
    1.63    (OCaml "Big'_int.mult'_big'_int")
    1.64    (Haskell infixl 7 "*")
    1.65 +  (Scala infixl 8 "*")
    1.66  
    1.67  code_const pdivmod
    1.68 -  (SML "(fn k => fn l =>/ IntInf.divMod/ (IntInf.abs k,/ IntInf.abs l))")
    1.69 -  (OCaml "(fun k -> fun l ->/ Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int k)/ (Big'_int.abs'_big'_int l))")
    1.70 -  (Haskell "(\\k l ->/ divMod/ (abs k)/ (abs l))")
    1.71 +  (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
    1.72 +  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.73 +  (Haskell "divMod/ (abs _)/ (abs _))")
    1.74 +  (Scala "!(_.abs '/% _.abs)")
    1.75  
    1.76  code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.77    (SML "!((_ : IntInf.int) = _)")
    1.78    (OCaml "Big'_int.eq'_big'_int")
    1.79    (Haskell infixl 4 "==")
    1.80 +  (Scala infixl 5 "==")
    1.81  
    1.82  code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.83    (SML "IntInf.<= ((_), (_))")
    1.84    (OCaml "Big'_int.le'_big'_int")
    1.85    (Haskell infix 4 "<=")
    1.86 +  (Scala infixl 4 "<=")
    1.87  
    1.88  code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.89    (SML "IntInf.< ((_), (_))")
    1.90    (OCaml "Big'_int.lt'_big'_int")
    1.91    (Haskell infix 4 "<")
    1.92 +  (Scala infixl 4 "<=")
    1.93  
    1.94  code_const Code_Numeral.int_of
    1.95    (SML "IntInf.fromInt")
    1.96    (OCaml "_")
    1.97    (Haskell "toEnum")
    1.98 +  (Scala "!BigInt(_)")
    1.99  
   1.100  code_reserved SML IntInf
   1.101 +code_reserved Scala BigInt
   1.102  
   1.103  text {* Evaluation *}
   1.104