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