examples/RegexMatcher.hs

   1 {-# OPTIONS_GHC -XModalTypes -XMultiParamTypeClasses -ddump-types #-}
   2 module RegexMatcher
   3 where
   4 import GHC.HetMet.CodeTypes hiding ((-))
   5
   6 --------------------------------------------------------------------------------
   7 --
   8 -- A one-level Regular Expression matcher, adapted from
   9 -- Nanevski+Pfenning's _Staged computation with names and necessity_,
  10 -- Figure 5
  11 --
  12
  13 data Regex
  14  = Empty
  15  | Plus  Regex Regex
  16  | Times Regex Regex
  17  | Star  Regex
  18  | Const Char
  19
  20 class Stream a where
  21   s_empty :: a -> Bool
  22   s_head  :: a -> Char
  23   s_tail  :: a -> a
  24
  25 -- A continuation-passing-style matcher.  If the "b" argument is false
  26 -- the expression must match at least one character before passing
  27 -- control to the continuation (this avoids the equality test in the
  28 -- Nanevski+Pfenning code)
  29
  30 accept :: Stream s =>
  31         Regex ->
  32         Bool ->           -- may only match the empty string if this is True
  33         (s -> Bool) ->
  34         s ->
  35         Bool
  36
  37 accept Empty False k s     =
  38   False
  39
  40 accept Empty True k s    =
  41   k s
  42
  43 accept (Plus e1 e2) emptyOk k s   =
  44  (accept e1 emptyOk k s) || (accept e2 emptyOk k s)
  45
  46 accept (Times e1 e2) True k s  =
  47  (accept e1 True (accept e2 True k)) s
  48
  49 accept (Times e1 e2) False k s  =
  50  (accept e1 False (accept e2 True  k)) s ||
  51  (accept e1 True  (accept e2 False k)) s
  52
  53 accept (Star e) emptyOk k s     =
  54  (emptyOk && (k s)) ||
  55  (accept e emptyOk (\s' -> accept (Star e) False k s') s)
  56
  57 accept (Const c) emptyOk k s      =
  58  if s_empty s
  59  then False
  60  else (s_head s) == c && k (s_tail s)
  61
  62
  63
  64 --------------------------------------------------------------------------------
  65 --
  66 -- A two-level Regular Expression matcher, adapted from
  67 -- Nanevski+Pfenning's _Staged computation with names and necessity_,
  68 -- Figure 6
  69 --
  70
  71 class GuestStream g a where
  72   <[ gs_empty ]> :: <[ a -> Bool ]>@g
  73   <[ gs_head  ]> :: <[ a -> Char ]>@g
  74   <[ gs_tail  ]> :: <[ a -> a    ]>@g
  75
  76 class GuestEqChar g where
  77   <[ (==) ]> :: <[ Char -> Char -> Bool ]>@g
  78
  79 staged_accept ::
  80     Regex
  81     -> Bool
  82     -> forall c s.
  83          GuestStream c s =>
  84          GuestCharLiteral c =>
  85          GuestLanguageBool c =>
  86          GuestEqChar c =>
  87          <[ s -> Bool ]>@c
  88       -> <[ s -> Bool ]>@c
  89
  90 staged_accept Empty False k      =
  91    <[ \s -> false ]>
  92
  93 staged_accept Empty True  k      =
  94    <[ \s -> gs_empty s ]>
  95
  96 staged_accept (Plus e1 e2) emptyOk k     =
  97    <[ \s -> let k' = ~~k
  98             in (~~(staged_accept e1 emptyOk <[k']>) s) ||
  99                (~~(staged_accept e2 emptyOk <[k']>) s)
 100             ]>
 101
 102 staged_accept (Times e1 e2) True k    =
 103    <[ \s -> ~~(staged_accept e1 True (staged_accept e2 True k)) s ]>
 104
 105 staged_accept (Times e1 e2) emptyOk k    =
 106    <[ \s -> ~~(staged_accept e1 True  (staged_accept e2 False k)) s ||
 107             ~~(staged_accept e1 False (staged_accept e2 True  k)) s
 108             ]>
 109
 110 staged_accept (Star e) emptyOk' k  =
 111    loop emptyOk'
 112     where
 113     -- loop :: Bool -> <[s -> Bool]>@g
 114      loop emptyOk = if emptyOk
 115                     then <[ \s -> ~~k s || ~~(staged_accept e True  (loop False)) s ]>
 116                     else <[ \s ->          ~~(staged_accept e False (loop False)) s ]>
 117     -- note that loop is not (forall c s. <[s -> Bool]>@c)
 118     -- because "k" is free in loop; it is analogous to the free
 119     -- environment variable in Nanevski's example
 120
 121 staged_accept (Const c) emptyOk k  =
 122     <[ \s -> if gs_empty s
 123              then false
 124              else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>
 125
 126 --
 127 -- Take particular note of the "Plus" case above: note that (following
 128 -- Nanevski+Pfenning) the code for "k" is not duplicated -- it is
 129 -- escapified into the constructed term only once, and a tiny scrap of
 130 -- code containing nothing more than the variable name k' is passed
 131 -- to the recursive call.  This is in contrast with the naive implementation
 132 -- shown below:
 133 --
 134 -- staged_accept (Plus e1 e2) emptyOk k     =
 135 --    <[ \s -> (~~(staged_accept e1 emptyOk k) s) ||
 136 --             (~~(staged_accept e2 emptyOk k) s)
 137 --             ]>
 138 --
 139
 140 --
 141 -- The following commented-out type is "too polymorphic" -- try
 142 -- uncommenting it to see what happens.  It's a great example of the
 143 -- kind of thing that environment classifiers guard against: the
 144 -- continuation code and the result code get their classifiers
 145 -- unified.
 146 --
 147 {-
 148 staged_accept ::
 149     Regex
 150     -> Bool
 151     -> (forall c s.
 152         GuestStream c s =>
 153         GuestCharLiteral c =>
 154         GuestLanguageBool c =>
 155         GuestEqChar c =>
 156         <[s -> Bool]>@c)
 157    -> (forall c s.
 158         GuestStream c s =>
 159         GuestCharLiteral c =>
 160         GuestLanguageBool c =>
 161         GuestEqChar c =>
 162         <[s -> Bool]>@c)
 163 -}