doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 24421 acfb2413faa3
child 26318 967323f93c67
permissions -rw-r--r--
updated;
     1 structure HOL = 
     2 struct
     3 
     4 fun leta s f = f s;
     5 
     6 end; (*struct HOL*)
     7 
     8 structure Nat = 
     9 struct
    10 
    11 datatype nat = Suc of nat | Zero_nat;
    12 
    13 fun less_nat n (Suc m) = less_eq_nat n m
    14   | less_nat n Zero_nat = false
    15 and less_eq_nat (Suc n) m = less_nat n m
    16   | less_eq_nat Zero_nat m = true;
    17 
    18 fun minus_nat (Suc m) (Suc n) = minus_nat m n
    19   | minus_nat Zero_nat n = Zero_nat
    20   | minus_nat m Zero_nat = m;
    21 
    22 end; (*struct Nat*)
    23 
    24 structure Product_Type = 
    25 struct
    26 
    27 fun split c (a, b) = c a b;
    28 
    29 end; (*struct Product_Type*)
    30 
    31 structure Codegen = 
    32 struct
    33 
    34 fun pick ((k, v) :: xs) n =
    35   (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    36   | pick (x :: xs) n =
    37     let
    38       val a = x;
    39       val (k, v) = a;
    40     in
    41       (if Nat.less_nat n k then v else pick xs (Nat.minus_nat n k))
    42     end;
    43 
    44 end; (*struct Codegen*)