progs/sml/re-bit.ML
author Chengsong
Sat, 01 Oct 2022 12:06:46 +0100
changeset 608 37b6fd310a16
parent 317 db0ff630bbb7
permissions -rw-r--r--
added related work chap
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
     1
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
     2
datatype bit =
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
     3
  Z | S | C of char
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
     4
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
     5
type bits = bit list
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
datatype rexp =
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
     8
   ZERO
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
     9
 | ONE 
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    10
 | CHAR of char 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    11
 | ALTS of rexp list
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    12
 | SEQ  of rexp * rexp 
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
 | STAR of rexp 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
 | RECD of string * rexp
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    16
fun alt r1 r2 = ALTS [r1, r2]
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    17
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    18
datatype arexp =
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    19
   AZERO
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    20
 | AONE  of bits
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    21
 | ACHAR of bits * char
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    22
 | AALTS of bits * (arexp list)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    23
 | ASEQ  of bits * arexp * arexp 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    24
 | ASTAR of bits * arexp 
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    25
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
datatype value =
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    27
   Empty
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
 | Chr of char
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
 | Sequ of value * value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
 | Left of value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
 | Right of value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
 | Stars of value list
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
 | Rec of string * value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    34
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    35
(* some helper functions for strings *)   
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    36
fun string_repeat s n = String.concat (List.tabulate (n, fn _ => s))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
(* some helper functions for rexps *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
fun seq s = case s of
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    40
    [] => ONE
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
  | [c] => CHAR(c)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
  | c::cs => SEQ(CHAR(c), seq cs)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    44
fun chr c = CHAR(c)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
fun str s = seq(explode s)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    47
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    48
fun plus r = SEQ(r, STAR(r))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    50
infix 9 ++
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    51
infix 9 --
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    52
infix 9 $
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    54
fun op ++ (r1, r2) = ALTS [r1, r2]
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    55
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    56
fun op -- (r1, r2) = SEQ(r1, r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
fun op $ (x, r) = RECD(x, r)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    60
fun alts rs = case rs of 
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    61
    [] => ZERO
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    62
  | [r] => r
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    63
  | r::rs => ALTS([r, alts rs])
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    64
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    65
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    66
fun sum (nil) = 0 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    67
  | sum (head::tail) = head + sum(tail);
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
(* size of a regular expressions - for testing purposes *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
fun size r = case r of
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    71
    ZERO => 1
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    72
  | ONE => 1
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    73
  | CHAR(_) => 1
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    74
  | ALTS(rs) => 1 + sum (map size rs)
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
  | SEQ(r1, r2) => 1 + (size r1) + (size r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
  | STAR(r) => 1 + (size r)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
  | RECD(_, r) => 1 + (size r)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    80
fun erase r = case r of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    81
    AZERO => ZERO
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    82
  | AONE(_) => ONE
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    83
  | ACHAR(_, c) => CHAR(c)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    84
  | AALTS(_, rs) => ALTS(map erase rs)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    85
  | ASEQ(_, r1, r2) => SEQ(erase r1, erase r2)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    86
  | ASTAR(_, r)=> STAR(erase r)
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    89
fun fuse bs r = case r of
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    90
    AZERO => AZERO
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    91
  | AONE(cs) => AONE(bs @ cs)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    92
  | ACHAR(cs, c) => ACHAR(bs @ cs, c)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    93
  | AALTS(cs, rs) => AALTS(bs @ cs, rs)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    94
  | ASEQ(cs, r1, r2) => ASEQ(bs @ cs, r1, r2)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
    95
  | ASTAR(cs, r) => ASTAR(bs @ cs, r)
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    96
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    97
fun internalise r = case r of
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    98
  ZERO => AZERO
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
    99
| ONE => AONE([])
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   100
| CHAR(c) => ACHAR([], c)
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   101
| ALTS([r1, r2]) => AALTS([], [fuse [Z] (internalise r1), fuse [S] (internalise r2)])
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   102
| SEQ(r1, r2) => ASEQ([], internalise r1, internalise r2)
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   103
| STAR(r) => ASTAR([], internalise r)
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   104
| RECD(x, r) => internalise r
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   105
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   106
fun decode_aux r bs = case (r, bs) of
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   107
  (ONE, bs) => (Empty, bs)
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   108
| (CHAR(c), bs) => (Chr(c), bs)
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   109
| (ALTS([r1]), bs) => decode_aux r1 bs
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   110
| (ALTS(rs), Z::bs1) => 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   111
     let val (v, bs2) = decode_aux (hd rs) bs1
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   112
     in (Left(v), bs2) end
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   113
| (ALTS(rs), S::bs1) => 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   114
     let val (v, bs2) = decode_aux (ALTS (tl rs)) bs1
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   115
     in (Right(v), bs2) end
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   116
| (SEQ(r1, r2), bs) => 
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   117
    let val (v1, bs1) = decode_aux r1 bs 
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   118
        val (v2, bs2) = decode_aux r2 bs1 
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   119
    in (Sequ(v1, v2), bs2) end
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   120
| (STAR(r1), Z::bs) => 
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   121
    let val (v, bs1) = decode_aux r1 bs 
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   122
        val (Stars(vs), bs2) = decode_aux (STAR r1) bs1
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   123
    in (Stars(v::vs), bs2) end
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   124
| (STAR(_), S::bs) => (Stars [], bs)
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   125
| (RECD(x, r1), bs) => 
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   126
    let val (v, bs1) = decode_aux r1 bs
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   127
    in (Rec(x, v), bs1) end
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   128
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   129
exception DecodeError
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   130
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   131
fun decode r bs = case (decode_aux r bs) of
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   132
  (v, []) => v
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   133
| _ => raise DecodeError
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   134
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   135
fun bnullable r = case r of
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   136
  AZERO => false
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   137
| AONE(_) => true
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   138
| ACHAR(_, _) => false
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   139
| AALTS(_, rs) => List.exists bnullable rs
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   140
| ASEQ(_, r1, r2) => bnullable(r1) andalso bnullable(r2)
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   141
| ASTAR(_, _) => true
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   142
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   143
fun bmkeps r = case r of
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   144
  AONE(bs) => bs
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   145
| AALTS(bs, rs) => 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   146
    let 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   147
      val SOME(r) = List.find bnullable rs
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   148
    in bs @ bmkeps(r) end
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   149
| ASEQ(bs, r1, r2) => bs @ bmkeps(r1) @ bmkeps(r2)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   150
| ASTAR(bs, r) => bs @ [S]
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   151
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   152
fun bder c r = case r of
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   153
  AZERO => AZERO
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   154
| AONE(_) => AZERO
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   155
| ACHAR(bs, d) => if c = d then AONE(bs) else AZERO
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   156
| AALTS(bs, rs) => AALTS(bs, map (bder c) rs)
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   157
| ASEQ(bs, r1, r2) => 
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   158
    if (bnullable r1) 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   159
    then AALTS(bs, [ASEQ([], bder c r1, r2), fuse (bmkeps r1) (bder c r2)])
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   160
    else ASEQ(bs, bder c r1, r2)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   161
| ASTAR(bs, r) => ASEQ(bs, fuse [Z] (bder c r), ASTAR([], r))
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   162
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   163
fun bders s r = case s of 
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   164
  [] => r
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   165
| c::s => bders s (bder c r)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   166
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   167
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   168
exception LexError
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   169
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   170
fun blex r s = case s of 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   171
    [] => if (bnullable r) then bmkeps r else raise LexError
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   172
  | c::cs => blex (bder c r) cs
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   173
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   174
fun blexing r s = decode r (blex (internalise r) (explode s))
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   175
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   176
(* Simplification *)
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   177
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   178
fun distinctBy xs f acc = case xs of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   179
   [] => []
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   180
 | x::xs =>
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   181
    let   
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   182
      val res = f x
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   183
    in  if (List.exists (fn x => x = res) acc)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   184
        then distinctBy xs f acc  
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   185
        else x::distinctBy xs f (res::acc)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   186
    end
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   187
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   188
fun flats rs = case rs of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   189
    [] => []
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   190
  | AZERO::rs1 => flats rs1
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   191
  | AALTS(bs, rs1)::rs2 => map (fuse bs) rs1 @ flats rs2
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   192
  | r1::rs2 => r1::flats rs2
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   193
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   194
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   195
fun stack r1 r2 = case r1 of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   196
    AONE(bs2) => fuse bs2 r2
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   197
  | _ => ASEQ([], r1, r2)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   198
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   199
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   200
fun bsimp r = case r of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   201
    ASEQ(bs1, r1, r2) => (case (bsimp r1, bsimp r2) of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   202
        (AZERO, _) => AZERO
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   203
      | (_, AZERO) => AZERO
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   204
      | (AONE(bs2), r2s) => fuse (bs1 @ bs2) r2s
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   205
      | (AALTS(bs2, rs), r2s) =>  
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   206
           AALTS(bs1 @ bs2, map (fn r => stack r r2s) rs)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   207
      | (r1s, r2s) => ASEQ(bs1, r1s, r2s)) 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   208
  | AALTS(bs1, rs) => (case distinctBy (flats (map bsimp rs)) erase [] of
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   209
        [] => AZERO
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   210
      | [r] => fuse bs1 r
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   211
      | rs2 => AALTS(bs1, rs2))  
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   212
  | r => r
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   213
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   214
fun bders_simp r s = case s of 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   215
  [] => r
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   216
| c::s => bders_simp (bsimp (bder c r)) s
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   217
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   218
fun blex_simp r s = case s of 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   219
    [] => if (bnullable r) then bmkeps r else raise LexError
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   220
  | c::cs => blex_simp (bsimp (bder c r)) cs
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   221
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   222
fun blexing_simp r s = 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   223
    decode r (blex_simp (internalise r) (explode s))
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   224
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   225
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   226
(* Lexing rules for a small WHILE language *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   227
val sym = alts (List.map chr (explode "abcdefghijklmnopqrstuvwxyz"))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
val digit = alts (List.map chr (explode "0123456789"))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   229
val idents =  sym -- STAR(sym ++ digit)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   230
val nums = plus(digit)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
val keywords = alts (List.map str ["skip", "while", "do", "if", "then", "else", "read", "write", "true", "false"])
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   232
val semicolon = str ";"
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   233
val ops = alts (List.map str [":=", "==", "-", "+", "*", "!=", "<", ">", "<=", ">=", "%", "/"])
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
val whitespace = plus(str " " ++ str "\n" ++ str "\t")
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
val rparen = str ")"
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   236
val lparen = str "("
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
val begin_paren = str "{"
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
val end_paren = str "}"
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   239
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
val while_regs = STAR(("k" $ keywords) ++
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   242
                      ("i" $ idents) ++
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   243
                      ("o" $ ops) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
                      ("n" $ nums) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   245
                      ("s" $ semicolon) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   246
                      ("p" $ (lparen ++ rparen)) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
                      ("b" $ (begin_paren ++ end_paren)) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   248
                      ("w" $ whitespace))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   249
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   250
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   251
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   252
(* Some Tests
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   253
  ============ *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   255
fun time f x =
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   256
  let
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   257
  val t_start = Timer.startCPUTimer()
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   258
  val f_x = (f x; f x; f x; f x; f x)
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   259
  val t_end = Time.toReal(#usr(Timer.checkCPUTimer(t_start))) / 5.0
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   260
in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   261
  (print ((Real.toString t_end) ^ "\n"); f_x)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   262
end
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   263
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   264
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   265
val prog2 = String.concatWith "\n" 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   266
  ["i := 2;",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   267
   "max := 100;",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   268
   "while i < max do {",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   269
   "  isprime := 1;",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   270
   "  j := 2;",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   271
   "  while (j * j) <= i + 1  do {",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   272
   "    if i % j == 0 then isprime := 0  else skip;",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   273
   "    j := j + 1",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   274
   "  };",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   275
   " if isprime == 1 then write i else skip;",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   276
   " i := i + 1",
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   277
   "}"];
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   278
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   279
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   280
(* loops in ML *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   281
datatype for = to of int * int
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   282
infix to 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   283
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   284
val for =
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   285
  fn lo to up =>
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   286
    (fn f => 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   287
       let fun loop lo = 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   288
         if lo > up then () else (f lo; loop (lo + 1))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   289
       in loop lo end)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   290
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   291
fun forby n =
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   292
  fn lo to up =>
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   293
    (fn f => 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   294
       let fun loop lo = 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   295
         if lo > up then () else (f lo; loop (lo + n))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   296
       in loop lo end)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   297
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   298
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   299
fun step_simp i = 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   300
  (print ((Int.toString i) ^ ": ") ;
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   301
   time (blexing_simp while_regs) (string_repeat prog2 i)); 
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   302
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   303
(*
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   304
val main1 = forby 1000 (1000 to 5000) step_simp;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   305
print "\n";
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   306
val main2 = forby 1000 (1000 to 5000) step_simp2;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   307
print "\n";
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   308
val main3 = forby 1000 (1000 to 5000) step_acc;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   309
print "\n";
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   310
val main4 = forby 1000 (1000 to 5000) step_acc2; 
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   311
*)
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   312
159
940530087f30 updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 156
diff changeset
   313
print "\n";
317
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   314
val main5 = forby 10 (10 to 50) step_simp; 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   315
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   316
print("Size after 50: " ^ 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   317
  PolyML.makestring(size (erase (bders_simp (internalise while_regs) (explode (string_repeat prog2 50))))) ^ "\n");
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   318
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   319
print("Size after 100: " ^ 
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   320
  PolyML.makestring(size (erase (bders_simp (internalise while_regs) (explode (string_repeat prog2 100))))) ^ "\n");
db0ff630bbb7 updated
Christian Urban <urbanc@in.tum.de>
parents: 159
diff changeset
   321