Code from Harper's Proof-Directed Debugging

regexp.sml

structure Regex =
struct
  datatype regexp =
      Zero
    | One
    | Char of char
    | Times of regexp * regexp
    | Plus of regexp * regexp
    | Star of regexp

  fun acc Zero cs k = false
    | acc One cs k = k cs
    | acc (Char d) [] k = false
    | acc (Char d) (c::cs) k = if c = d then k cs else false
    | acc (Plus (r1, r2)) cs k = acc r1 cs k orelse acc r2 cs k
    | acc (Times (r1, r2)) cs k = acc r1 cs (fn cs' => acc r2 cs' k)
    | acc (r as (Star r1)) cs k = k cs orelse acc r1 cs (fn cs' => acc r cs' k)

  infix <+>
  fun op<+> (One, _) = One
    | op<+> (_, One) = One
    | op<+> (_, _) = Zero

  infix <*>
  fun op<*> (Zero, _) = Zero
    | op<*> (_, Zero) = Zero
    | op<*> (_, _) = One

  fun delta Zero = Zero
    | delta One = One
    | delta (Char _) = Zero
    | delta (Plus (r1, r2)) = (delta r1) <+> (delta r2)
    | delta (Times (r1, r2)) = (delta r2) <*> (delta r2)
    | delta (Star _) = One

  fun minus Zero = Zero
    | minus One = Zero
    | minus (Char c) = Char c
    | minus (Plus (r1, r2)) = Plus (minus r1, minus r2)
    | minus (Star r1) = Times (minus r1, Star (minus r1))
    | minus (Times (r1, r2)) =
        let
          val a = Times (delta r1, minus r2)
          val b = Times (r1, delta r2)
          val c = Times (minus r1, minus r2)
        in
          Plus (a, Plus (b, c))
        end

  fun accept r s =
    let
      val normal = Plus (delta r, minus r)
    in
      acc normal (String.explode s) (fn nil => true | _ => false)
    end
end