doc-src/IsarAdvanced/Codegen/Thy/examples/pick1.ML
author wenzelm
Sat, 04 Nov 2006 19:25:39 +0100
changeset 21172 eea3c9048c7a
parent 21147 737a94f047e3
child 21190 08ec81dfc7fb
permissions -rw-r--r--
updated;
haftmann@21147
     1
structure ROOT = 
haftmann@21147
     2
struct
haftmann@21147
     3
haftmann@21147
     4
structure IntDef = 
haftmann@21147
     5
struct
haftmann@21147
     6
haftmann@21147
     7
datatype nat = Zero_nat | Succ_nat of nat;
haftmann@21147
     8
haftmann@21147
     9
fun less_nat Zero_nat (Succ_nat n) = true
wenzelm@21172
    10
  | less_nat n Zero_nat = false
wenzelm@21172
    11
  | less_nat (Succ_nat m) (Succ_nat n) = less_nat m n;
haftmann@21147
    12
haftmann@21147
    13
fun minus_nat (Succ_nat m) (Succ_nat n) = minus_nat m n
wenzelm@21172
    14
  | minus_nat Zero_nat n = Zero_nat
haftmann@21147
    15
  | minus_nat y Zero_nat = y;
haftmann@21147
    16
haftmann@21147
    17
end; (*struct IntDef*)
haftmann@21147
    18
haftmann@21147
    19
structure Codegen = 
haftmann@21147
    20
struct
haftmann@21147
    21
haftmann@21147
    22
fun pick ((k, v) :: xs) n =
haftmann@21147
    23
  (if IntDef.less_nat n k then v else pick xs (IntDef.minus_nat n k))
wenzelm@21172
    24
  | pick (x :: xs) n =
haftmann@21147
    25
    let
haftmann@21147
    26
      val (ka, va) = x;
haftmann@21147
    27
    in
wenzelm@21172
    28
      (if IntDef.less_nat n ka then va else pick xs (IntDef.minus_nat n ka))
haftmann@21147
    29
    end;
haftmann@21147
    30
haftmann@21147
    31
end; (*struct Codegen*)
haftmann@21147
    32
haftmann@21147
    33
end; (*struct ROOT*)