doc-src/Codegen/Thy/examples/tree.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Codegen/Thy/examples/tree.ML	Tue Mar 03 11:00:51 2009 +0100
@@ -0,0 +1,95 @@
+structure HOL = 
+struct
+
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
+
+type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
+fun less_eq (A_:'a ord) = #less_eq A_;
+fun less (A_:'a ord) = #less A_;
+
+fun eqop A_ a = eq A_ a;
+
+end; (*struct HOL*)
+
+structure Orderings = 
+struct
+
+type 'a preorder = {Orderings__ord_preorder : 'a HOL.ord};
+fun ord_preorder (A_:'a preorder) = #Orderings__ord_preorder A_;
+
+type 'a order = {Orderings__preorder_order : 'a preorder};
+fun preorder_order (A_:'a order) = #Orderings__preorder_order A_;
+
+type 'a linorder = {Orderings__order_linorder : 'a order};
+fun order_linorder (A_:'a linorder) = #Orderings__order_linorder A_;
+
+end; (*struct Orderings*)
+
+structure Nat = 
+struct
+
+datatype nat = Suc of nat | Zero_nat;
+
+fun eq_nat (Suc a) Zero_nat = false
+  | eq_nat Zero_nat (Suc a) = false
+  | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
+  | eq_nat Zero_nat Zero_nat = true;
+
+val eq_nata = {eq = eq_nat} : nat HOL.eq;
+
+fun less_nat m (Suc n) = less_eq_nat m n
+  | less_nat n Zero_nat = false
+and less_eq_nat (Suc m) n = less_nat m n
+  | less_eq_nat Zero_nat n = true;
+
+val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat HOL.ord;
+
+val preorder_nat = {Orderings__ord_preorder = ord_nat} :
+  nat Orderings.preorder;
+
+val order_nat = {Orderings__preorder_order = preorder_nat} :
+  nat Orderings.order;
+
+val linorder_nat = {Orderings__order_linorder = order_nat} :
+  nat Orderings.linorder;
+
+end; (*struct Nat*)
+
+structure Codegen = 
+struct
+
+datatype ('a, 'b) searchtree =
+  Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree |
+  Leaf of 'a * 'b;
+
+fun update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
+  (if HOL.eqop A1_ it key then Leaf (key, entry)
+    else (if HOL.less_eq
+               ((Orderings.ord_preorder o Orderings.preorder_order o
+                  Orderings.order_linorder)
+                 A2_)
+               it key
+           then Branch (Leaf (it, entry), it, Leaf (key, vala))
+           else Branch (Leaf (key, vala), it, Leaf (it, entry))))
+  | update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
+    (if HOL.less_eq
+          ((Orderings.ord_preorder o Orderings.preorder_order o
+             Orderings.order_linorder)
+            A2_)
+          it key
+      then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
+      else Branch (t1, key, update (A1_, A2_) (it, entry) t2));
+
+val example : (Nat.nat, (Nat.nat list)) searchtree =
+  update (Nat.eq_nata, Nat.linorder_nat)
+    (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
+      [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
+    (update (Nat.eq_nata, Nat.linorder_nat)
+      (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
+        [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
+      (update (Nat.eq_nata, Nat.linorder_nat)
+        (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
+        (Leaf (Nat.Suc Nat.Zero_nat, []))));
+
+end; (*struct Codegen*)