TFL/test1.sml
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
     1 (*---------------------------------------------------------------------------
     2  * Pattern matching extensions.
     3  *---------------------------------------------------------------------------*)
     4 
     5 fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
     6 fun read thy = term_of o cread thy;
     7 fun Term s = read WF1.thy s;
     8 
     9 fun Rfunc thy R eqs =
    10    let val {induction,rules,theory,tcs} = 
    11               timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
    12    in {induction=induction, rules=rules, theory=theory, 
    13        tcs = map (cterm_of (sign_of theory)) tcs}
    14    end;
    15 
    16 fun def tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
    17 
    18 
    19 
    20 
    21 (*---------------------------------------------------------------------------
    22  * Normal patterns
    23  *---------------------------------------------------------------------------*)
    24 def "(f(x,y) = x+y)";
    25 
    26 def "(f1 0 = 1) & (f1 (Suc n) = 2)";
    27 
    28 (*---------------------------------------------------------------------------
    29  * Omitted patterns
    30  *---------------------------------------------------------------------------*)
    31 def "(f2 0 = 1)";
    32 
    33 def "(f3 (h#t) = h)";
    34 
    35 def "(f4 [a,b] = a)  &  (f4 [b] = b)";
    36 
    37 def "(f5 (0,0) = 0)";
    38 
    39 def "(f6 (0,0) = 0) & (f6 (0,Suc x) = x) & (f6 (Suc x, y) = y+x)"; 
    40 
    41 def "(f7 (Suc 0, h#t) = 1) & (f7 (Suc(Suc n),h1#h2#t) = h1)";
    42 
    43 def "(f8 (Suc(Suc n),h1#h2#t) = h1)";
    44 
    45 
    46 (*---------------------------------------------------------------------------
    47  * Overlapping patterns 
    48  *---------------------------------------------------------------------------*)
    49 def "(f9 (h1#h2#t) = t) & (f9 x = x)";
    50 
    51 def "(g (x,0) = 1) & (g (0,x) = 2)"; 
    52 
    53 def "(g1 (0,x) = x) & (g1 (x,0) = x)"; 
    54 
    55 def "(g2 ([], a#b#x) = 1) & (g2 (a#b#x, y) = 2) & (g2 (z, a#y) = a)";	
    56 
    57 def "(g3 (x,y,0) = 1) & (g3 (x,0,y) = 2) & (g3 (0,x,y) = x)";
    58 
    59 def "(g4 (0,y,z) = 1) & (g4 (x,0,z) = 2) & (g4 (x,y,0) = x)";
    60 
    61 def "(g5(0,x,y,z) = 1) & (g5(w,0,y,z) = 2) & (g5(w,x,0,z) = z) & \
    62   \  (g5(w,x,y,0) = y)";
    63 
    64 def "(g6 (0,w,x,y,z) = 1) & (g6 (v,0,x,y,z) = 2) & (g6 (v,w,0,y,z) = z) & \
    65   \  (g6 (v,w,x,0,z) = z) & (g6 (v,w,x,y,0) = 0)";
    66 
    67 def "(g7 [x, 0] = x) & (g7 [Suc v] = 1) & (g7 z = 2)";
    68 
    69 def "(g8 (h1#h2#h3#h4#h5#h6) = [h1,h2,h3,h4,h5]# g8 h6) & (g8 x = [x])";
    70 
    71 (* Normal *)
    72 def "(g9 (Suc(Suc x)) = 1) & (g9 (Suc x) = 2) & (g9 0 = 0)";
    73 
    74 (*---------------------------------------------------------------------------
    75  * Inaccessible patterns
    76  *---------------------------------------------------------------------------*)
    77 def "(h x = 1) & (h x = 2)";
    78 
    79 def "(h1 (x,0) = 1) & (h1 (x,Suc y) = 2) & \
    80   \  (h1 (x,y) = x) & (h1 (x,y) = y)";
    81 
    82 def "(h2 (x,0) = 1) & (h2 (0,x) = 2) & \
    83   \  (h2 (0,0) = 0) & (h2 (x,y) = x)";