src/HOL/Code_Numeral.thy
changeset 52435 6646bb548c6b
parent 51375 d9e62d9c98de
child 53069 d165213e3924
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -519,21 +519,22 @@
     1.4  
     1.5  code_reserved Eval int Integer abs
     1.6  
     1.7 -code_type integer
     1.8 -  (SML "IntInf.int")
     1.9 -  (OCaml "Big'_int.big'_int")
    1.10 -  (Haskell "Integer")
    1.11 -  (Scala "BigInt")
    1.12 -  (Eval "int")
    1.13 +code_printing
    1.14 +  type_constructor integer \<rightharpoonup>
    1.15 +    (SML) "IntInf.int"
    1.16 +    and (OCaml) "Big'_int.big'_int"
    1.17 +    and (Haskell) "Integer"
    1.18 +    and (Scala) "BigInt"
    1.19 +    and (Eval) "int"
    1.20 +| class_instance integer :: equal \<rightharpoonup>
    1.21 +    (Haskell) -
    1.22  
    1.23 -code_instance integer :: equal
    1.24 -  (Haskell -)
    1.25 -
    1.26 -code_const "0::integer"
    1.27 -  (SML "0")
    1.28 -  (OCaml "Big'_int.zero'_big'_int")
    1.29 -  (Haskell "0")
    1.30 -  (Scala "BigInt(0)")
    1.31 +code_printing
    1.32 +  constant "0::integer" \<rightharpoonup>
    1.33 +    (SML) "0"
    1.34 +    and (OCaml) "Big'_int.zero'_big'_int"
    1.35 +    and (Haskell) "0"
    1.36 +    and (Scala) "BigInt(0)"
    1.37  
    1.38  setup {*
    1.39    fold (Numeral.add_code @{const_name Code_Numeral.Pos}
    1.40 @@ -545,83 +546,69 @@
    1.41      true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    1.42  *}
    1.43  
    1.44 -code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _"
    1.45 -  (SML "IntInf.+ ((_), (_))")
    1.46 -  (OCaml "Big'_int.add'_big'_int")
    1.47 -  (Haskell infixl 6 "+")
    1.48 -  (Scala infixl 7 "+")
    1.49 -  (Eval infixl 8 "+")
    1.50 -
    1.51 -code_const "uminus :: integer \<Rightarrow> _"
    1.52 -  (SML "IntInf.~")
    1.53 -  (OCaml "Big'_int.minus'_big'_int")
    1.54 -  (Haskell "negate")
    1.55 -  (Scala "!(- _)")
    1.56 -  (Eval "~/ _")
    1.57 -
    1.58 -code_const "minus :: integer \<Rightarrow> _"
    1.59 -  (SML "IntInf.- ((_), (_))")
    1.60 -  (OCaml "Big'_int.sub'_big'_int")
    1.61 -  (Haskell infixl 6 "-")
    1.62 -  (Scala infixl 7 "-")
    1.63 -  (Eval infixl 8 "-")
    1.64 -
    1.65 -code_const Code_Numeral.dup
    1.66 -  (SML "IntInf.*/ (2,/ (_))")
    1.67 -  (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)")
    1.68 -  (Haskell "!(2 * _)")
    1.69 -  (Scala "!(2 * _)")
    1.70 -  (Eval "!(2 * _)")
    1.71 -
    1.72 -code_const Code_Numeral.sub
    1.73 -  (SML "!(raise/ Fail/ \"sub\")")
    1.74 -  (OCaml "failwith/ \"sub\"")
    1.75 -  (Haskell "error/ \"sub\"")
    1.76 -  (Scala "!sys.error(\"sub\")")
    1.77 +code_printing
    1.78 +  constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    1.79 +    (SML) "IntInf.+ ((_), (_))"
    1.80 +    and (OCaml) "Big'_int.add'_big'_int"
    1.81 +    and (Haskell) infixl 6 "+"
    1.82 +    and (Scala) infixl 7 "+"
    1.83 +    and (Eval) infixl 8 "+"
    1.84 +| constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
    1.85 +    (SML) "IntInf.~"
    1.86 +    and (OCaml) "Big'_int.minus'_big'_int"
    1.87 +    and (Haskell) "negate"
    1.88 +    and (Scala) "!(- _)"
    1.89 +    and (Eval) "~/ _"
    1.90 +| constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
    1.91 +    (SML) "IntInf.- ((_), (_))"
    1.92 +    and (OCaml) "Big'_int.sub'_big'_int"
    1.93 +    and (Haskell) infixl 6 "-"
    1.94 +    and (Scala) infixl 7 "-"
    1.95 +    and (Eval) infixl 8 "-"
    1.96 +| constant Code_Numeral.dup \<rightharpoonup>
    1.97 +    (SML) "IntInf.*/ (2,/ (_))"
    1.98 +    and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
    1.99 +    and (Haskell) "!(2 * _)"
   1.100 +    and (Scala) "!(2 * _)"
   1.101 +    and (Eval) "!(2 * _)"
   1.102 +| constant Code_Numeral.sub \<rightharpoonup>
   1.103 +    (SML) "!(raise/ Fail/ \"sub\")"
   1.104 +    and (OCaml) "failwith/ \"sub\""
   1.105 +    and (Haskell) "error/ \"sub\""
   1.106 +    and (Scala) "!sys.error(\"sub\")"
   1.107 +| constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   1.108 +    (SML) "IntInf.* ((_), (_))"
   1.109 +    and (OCaml) "Big'_int.mult'_big'_int"
   1.110 +    and (Haskell) infixl 7 "*"
   1.111 +    and (Scala) infixl 8 "*"
   1.112 +    and (Eval) infixl 9 "*"
   1.113 +| constant Code_Numeral.divmod_abs \<rightharpoonup>
   1.114 +    (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
   1.115 +    and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
   1.116 +    and (Haskell) "divMod/ (abs _)/ (abs _)"
   1.117 +    and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
   1.118 +    and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
   1.119 +| constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   1.120 +    (SML) "!((_ : IntInf.int) = _)"
   1.121 +    and (OCaml) "Big'_int.eq'_big'_int"
   1.122 +    and (Haskell) infix 4 "=="
   1.123 +    and (Scala) infixl 5 "=="
   1.124 +    and (Eval) infixl 6 "="
   1.125 +| constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   1.126 +    (SML) "IntInf.<= ((_), (_))"
   1.127 +    and (OCaml) "Big'_int.le'_big'_int"
   1.128 +    and (Haskell) infix 4 "<="
   1.129 +    and (Scala) infixl 4 "<="
   1.130 +    and (Eval) infixl 6 "<="
   1.131 +| constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   1.132 +    (SML) "IntInf.< ((_), (_))"
   1.133 +    and (OCaml) "Big'_int.lt'_big'_int"
   1.134 +    and (Haskell) infix 4 "<"
   1.135 +    and (Scala) infixl 4 "<"
   1.136 +    and (Eval) infixl 6 "<"
   1.137  
   1.138 -code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _"
   1.139 -  (SML "IntInf.* ((_), (_))")
   1.140 -  (OCaml "Big'_int.mult'_big'_int")
   1.141 -  (Haskell infixl 7 "*")
   1.142 -  (Scala infixl 8 "*")
   1.143 -  (Eval infixl 9 "*")
   1.144 -
   1.145 -code_const Code_Numeral.divmod_abs
   1.146 -  (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
   1.147 -  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   1.148 -  (Haskell "divMod/ (abs _)/ (abs _)")
   1.149 -  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   1.150 -  (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   1.151 -
   1.152 -code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool"
   1.153 -  (SML "!((_ : IntInf.int) = _)")
   1.154 -  (OCaml "Big'_int.eq'_big'_int")
   1.155 -  (Haskell infix 4 "==")
   1.156 -  (Scala infixl 5 "==")
   1.157 -  (Eval infixl 6 "=")
   1.158 -
   1.159 -code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool"
   1.160 -  (SML "IntInf.<= ((_), (_))")
   1.161 -  (OCaml "Big'_int.le'_big'_int")
   1.162 -  (Haskell infix 4 "<=")
   1.163 -  (Scala infixl 4 "<=")
   1.164 -  (Eval infixl 6 "<=")
   1.165 -
   1.166 -code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool"
   1.167 -  (SML "IntInf.< ((_), (_))")
   1.168 -  (OCaml "Big'_int.lt'_big'_int")
   1.169 -  (Haskell infix 4 "<")
   1.170 -  (Scala infixl 4 "<")
   1.171 -  (Eval infixl 6 "<")
   1.172 -
   1.173 -code_modulename SML
   1.174 -  Code_Numeral Arith
   1.175 -
   1.176 -code_modulename OCaml
   1.177 -  Code_Numeral Arith
   1.178 -
   1.179 -code_modulename Haskell
   1.180 -  Code_Numeral Arith
   1.181 +code_identifier
   1.182 +  code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   1.183  
   1.184  
   1.185  subsection {* Type of target language naturals *}