author | haftmann |
Wed, 03 Dec 2008 15:58:44 +0100 | |
changeset 28952 | 15a4b2cf8c34 |
parent 28227 | 77221ee0f7b9 |
child 30021 | 19c06d4763e0 |
permissions | -rw-r--r-- |
23268 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Small examples for evaluation mechanisms *} |
|
6 |
||
7 |
theory Eval_Examples |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28227
diff
changeset
|
8 |
imports Code_Eval Rational |
23268 | 9 |
begin |
10 |
||
25099 | 11 |
text {* evaluation oracle *} |
12 |
||
13 |
lemma "True \<or> False" by eval |
|
14 |
lemma "\<not> (Suc 0 = Suc 1)" by eval |
|
15 |
lemma "[] = ([]\<Colon> int list)" by eval |
|
16 |
lemma "[()] = [()]" by eval |
|
17 |
lemma "fst ([]::nat list, Suc 0) = []" by eval |
|
18 |
||
24292 | 19 |
text {* SML evaluation oracle *} |
20 |
||
21 |
lemma "True \<or> False" by evaluation |
|
22 |
lemma "\<not> (Suc 0 = Suc 1)" by evaluation |
|
23 |
lemma "[] = ([]\<Colon> int list)" by evaluation |
|
24 |
lemma "[()] = [()]" by evaluation |
|
25 |
lemma "fst ([]::nat list, Suc 0) = []" by evaluation |
|
26 |
||
25099 | 27 |
text {* normalization *} |
23268 | 28 |
|
25099 | 29 |
lemma "True \<or> False" by normalization |
30 |
lemma "\<not> (Suc 0 = Suc 1)" by normalization |
|
31 |
lemma "[] = ([]\<Colon> int list)" by normalization |
|
32 |
lemma "[()] = [()]" by normalization |
|
33 |
lemma "fst ([]::nat list, Suc 0) = []" by normalization |
|
23268 | 34 |
|
35 |
text {* term evaluation *} |
|
36 |
||
24587 | 37 |
value "(Suc 2 + 1) * 4" |
28227 | 38 |
value [code] "(Suc 2 + 1) * 4" |
39 |
value [SML] "(Suc 2 + 1) * 4" |
|
40 |
value [nbe] "(Suc 2 + 1) * 4" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
41 |
|
24587 | 42 |
value "(Suc 2 + Suc 0) * Suc 3" |
28227 | 43 |
value [code] "(Suc 2 + Suc 0) * Suc 3" |
44 |
value [SML] "(Suc 2 + Suc 0) * Suc 3" |
|
45 |
value [nbe] "(Suc 2 + Suc 0) * Suc 3" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
46 |
|
24587 | 47 |
value "nat 100" |
28227 | 48 |
value [code] "nat 100" |
49 |
value [SML] "nat 100" |
|
50 |
value [nbe] "nat 100" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
51 |
|
24587 | 52 |
value "(10\<Colon>int) \<le> 12" |
28227 | 53 |
value [code] "(10\<Colon>int) \<le> 12" |
54 |
value [SML] "(10\<Colon>int) \<le> 12" |
|
55 |
value [nbe] "(10\<Colon>int) \<le> 12" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
56 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
57 |
value "max (2::int) 4" |
28227 | 58 |
value [code] "max (2::int) 4" |
59 |
value [SML] "max (2::int) 4" |
|
60 |
value [nbe] "max (2::int) 4" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
61 |
|
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
62 |
value "of_int 2 / of_int 4 * (1::rat)" |
28227 | 63 |
value [code] "of_int 2 / of_int 4 * (1::rat)" |
64 |
value [SML] "of_int 2 / of_int 4 * (1::rat)" |
|
65 |
value [nbe] "of_int 2 / of_int 4 * (1::rat)" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
66 |
|
24587 | 67 |
value "[]::nat list" |
28227 | 68 |
value [code] "[]::nat list" |
69 |
value [SML] "[]::nat list" |
|
70 |
value [nbe] "[]::nat list" |
|
24835
8c26128f8997
clarified relationship of code generator conversions and evaluations
haftmann
parents:
24659
diff
changeset
|
71 |
|
24587 | 72 |
value "[(nat 100, ())]" |
28227 | 73 |
value [code] "[(nat 100, ())]" |
74 |
value [SML] "[(nat 100, ())]" |
|
75 |
value [nbe] "[(nat 100, ())]" |
|
24659 | 76 |
|
23268 | 77 |
|
78 |
text {* a fancy datatype *} |
|
79 |
||
80 |
datatype ('a, 'b) bair = |
|
81 |
Bair "'a\<Colon>order" 'b |
|
82 |
| Shift "('a, 'b) cair" |
|
83 |
| Dummy unit |
|
84 |
and ('a, 'b) cair = |
|
85 |
Cair 'a 'b |
|
86 |
||
24587 | 87 |
value "Shift (Cair (4::nat) [Suc 0])" |
28227 | 88 |
value [code] "Shift (Cair (4::nat) [Suc 0])" |
89 |
value [SML] "Shift (Cair (4::nat) [Suc 0])" |
|
90 |
value [nbe] "Shift (Cair (4::nat) [Suc 0])" |
|
23268 | 91 |
|
92 |
end |