fixed and tuned
authorhaftmann
Fri Jan 25 14:54:46 2008 +0100 (2008-01-25)
changeset 25967dd602eb20f3f
parent 25966 74f6817870f9
child 25968 66cfe1d00be0
fixed and tuned
src/HOL/Library/Code_Index.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Tools/numeral.ML
     1.1 --- a/src/HOL/Library/Code_Index.thy	Fri Jan 25 14:54:44 2008 +0100
     1.2 +++ b/src/HOL/Library/Code_Index.thy	Fri Jan 25 14:54:46 2008 +0100
     1.3 @@ -17,6 +17,10 @@
     1.4  
     1.5  datatype index = index_of_nat nat
     1.6  
     1.7 +lemma [code func]:
     1.8 +  "index_size k = 0"
     1.9 +  by (cases k) simp
    1.10 +
    1.11  lemmas [code func del] = index.recs index.cases
    1.12  
    1.13  primrec
    1.14 @@ -76,6 +80,8 @@
    1.15  lemma zero_index_code [code inline, code func]:
    1.16    "(0\<Colon>index) = Numeral0"
    1.17    by (simp add: number_of_index_def Pls_def)
    1.18 +lemma [code post]: "Numeral0 = (0\<Colon>index)"
    1.19 +  using zero_index_code ..
    1.20  
    1.21  definition [simp, code func del]:
    1.22    "(1\<Colon>index) = index_of_nat 1"
    1.23 @@ -83,6 +89,8 @@
    1.24  lemma one_index_code [code inline, code func]:
    1.25    "(1\<Colon>index) = Numeral1"
    1.26    by (simp add: number_of_index_def Pls_def Bit_def)
    1.27 +lemma [code post]: "Numeral1 = (1\<Colon>index)"
    1.28 +  using one_index_code ..
    1.29  
    1.30  definition [simp, code func del]:
    1.31    "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
    1.32 @@ -179,7 +187,7 @@
    1.33  code_type index
    1.34    (SML "int")
    1.35    (OCaml "int")
    1.36 -  (Haskell "Integer")
    1.37 +  (Haskell "Int")
    1.38  
    1.39  code_instance index :: eq
    1.40    (Haskell -)
    1.41 @@ -194,7 +202,7 @@
    1.42  
    1.43  code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.44    (SML "Int.+/ ((_),/ (_))")
    1.45 -  (OCaml "Pervasives.(+)")
    1.46 +  (OCaml "Pervasives.( + )")
    1.47    (Haskell infixl 6 "+")
    1.48  
    1.49  code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.50 @@ -204,12 +212,12 @@
    1.51  
    1.52  code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.53    (SML "Int.*/ ((_),/ (_))")
    1.54 -  (OCaml "Pervasives.(*)")
    1.55 +  (OCaml "Pervasives.( * )")
    1.56    (Haskell infixl 7 "*")
    1.57  
    1.58  code_const "op div \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.59    (SML "Int.div/ ((_),/ (_))")
    1.60 -  (OCaml "Pervasives.(/)")
    1.61 +  (OCaml "Pervasives.( / )")
    1.62    (Haskell "div")
    1.63  
    1.64  code_const "op mod \<Colon> index \<Rightarrow> index \<Rightarrow> index"
    1.65 @@ -219,17 +227,17 @@
    1.66  
    1.67  code_const "op = \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
    1.68    (SML "!((_ : Int.int) = _)")
    1.69 -  (OCaml "!((_ : Pervasives.int) = _)")
    1.70 +  (OCaml "!((_ : int) = _)")
    1.71    (Haskell infixl 4 "==")
    1.72  
    1.73  code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
    1.74    (SML "Int.<=/ ((_),/ (_))")
    1.75 -  (OCaml "!((_ : Pervasives.int) <= _)")
    1.76 +  (OCaml "!((_ : int) <= _)")
    1.77    (Haskell infix 4 "<=")
    1.78  
    1.79  code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
    1.80    (SML "Int.</ ((_),/ (_))")
    1.81 -  (OCaml "!((_ : Pervasives.int) < _)")
    1.82 +  (OCaml "!((_ : int) < _)")
    1.83    (Haskell infix 4 "<")
    1.84  
    1.85  end
     2.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Jan 25 14:54:44 2008 +0100
     2.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Jan 25 14:54:46 2008 +0100
     2.3 @@ -207,11 +207,14 @@
     2.4      then remove_suc_clause thy ths else ths
     2.5    end;
     2.6  
     2.7 -fun lift_obj_eq f thy =
     2.8 -  map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
     2.9 -  #> f thy
    2.10 -  #> map (fn thm => thm RS @{thm eq_reflection})
    2.11 -  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
    2.12 +fun lift_obj_eq f thy thms =
    2.13 +  thms
    2.14 +  |> try (
    2.15 +    map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
    2.16 +    #> f thy
    2.17 +    #> map (fn thm => thm RS @{thm eq_reflection})
    2.18 +    #> map (Conv.fconv_rule Drule.beta_eta_conversion))
    2.19 +  |> the_default thms
    2.20  *}
    2.21  
    2.22  setup {*
    2.23 @@ -222,18 +225,16 @@
    2.24  *}
    2.25  (*>*)
    2.26  
    2.27 -
    2.28  subsection {* Target language setup *}
    2.29  
    2.30  text {*
    2.31 -  We map @{typ nat} to target language integers, where we
    2.32 +  For ML, we map @{typ nat} to target language integers, where we
    2.33    assert that values are always non-negative.
    2.34  *}
    2.35  
    2.36  code_type nat
    2.37    (SML "int")
    2.38    (OCaml "Big'_int.big'_int")
    2.39 -  (Haskell "Integer")
    2.40  
    2.41  types_code
    2.42    nat ("int")
    2.43 @@ -247,22 +248,70 @@
    2.44  *}
    2.45  
    2.46  text {*
    2.47 +  For Haskell we define our own @{typ nat} type.  The reason
    2.48 +  is that we have to distinguish type class instances
    2.49 +  for @{typ nat} and @{typ int}.
    2.50 +*}
    2.51 +
    2.52 +code_include Haskell "Nat" {*
    2.53 +newtype Nat = Nat Integer deriving (Show, Eq);
    2.54 +
    2.55 +instance Num Nat where {
    2.56 +  fromInteger k = Nat (if k >= 0 then k else 0);
    2.57 +  Nat n + Nat m = Nat (n + m);
    2.58 +  Nat n - Nat m = fromInteger (n - m);
    2.59 +  Nat n * Nat m = Nat (n * m);
    2.60 +  abs n = n;
    2.61 +  signum _ = 1;
    2.62 +  negate n = error "negate Nat";
    2.63 +};
    2.64 +
    2.65 +instance Ord Nat where {
    2.66 +  Nat n <= Nat m = n <= m;
    2.67 +  Nat n < Nat m = n < m;
    2.68 +};
    2.69 +
    2.70 +instance Real Nat where {
    2.71 +  toRational (Nat n) = toRational n;
    2.72 +};
    2.73 +
    2.74 +instance Enum Nat where {
    2.75 +  toEnum k = fromInteger (toEnum k);
    2.76 +  fromEnum (Nat n) = fromEnum n;
    2.77 +};
    2.78 +
    2.79 +instance Integral Nat where {
    2.80 +  toInteger (Nat n) = n;
    2.81 +  divMod n m = quotRem n m;
    2.82 +  quotRem (Nat n) (Nat m) = (Nat k, Nat l) where (k, l) = quotRem n m;
    2.83 +};
    2.84 +*}
    2.85 +
    2.86 +code_reserved Haskell Nat
    2.87 +
    2.88 +code_type nat
    2.89 +  (Haskell "Nat")
    2.90 +
    2.91 +code_instance nat :: eq
    2.92 +  (Haskell -)
    2.93 +
    2.94 +text {*
    2.95    Natural numerals.
    2.96  *}
    2.97  
    2.98 -lemma [code inline]:
    2.99 +lemma [code inline, symmetric, code post]:
   2.100    "nat (number_of i) = number_nat_inst.number_of_nat i"
   2.101    -- {* this interacts as desired with @{thm nat_number_of_def} *}
   2.102    by (simp add: number_nat_inst.number_of_nat)
   2.103  
   2.104  setup {*
   2.105    fold (Numeral.add_code @{const_name number_nat_inst.number_of_nat}
   2.106 -    false false) ["SML", "OCaml", "Haskell"]
   2.107 +    true false) ["SML", "OCaml", "Haskell"]
   2.108  *}
   2.109  
   2.110  text {*
   2.111    Since natural numbers are implemented
   2.112 -  using integers, the coercion function @{const "of_nat"} of type
   2.113 +  using integers in ML, the coercion function @{const "of_nat"} of type
   2.114    @{typ "nat \<Rightarrow> int"} is simply implemented by the identity function.
   2.115    For the @{const "nat"} function for converting an integer to a natural
   2.116    number, we give a specific implementation using an ML function that
   2.117 @@ -285,16 +334,11 @@
   2.118  
   2.119  lemma of_nat_int [code unfold]:
   2.120    "of_nat = int" by (simp add: int_def)
   2.121 +declare of_nat_int [symmetric, code post]
   2.122  
   2.123  code_const int
   2.124    (SML "_")
   2.125    (OCaml "_")
   2.126 -  (Haskell "_")
   2.127 -
   2.128 -code_const nat
   2.129 -  (SML "IntInf.max/ (/0,/ _)")
   2.130 -  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
   2.131 -  (Haskell "max 0")
   2.132  
   2.133  consts_code
   2.134    int ("(_)")
   2.135 @@ -303,19 +347,26 @@
   2.136  fun nat i = if i < 0 then 0 else i;
   2.137  *}
   2.138  
   2.139 +code_const nat
   2.140 +  (SML "IntInf.max/ (/0,/ _)")
   2.141 +  (OCaml "Big'_int.max'_big'_int/ Big'_int.zero'_big'_int")
   2.142 +
   2.143 +text {* For Haskell, things are slightly different again. *}
   2.144 +
   2.145 +code_const int and nat
   2.146 +  (Haskell "toInteger" and "fromInteger")
   2.147  
   2.148  text {* Conversion from and to indices. *}
   2.149  
   2.150 +code_const index_of_nat
   2.151 +  (SML "IntInf.toInt")
   2.152 +  (OCaml "Big'_int.int'_of'_big'_int")
   2.153 +  (Haskell "toEnum")
   2.154 +
   2.155  code_const nat_of_index
   2.156    (SML "IntInf.fromInt")
   2.157    (OCaml "Big'_int.big'_int'_of'_int")
   2.158 -  (Haskell "toInteger")
   2.159 -
   2.160 -code_const index_of_nat
   2.161 -  (SML "IntInf.toInt")
   2.162 -  (OCaml "Big'_int.int'_of'_big'_int")
   2.163 -  (Haskell "fromInteger")
   2.164 -
   2.165 +  (Haskell "fromEnum")
   2.166  
   2.167  text {* Using target language arithmetic operations whenever appropriate *}
   2.168  
     3.1 --- a/src/HOL/Tools/numeral.ML	Fri Jan 25 14:54:44 2008 +0100
     3.2 +++ b/src/HOL/Tools/numeral.ML	Fri Jan 25 14:54:46 2008 +0100
     3.3 @@ -56,7 +56,7 @@
     3.4  (* code generator *)
     3.5  
     3.6  fun add_code number_of negative unbounded target =
     3.7 -  CodeTarget.add_pretty_numeral target unbounded negative number_of
     3.8 +  CodeTarget.add_pretty_numeral target negative unbounded number_of
     3.9    @{const_name Int.B0} @{const_name Int.B1}
    3.10    @{const_name Int.Pls} @{const_name Int.Min}
    3.11    @{const_name Int.Bit};