Decision of regular expression membership

Decision algorithm based on residuals

module Residual

  type char

  val predicate eq (x y : char)
    ensures { result <-> x = y }

  clone regexp.Regexp with type char = char

  use seq.Seq
  use int.Int

  let rec accepts_epsilon (r: regexp) : bool
    variant { r }
    ensures { result <-> mem empty r }
  = match r with
    | Empty -> false
    | Epsilon -> true
    | Char _ -> false
    | Alt r1 r2 -> accepts_epsilon r1 || accepts_epsilon r2
    | Concat r1 r2 -> accepts_epsilon r1 && accepts_epsilon r2
    | Star _ -> true
    end

  lemma inversion_mem_star_gen :
    forall c w r w' r'.
      w' = cons c w /\ r' = Star r ->
      mem w' r' ->
      exists w1 w2. w = w1 ++ w2 /\ mem (cons c w1) r /\ mem w2 r'

  lemma inversion_mem_star :
    forall c w r. mem (cons c w) (Star r) ->
      exists w1 w2. w = w1 ++ w2 /\ mem (cons c w1) r /\ mem w2 (Star r)

  let rec residual (r: regexp) (c: char) : regexp
    variant { r }
    ensures { forall w. mem w result <-> mem (cons c w) r }
  = match r with
    | Empty -> Empty
    | Epsilon -> Empty
    | Char c' -> if eq c c' then Epsilon else Empty
    | Alt r1 r2 -> alt (residual r1 c) (residual r2 c)
    | Concat r1 r2 ->
        let r1' = residual r1 c in
        let r2' = residual r2 c in
        if accepts_epsilon r1 then (
          assert {
            forall w: word.
              mem w (Alt (Concat r1' r2) r2') <->
              mem (cons c w) r
          };
          alt (concat r1' r2) r2')
        else concat r1' r2
    | Star r1 -> concat (residual r1 c) r
    end

  let decide_mem (w: word) (r: regexp) : bool
    ensures { result <-> mem w r }
  = let ref r' = r in
    for i = 0 to length w - 1 do
      invariant { mem w[i..] r' <-> mem w r }
      r' <- residual r' w[i]
    done;
    accepts_epsilon r'

end

module ResidualOCaml

  use int.Int
  use mach.int.Int63
  use seq.Seq
  clone export Residual
  import Regexp

  type ostring = abstract {
     str: seq char
  }
  meta coercion function str

  val ([]) (s: ostring) (i: int63) : char
    requires { 0 <= i < length s }
    ensures  { result = get s i }

  val partial length (s: ostring) : int63
    ensures { result = length s >= 0 }

  let partial decide (w: ostring) (r: regexp) : bool
    ensures { result <-> mem w r }
  = let ref r' = r in
    for i = 0 to length w - 1 do
      invariant { mem w[i..] r' <-> mem w r }
      r' <- residual r' w[i]
    done;
    accepts_epsilon r'

end