progs/fsharp/re.ml
author Chengsong
Tue, 20 Dec 2022 22:32:54 +0000
changeset 635 7ce2389dff4b
parent 156 6a43ea9305ba
permissions -rw-r--r--
more
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     1
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     2
type rexp =
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
     3
   ZERO 
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
     4
 | ONE 
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     5
 | CHAR of char
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     6
 | ALT of rexp * rexp
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
 | SEQ of rexp * rexp 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
 | STAR of rexp 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
 | RECD of string * rexp;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    10
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    11
type value =
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    12
   Empty
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
 | Chr of char
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    14
 | Sequ of value * value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    15
 | Left of value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    16
 | Right of value
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
 | Stars of value list
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
 | Rec of string * value;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    20
(* some helper functions for strings *)   
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
let explode s = [for c in s -> c];;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
let string_repeat s n =  String.replicate n s;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    24
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    25
(* some helper functions for rexps *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
let rec seq s = match s with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    27
  | [] -> ONE
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
  | [c] -> CHAR(c)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
  | 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
    30
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    31
let chr c = CHAR(c)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    32
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
let str s = seq(explode s);;
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
let 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
    36
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    37
let (++) r1 r2 = ALT(r1, r2);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    38
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    39
let (--) r1 r2 = SEQ(r1, r2);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    40
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    41
let ($) x r = RECD(x, r);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    42
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    43
let alts rs = match rs with 
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    44
  | [] -> ZERO
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    45
  | [r] -> r
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    46
  | r::rs -> List.fold (++) r rs;;
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
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    49
(* 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
    50
let rec size r = match r with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    51
  | ZERO -> 1
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    52
  | ONE -> 1
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    53
  | CHAR(_) -> 1
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    54
  | ALT(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
    55
  | 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
    56
  | STAR(r) -> 1 + (size r)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    57
  | RECD(_, r) -> 1 + (size r);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    58
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    59
(* nullable function: tests whether the regular 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    60
   expression can recognise the empty string *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    61
let rec nullable r = match r with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    62
  | ZERO -> false
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    63
  | ONE -> true
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    64
  | CHAR(_) -> false
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    65
  | ALT(r1, r2) -> nullable(r1) || nullable(r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    66
  | SEQ(r1, r2) -> nullable(r1) && nullable(r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    67
  | STAR(_) -> true
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    68
  | RECD(_, r) -> nullable(r);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    69
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    70
(* derivative of a regular expression r w.r.t. a character c *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    71
let rec der c r = match r with 
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    72
  | ZERO -> ZERO
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    73
  | ONE -> ZERO
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    74
  | CHAR(d) -> if c = d then ONE else ZERO
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    75
  | ALT(r1, r2) -> ALT(der c r1, der c r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    76
  | SEQ(r1, r2) -> 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    77
      if nullable r1 then ALT(SEQ(der c r1, r2), der c r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    78
      else SEQ(der c r1, r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    79
  | STAR(r) -> SEQ(der c r, STAR(r))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    80
  | RECD(_, r) -> der c r;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    81
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    82
(* derivative w.r.t. a list of chars (iterates der) *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    83
let rec ders s r = match s with 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    84
  | [] -> r
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    85
  | c::s -> ders s (der c r);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    86
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    87
(* extracts a string from value *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    88
let rec flatten v = match v with 
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
    89
  | Empty -> ""
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    90
  | Chr(c) -> System.Convert.ToString(c)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    91
  | Left(v) -> flatten v
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    92
  | Right(v) -> flatten v
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    93
  | Sequ(v1, v2) -> flatten v1 ^ flatten v2
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    94
  | Stars(vs) -> String.concat "" (List.map flatten vs)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    95
  | Rec(_, v) -> flatten v;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    96
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    97
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    98
(* extracts an environment from a value *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    99
let rec env v = match v with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   100
  | Empty -> []
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   101
  | Chr(c) -> []
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   102
  | Left(v) -> env v
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   103
  | Right(v) -> env v
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   104
  | Sequ(v1, v2) -> env v1 @ env v2
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   105
  | Stars(vs) -> List.fold (@) [] (List.map env vs)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   106
  | Rec(x, v) -> (x, flatten v) :: env v;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   107
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   108
let string_of_pair (x, s) = "(" ^ x ^ "," ^ s ^ ")";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   109
let string_of_env xs = String.concat "," (List.map string_of_pair xs);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   110
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   111
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   112
(* the value for a nullable rexp *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   113
let rec mkeps r = match r with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   114
  | ONE -> Empty
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   115
  | ALT(r1, r2) -> 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   116
      if nullable r1 then Left(mkeps r1) else Right(mkeps r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   117
  | SEQ(r1, r2) -> Sequ(mkeps r1, mkeps r2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   118
  | STAR(r) -> Stars([])
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   119
  | RECD(x, r) -> Rec(x, mkeps r);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   120
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   121
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   122
(* injection of a char into a value *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   123
let rec inj r c v = match r, v with
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   124
  | STAR(r), Sequ(v1, Stars(vs)) -> Stars(inj r c v1 :: vs)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   125
  | SEQ(r1, r2), Sequ(v1, v2) -> Sequ(inj r1 c v1, v2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   126
  | SEQ(r1, r2), Left(Sequ(v1, v2)) -> Sequ(inj r1 c v1, v2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   127
  | SEQ(r1, r2), Right(v2) -> Sequ(mkeps r1, inj r2 c v2)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   128
  | ALT(r1, r2), Left(v1) -> Left(inj r1 c v1)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   129
  | ALT(r1, r2), Right(v2) -> Right(inj r2 c v2)
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   130
  | CHAR(d), Empty -> Chr(d) 
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   131
  | RECD(x, r1), _ -> Rec(x, inj r1 c v);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   132
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   133
(* some "rectification" functions for simplification *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   134
let f_id v = v;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   135
let f_right f = fun v -> Right(f v);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   136
let f_left f = fun v -> Left(f v);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   137
let f_alt f1 f2 = fun v -> match v with 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   138
    Right(v) -> Right(f2 v)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   139
  | Left(v) -> Left(f1 v);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   140
let f_seq f1 f2 = fun v -> match v with 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   141
  Sequ(v1, v2) -> Sequ(f1 v1, f2 v2);;
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   142
let f_seq_Empty1 f1 f2 = fun v -> Sequ(f1 Empty, f2 v);;
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   143
let f_seq_Empty2 f1 f2 = fun v -> Sequ(f1 v, f2 Empty);;
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   144
let f_rec f = fun v -> match v with
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   145
    Rec(x, v) -> Rec(x, f v);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   146
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   147
(* simplification of regular expressions returning also an 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   148
   rectification function; no simplification under STARs *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   149
let rec simp r = match r with
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   150
    ALT(r1, r2) -> 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   151
      let (r1s, f1s) = simp r1 in 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   152
      let (r2s, f2s) = simp r2 in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   153
      (match r1s, r2s with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   154
          ZERO, _ -> (r2s, f_right f2s)
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   155
        | _, ZERO -> (r1s, f_left f1s)
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   156
        | _, _    -> if r1s = r2s then (r1s, f_left f1s)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   157
                     else (ALT (r1s, r2s), f_alt f1s f2s)) 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   158
  | SEQ(r1, r2) -> 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   159
      let (r1s, f1s) = simp r1 in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   160
      let (r2s, f2s) = simp r2 in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   161
      (match r1s, r2s with
156
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   162
          ZERO, _  -> (ZERO, f_right f2s)
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   163
        | _, ZERO  -> (ZERO, f_left f1s)
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   164
        | ONE, _ -> (r2s, f_seq_Empty1 f1s f2s)
6a43ea9305ba updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3
diff changeset
   165
        | _, ONE -> (r1s, f_seq_Empty2 f1s f2s)
3
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   166
        | _, _     -> (SEQ(r1s, r2s), f_seq f1s f2s))
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   167
  | RECD(x, r1) -> 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   168
      let (r1s, f1s) = simp r1 in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   169
      (RECD(x, r1s), f_rec f1s)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   170
  | r -> (r, f_id)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   171
;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   172
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   173
(* matcher function *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   174
let matcher r s = nullable(ders (explode s) r);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   175
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   176
(* lexing function (produces a value) *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   177
exception LexError;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   178
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   179
let rec lex r s = match s with
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   180
    [] -> if (nullable r) then mkeps r else raise LexError
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   181
  | c::cs -> inj r c (lex (der c r) cs);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   182
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   183
let lexing r s = lex r (explode s);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   184
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   185
(* lexing with simplification *)
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   186
let rec lex_simp r s = match s with
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   187
    [] -> if (nullable r) then mkeps r else raise LexError
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   188
  | c::cs -> 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   189
    let (r_simp, f_simp) = simp (der c r) in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   190
    inj r c (f_simp (lex_simp r_simp cs));;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   191
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   192
let lexing_simp r s = lex_simp r (explode s);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   193
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   194
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   195
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   196
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   197
(* 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
   198
let 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
   199
let 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
   200
let idents =  sym -- STAR(sym ++ digit);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   201
let nums = plus(digit);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   202
let 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
   203
let semicolon = str ";"
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   204
let ops = alts (List.map str [":="; "=="; "-"; "+"; "*"; "!="; "<"; ">"; "<="; ">="; "%"; "/"]);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   205
let 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
   206
let rparen = str ")";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   207
let lparen = str "(";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   208
let begin_paren = str "{";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   209
let end_paren = str "}";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   210
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   211
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   212
let while_regs = STAR(("k" $ keywords) ++
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   213
                      ("i" $ idents) ++
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   214
                      ("o" $ ops) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   215
                      ("n" $ nums) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   216
                      ("s" $ semicolon) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   217
                      ("p" $ (lparen ++ rparen)) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   218
                      ("b" $ (begin_paren ++ end_paren)) ++ 
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   219
                      ("w" $ whitespace));;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   220
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   221
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   222
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   223
(* Some Tests
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   224
  ============ *)
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
let time f x =
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   227
  let t = System.DateTime.Now in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   228
  let f_x = f x in
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   229
  (printfn "%O" (System.DateTime.Now - t); f_x);;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   230
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   231
let prog0 = "read n";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   232
string_of_env (env (lexing while_regs prog0));;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   233
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   234
let prog1 = "read  n; write (n)";;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   235
string_of_env (env (lexing_simp while_regs prog1));;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   236
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   237
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   238
let prog2 = "
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   239
i := 2;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   240
max := 100;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   241
while i < max do {
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   242
  isprime := 1;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   243
  j := 2;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   244
  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
   245
    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
   246
    j := j + 1
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   247
  };
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   248
  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
   249
  i := i + 1
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
for i = 1 to 100 do
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   253
  printf "%i: " i ;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   254
  time (lexing_simp while_regs) (string_repeat prog2 i);
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   255
done;;
94824659f6d7 added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
   256