# HG changeset patch # User haftmann # Date 1342559271 -7200 # Node ID 6659c5913ebf7c0aec02f6033485894331cac735 # Parent 7d86239986c21c12076e547133a789fd5fab7b3a dropped ancient example generates diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/Codegen.hs --- a/doc-src/Codegen/Thy/examples/Codegen.hs Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -module Codegen where { - -import qualified Nat; - -class Null a where { - nulla :: a; -}; - -heada :: forall a. (Codegen.Null a) => [a] -> a; -heada (x : xs) = x; -heada [] = Codegen.nulla; - -null_option :: forall a. Maybe a; -null_option = Nothing; - -instance Codegen.Null (Maybe a) where { - nulla = Codegen.null_option; -}; - -dummy :: Maybe Nat.Nat; -dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]; - -} diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/arbitrary.ML --- a/doc-src/Codegen/Thy/examples/arbitrary.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -structure Codegen = -struct - -val arbitrary_option : 'a option = NONE; - -fun dummy_option [] = arbitrary_option - | dummy_option (x :: xs) = SOME x; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/bool_infix.ML --- a/doc-src/Codegen/Thy/examples/bool_infix.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -structure Nat = -struct - -datatype nat = Suc of nat | Zero_nat; - -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; - -end; (*struct Nat*) - -structure Codegen = -struct - -fun in_interval (k, l) n = - Nat.less_eq_nat k n andalso Nat.less_eq_nat n l; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/bool_literal.ML --- a/doc-src/Codegen/Thy/examples/bool_literal.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -structure HOL = -struct - -datatype boola = False | True; - -fun anda x True = x - | anda x False = False - | anda True x = x - | anda False x = False; - -end; (*struct HOL*) - -structure Nat = -struct - -datatype nat = Suc of nat | Zero_nat; - -fun less_nat m (Suc n) = less_eq_nat m n - | less_nat n Zero_nat = HOL.False -and less_eq_nat (Suc m) n = less_nat m n - | less_eq_nat Zero_nat n = HOL.True; - -end; (*struct Nat*) - -structure Codegen = -struct - -fun in_interval (k, l) n = - HOL.anda (Nat.less_eq_nat k n) (Nat.less_eq_nat n l); - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/bool_mlbool.ML --- a/doc-src/Codegen/Thy/examples/bool_mlbool.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -structure Nat = -struct - -datatype nat = Suc of nat | Zero_nat; - -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; - -end; (*struct Nat*) - -structure Codegen = -struct - -fun in_interval (k, l) n = - (Nat.less_eq_nat k n) andalso (Nat.less_eq_nat n l); - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/class.ML --- a/doc-src/Codegen/Thy/examples/class.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -structure Nat = -struct - -datatype nat = Suc of nat | Zero_nat; - -end; (*struct Nat*) - -structure Codegen = -struct - -type 'a null = {null : 'a}; -fun null (A_:'a null) = #null A_; - -fun head A_ (x :: xs) = x - | head A_ [] = null A_; - -val null_option : 'a option = NONE; - -fun null_optiona () = {null = null_option} : ('a option) null; - -val dummy : Nat.nat option = - head (null_optiona ()) [SOME (Nat.Suc Nat.Zero_nat), NONE]; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/class.ocaml --- a/doc-src/Codegen/Thy/examples/class.ocaml Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -module Nat = -struct - -type nat = Suc of nat | Zero_nat;; - -end;; (*struct Nat*) - -module Codegen = -struct - -type 'a null = {null : 'a};; -let null _A = _A.null;; - -let rec head _A = function x :: xs -> x - | [] -> null _A;; - -let rec null_option = None;; - -let null_optiona () = ({null = null_option} : ('a option) null);; - -let rec dummy - = head (null_optiona ()) [Some (Nat.Suc Nat.Zero_nat); None];; - -end;; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/collect_duplicates.ML --- a/doc-src/Codegen/Thy/examples/collect_duplicates.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -structure HOL = -struct - -type 'a eq = {eq : 'a -> 'a -> bool}; -fun eq (A_:'a eq) = #eq A_; - -fun eqop A_ a = eq A_ a; - -end; (*struct HOL*) - -structure List = -struct - -fun member A_ x (y :: ys) = - (if HOL.eqop A_ y x then true else member A_ x ys) - | member A_ x [] = false; - -end; (*struct List*) - -structure Codegen = -struct - -fun collect_duplicates A_ xs ys (z :: zs) = - (if List.member A_ z xs - then (if List.member A_ z ys then collect_duplicates A_ xs ys zs - else collect_duplicates A_ xs (z :: ys) zs) - else collect_duplicates A_ (z :: xs) (z :: ys) zs) - | collect_duplicates A_ xs ys [] = xs; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/dirty_set.ML --- a/doc-src/Codegen/Thy/examples/dirty_set.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,102 +0,0 @@ -structure ROOT = -struct - -structure Nat = -struct - -datatype nat = Zero_nat | Suc of nat; - -end; (*struct Nat*) - -structure Integer = -struct - -datatype bit = B0 | B1; - -datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; - -fun pred (Bit (k, B0)) = Bit (pred k, B1) - | pred (Bit (k, B1)) = Bit (k, B0) - | pred Min = Bit (Min, B0) - | pred Pls = Min; - -fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) - | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) - | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) - | uminus_int Min = Bit (Pls, B1) - | uminus_int Pls = Pls; - -fun succ (Bit (k, B0)) = Bit (k, B1) - | succ (Bit (k, B1)) = Bit (succ k, B0) - | succ Min = Pls - | succ Pls = Bit (Pls, B1); - -fun plus_int (Number_of_int v) (Number_of_int w) = - Number_of_int (plus_int v w) - | plus_int k Min = pred k - | plus_int k Pls = k - | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) - | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) - | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) - | plus_int Min k = pred k - | plus_int Pls k = k; - -fun minus_int (Number_of_int v) (Number_of_int w) = - Number_of_int (plus_int v (uminus_int w)) - | minus_int z w = plus_int z (uminus_int w); - -fun less_eq_int (Number_of_int k) (Number_of_int l) = less_eq_int k l - | less_eq_int (Bit (k1, B1)) (Bit (k2, B0)) = less_int k1 k2 - | less_eq_int (Bit (k1, v)) (Bit (k2, B1)) = less_eq_int k1 k2 - | less_eq_int (Bit (k1, B0)) (Bit (k2, v)) = less_eq_int k1 k2 - | less_eq_int (Bit (k, v)) Min = less_eq_int k Min - | less_eq_int (Bit (k, B1)) Pls = less_int k Pls - | less_eq_int (Bit (k, B0)) Pls = less_eq_int k Pls - | less_eq_int Min (Bit (k, B1)) = less_eq_int Min k - | less_eq_int Min (Bit (k, B0)) = less_int Min k - | less_eq_int Min Min = true - | less_eq_int Min Pls = true - | less_eq_int Pls (Bit (k, v)) = less_eq_int Pls k - | less_eq_int Pls Min = false - | less_eq_int Pls Pls = true -and less_int (Number_of_int k) (Number_of_int l) = less_int k l - | less_int (Bit (k1, B0)) (Bit (k2, B1)) = less_eq_int k1 k2 - | less_int (Bit (k1, B1)) (Bit (k2, v)) = less_int k1 k2 - | less_int (Bit (k1, v)) (Bit (k2, B0)) = less_int k1 k2 - | less_int (Bit (k, B1)) Min = less_int k Min - | less_int (Bit (k, B0)) Min = less_eq_int k Min - | less_int (Bit (k, v)) Pls = less_int k Pls - | less_int Min (Bit (k, v)) = less_int Min k - | less_int Min Min = false - | less_int Min Pls = true - | less_int Pls (Bit (k, B1)) = less_eq_int Pls k - | less_int Pls (Bit (k, B0)) = less_int Pls k - | less_int Pls Min = false - | less_int Pls Pls = false; - -fun nat_aux n i = - (if less_eq_int i (Number_of_int Pls) then n - else nat_aux (Nat.Suc n) - (minus_int i (Number_of_int (Bit (Pls, B1))))); - -fun nat i = nat_aux Nat.Zero_nat i; - -end; (*struct Integer*) - -structure Codegen = -struct - -val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: []; - -val foobar_set : Nat.nat list = - Nat.Zero_nat :: - (Nat.Suc Nat.Zero_nat :: - (Integer.nat - (Integer.Number_of_int - (Integer.Bit - (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0))) - :: [])); - -end; (*struct Codegen*) - -end; (*struct ROOT*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/fac.ML --- a/doc-src/Codegen/Thy/examples/fac.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -structure Nat = -struct - -datatype nat = Suc of nat | Zero_nat; - -val one_nat : nat = Suc Zero_nat; - -fun plus_nat (Suc m) n = plus_nat m (Suc n) - | plus_nat Zero_nat n = n; - -fun times_nat (Suc m) n = plus_nat n (times_nat m n) - | times_nat Zero_nat n = Zero_nat; - -end; (*struct Nat*) - -structure Codegen = -struct - -fun fac (Nat.Suc n) = Nat.times_nat (Nat.Suc n) (fac n) - | fac Nat.Zero_nat = Nat.one_nat; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/integers.ML --- a/doc-src/Codegen/Thy/examples/integers.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -structure ROOT = -struct - -structure Integer = -struct - -datatype bit = B0 | B1; - -datatype int = Pls | Min | Bit of int * bit | Number_of_int of int; - -fun pred (Bit (k, B0)) = Bit (pred k, B1) - | pred (Bit (k, B1)) = Bit (k, B0) - | pred Min = Bit (Min, B0) - | pred Pls = Min; - -fun succ (Bit (k, B0)) = Bit (k, B1) - | succ (Bit (k, B1)) = Bit (succ k, B0) - | succ Min = Pls - | succ Pls = Bit (Pls, B1); - -fun plus_int (Number_of_int v) (Number_of_int w) = - Number_of_int (plus_int v w) - | plus_int k Min = pred k - | plus_int k Pls = k - | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0) - | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1) - | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b) - | plus_int Min k = pred k - | plus_int Pls k = k; - -fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w) - | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0) - | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1) - | uminus_int Min = Bit (Pls, B1) - | uminus_int Pls = Pls; - -fun times_int (Number_of_int v) (Number_of_int w) = - Number_of_int (times_int v w) - | times_int (Bit (k, B0)) l = Bit (times_int k l, B0) - | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l - | times_int Min k = uminus_int k - | times_int Pls w = Pls; - -end; (*struct Integer*) - -structure Codegen = -struct - -fun double_inc k = - Integer.plus_int - (Integer.times_int - (Integer.Number_of_int - (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0))) - k) - (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1))); - -end; (*struct Codegen*) - -end; (*struct ROOT*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/lexicographic.ML --- a/doc-src/Codegen/Thy/examples/lexicographic.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -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_; - -end; (*struct HOL*) - -structure Codegen = -struct - -fun less_eq (A1_, A2_) B_ (x1, y1) (x2, y2) = - HOL.less A2_ x1 x2 orelse HOL.eq A1_ x1 x2 andalso HOL.less_eq B_ y1 y2; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/lookup.ML --- a/doc-src/Codegen/Thy/examples/lookup.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -structure ROOT = -struct - -structure Codegen = -struct - -fun lookup ((k, v) :: xs) l = - (if ((k : string) = l) then SOME v else lookup xs l) - | lookup [] l = NONE; - -end; (*struct Codegen*) - -end; (*struct ROOT*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/monotype.ML --- a/doc-src/Codegen/Thy/examples/monotype.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -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; - -end; (*struct Nat*) - -structure List = -struct - -fun null (x :: xs) = false - | null [] = true; - -fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys - | list_all2 p xs [] = null xs - | list_all2 p [] ys = null ys; - -end; (*struct List*) - -structure Codegen = -struct - -datatype monotype = Mono of Nat.nat * monotype list; - -fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) = - Nat.eq_nat tyco1 tyco2 andalso - List.list_all2 eq_monotype typargs1 typargs2; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/nat_binary.ML --- a/doc-src/Codegen/Thy/examples/nat_binary.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -structure Nat = -struct - -datatype nat = Dig1 of nat | Dig0 of nat | One_nat | Zero_nat; - -fun plus_nat (Dig1 m) (Dig1 n) = Dig0 (plus_nat (plus_nat m n) One_nat) - | plus_nat (Dig1 m) (Dig0 n) = Dig1 (plus_nat m n) - | plus_nat (Dig0 m) (Dig1 n) = Dig1 (plus_nat m n) - | plus_nat (Dig0 m) (Dig0 n) = Dig0 (plus_nat m n) - | plus_nat (Dig1 m) One_nat = Dig0 (plus_nat m One_nat) - | plus_nat One_nat (Dig1 n) = Dig0 (plus_nat n One_nat) - | plus_nat (Dig0 m) One_nat = Dig1 m - | plus_nat One_nat (Dig0 n) = Dig1 n - | plus_nat m Zero_nat = m - | plus_nat Zero_nat n = n; - -end; (*struct Nat*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/pick1.ML --- a/doc-src/Codegen/Thy/examples/pick1.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,44 +0,0 @@ -structure HOL = -struct - -fun leta s f = f s; - -end; (*struct HOL*) - -structure Nat = -struct - -datatype nat = Suc of nat | Zero_nat; - -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; - -fun minus_nat (Suc m) (Suc n) = minus_nat m n - | minus_nat Zero_nat n = Zero_nat - | minus_nat m Zero_nat = m; - -end; (*struct Nat*) - -structure Product_Type = -struct - -fun split f (a, b) = f a b; - -end; (*struct Product_Type*) - -structure Codegen = -struct - -fun pick ((k, v) :: xs) n = - (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k)) - | pick (x :: xs) n = - let - val a = x; - val (k, v) = a; - in - (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k)) - end; - -end; (*struct Codegen*) diff -r 7d86239986c2 -r 6659c5913ebf doc-src/Codegen/Thy/examples/tree.ML --- a/doc-src/Codegen/Thy/examples/tree.ML Tue Jul 17 22:34:29 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,95 +0,0 @@ -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*)