equal
deleted
inserted
replaced
|
1 (* Title: HOL/ex/Codegenerator_Pretty.thy |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Simple examples for pretty numerals and such *} |
|
7 |
|
8 theory Codegenerator_Pretty |
|
9 imports Executable_Rat Executable_Real Efficient_Nat |
|
10 begin |
|
11 |
|
12 definition |
|
13 foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where |
|
14 "foo r s t = (t + s) / t" |
|
15 |
|
16 definition |
|
17 bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where |
|
18 "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r" |
|
19 |
|
20 definition |
|
21 "R1 = Fract 3 7" |
|
22 |
|
23 definition |
|
24 "R2 = Fract (-7) 5" |
|
25 |
|
26 definition |
|
27 "R3 = Fract 11 (-9)" |
|
28 |
|
29 definition |
|
30 "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)" |
|
31 |
|
32 definition |
|
33 foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where |
|
34 "foo' r s t = (t + s) / t" |
|
35 |
|
36 definition |
|
37 bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where |
|
38 "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r" |
|
39 |
|
40 definition |
|
41 "R1' = real_of_rat (Fract 3 7)" |
|
42 |
|
43 definition |
|
44 "R2' = real_of_rat (Fract (-7) 5)" |
|
45 |
|
46 definition |
|
47 "R3' = real_of_rat (Fract 11 (-9))" |
|
48 |
|
49 definition |
|
50 "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')" |
|
51 |
|
52 code_gen foobar foobar' in SML to Foo |
|
53 in OCaml file - |
|
54 in Haskell file - |
|
55 ML {* (Foo.foobar, Foo.foobar') *} |
|
56 |
|
57 end |