doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
author haftmann
Wed, 21 Mar 2007 08:07:19 +0100
changeset 22490 1822ec4fcecd
child 22798 e3962371f568
permissions -rw-r--r--
added example file
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@22490
    16
type 'a eq = {op_eq : 'a -> 'a -> bool};
haftmann@22490
    17
fun op_eq (A_:'a eq) = #op_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@22490
    26
fun op_eq_nat Zero_nat (Suc m) = false
haftmann@22490
    27
  | op_eq_nat (Suc n) Zero_nat = false
haftmann@22490
    28
  | op_eq_nat (Suc n) (Suc m) = op_eq_nat n m
haftmann@22490
    29
  | op_eq_nat Zero_nat Zero_nat = true;
haftmann@22490
    30
haftmann@22490
    31
val eq_nat = {op_eq = op_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 List = 
haftmann@22490
    44
struct
haftmann@22490
    45
haftmann@22490
    46
datatype nibble = Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 |
haftmann@22490
    47
  Nibble5 | Nibble6 | Nibble7 | Nibble8 | Nibble9 | NibbleA | NibbleB |
haftmann@22490
    48
  NibbleC | NibbleD | NibbleE | NibbleF;
haftmann@22490
    49
haftmann@22490
    50
end; (*struct List*)
haftmann@22490
    51
haftmann@22490
    52
structure Codegen = 
haftmann@22490
    53
struct
haftmann@22490
    54
haftmann@22490
    55
datatype ('a, 'b) searchtree = Leaf of 'a * 'b |
haftmann@22490
    56
  Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
haftmann@22490
    57
haftmann@22490
    58
fun update (A1_, A2_) (it, entry) (Branch (t1, key, t2)) =
haftmann@22490
    59
  (if Orderings.less_eq A2_ it key
haftmann@22490
    60
    then Branch (update (A1_, A2_) (it, entry) t1, key, t2)
haftmann@22490
    61
    else Branch (t1, key, update (A1_, A2_) (it, entry) t2))
haftmann@22490
    62
  | update (A1_, A2_) (it, entry) (Leaf (key, vala)) =
haftmann@22490
    63
    (if Code_Generator.op_eq A1_ it key then Leaf (key, entry)
haftmann@22490
    64
      else (if Orderings.less_eq A2_ it key
haftmann@22490
    65
             then Branch (Leaf (it, entry), it, Leaf (key, vala))
haftmann@22490
    66
             else Branch (Leaf (key, vala), it, Leaf (it, entry))));
haftmann@22490
    67
haftmann@22490
    68
fun example n =
haftmann@22490
    69
  update (Nat.eq_nat, Nat.ord_nat) (n, [#"b", #"a", #"r"])
haftmann@22490
    70
    (Leaf (Nat.Zero_nat, [#"f", #"o", #"o"]));
haftmann@22490
    71
haftmann@22490
    72
end; (*struct Codegen*)
haftmann@22490
    73
haftmann@22490
    74
end; (*struct ROOT*)