src/HOL/Code_Numeral.thy
changeset 34886 873c31d9f10d
parent 33340 a165b97f3658
child 34898 62d70417f8ce
     1.1 --- a/src/HOL/Code_Numeral.thy	Tue Jan 12 13:36:01 2010 +0100
     1.2 +++ b/src/HOL/Code_Numeral.thy	Wed Jan 13 08:56:15 2010 +0100
     1.3 @@ -289,33 +289,38 @@
     1.4    (SML "int")
     1.5    (OCaml "Big'_int.big'_int")
     1.6    (Haskell "Int")
     1.7 +  (Scala "Int")
     1.8  
     1.9  code_instance code_numeral :: eq
    1.10    (Haskell -)
    1.11  
    1.12  setup {*
    1.13    fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
    1.14 -    false false) ["SML", "Haskell"]
    1.15 +    false false) ["SML", "Haskell", "Scala"]
    1.16    #> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
    1.17  *}
    1.18  
    1.19  code_reserved SML Int int
    1.20  code_reserved OCaml Big_int
    1.21 +code_reserved Scala Int
    1.22  
    1.23  code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.24    (SML "Int.+/ ((_),/ (_))")
    1.25    (OCaml "Big'_int.add'_big'_int")
    1.26    (Haskell infixl 6 "+")
    1.27 +  (Scala infixl 7 "+")
    1.28  
    1.29  code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.30    (SML "Int.max/ (_/ -/ _,/ 0 : int)")
    1.31    (OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
    1.32    (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
    1.33 +  (Scala "!(_/ -/ _).max(0)")
    1.34  
    1.35  code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
    1.36    (SML "Int.*/ ((_),/ (_))")
    1.37    (OCaml "Big'_int.mult'_big'_int")
    1.38    (Haskell infixl 7 "*")
    1.39 +  (Scala infixl 8 "*")
    1.40  
    1.41  code_const div_mod_code_numeral
    1.42    (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
    1.43 @@ -326,15 +331,18 @@
    1.44    (SML "!((_ : Int.int) = _)")
    1.45    (OCaml "Big'_int.eq'_big'_int")
    1.46    (Haskell infixl 4 "==")
    1.47 +  (Scala infixl 5 "==")
    1.48  
    1.49  code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.50    (SML "Int.<=/ ((_),/ (_))")
    1.51    (OCaml "Big'_int.le'_big'_int")
    1.52    (Haskell infix 4 "<=")
    1.53 +  (Scala infix 4 "<=")
    1.54  
    1.55  code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.56    (SML "Int.</ ((_),/ (_))")
    1.57    (OCaml "Big'_int.lt'_big'_int")
    1.58    (Haskell infix 4 "<")
    1.59 +  (Scala infix 4 "<")
    1.60  
    1.61  end