doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
author haftmann
Wed, 02 Apr 2008 15:58:32 +0200
changeset 26513 6f306c8c2c54
parent 26318 967323f93c67
child 27190 431f695fc865
permissions -rw-r--r--
explicit class "eq" for operational equality
haftmann@22850
     1
structure Nat = 
haftmann@22850
     2
struct
haftmann@22850
     3
haftmann@24421
     4
datatype nat = Suc of nat | Zero_nat;
haftmann@22850
     5
haftmann@26513
     6
fun eq_nat Zero_nat Zero_nat = true
haftmann@26513
     7
  | eq_nat (Suc m) (Suc n) = eq_nat m n
haftmann@26513
     8
  | eq_nat Zero_nat (Suc a) = false
haftmann@26513
     9
  | eq_nat (Suc a) Zero_nat = false;
haftmann@23107
    10
wenzelm@25056
    11
end; (*struct Nat*)
haftmann@24193
    12
haftmann@22850
    13
structure List = 
haftmann@22850
    14
struct
haftmann@22850
    15
haftmann@22850
    16
fun null (x :: xs) = false
haftmann@22850
    17
  | null [] = true;
haftmann@22850
    18
haftmann@22850
    19
fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
haftmann@22850
    20
  | list_all2 p xs [] = null xs
wenzelm@26318
    21
  | list_all2 p [] ys = null ys;
haftmann@22850
    22
haftmann@22850
    23
end; (*struct List*)
haftmann@22850
    24
haftmann@22850
    25
structure Codegen = 
haftmann@22850
    26
struct
haftmann@22850
    27
haftmann@23132
    28
datatype monotype = Mono of Nat.nat * monotype list;
haftmann@22850
    29
haftmann@26513
    30
fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
haftmann@26513
    31
  Nat.eq_nat tyco1 tyco2 andalso
haftmann@26513
    32
    List.list_all2 eq_monotype typargs1 typargs2;
haftmann@22850
    33
haftmann@22850
    34
end; (*struct Codegen*)