doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
author haftmann
Wed, 30 May 2007 21:09:13 +0200
changeset 23132 ae52b82dc5d8
parent 23107 0c3c55b7c98f
child 23250 9886802cbbd6
permissions -rw-r--r--
updated
haftmann@22490
     1
structure ROOT = 
haftmann@22490
     2
struct
haftmann@22490
     3
haftmann@22490
     4
structure Orderings = 
haftmann@22490
     5
struct
haftmann@22490
     6
haftmann@22490
     7
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
haftmann@22490
     8
fun less_eq (A_:'a ord) = #less_eq A_;
haftmann@22490
     9
fun less (A_:'a ord) = #less A_;
haftmann@22490
    10
haftmann@22490
    11
end; (*struct Orderings*)
haftmann@22490
    12
haftmann@22490
    13
structure Code_Generator = 
haftmann@22490
    14
struct
haftmann@22490
    15
haftmann@23107
    16
type 'a eq = {eq : 'a -> 'a -> bool};
haftmann@23107
    17
fun eq (A_:'a eq) = #eq A_;
haftmann@22490
    18
haftmann@22490
    19
end; (*struct Code_Generator*)
haftmann@22490
    20
haftmann@22490
    21
structure Nat = 
haftmann@22490
    22
struct
haftmann@22490
    23
haftmann@22490
    24
datatype nat = Zero_nat | Suc of nat;
haftmann@22490
    25
haftmann@23107
    26
fun eq_nat Zero_nat (Suc m) = false
haftmann@23107
    27
  | eq_nat (Suc n) Zero_nat = false
haftmann@23107
    28
  | eq_nat (Suc n) (Suc m) = eq_nat n m
haftmann@23107
    29
  | eq_nat Zero_nat Zero_nat = true;
haftmann@22490
    30
haftmann@23107
    31
val eq_nata = {eq = eq_nat} : nat Code_Generator.eq;
haftmann@22490
    32
haftmann@22490
    33
fun less_nat n (Suc m) = less_eq_nat n m
haftmann@22490
    34
  | less_nat n Zero_nat = false
haftmann@22490
    35
and less_eq_nat (Suc n) m = less_nat n m
haftmann@22490
    36
  | less_eq_nat Zero_nat m = true;
haftmann@22490
    37
haftmann@22490
    38
val ord_nat = {less_eq = less_eq_nat, less = less_nat} :
haftmann@22490
    39
  nat Orderings.ord;
haftmann@22490
    40
haftmann@22490
    41
end; (*struct Nat*)
haftmann@22490
    42
haftmann@22490
    43
structure Codegen = 
haftmann@22490
    44
struct
haftmann@22490
    45
haftmann@22490
    46
datatype ('a, 'b) searchtree = Leaf of 'a * 'b |
haftmann@22490
    47
  Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
haftmann@22490
    48
haftmann@22798
    49
fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
haftmann@22798
    50
  (if Orderings.less_eq C2_ it key
haftmann@22798
    51
    then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
haftmann@22798
    52
    else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
haftmann@22798
    53
  | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
haftmann@23107
    54
    (if Code_Generator.eq C1_ it key then Leaf (key, entry)
haftmann@22798
    55
      else (if Orderings.less_eq C2_ it key
haftmann@22490
    56
             then Branch (Leaf (it, entry), it, Leaf (key, vala))
haftmann@22490
    57
             else Branch (Leaf (key, vala), it, Leaf (it, entry))));
haftmann@22490
    58
haftmann@23132
    59
val example : (Nat.nat, (Nat.nat list)) searchtree =
haftmann@23107
    60
  update (Nat.eq_nata, Nat.ord_nat)
haftmann@23132
    61
    (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
haftmann@23132
    62
      [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
haftmann@23132
    63
    (update (Nat.eq_nata, Nat.ord_nat)
haftmann@23132
    64
      (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
haftmann@23132
    65
        [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
haftmann@23132
    66
      (update (Nat.eq_nata, Nat.ord_nat)
haftmann@23132
    67
        (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
haftmann@23132
    68
        (Leaf (Nat.Suc Nat.Zero_nat, []))));
haftmann@22490
    69
haftmann@22490
    70
end; (*struct Codegen*)
haftmann@22490
    71
haftmann@22490
    72
end; (*struct ROOT*)