doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 24421 acfb2413faa3
child 25731 b3e415b0cf5c
permissions -rw-r--r--
updated;
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@24421
     6
fun eqop_nat Zero_nat (Suc m) = false
haftmann@24421
     7
  | eqop_nat (Suc n) Zero_nat = false
haftmann@24421
     8
  | eqop_nat (Suc n) (Suc m) = eqop_nat n m
haftmann@24421
     9
  | eqop_nat Zero_nat Zero_nat = true;
haftmann@23107
    10
haftmann@22850
    11
fun plus_nat (Suc m) n = plus_nat m (Suc n)
haftmann@22850
    12
  | plus_nat Zero_nat n = n;
haftmann@22850
    13
wenzelm@25056
    14
end; (*struct Nat*)
haftmann@24193
    15
wenzelm@25056
    16
structure Product_Type = 
wenzelm@25056
    17
struct
wenzelm@25056
    18
wenzelm@25056
    19
fun split c (a, b) = c a b;
wenzelm@25056
    20
wenzelm@25056
    21
end; (*struct Product_Type*)
haftmann@22850
    22
haftmann@22850
    23
structure List = 
haftmann@22850
    24
struct
haftmann@22850
    25
haftmann@24193
    26
fun list_case f1 f2 [] = f1
haftmann@24193
    27
  | list_case f1 f2 (a :: lista) = f2 a lista;
haftmann@24193
    28
haftmann@22850
    29
fun zip xs (y :: ys) =
haftmann@22850
    30
  (case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
haftmann@22850
    31
  | zip xs [] = [];
haftmann@22850
    32
haftmann@22850
    33
fun null (x :: xs) = false
haftmann@22850
    34
  | null [] = true;
haftmann@22850
    35
haftmann@22850
    36
fun list_all p (x :: xs) = p x andalso list_all p xs
haftmann@22850
    37
  | list_all p [] = true;
haftmann@22850
    38
haftmann@22850
    39
fun size_list (a :: lista) =
haftmann@22850
    40
  Nat.plus_nat (size_list lista) (Nat.Suc Nat.Zero_nat)
haftmann@22850
    41
  | size_list [] = Nat.Zero_nat;
haftmann@22850
    42
haftmann@22850
    43
fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
haftmann@22850
    44
  | list_all2 p xs [] = null xs
haftmann@22850
    45
  | list_all2 p [] ys = null ys
haftmann@22850
    46
  | list_all2 p xs ys =
haftmann@24421
    47
    Nat.eqop_nat (size_list xs) (size_list ys) andalso
haftmann@22850
    48
      list_all (fn a as (aa, b) => p aa b) (zip xs ys);
haftmann@22850
    49
haftmann@22850
    50
end; (*struct List*)
haftmann@22850
    51
haftmann@22850
    52
structure Codegen = 
haftmann@22850
    53
struct
haftmann@22850
    54
haftmann@23132
    55
datatype monotype = Mono of Nat.nat * monotype list;
haftmann@22850
    56
haftmann@24421
    57
fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
haftmann@24421
    58
  Nat.eqop_nat tyco1 tyco2 andalso
haftmann@24421
    59
    List.list_all2 eqop_monotype typargs1 typargs2;
haftmann@22850
    60
haftmann@22850
    61
end; (*struct Codegen*)