some syntax setup for Scala
authorhaftmann
Wed Jan 13 08:56:15 2010 +0100 (2010-01-13)
changeset 34886873c31d9f10d
parent 34878 d7786f56f081
child 34887 31209fb24176
some syntax setup for Scala
src/HOL/Code_Numeral.thy
src/HOL/HOL.thy
src/HOL/List.thy
src/HOL/Option.thy
src/HOL/Product_Type.thy
src/HOL/String.thy
     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
     2.1 --- a/src/HOL/HOL.thy	Tue Jan 12 13:36:01 2010 +0100
     2.2 +++ b/src/HOL/HOL.thy	Wed Jan 13 08:56:15 2010 +0100
     2.3 @@ -1954,6 +1954,7 @@
     2.4    (SML "!(raise/ Fail/ \"undefined\")")
     2.5    (OCaml "failwith/ \"undefined\"")
     2.6    (Haskell "error/ \"undefined\"")
     2.7 +  (Scala "!error(\"undefined\")")
     2.8  
     2.9  subsubsection {* Evaluation and normalization by evaluation *}
    2.10  
     3.1 --- a/src/HOL/List.thy	Tue Jan 12 13:36:01 2010 +0100
     3.2 +++ b/src/HOL/List.thy	Wed Jan 13 08:56:15 2010 +0100
     3.3 @@ -3890,12 +3890,14 @@
     3.4  code_type list
     3.5    (SML "_ list")
     3.6    (OCaml "_ list")
     3.7 -  (Haskell "![_]")
     3.8 +  (Haskell "![(_)]")
     3.9 +  (Scala "List[(_)]")
    3.10  
    3.11  code_const Nil
    3.12    (SML "[]")
    3.13    (OCaml "[]")
    3.14    (Haskell "[]")
    3.15 +  (Scala "Nil")
    3.16  
    3.17  code_instance list :: eq
    3.18    (Haskell -)
    3.19 @@ -3938,7 +3940,7 @@
    3.20          (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
    3.21      in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
    3.22  in
    3.23 -  fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
    3.24 +  fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
    3.25    #> Codegen.add_codegen "list_codegen" list_codegen
    3.26  end
    3.27  *}
     4.1 --- a/src/HOL/Option.thy	Tue Jan 12 13:36:01 2010 +0100
     4.2 +++ b/src/HOL/Option.thy	Wed Jan 13 08:56:15 2010 +0100
     4.3 @@ -115,11 +115,13 @@
     4.4    (SML "_ option")
     4.5    (OCaml "_ option")
     4.6    (Haskell "Maybe _")
     4.7 +  (Scala "!Option[(_)]")
     4.8  
     4.9  code_const None and Some
    4.10    (SML "NONE" and "SOME")
    4.11    (OCaml "None" and "Some _")
    4.12    (Haskell "Nothing" and "Just")
    4.13 +  (Scala "None" and "!Some((_))")
    4.14  
    4.15  code_instance option :: eq
    4.16    (Haskell -)
    4.17 @@ -133,4 +135,7 @@
    4.18  code_reserved OCaml
    4.19    option None Some
    4.20  
    4.21 +code_reserved Scala
    4.22 +  Option None Some
    4.23 +
    4.24  end
     5.1 --- a/src/HOL/Product_Type.thy	Tue Jan 12 13:36:01 2010 +0100
     5.2 +++ b/src/HOL/Product_Type.thy	Wed Jan 13 08:56:15 2010 +0100
     5.3 @@ -99,6 +99,7 @@
     5.4    (SML "unit")
     5.5    (OCaml "unit")
     5.6    (Haskell "()")
     5.7 +  (Scala "Unit")
     5.8  
     5.9  code_instance unit :: eq
    5.10    (Haskell -)
    5.11 @@ -110,6 +111,7 @@
    5.12    (SML "()")
    5.13    (OCaml "()")
    5.14    (Haskell "()")
    5.15 +  (Scala "()")
    5.16  
    5.17  code_reserved SML
    5.18    unit
    5.19 @@ -117,6 +119,9 @@
    5.20  code_reserved OCaml
    5.21    unit
    5.22  
    5.23 +code_reserved Scala
    5.24 +  Unit
    5.25 +
    5.26  
    5.27  subsection {* Pairs *}
    5.28  
    5.29 @@ -995,6 +1000,7 @@
    5.30    (SML infix 2 "*")
    5.31    (OCaml infix 2 "*")
    5.32    (Haskell "!((_),/ (_))")
    5.33 +  (Scala "!((_),/ (_))")
    5.34  
    5.35  code_instance * :: eq
    5.36    (Haskell -)
    5.37 @@ -1006,6 +1012,7 @@
    5.38    (SML "!((_),/ (_))")
    5.39    (OCaml "!((_),/ (_))")
    5.40    (Haskell "!((_),/ (_))")
    5.41 +  (Scala "!((_),/ (_))")
    5.42  
    5.43  code_const fst and snd
    5.44    (Haskell "fst" and "snd")
     6.1 --- a/src/HOL/String.thy	Tue Jan 12 13:36:01 2010 +0100
     6.2 +++ b/src/HOL/String.thy	Wed Jan 13 08:56:15 2010 +0100
     6.3 @@ -170,14 +170,16 @@
     6.4  
     6.5  code_reserved SML string
     6.6  code_reserved OCaml string
     6.7 +code_reserved Scala string
     6.8  
     6.9  code_type literal
    6.10    (SML "string")
    6.11    (OCaml "string")
    6.12    (Haskell "String")
    6.13 +  (Scala "String")
    6.14  
    6.15  setup {*
    6.16 -  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
    6.17 +  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
    6.18  *}
    6.19  
    6.20  code_instance literal :: eq
    6.21 @@ -187,7 +189,7 @@
    6.22    (SML "!((_ : string) = _)")
    6.23    (OCaml "!((_ : string) = _)")
    6.24    (Haskell infixl 4 "==")
    6.25 -
    6.26 +  (Scala infixl 5 "==")
    6.27  
    6.28  types_code
    6.29    "char" ("string")