doc-src/Codegen/Thy/examples/integers.ML
author haftmann
Tue, 03 Mar 2009 11:00:51 +0100
changeset 30209 2f4684e2ea95
parent 22798 doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML@e3962371f568
permissions -rw-r--r--
more canonical directory structure of manuals
     1 structure ROOT = 
     2 struct
     3 
     4 structure Integer = 
     5 struct
     6 
     7 datatype bit = B0 | B1;
     8 
     9 datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
    10 
    11 fun pred (Bit (k, B0)) = Bit (pred k, B1)
    12   | pred (Bit (k, B1)) = Bit (k, B0)
    13   | pred Min = Bit (Min, B0)
    14   | pred Pls = Min;
    15 
    16 fun succ (Bit (k, B0)) = Bit (k, B1)
    17   | succ (Bit (k, B1)) = Bit (succ k, B0)
    18   | succ Min = Pls
    19   | succ Pls = Bit (Pls, B1);
    20 
    21 fun plus_int (Number_of_int v) (Number_of_int w) =
    22   Number_of_int (plus_int v w)
    23   | plus_int k Min = pred k
    24   | plus_int k Pls = k
    25   | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
    26   | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
    27   | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
    28   | plus_int Min k = pred k
    29   | plus_int Pls k = k;
    30 
    31 fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
    32   | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
    33   | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
    34   | uminus_int Min = Bit (Pls, B1)
    35   | uminus_int Pls = Pls;
    36 
    37 fun times_int (Number_of_int v) (Number_of_int w) =
    38   Number_of_int (times_int v w)
    39   | times_int (Bit (k, B0)) l = Bit (times_int k l, B0)
    40   | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l
    41   | times_int Min k = uminus_int k
    42   | times_int Pls w = Pls;
    43 
    44 end; (*struct Integer*)
    45 
    46 structure Codegen = 
    47 struct
    48 
    49 fun double_inc k =
    50   Integer.plus_int
    51     (Integer.times_int
    52       (Integer.Number_of_int
    53         (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
    54       k)
    55     (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1)));
    56 
    57 end; (*struct Codegen*)
    58 
    59 end; (*struct ROOT*)