haftmann@23250
|
1 |
structure HOL =
|
haftmann@23250
|
2 |
struct
|
haftmann@23250
|
3 |
|
haftmann@26513
|
4 |
type 'a eq = {eq : 'a -> 'a -> bool};
|
haftmann@26513
|
5 |
fun eq (A_:'a eq) = #eq A_;
|
haftmann@23250
|
6 |
|
haftmann@24193
|
7 |
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
|
haftmann@24193
|
8 |
fun less_eq (A_:'a ord) = #less_eq A_;
|
haftmann@24193
|
9 |
fun less (A_:'a ord) = #less A_;
|
haftmann@24193
|
10 |
|
haftmann@26513
|
11 |
fun eqop A_ a = eq A_ a;
|
haftmann@26513
|
12 |
|
haftmann@23250
|
13 |
end; (*struct HOL*)
|
haftmann@23250
|
14 |
|
haftmann@22490
|
15 |
structure Orderings =
|
haftmann@22490
|
16 |
struct
|
haftmann@22490
|
17 |
|
haftmann@28052
|
18 |
type 'a preorder = {Orderings__ord_preorder : 'a HOL.ord};
|
haftmann@28052
|
19 |
fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;
|
haftmann@28052
|
20 |
|
haftmann@28052
|
21 |
type 'a order = {Orderings__preorder_order : 'a preorder};
|
haftmann@28052
|
22 |
fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;
|
haftmann@22490
|
23 |
|
haftmann@24193
|
24 |
type 'a linorder = {Orderings__order_linorder : 'a order};
|
haftmann@24193
|
25 |
fun order_linorder (A_:'a linorder) = #Orderings__order_linorder A_;
|
haftmann@23250
|
26 |
|
haftmann@22490
|
27 |
end; (*struct Orderings*)
|
haftmann@22490
|
28 |
|
haftmann@22490
|
29 |
structure Nat =
|
haftmann@22490
|
30 |
struct
|
haftmann@22490
|
31 |
|
haftmann@24421
|
32 |
datatype nat = Suc of nat | Zero_nat;
|
haftmann@22490
|
33 |
|
haftmann@28143
|
34 |
fun eq_nat (Suc a) Zero_nat = false
|
haftmann@28143
|
35 |
| eq_nat Zero_nat (Suc a) = false
|
wenzelm@27190
|
36 |
| eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
|
haftmann@28143
|
37 |
| eq_nat Zero_nat Zero_nat = true;
|
haftmann@22490
|
38 |
|
haftmann@26513
|
39 |
val eq_nata = {eq = eq_nat} : nat HOL.eq;
|
haftmann@22490
|
40 |
|
wenzelm@26318
|
41 |
fun less_nat m (Suc n) = less_eq_nat m n
|
haftmann@22490
|
42 |
| less_nat n Zero_nat = false
|
wenzelm@26318
|
43 |
and less_eq_nat (Suc m) n = less_nat m n
|
wenzelm@26318
|
44 |
| less_eq_nat Zero_nat n = true;
|
haftmann@22490
|
45 |
|
haftmann@24193
|
46 |
val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat HOL.ord;
|
haftmann@22490
|
47 |
|
haftmann@28052
|
48 |
val preorder_nat = {Orderings__ord_preorder = ord_nat} :
|
haftmann@28052
|
49 |
nat Orderings.preorder;
|
haftmann@28052
|
50 |
|
haftmann@28052
|
51 |
val order_nat = {Orderings__preorder_order = preorder_nat} :
|
haftmann@28052
|
52 |
nat Orderings.order;
|
haftmann@23250
|
53 |
|
haftmann@24193
|
54 |
val linorder_nat = {Orderings__order_linorder = order_nat} :
|
haftmann@23250
|
55 |
nat Orderings.linorder;
|
haftmann@23250
|
56 |
|
haftmann@22490
|
57 |
end; (*struct Nat*)
|
haftmann@22490
|
58 |
|
haftmann@22490
|
59 |
structure Codegen =
|
haftmann@22490
|
60 |
struct
|
haftmann@22490
|
61 |
|
haftmann@24421
|
62 |
datatype ('a, 'b) searchtree =
|
haftmann@24421
|
63 |
Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree |
|
haftmann@24421
|
64 |
Leaf of 'a * 'b;
|
haftmann@22490
|
65 |
|
haftmann@28143
|
66 |
fun update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
|
haftmann@28143
|
67 |
(if HOL.eqop A1_ it key then Leaf (key, entry)
|
haftmann@28143
|
68 |
else (if HOL.less_eq
|
haftmann@28143
|
69 |
((Orderings.ord_preorder o Orderings.preorder_order o
|
haftmann@28143
|
70 |
Orderings.order_linorder)
|
haftmann@28143
|
71 |
A2_)
|
haftmann@28143
|
72 |
it key
|
haftmann@28143
|
73 |
then Branch (Leaf (it, entry), it, Leaf (key, vala))
|
haftmann@28143
|
74 |
else Branch (Leaf (key, vala), it, Leaf (it, entry))))
|
haftmann@28143
|
75 |
| update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
|
haftmann@28143
|
76 |
(if HOL.less_eq
|
haftmann@28143
|
77 |
((Orderings.ord_preorder o Orderings.preorder_order o
|
haftmann@28143
|
78 |
Orderings.order_linorder)
|
haftmann@28143
|
79 |
A2_)
|
haftmann@28143
|
80 |
it key
|
haftmann@28143
|
81 |
then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
|
haftmann@28143
|
82 |
else Branch (t1, key, update (A1_, A2_) (it, entry) t2));
|
haftmann@22490
|
83 |
|
haftmann@23132
|
84 |
val example : (Nat.nat, (Nat.nat list)) searchtree =
|
haftmann@26513
|
85 |
update (Nat.eq_nata, Nat.linorder_nat)
|
haftmann@23132
|
86 |
(Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
|
haftmann@23132
|
87 |
[Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
|
haftmann@26513
|
88 |
(update (Nat.eq_nata, Nat.linorder_nat)
|
haftmann@23132
|
89 |
(Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
|
haftmann@23132
|
90 |
[Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
|
haftmann@26513
|
91 |
(update (Nat.eq_nata, Nat.linorder_nat)
|
haftmann@23132
|
92 |
(Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
|
haftmann@23132
|
93 |
(Leaf (Nat.Suc Nat.Zero_nat, []))));
|
haftmann@22490
|
94 |
|
haftmann@22490
|
95 |
end; (*struct Codegen*)
|