1 (* Title: HOL/Library/Code_Natural.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 theory Code_Natural |
|
6 imports "../Main" |
|
7 begin |
|
8 |
|
9 section {* Alternative representation of @{typ code_numeral} for @{text Haskell} and @{text Scala} *} |
|
10 |
|
11 code_include Haskell "Natural" |
|
12 {*import Data.Array.ST; |
|
13 |
|
14 newtype Natural = Natural Integer deriving (Eq, Show, Read); |
|
15 |
|
16 instance Num Natural where { |
|
17 fromInteger k = Natural (if k >= 0 then k else 0); |
|
18 Natural n + Natural m = Natural (n + m); |
|
19 Natural n - Natural m = fromInteger (n - m); |
|
20 Natural n * Natural m = Natural (n * m); |
|
21 abs n = n; |
|
22 signum _ = 1; |
|
23 negate n = error "negate Natural"; |
|
24 }; |
|
25 |
|
26 instance Ord Natural where { |
|
27 Natural n <= Natural m = n <= m; |
|
28 Natural n < Natural m = n < m; |
|
29 }; |
|
30 |
|
31 instance Ix Natural where { |
|
32 range (Natural n, Natural m) = map Natural (range (n, m)); |
|
33 index (Natural n, Natural m) (Natural q) = index (n, m) q; |
|
34 inRange (Natural n, Natural m) (Natural q) = inRange (n, m) q; |
|
35 rangeSize (Natural n, Natural m) = rangeSize (n, m); |
|
36 }; |
|
37 |
|
38 instance Real Natural where { |
|
39 toRational (Natural n) = toRational n; |
|
40 }; |
|
41 |
|
42 instance Enum Natural where { |
|
43 toEnum k = fromInteger (toEnum k); |
|
44 fromEnum (Natural n) = fromEnum n; |
|
45 }; |
|
46 |
|
47 instance Integral Natural where { |
|
48 toInteger (Natural n) = n; |
|
49 divMod n m = quotRem n m; |
|
50 quotRem (Natural n) (Natural m) |
|
51 | (m == 0) = (0, Natural n) |
|
52 | otherwise = (Natural k, Natural l) where (k, l) = quotRem n m; |
|
53 };*} |
|
54 |
|
55 |
|
56 code_reserved Haskell Natural |
|
57 |
|
58 code_include Scala "Natural" |
|
59 {*object Natural { |
|
60 |
|
61 def apply(numeral: BigInt): Natural = new Natural(numeral max 0) |
|
62 def apply(numeral: Int): Natural = Natural(BigInt(numeral)) |
|
63 def apply(numeral: String): Natural = Natural(BigInt(numeral)) |
|
64 |
|
65 } |
|
66 |
|
67 class Natural private(private val value: BigInt) { |
|
68 |
|
69 override def hashCode(): Int = this.value.hashCode() |
|
70 |
|
71 override def equals(that: Any): Boolean = that match { |
|
72 case that: Natural => this equals that |
|
73 case _ => false |
|
74 } |
|
75 |
|
76 override def toString(): String = this.value.toString |
|
77 |
|
78 def equals(that: Natural): Boolean = this.value == that.value |
|
79 |
|
80 def as_BigInt: BigInt = this.value |
|
81 def as_Int: Int = if (this.value >= scala.Int.MinValue && this.value <= scala.Int.MaxValue) |
|
82 this.value.intValue |
|
83 else error("Int value out of range: " + this.value.toString) |
|
84 |
|
85 def +(that: Natural): Natural = new Natural(this.value + that.value) |
|
86 def -(that: Natural): Natural = Natural(this.value - that.value) |
|
87 def *(that: Natural): Natural = new Natural(this.value * that.value) |
|
88 |
|
89 def /%(that: Natural): (Natural, Natural) = if (that.value == 0) (new Natural(0), this) |
|
90 else { |
|
91 val (k, l) = this.value /% that.value |
|
92 (new Natural(k), new Natural(l)) |
|
93 } |
|
94 |
|
95 def <=(that: Natural): Boolean = this.value <= that.value |
|
96 |
|
97 def <(that: Natural): Boolean = this.value < that.value |
|
98 |
|
99 } |
|
100 *} |
|
101 |
|
102 code_reserved Scala Natural |
|
103 |
|
104 code_type code_numeral |
|
105 (Haskell "Natural.Natural") |
|
106 (Scala "Natural") |
|
107 |
|
108 setup {* |
|
109 fold (Numeral.add_code @{const_name Code_Numeral.Num} |
|
110 false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"] |
|
111 *} |
|
112 |
|
113 code_instance code_numeral :: equal |
|
114 (Haskell -) |
|
115 |
|
116 code_const "0::code_numeral" |
|
117 (Haskell "0") |
|
118 (Scala "Natural(0)") |
|
119 |
|
120 code_const "plus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
|
121 (Haskell infixl 6 "+") |
|
122 (Scala infixl 7 "+") |
|
123 |
|
124 code_const "minus \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
|
125 (Haskell infixl 6 "-") |
|
126 (Scala infixl 7 "-") |
|
127 |
|
128 code_const "times \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" |
|
129 (Haskell infixl 7 "*") |
|
130 (Scala infixl 8 "*") |
|
131 |
|
132 code_const Code_Numeral.div_mod |
|
133 (Haskell "divMod") |
|
134 (Scala infixl 8 "/%") |
|
135 |
|
136 code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" |
|
137 (Haskell infix 4 "==") |
|
138 (Scala infixl 5 "==") |
|
139 |
|
140 code_const "less_eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" |
|
141 (Haskell infix 4 "<=") |
|
142 (Scala infixl 4 "<=") |
|
143 |
|
144 code_const "less \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool" |
|
145 (Haskell infix 4 "<") |
|
146 (Scala infixl 4 "<") |
|
147 |
|
148 end |
|