1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Wed Mar 04 11:05:02 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,59 +0,0 @@
     1.4 -structure ROOT = 
     1.5 -struct
     1.6 -
     1.7 -structure Integer = 
     1.8 -struct
     1.9 -
    1.10 -datatype bit = B0 | B1;
    1.11 -
    1.12 -datatype int = Pls | Min | Bit of int * bit | Number_of_int of int;
    1.13 -
    1.14 -fun pred (Bit (k, B0)) = Bit (pred k, B1)
    1.15 -  | pred (Bit (k, B1)) = Bit (k, B0)
    1.16 -  | pred Min = Bit (Min, B0)
    1.17 -  | pred Pls = Min;
    1.18 -
    1.19 -fun succ (Bit (k, B0)) = Bit (k, B1)
    1.20 -  | succ (Bit (k, B1)) = Bit (succ k, B0)
    1.21 -  | succ Min = Pls
    1.22 -  | succ Pls = Bit (Pls, B1);
    1.23 -
    1.24 -fun plus_int (Number_of_int v) (Number_of_int w) =
    1.25 -  Number_of_int (plus_int v w)
    1.26 -  | plus_int k Min = pred k
    1.27 -  | plus_int k Pls = k
    1.28 -  | plus_int (Bit (k, B1)) (Bit (l, B1)) = Bit (plus_int k (succ l), B0)
    1.29 -  | plus_int (Bit (k, B1)) (Bit (l, B0)) = Bit (plus_int k l, B1)
    1.30 -  | plus_int (Bit (k, B0)) (Bit (l, b)) = Bit (plus_int k l, b)
    1.31 -  | plus_int Min k = pred k
    1.32 -  | plus_int Pls k = k;
    1.33 -
    1.34 -fun uminus_int (Number_of_int w) = Number_of_int (uminus_int w)
    1.35 -  | uminus_int (Bit (k, B0)) = Bit (uminus_int k, B0)
    1.36 -  | uminus_int (Bit (k, B1)) = Bit (pred (uminus_int k), B1)
    1.37 -  | uminus_int Min = Bit (Pls, B1)
    1.38 -  | uminus_int Pls = Pls;
    1.39 -
    1.40 -fun times_int (Number_of_int v) (Number_of_int w) =
    1.41 -  Number_of_int (times_int v w)
    1.42 -  | times_int (Bit (k, B0)) l = Bit (times_int k l, B0)
    1.43 -  | times_int (Bit (k, B1)) l = plus_int (Bit (times_int k l, B0)) l
    1.44 -  | times_int Min k = uminus_int k
    1.45 -  | times_int Pls w = Pls;
    1.46 -
    1.47 -end; (*struct Integer*)
    1.48 -
    1.49 -structure Codegen = 
    1.50 -struct
    1.51 -
    1.52 -fun double_inc k =
    1.53 -  Integer.plus_int
    1.54 -    (Integer.times_int
    1.55 -      (Integer.Number_of_int
    1.56 -        (Integer.Bit (Integer.Bit (Integer.Pls, Integer.B1), Integer.B0)))
    1.57 -      k)
    1.58 -    (Integer.Number_of_int (Integer.Bit (Integer.Pls, Integer.B1)));
    1.59 -
    1.60 -end; (*struct Codegen*)
    1.61 -
    1.62 -end; (*struct ROOT*)