src/Symantic/Parser/Automaton/Instructions.hs

   1 {-# LANGUAGE ConstraintKinds #-} -- For Executable
   2 {-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
   3 {-# LANGUAGE DerivingStrategies #-} -- For Show (Addr a)
   4 module Symantic.Parser.Automaton.Instructions where
   5
   6 import Data.Bool (Bool)
   7 import Data.Char (Char)
   8 import Data.Either (Either)
   9 import Data.Eq (Eq)
  10 import Data.Function (($), (.))
  11 import Text.Show (Show(..), showString)
  12 import qualified Data.Functor as Functor
  13 import qualified Language.Haskell.TH.Syntax as TH
  14 import qualified Symantic.Parser.Staging as Hask
  15
  16 import Symantic.Parser.Grammar
  17 import Symantic.Univariant.Trans
  18
  19 -- * Class 'InputPosition'
  20 -- | TODO
  21 class InputPosition inp where
  22 instance InputPosition ()
  23
  24 -- * Type 'Instr'
  25 -- | 'Instr'uctions for the 'Automaton'.
  26 data Instr input valueStack (exceptionStack::Peano) returnValue a where
  27   -- | @('Push' x k)@ pushes @(x)@ on the value-stack
  28   -- and continues with the next 'Instr'uction @(k)@.
  29   Push ::
  30     InstrPure x ->
  31     Instr inp (x ': vs) es ret a ->
  32     Instr inp vs es ret a
  33   -- | @('Pop' k)@ pushes @(x)@ on the value-stack.
  34   Pop ::
  35     Instr inp vs es ret a ->
  36     Instr inp (x ': vs) es ret a
  37   -- | @('LiftI2' f k)@ pops two values from the value-stack,
  38   -- and pushes the result of @(f)@ applied to them.
  39   LiftI2 ::
  40     InstrPure (x -> y -> z) ->
  41     Instr inp (z : vs) es ret a ->
  42     Instr inp (y : x : vs) es ret a
  43   -- | @('Fail')@ raises an error from the exception-stack.
  44   Fail ::
  45     Instr inp vs ('Succ es) ret a
  46   -- | @('Commit' k)@ removes an exception from the exception-stack
  47   -- and continues with the next 'Instr'uction @(k)@.
  48   Commit ::
  49     Instr inp vs es ret a ->
  50     Instr inp vs ('Succ es) ret a
  51   -- | @('Catch' l r)@ tries the @(l)@ 'Instr'uction,
  52   -- if it raises an exception, catches it,
  53   -- pushes the input on the value-stack
  54   -- and continues with the @(r)@ 'Instr'uction.
  55   Catch ::
  56     Instr inp vs ('Succ es) ret a ->
  57     Instr inp (inp ': vs) es ret a ->
  58     Instr inp vs es ret a
  59   -- | @('Seek' k)@ removes the input from the value-stack
  60   -- and continues with the next 'Instr'uction @(k)@.
  61   Seek ::
  62     Instr inp vs es r a ->
  63     Instr inp (inp : vs) es r a
  64   -- | @('Tell' k)@ pushes the input @(inp)@ on the value-stack
  65   -- and continues with the next 'Instr'uction @(k)@.
  66   Tell ::
  67     Instr inp (inp ': vs) es ret a ->
  68     Instr inp vs es ret a
  69   -- | @('Case' l r)@.
  70   Case ::
  71     Instr inp (x ': vs) es r a ->
  72     Instr inp (y ': vs) es r a ->
  73     Instr inp (Either x y ': vs) es r a
  74   -- | @('Swap' k)@ pops two values on the value-stack,
  75   -- pushes the first popped-out, then the second,
  76   -- and continues with the next 'Instr'uction @(k)@.
  77   Swap ::
  78     Instr inp (x ': y ': vs) es r a ->
  79     Instr inp (y ': x ': vs) es r a
  80   -- | @('Choices' ps bs d)@.
  81   Choices ::
  82     [InstrPure (x -> Bool)] ->
  83     [Instr inp vs es ret a] ->
  84     Instr inp vs es ret a ->
  85     Instr inp (x ': vs) es ret a
  86   -- | @('Subroutine' n v k)@ binds the 'Addr' @(n)@ to the 'Instr'uction's @(v)@,
  87   -- continues with the next 'Instr'uction @(k)@.
  88   Subroutine ::
  89     Addr x ->
  90     Instr inp '[] ('Succ es) x a ->
  91     Instr inp vs ('Succ es) ret a ->
  92     Instr inp vs ('Succ es) ret a
  93   -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
  94   Jump ::
  95     Addr ret ->
  96     Instr inp '[] ('Succ es) ret a
  97   -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
  98   -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
  99   Call ::
 100     Addr x ->
 101     Instr inp (x ': vs) ('Succ es) ret a ->
 102     Instr inp vs ('Succ es) ret a
 103   -- | @('Ret')@ returns the value stored in a singleton value-stack.
 104   Ret ::
 105     Instr inp '[ret] es ret a
 106   -- | @('Read' p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
 107   -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
 108   -- otherwise 'Fail'.
 109   Read ::
 110     InstrPure (Char -> Bool) ->
 111     Instr inp (Char ': vs) ('Succ es) ret a ->
 112     Instr inp vs ('Succ es) ret a
 113
 114 -- ** Type 'InstrPure'
 115 data InstrPure a
 116   =  InstrPureHaskell (Hask.Haskell a)
 117   |  InstrPureSameOffset
 118 instance Show (InstrPure a) where
 119   showsPrec p = \case
 120     InstrPureHaskell x -> showsPrec p x
 121     InstrPureSameOffset -> showString "InstrPureSameOffset"
 122
 123 -- ** Type 'Addr'
 124 newtype Addr a = Addr { unLabel :: TH.Name }
 125   deriving (Eq)
 126   deriving newtype Show
 127
 128 -- * Class 'Executable'
 129 type Executable repr =
 130   ( Stackable repr
 131   , Branchable repr
 132   , Exceptionable repr
 133   , Inputable repr
 134   , Routinable repr
 135   , Readable repr
 136   )
 137
 138 -- ** Class 'Stackable'
 139 class Stackable (repr :: * -> [*] -> Peano -> * -> * -> *) where
 140   push ::
 141     InstrPure x ->
 142     repr inp (x ': vs) n ret a ->
 143     repr inp vs n ret a
 144   pop ::
 145     repr inp vs n ret a ->
 146     repr inp (x ': vs) n ret a
 147   liftI2 ::
 148     InstrPure (x -> y -> z) ->
 149     repr inp (z ': vs) es ret a ->
 150     repr inp (y ': x ': vs) es ret a
 151   swap ::
 152     repr inp (x ': y ': vs) n r a ->
 153     repr inp (y ': x ': vs) n r a
 154
 155 -- ** Class 'Branchable'
 156 class Branchable (repr :: * -> [*] -> Peano -> * -> * -> *) where
 157   case_ ::
 158     repr inp (x ': vs) n r a ->
 159     repr inp (y ': vs) n r a ->
 160     repr inp (Either x y ': vs) n r a
 161   choices ::
 162     [InstrPure (x -> Bool)] ->
 163     [repr inp vs es ret a] ->
 164     repr inp vs es ret a ->
 165     repr inp (x ': vs) es ret a
 166
 167 -- ** Class 'Exceptionable'
 168 class Exceptionable (repr :: * -> [*] -> Peano -> * -> * -> *) where
 169   fail :: repr inp vs ('Succ es) ret a
 170   commit ::
 171     repr inp vs es ret a ->
 172     repr inp vs ('Succ es) ret a
 173   catch ::
 174     repr inp vs ('Succ es) ret a ->
 175     repr inp (inp ': vs) es ret a ->
 176     repr inp vs es ret a
 177
 178 -- ** Class 'Inputable'
 179 class Inputable (repr :: * -> [*] -> Peano -> * -> * -> *) where
 180   seek ::
 181     repr inp vs es r a ->
 182     repr inp (inp ': vs) es r a
 183   tell ::
 184     repr inp (inp ': vs) es ret a ->
 185     repr inp vs es ret a
 186
 187 -- ** Class 'Routinable'
 188 class Routinable (repr :: * -> [*] -> Peano -> * -> * -> *) where
 189   subroutine ::
 190     Addr x ->
 191     repr inp '[] ('Succ es) x a ->
 192     repr inp vs ('Succ es) ret a ->
 193     repr inp vs ('Succ es) ret a
 194   call ::
 195     Addr x ->
 196     repr inp (x ': vs) ('Succ es) ret a ->
 197     repr inp vs ('Succ es) ret a
 198   ret ::
 199     repr inp '[ret] es ret a
 200   jump ::
 201     Addr ret ->
 202     repr inp '[] ('Succ es) ret a
 203
 204 -- ** Class 'Readable'
 205 class Readable (repr :: * -> [*] -> Peano -> * -> * -> *) where
 206   read ::
 207     InstrPure (Char -> Bool) ->
 208     repr inp (Char ': vs) ('Succ es) ret a ->
 209     repr inp vs ('Succ es) ret a
 210
 211 instance
 212   Executable repr =>
 213   Trans (Instr inp vs es ret) (repr inp vs es ret) where
 214   trans = \case
 215     Push x k -> push x (trans k)
 216     Pop k -> pop (trans k)
 217     LiftI2 f k -> liftI2 f (trans k)
 218     Fail -> fail
 219     Commit k -> commit (trans k)
 220     Catch l r -> catch (trans l) (trans r)
 221     Seek k -> seek (trans k)
 222     Tell k -> tell (trans k)
 223     Case l r -> case_ (trans l) (trans r)
 224     Swap k -> swap (trans k)
 225     Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
 226     Subroutine n v k -> subroutine n (trans v) (trans k)
 227     Jump n -> jump n
 228     Call n (k::Instr inp (x ': vs) ('Succ es') ret a) ->
 229       call n (trans k :: repr inp (x ': vs) ('Succ es') ret a)
 230     Ret -> ret
 231     Read p k -> read p (trans k)
 232
 233 -- ** Type 'Peano'
 234 -- | Type-level natural numbers, using the Peano recursive encoding.
 235 data Peano = Zero | Succ Peano
 236
 237 -- | @('Fmap' f k)@.
 238 pattern Fmap ::
 239   InstrPure (x -> y) ->
 240   Instr inp (y ': xs) es ret a ->
 241   Instr inp (x ': xs) es ret a
 242 pattern Fmap f k = Push f (LiftI2 (InstrPureHaskell (Hask.Flip Hask.:@ (Hask.:$))) k)
 243
 244 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the value-stack,
 245 -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
 246 pattern App :: Instr inp (y : vs) es ret a -> Instr inp (x : (x -> y) : vs) es ret a
 247 pattern App k = LiftI2 (InstrPureHaskell (Hask.:$)) k
 248
 249 -- | @('If' ok ko)@ pops a 'Bool' from the value-stack
 250 -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
 251 -- or @(ko)@ otherwise.
 252 pattern If :: Instr inp vs es ret a -> Instr inp vs es ret a -> Instr inp (Bool ': vs) es ret a
 253 pattern If ok ko = Choices [InstrPureHaskell Hask.Id] [ok] ko
 254
 255 parsecHandler :: InputPosition inp => Instr inp vs ('Succ es) ret a -> Instr inp (inp : vs) ('Succ es) ret a
 256 parsecHandler k = Tell (LiftI2 InstrPureSameOffset (If k Fail))
 257
 258 -- * Type 'Automaton'
 259 -- | Making the control-flow explicit.
 260 data Automaton inp a x = Automaton { unAutomaton ::
 261   forall vs es ret.
 262   {-next-}Instr inp (x ': vs) ('Succ es) ret a ->
 263   Instr inp vs ('Succ es) ret a
 264   }
 265
 266 runAutomaton ::
 267   forall inp a es repr.
 268   Executable repr =>
 269   Automaton inp a a -> (repr inp '[] ('Succ es) a) a
 270 runAutomaton =
 271   trans @(Instr inp '[] ('Succ es) a) .
 272   ($ Ret) .
 273   unAutomaton
 274
 275 instance Applicable (Automaton inp a) where
 276   pure x = Automaton $ Push (InstrPureHaskell x)
 277   Automaton f <*> Automaton x = Automaton $ f . x . App
 278   liftA2 f (Automaton x) (Automaton y) = Automaton $
 279     x . y . LiftI2 (InstrPureHaskell f)
 280   Automaton x *> Automaton y = Automaton $ x . Pop . y
 281   Automaton x <* Automaton y = Automaton $ x . y . Pop
 282 instance
 283   InputPosition inp =>
 284   Alternable (Automaton inp a) where
 285   empty = Automaton $ \_k -> Fail
 286   Automaton l <|> Automaton r = Automaton $ \k ->
 287     -- TODO: join points
 288     Catch (l (Commit k)) (parsecHandler (r k))
 289   try (Automaton x) = Automaton $ \k ->
 290     Catch (x (Commit k)) (Seek Fail)
 291 instance Charable (Automaton inp a) where
 292   satisfy p = Automaton $ Read (InstrPureHaskell p)
 293 instance Selectable (Automaton inp a) where
 294   branch (Automaton lr) (Automaton l) (Automaton r) = Automaton $ \k ->
 295     -- TODO: join points
 296     lr (Case (l (Swap (App k)))
 297              (r (Swap (App k))))
 298 instance Matchable (Automaton inp a) where
 299   conditional ps bs (Automaton a) (Automaton default_) = Automaton $ \k ->
 300     -- TODO: join points
 301     a (Choices (InstrPureHaskell Functor.<$> ps)
 302                ((\b -> unAutomaton b k) Functor.<$> bs)
 303                (default_ k))
 304 instance Lookable (Automaton inp a) where
 305   look (Automaton x) = Automaton $ \k ->
 306     Tell (x (Swap (Seek k)))
 307   negLook (Automaton x) = Automaton $ \k ->
 308     Catch (Tell (x (Pop (Seek (Commit Fail)))))
 309           (Seek (Push (InstrPureHaskell Hask.unit) k))
 310 instance Letable TH.Name (Automaton inp a) where
 311   def n (Automaton v) = Automaton $ \k ->
 312     Subroutine (Addr n) (v Ret) (Call (Addr n) k)
 313   ref _isRec n = Automaton $ \case
 314     Ret -> Jump (Addr n)
 315     k -> Call (Addr n) k
 316 instance InputPosition inp => Foldable (Automaton inp a) where
 317   {-
 318   chainPre op p = go <*> p
 319     where go = (Hask..) <$> op <*> go <|> pure Hask.id
 320   chainPost p op = p <**> go
 321     where go = (Hask..) <$> op <*> go <|> pure Hask.id
 322   -}