stdlib/regexp.mlw

   1
   2 (** {1 Theory of regular expressions} *)
   3
   4 module Regexp
   5
   6   type char
   7
   8   (** {2 Syntax} *)
   9
  10   type regexp =
  11     | Empty
  12     | Epsilon
  13     | Char    char
  14     | Alt     regexp regexp
  15     | Concat  regexp regexp
  16     | Star    regexp
  17
  18   (** {2 Semantics} *)
  19
  20   (** Words are sequences of characters. *)
  21
  22   use seq.Seq
  23   use seq.FreeMonoid
  24   use int.Int
  25
  26   type word = seq char
  27
  28   (** Inductive predicate `mem w r` means
  29       "word `w` belongs to the language of `r`". *)
  30
  31   inductive mem (w: word) (r: regexp) =
  32     | mem_eps:
  33         mem empty Epsilon
  34     | mem_char:
  35         forall c: char. mem (singleton c) (Char c)
  36     | mem_altl:
  37         forall w: word, r1 r2: regexp. mem w r1 -> mem w (Alt r1 r2)
  38     | mem_altr:
  39         forall w: word, r1 r2: regexp. mem w r2 -> mem w (Alt r1 r2)
  40     | mem_concat:
  41         forall w1 w2: word, r1 r2: regexp.
  42         mem w1 r1 -> mem w2 r2 -> mem (w1 ++ w2) (Concat r1 r2)
  43     | mems1:
  44         forall r: regexp. mem empty (Star r)
  45     | mems2:
  46         forall w1 w2: word, r: regexp.
  47         mem w1 r -> mem w2 (Star r) -> mem (w1 ++ w2) (Star r)
  48
  49   (** Optimizing constructors for Alt and Concat *)
  50
  51   let alt (r1 r2: regexp) : regexp
  52     ensures { forall w: word. mem w result <-> mem w (Alt r1 r2) }
  53   = match r1, r2 with
  54     | Empty, _ -> r2
  55     | _, Empty -> r1
  56     | _        -> Alt r1 r2
  57     end
  58
  59   let concat (r1 r2: regexp) : regexp
  60     ensures { forall w: word. mem w result <-> mem w (Concat r1 r2) }
  61   = match r1, r2 with
  62     | Empty, _   -> Empty
  63     | _, Empty   -> Empty
  64     | Epsilon, _ -> r2
  65     | _, Epsilon -> r1
  66     | _          -> Concat r1 r2
  67     end
  68
  69 end