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;
     1 structure Nat = 
     2 struct
     3 
     4 datatype nat = Suc of nat | Zero_nat;
     5 
     6 fun eqop_nat Zero_nat (Suc m) = false
     7   | eqop_nat (Suc n) Zero_nat = false
     8   | eqop_nat (Suc n) (Suc m) = eqop_nat n m
     9   | eqop_nat Zero_nat Zero_nat = true;
    10 
    11 fun plus_nat (Suc m) n = plus_nat m (Suc n)
    12   | plus_nat Zero_nat n = n;
    13 
    14 end; (*struct Nat*)
    15 
    16 structure Product_Type = 
    17 struct
    18 
    19 fun split c (a, b) = c a b;
    20 
    21 end; (*struct Product_Type*)
    22 
    23 structure List = 
    24 struct
    25 
    26 fun list_case f1 f2 [] = f1
    27   | list_case f1 f2 (a :: lista) = f2 a lista;
    28 
    29 fun zip xs (y :: ys) =
    30   (case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
    31   | zip xs [] = [];
    32 
    33 fun null (x :: xs) = false
    34   | null [] = true;
    35 
    36 fun list_all p (x :: xs) = p x andalso list_all p xs
    37   | list_all p [] = true;
    38 
    39 fun size_list (a :: lista) =
    40   Nat.plus_nat (size_list lista) (Nat.Suc Nat.Zero_nat)
    41   | size_list [] = Nat.Zero_nat;
    42 
    43 fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
    44   | list_all2 p xs [] = null xs
    45   | list_all2 p [] ys = null ys
    46   | list_all2 p xs ys =
    47     Nat.eqop_nat (size_list xs) (size_list ys) andalso
    48       list_all (fn a as (aa, b) => p aa b) (zip xs ys);
    49 
    50 end; (*struct List*)
    51 
    52 structure Codegen = 
    53 struct
    54 
    55 datatype monotype = Mono of Nat.nat * monotype list;
    56 
    57 fun eqop_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
    58   Nat.eqop_nat tyco1 tyco2 andalso
    59     List.list_all2 eqop_monotype typargs1 typargs2;
    60 
    61 end; (*struct Codegen*)