131 |
131 |
132 instance by default (auto simp add: left_distrib index) |
132 instance by default (auto simp add: left_distrib index) |
133 |
133 |
134 end |
134 end |
135 |
135 |
|
136 lemma index_of_nat_code [code func]: |
|
137 "index_of_nat = of_nat" |
|
138 proof |
|
139 fix n :: nat |
|
140 have "of_nat n = index_of_nat n" |
|
141 by (induct n) simp_all |
|
142 then show "index_of_nat n = of_nat n" |
|
143 by (rule sym) |
|
144 qed |
|
145 |
|
146 lemma nat_of_index_code [code func]: |
|
147 "nat_of_index n = (if n = 0 then 0 else Suc (nat_of_index (n - 1)))" |
|
148 by (induct n) simp |
|
149 |
136 |
150 |
137 subsection {* ML interface *} |
151 subsection {* ML interface *} |
138 |
152 |
139 ML {* |
153 ML {* |
140 structure Index = |
154 structure Index = |
145 end; |
159 end; |
146 *} |
160 *} |
147 |
161 |
148 |
162 |
149 subsection {* Code serialization *} |
163 subsection {* Code serialization *} |
150 |
|
151 text {* Pecularity for operations with potentially negative result *} |
|
152 |
|
153 definition |
|
154 minus_index' :: "index \<Rightarrow> index \<Rightarrow> index" |
|
155 where |
|
156 [code func del]: "minus_index' = op -" |
|
157 |
|
158 lemma minus_index_code [code func]: |
|
159 "n - m = (let q = minus_index' n m |
|
160 in if q < 0 then 0 else q)" |
|
161 by (simp add: minus_index'_def Let_def) |
|
162 |
164 |
163 text {* Implementation of indices by bounded integers *} |
165 text {* Implementation of indices by bounded integers *} |
164 |
166 |
165 code_type index |
167 code_type index |
166 (SML "int") |
168 (SML "int") |
169 |
171 |
170 code_instance index :: eq |
172 code_instance index :: eq |
171 (Haskell -) |
173 (Haskell -) |
172 |
174 |
173 setup {* |
175 setup {* |
174 fold (fn target => CodeTarget.add_pretty_numeral target true |
176 fold (fn target => CodeTarget.add_pretty_numeral target false |
175 @{const_name number_index_inst.number_of_index} |
177 @{const_name number_index_inst.number_of_index} |
176 @{const_name Numeral.B0} @{const_name Numeral.B1} |
178 @{const_name Int.B0} @{const_name Int.B1} |
177 @{const_name Numeral.Pls} @{const_name Numeral.Min} |
179 @{const_name Int.Pls} @{const_name Int.Min} |
178 @{const_name Numeral.Bit} |
180 @{const_name Int.Bit} |
179 ) ["SML", "OCaml", "Haskell"] |
181 ) ["SML", "OCaml", "Haskell"] |
180 *} |
182 *} |
181 |
183 |
182 code_reserved SML int |
184 code_reserved SML Int int |
183 code_reserved OCaml int |
185 code_reserved OCaml Pervasives int |
184 |
186 |
185 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
187 code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
186 (SML "Int.+ ((_), (_))") |
188 (SML "Int.+ ((_), (_))") |
187 (OCaml "Pervasives.+") |
189 (OCaml "Pervasives.+") |
188 (Haskell infixl 6 "+") |
190 (Haskell infixl 6 "+") |
189 |
191 |
190 code_const "minus_index' \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
192 code_const "op - \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
191 (SML "Int.- ((_), (_))") |
193 (SML "Int.max/ (_/ -/ _,/ 0 : int)") |
192 (OCaml "Pervasives.-") |
194 (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ") |
193 (Haskell infixl 6 "-") |
195 (Haskell "max/ (_/ -/ _)/ (0 :: Int)") |
194 |
196 |
195 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
197 code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index" |
196 (SML "Int.* ((_), (_))") |
198 (SML "Int.* ((_), (_))") |
197 (OCaml "Pervasives.*") |
199 (OCaml "Pervasives.*") |
198 (Haskell infixl 7 "*") |
200 (Haskell infixl 7 "*") |