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