doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML
author wenzelm
Fri, 13 Jun 2008 20:57:51 +0200
changeset 27190 431f695fc865
parent 26513 6f306c8c2c54
child 28143 e5c6c4aac52c
permissions -rw-r--r--
updated generated file;
     1 structure Nat = 
     2 struct
     3 
     4 datatype nat = Suc of nat | Zero_nat;
     5 
     6 fun eq_nat Zero_nat Zero_nat = true
     7   | eq_nat (Suc nat) (Suc nat') = eq_nat nat nat'
     8   | eq_nat Zero_nat (Suc a) = false
     9   | eq_nat (Suc a) Zero_nat = false;
    10 
    11 end; (*struct Nat*)
    12 
    13 structure List = 
    14 struct
    15 
    16 fun null (x :: xs) = false
    17   | null [] = true;
    18 
    19 fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
    20   | list_all2 p xs [] = null xs
    21   | list_all2 p [] ys = null ys;
    22 
    23 end; (*struct List*)
    24 
    25 structure Codegen = 
    26 struct
    27 
    28 datatype monotype = Mono of Nat.nat * monotype list;
    29 
    30 fun eq_monotype (Mono (tyco1, typargs1)) (Mono (tyco2, typargs2)) =
    31   Nat.eq_nat tyco1 tyco2 andalso
    32     List.list_all2 eq_monotype typargs1 typargs2;
    33 
    34 end; (*struct Codegen*)