src/HOL/Code_Numeral.thy
changeset 37958 9728342bcd56
parent 37947 844977c7abeb
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Code_Numeral.thy	Fri Jul 23 18:42:46 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sat Jul 24 18:08:41 2010 +0200
     1.3 @@ -123,7 +123,7 @@
     1.4    by (rule HOL.eq_refl)
     1.5  
     1.6  
     1.7 -subsection {* Indices as datatype of ints *}
     1.8 +subsection {* Code numerals as datatype of ints *}
     1.9  
    1.10  instantiation code_numeral :: number
    1.11  begin
    1.12 @@ -293,67 +293,74 @@
    1.13  
    1.14  subsection {* Code generator setup *}
    1.15  
    1.16 -text {* Implementation of indices by bounded integers *}
    1.17 +text {* Implementation of code numerals by bounded integers *}
    1.18  
    1.19  code_type code_numeral
    1.20    (SML "int")
    1.21    (OCaml "Big'_int.big'_int")
    1.22    (Haskell "Integer")
    1.23 -  (Scala "Int")
    1.24 +  (Scala "BigInt")
    1.25  
    1.26  code_instance code_numeral :: eq
    1.27    (Haskell -)
    1.28  
    1.29  setup {*
    1.30 -  fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.31 -    false Code_Printer.literal_naive_numeral) ["SML", "Scala"]
    1.32 +  Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.33 +    false Code_Printer.literal_naive_numeral "SML"
    1.34    #> fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.35 -    false Code_Printer.literal_numeral) ["OCaml", "Haskell"]
    1.36 +    false Code_Printer.literal_numeral) ["OCaml", "Haskell", "Scala"]
    1.37  *}
    1.38  
    1.39  code_reserved SML Int int
    1.40 -code_reserved Scala Int
    1.41 +code_reserved Eval Integer
    1.42  
    1.43  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.44    (SML "Int.+/ ((_),/ (_))")
    1.45    (OCaml "Big'_int.add'_big'_int")
    1.46    (Haskell infixl 6 "+")
    1.47    (Scala infixl 7 "+")
    1.48 +  (Eval infixl 8 "+")
    1.49  
    1.50  code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.51    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.52    (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
    1.53    (Haskell "max/ (_/ -/ _)/ (0 :: Integer)")
    1.54    (Scala "!(_/ -/ _).max(0)")
    1.55 +  (Eval "Integer.max/ (_/ -/ _)/ 0")
    1.56  
    1.57  code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.58    (SML "Int.*/ ((_),/ (_))")
    1.59    (OCaml "Big'_int.mult'_big'_int")
    1.60    (Haskell infixl 7 "*")
    1.61    (Scala infixl 8 "*")
    1.62 +  (Eval infixl 8 "*")
    1.63  
    1.64  code_const div_mod_code_numeral
    1.65 -  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.66 +  (SML "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (Int.div (n, m), Int.mod (n, m)))")
    1.67    (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
    1.68    (Haskell "divMod")
    1.69 -  (Scala "!((n: Int) => (m: Int) =>/ if (m == 0)/ (0, n) else/ (n '/ m, n % m))")
    1.70 +  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
    1.71 +  (Eval "!(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.72  
    1.73  code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.74    (SML "!((_ : Int.int) = _)")
    1.75    (OCaml "Big'_int.eq'_big'_int")
    1.76    (Haskell infixl 4 "==")
    1.77    (Scala infixl 5 "==")
    1.78 +  (Eval "!((_ : int) = _)")
    1.79  
    1.80  code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.81    (SML "Int.<=/ ((_),/ (_))")
    1.82    (OCaml "Big'_int.le'_big'_int")
    1.83    (Haskell infix 4 "<=")
    1.84    (Scala infixl 4 "<=")
    1.85 +  (Eval infixl 6 "<=")
    1.86  
    1.87  code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.88    (SML "Int.</ ((_),/ (_))")
    1.89    (OCaml "Big'_int.lt'_big'_int")
    1.90    (Haskell infix 4 "<")
    1.91    (Scala infixl 4 "<")
    1.92 +  (Eval infixl 6 "<")
    1.93  
    1.94  end