1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/Codegen/Thy/examples/pick1.ML	Tue Mar 03 11:00:51 2009 +0100
     1.3 @@ -0,0 +1,44 @@
     1.4 +structure HOL = 
     1.5 +struct
     1.6 +
     1.7 +fun leta s f = f s;
     1.8 +
     1.9 +end; (*struct HOL*)
    1.10 +
    1.11 +structure Nat = 
    1.12 +struct
    1.13 +
    1.14 +datatype nat = Suc of nat | Zero_nat;
    1.15 +
    1.16 +fun less_nat m (Suc n) = less_eq_nat m n
    1.17 +  | less_nat n Zero_nat = false
    1.18 +and less_eq_nat (Suc m) n = less_nat m n
    1.19 +  | less_eq_nat Zero_nat n = true;
    1.20 +
    1.21 +fun minus_nat (Suc m) (Suc n) = minus_nat m n
    1.22 +  | minus_nat Zero_nat n = Zero_nat
    1.23 +  | minus_nat m Zero_nat = m;
    1.24 +
    1.25 +end; (*struct Nat*)
    1.26 +
    1.27 +structure Product_Type = 
    1.28 +struct
    1.29 +
    1.30 +fun split f (a, b) = f a b;
    1.31 +
    1.32 +end; (*struct Product_Type*)
    1.33 +
    1.34 +structure Codegen = 
    1.35 +struct
    1.36 +
    1.37 +fun pick ((k, v) :: xs) n =
    1.38 +  (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    1.39 +  | pick (x :: xs) n =
    1.40 +    let
    1.41 +      val a = x;
    1.42 +      val (k, v) = a;
    1.43 +    in
    1.44 +      (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    1.45 +    end;
    1.46 +
    1.47 +end; (*struct Codegen*)