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      -- Note that the type of "loop" is NOT (forall c s. <[s -> Bool]>@c)
 114      -- because "k" is free here; this restrictionis analogous to the free
 115      -- environment variable in Nanevski's example.
 116      loop emptyOk = if emptyOk
 117                     then <[ \s -> ~~k s || ~~(staged_accept e True  (loop False)) s ]>
 118                     else <[ \s ->          ~~(staged_accept e False (loop False)) s ]>
 119
 120 staged_accept (Const c) emptyOk k  =
 121     <[ \s -> if gs_empty s
 122              then false
 123              else (gs_head s) == ~~(guestCharLiteral c) && ~~k (gs_tail s) ]>
 124
 125 --
 126 -- Take particular note of the "Plus" case above: note that (following
 127 -- Nanevski+Pfenning) the code for "k" is not duplicated -- it is
 128 -- escapified into the constructed term only once, and a tiny scrap of
 129 -- code containing nothing more than the variable name k' is passed
 130 -- to the recursive call.  This is in contrast with the naive implementation
 131 -- shown below:
 132 --
 133 -- staged_accept (Plus e1 e2) emptyOk k     =
 134 --    <[ \s -> (~~(staged_accept e1 emptyOk k) s) ||
 135 --             (~~(staged_accept e2 emptyOk k) s)
 136 --             ]>
 137 --
 138
 139 --
 140 -- The following commented-out type is "too polymorphic" -- try
 141 -- uncommenting it to see what happens.  It's a great example of the
 142 -- kind of thing that environment classifiers guard against: the
 143 -- continuation code and the result code get their classifiers
 144 -- unified.
 145 --
 146 {-
 147 staged_accept ::
 148     Regex
 149     -> Bool
 150     -> (forall c s.
 151         GuestStream c s =>
 152         GuestCharLiteral c =>
 153         GuestLanguageBool c =>
 154         GuestEqChar c =>
 155         <[s -> Bool]>@c)
 156    -> (forall c s.
 157         GuestStream c s =>
 158         GuestCharLiteral c =>
 159         GuestLanguageBool c =>
 160         GuestEqChar c =>
 161         <[s -> Bool]>@c)
 162 -}