-{-# LANGUAGE ConstraintKinds #-} -- For Executable
+{-# LANGUAGE ConstraintKinds #-} -- For Machine
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
-{-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
-{-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
+-- | Semantic of the parsing instructions used
+-- to make the parsing control-flow explicit,
+-- in the convenient tagless-final encoding.
module Symantic.Parser.Machine.Instructions where
import Data.Bool (Bool(..))
import Data.Either (Either)
-import Data.Eq (Eq)
-import Data.Ord (Ord)
-import Data.Function (($), (.))
+import Data.Eq (Eq(..))
+import Data.Function ((.))
import Data.Kind (Type)
-import System.IO.Unsafe (unsafePerformIO)
-import Text.Show (Show(..), showString)
-import qualified Data.Functor as Functor
+import GHC.TypeLits (KnownSymbol)
+import Text.Show (Show(..))
+import Data.Proxy (Proxy(..))
import qualified Language.Haskell.TH as TH
-import qualified Language.Haskell.TH.Syntax as TH
-import qualified Symantic.Parser.Grammar.Pure as H
+import qualified Symantic.Parser.Haskell as H
import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input
-import Symantic.Univariant.Trans
--- * Type 'Instr'
--- | 'Instr'uctions for the 'Machine'.
-data Instr input valueStack (failStack::Peano) returnValue where
- -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
- -- and continues with the next 'Instr'uction @(k)@.
- Push ::
- InstrPure v ->
- Instr inp (v ': vs) es ret ->
- Instr inp vs es ret
- -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
- Pop ::
- Instr inp vs es ret ->
- Instr inp (v ': vs) es ret
- -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
- -- and pushes the result of @(f)@ applied to them.
- LiftI2 ::
- InstrPure (x -> y -> z) ->
- Instr inp (z : vs) es ret ->
- Instr inp (y : x : vs) es ret
- -- | @('Fail')@ raises an error from the 'failStack'.
- Fail ::
+-- * Type 'TermInstr'
+type TermInstr = H.Term TH.CodeQ
+
+-- * Class 'Machine'
+-- | All the 'Instr'uctions.
+type Machine tok repr =
+ ( InstrBranchable repr
+ , InstrExceptionable repr
+ , InstrInputable repr
+ , InstrJoinable repr
+ , InstrLetable repr
+ , InstrValuable repr
+ , InstrReadable tok repr
+ )
+
+-- ** Type 'ReprInstr'
+type ReprInstr = {-input-}Type -> {-valueStack-}[Type] -> {-a-}Type -> Type
+
+-- ** Type 'LetName'
+-- | 'TH.Name' of a 'defLet' or 'defJoin'
+-- indexed by the return type of the factorized 'Instr'uctions.
+-- This helps type-inferencing.
+newtype LetName a = LetName { unLetName :: TH.Name }
+ deriving Eq
+ deriving newtype Show
+
+-- ** Class 'InstrValuable'
+class InstrValuable (repr::ReprInstr) where
+ pushValue ::
+ TermInstr v ->
+ repr inp (v ': vs) a ->
+ repr inp vs a
+ popValue ::
+ repr inp vs a ->
+ repr inp (v ': vs) a
+ lift2Value ::
+ TermInstr (x -> y -> z) ->
+ repr inp (z ': vs) a ->
+ repr inp (y ': x ': vs) a
+ swapValue ::
+ repr inp (x ': y ': vs) a ->
+ repr inp (y ': x ': vs) a
+ -- | @('mapValue' f k)@.
+ mapValue ::
+ TermInstr (x -> y) ->
+ repr inp (y ': vs) a ->
+ repr inp (x ': vs) a
+ mapValue f = pushValue f . lift2Value (H.flip H..@ (H.$))
+ -- | @('applyValue' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
+ -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
+ applyValue ::
+ repr inp (y ': vs) a ->
+ repr inp (x ': (x -> y) ': vs) a
+ applyValue = lift2Value (H.$)
+
+-- ** Class 'InstrExceptionable'
+class InstrExceptionable (repr::ReprInstr) where
+ -- | @('raiseException' lbl es)@ raises labeled error from the 'failStack'.
+ raiseException ::
+ KnownSymbol lbl =>
+ Proxy lbl ->
+ [ErrorItem (InputToken inp)] ->
+ repr inp vs a
+ -- | Like using 'raiseException' with the @"fail"@ label.
+ fail ::
[ErrorItem (InputToken inp)] ->
- Instr inp vs ('Succ es) ret
- -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
+ repr inp vs a
+ fail = raiseException (Proxy @"fail")
+ -- | @('popException' lbl k)@ removes a 'Catcher'
+ -- from the @catchStackByLabel@ at given label,
-- and continues with the next 'Instr'uction @(k)@.
- PopFail ::
- Instr inp vs es ret ->
- Instr inp vs ('Succ es) ret
- -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
+ popException ::
+ KnownSymbol lbl =>
+ Proxy lbl ->
+ repr inp vs a ->
+ repr inp vs a
+ -- | @('catchException' lbl l r)@ tries the @(l)@ 'Instr'uction
-- in a new failure scope such that if @(l)@ raises a failure, it is caught,
-- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
-- and the control flow goes on with the @(r)@ 'Instr'uction.
- CatchFail ::
- Instr inp vs ('Succ es) ret ->
- Instr inp (Cursor inp ': vs) es ret ->
- Instr inp vs es ret
- -- | @('LoadInput' k)@ removes the input from the 'valueStack'
- -- and continues with the next 'Instr'uction @(k)@ using that input.
- LoadInput ::
- Instr inp vs es r ->
- Instr inp (Cursor inp : vs) es r
- -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
- -- and continues with the next 'Instr'uction @(k)@.
- PushInput ::
- Instr inp (Cursor inp ': vs) es ret ->
- Instr inp vs es ret
- -- | @('Case' l r)@.
- Case ::
- Instr inp (x ': vs) es r ->
- Instr inp (y ': vs) es r ->
- Instr inp (Either x y ': vs) es r
- -- | @('Swap' k)@ pops two values on the 'valueStack',
- -- pushes the first popped-out, then the second,
- -- and continues with the next 'Instr'uction @(k)@.
- Swap ::
- Instr inp (x ': y ': vs) es r ->
- Instr inp (y ': x ': vs) es r
- -- | @('Choices' ps bs d)@.
- Choices ::
- [InstrPure (v -> Bool)] ->
- [Instr inp vs es ret] ->
- Instr inp vs es ret ->
- Instr inp (v ': vs) es ret
- -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
+ catchException ::
+ KnownSymbol lbl =>
+ Proxy lbl ->
+ repr inp vs ret ->
+ repr inp (Cursor inp ': vs) ret ->
+ repr inp vs ret
+
+-- ** Class 'InstrBranchable'
+class InstrBranchable (repr::ReprInstr) where
+ -- | @('caseBranch' l r)@.
+ caseBranch ::
+ repr inp (x ': vs) r ->
+ repr inp (y ': vs) r ->
+ repr inp (Either x y ': vs) r
+ -- | @('choicesBranch' ps bs d)@.
+ choicesBranch ::
+ [TermInstr (v -> Bool)] ->
+ [repr inp vs a] ->
+ repr inp vs a ->
+ repr inp (v ': vs) a
+ -- | @('ifBranch' ok ko)@ pops a 'Bool' from the 'valueStack'
+ -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
+ -- or @(ko)@ otherwise.
+ ifBranch ::
+ repr inp vs a ->
+ repr inp vs a ->
+ repr inp (Bool ': vs) a
+ ifBranch ok ko = choicesBranch [H.id] [ok] ko
+
+-- ** Class 'InstrLetable'
+class InstrLetable (repr::ReprInstr) where
+ -- | @('defLet' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
-- 'Call's @(n)@ and
-- continues with the next 'Instr'uction @(k)@.
- Subroutine ::
- LetName v -> Instr inp '[] ('Succ 'Zero) v ->
- Instr inp vs ('Succ es) ret ->
- Instr inp vs ('Succ es) ret
- -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
- Jump ::
- LetName ret ->
- Instr inp '[] ('Succ es) ret
- -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
+ defLet ::
+ LetName v -> repr inp '[] v ->
+ repr inp vs a ->
+ repr inp vs a
+ -- | @('call' n k)@ pass the control-flow to the 'DefLet' named @(n)@,
-- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
- Call ::
- LetName v ->
- Instr inp (v ': vs) ('Succ es) ret ->
- Instr inp vs ('Succ es) ret
- -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
- Ret ::
- Instr inp '[ret] es ret
- -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
- -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
- -- otherwise 'Fail'.
- Read ::
- [ErrorItem (InputToken inp)] ->
- InstrPure (InputToken inp -> Bool) ->
- Instr inp (InputToken inp ': vs) ('Succ es) ret ->
- Instr inp vs ('Succ es) ret
- DefJoin ::
- LetName v -> Instr inp (v ': vs) es ret ->
- Instr inp vs es ret ->
- Instr inp vs es ret
- RefJoin ::
- LetName v ->
- Instr inp (v ': vs) es ret
-
--- ** Type 'InstrPure'
-data InstrPure a where
- InstrPure :: H.CombPure a -> InstrPure a
- InstrPureSameOffset :: CodeQ (cur -> cur -> Bool) -> InstrPure (cur -> cur -> Bool)
- InstrP
-
-instance Show (InstrPure a) where
- showsPrec p = \case
- InstrPure x -> showsPrec p x
- InstrPureSameOffset{} -> showString "InstrPureSameOffset"
-instance Trans InstrPure TH.CodeQ where
- trans = \case
- InstrPure x -> trans x
- InstrPureSameOffset x -> x
-
--- ** Type 'LetName'
-newtype LetName a = LetName { unLetName :: TH.Name }
- deriving (Eq)
- deriving newtype Show
-
--- * Class 'Executable'
-type Executable repr =
- ( Stackable repr
- , Branchable repr
- , Failable repr
- , Inputable repr
- , Routinable repr
- , Joinable repr
- )
-
--- ** Class 'Stackable'
-class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
- push ::
- InstrPure v ->
- repr inp (v ': vs) n ret ->
- repr inp vs n ret
- pop ::
- repr inp vs n ret ->
- repr inp (v ': vs) n ret
- liftI2 ::
- InstrPure (x -> y -> z) ->
- repr inp (z ': vs) es ret ->
- repr inp (y ': x ': vs) es ret
- swap ::
- repr inp (x ': y ': vs) n r ->
- repr inp (y ': x ': vs) n r
-
--- ** Class 'Branchable'
-class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
- case_ ::
- repr inp (x ': vs) n r ->
- repr inp (y ': vs) n r ->
- repr inp (Either x y ': vs) n r
- choices ::
- [InstrPure (v -> Bool)] ->
- [repr inp vs es ret] ->
- repr inp vs es ret ->
- repr inp (v ': vs) es ret
-
--- ** Class 'Failable'
-class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
- fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
- popFail ::
- repr inp vs es ret ->
- repr inp vs ('Succ es) ret
- catchFail ::
- repr inp vs ('Succ es) ret ->
- repr inp (Cursor inp ': vs) es ret ->
- repr inp vs es ret
-
--- ** Class 'Inputable'
-class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
- loadInput ::
- repr inp vs es r ->
- repr inp (Cursor inp ': vs) es r
- pushInput ::
- repr inp (Cursor inp ': vs) es ret ->
- repr inp vs es ret
-
--- ** Class 'Routinable'
-class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
- subroutine ::
- LetName v -> repr inp '[] ('Succ 'Zero) v ->
- repr inp vs ('Succ es) ret ->
- repr inp vs ('Succ es) ret
call ::
- LetName v -> repr inp (v ': vs) ('Succ es) ret ->
- repr inp vs ('Succ es) ret
+ LetName v -> repr inp (v ': vs) a ->
+ repr inp vs a
+ -- | @('ret')@ returns the value stored in a singleton 'valueStack'.
ret ::
- repr inp '[ret] es ret
+ repr inp '[a] a
+ -- | @('jump' n k)@ pass the control-flow to the 'DefLet' named @(n)@.
jump ::
- LetName ret ->
- repr inp '[] ('Succ es) ret
+ LetName a ->
+ repr inp '[] a
--- ** Class 'Joinable'
-class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
+-- ** Class 'InstrJoinable'
+class InstrJoinable (repr::ReprInstr) where
defJoin ::
- LetName v ->
- repr inp (v ': vs) es ret ->
- repr inp vs es ret ->
- repr inp vs es ret
+ LetName v -> repr inp (v ': vs) a ->
+ repr inp vs a ->
+ repr inp vs a
refJoin ::
LetName v ->
- repr inp (v ': vs) es ret
+ repr inp (v ': vs) a
+
+-- ** Class 'InstrInputable'
+class InstrInputable (repr::ReprInstr) where
+ -- | @('loadInput' k)@ removes the input from the 'valueStack'
+ -- and continues with the next 'Instr'uction @(k)@ using that input.
+ loadInput ::
+ repr inp vs a ->
+ repr inp (Cursor inp ': vs) a
+ -- | @('pushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
+ -- and continues with the next 'Instr'uction @(k)@.
+ pushInput ::
+ repr inp (Cursor inp ': vs) a ->
+ repr inp vs a
--- ** Class 'Readable'
-class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
+-- ** Class 'InstrReadable'
+class InstrReadable (tok::Type) (repr::ReprInstr) where
+ -- | @('read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
+ -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
+ -- otherwise 'RaiseException'.
read ::
tok ~ InputToken inp =>
[ErrorItem tok] ->
- InstrPure (tok -> Bool) ->
- repr inp (tok ': vs) ('Succ es) ret ->
- repr inp vs ('Succ es) ret
-
-instance
- ( Executable repr
- , Readable repr (InputToken inp)
- ) => Trans (Instr inp vs es) (repr inp vs es) where
- trans = \case
- Push x k -> push x (trans k)
- Pop k -> pop (trans k)
- LiftI2 f k -> liftI2 f (trans k)
- Fail err -> fail err
- PopFail k -> popFail (trans k)
- CatchFail l r -> catchFail (trans l) (trans r)
- LoadInput k -> loadInput (trans k)
- PushInput k -> pushInput (trans k)
- Case l r -> case_ (trans l) (trans r)
- Swap k -> swap (trans k)
- Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
- Subroutine n sub k -> subroutine n (trans sub) (trans k)
- Jump n -> jump n
- Call n k -> call n (trans k)
- Ret -> ret
- Read es p k -> read es p (trans k)
- DefJoin n sub k -> defJoin n (trans sub) (trans k)
- RefJoin n -> refJoin n
-
--- ** Type 'Peano'
--- | Type-level natural numbers, using the Peano recursive encoding.
-data Peano = Zero | Succ Peano
-
--- | @('Fmap' f k)@.
-pattern Fmap ::
- InstrPure (x -> y) ->
- Instr inp (y ': xs) es ret ->
- Instr inp (x ': xs) es ret
-pattern Fmap f k = Push f (LiftI2 (InstrPure (H.Flip H.:@ (H.:$))) k)
-
--- | @('App' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
--- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
-pattern App ::
- Instr inp (y : vs) es ret ->
- Instr inp (x : (x -> y) : vs) es ret
-pattern App k = LiftI2 (InstrPure (H.:$)) k
-
--- | @('If' ok ko)@ pops a 'Bool' from the 'valueStack'
--- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
--- or @(ko)@ otherwise.
-pattern If ::
- Instr inp vs es ret ->
- Instr inp vs es ret ->
- Instr inp (Bool ': vs) es ret
-pattern If ok ko = Choices [InstrPure H.Id] [ok] ko
-
--- * Type 'Machine'
--- | Making the control-flow explicit.
-data Machine inp v = Machine { unMachine ::
- forall vs es ret.
- {-k-}Instr inp (v ': vs) ('Succ es) ret ->
- Instr inp vs ('Succ es) ret
- }
-
-runMachine ::
- forall inp v es repr.
- Executable repr =>
- Readable repr (InputToken inp) =>
- Machine inp v -> repr inp '[] ('Succ es) v
-runMachine (Machine auto) =
- trans @(Instr inp '[] ('Succ es)) $
- auto Ret
-
-instance Applicable (Machine inp) where
- pure x = Machine $ Push (InstrPure x)
- Machine f <*> Machine x = Machine $ f . x . App
- liftA2 f (Machine x) (Machine y) = Machine $
- x . y . LiftI2 (InstrPure f)
- Machine x *> Machine y = Machine $ x . Pop . y
- Machine x <* Machine y = Machine $ x . y . Pop
-instance
- Cursorable (Cursor inp) =>
- Alternable (Machine inp) where
- empty = Machine $ \_k -> Fail []
- Machine l <|> Machine r = Machine $ \k ->
- makeJoin k $ \j ->
- CatchFail
- (l (PopFail j))
- (failIfConsumed (r j))
- try (Machine x) = Machine $ \k ->
- CatchFail (x (PopFail k))
- -- On exception, reset the input,
- -- and propagate the failure.
- (LoadInput (Fail []))
-
--- | If no input has been consumed by the failing alternative
--- then continue with the given continuation.
--- Otherwise, propagate the 'Fail'ure.
-failIfConsumed ::
- Cursorable (Cursor inp) =>
- Instr inp vs ('Succ es) ret ->
- Instr inp (Cursor inp : vs) ('Succ es) ret
-failIfConsumed k = PushInput (LiftI2 (InstrPureSameOffset sameOffset) (If k (Fail [])))
-
--- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
--- by introducing a 'DefJoin' if necessary,
--- and passing the corresponding 'RefJoin' to @(f)@,
--- or @(k)@ as is when factorizing is useless.
-makeJoin ::
- Instr inp (v : vs) es ret ->
- (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
- Instr inp vs es ret
--- Double RefJoin Optimization:
--- If a join-node points directly to another join-node,
--- then reuse it
-makeJoin k@RefJoin{} = ($ k)
--- Terminal RefJoin Optimization:
--- If a join-node points directly to a terminal operation,
--- then it's useless to introduce a join-point.
-makeJoin k@Ret = ($ k)
-makeJoin k =
- let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
- \f -> DefJoin joinName k (f (RefJoin joinName))
-
-instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
- satisfy es p = Machine $ Read es (InstrPure p)
-instance Selectable (Machine inp) where
- branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
- makeJoin k $ \j ->
- lr (Case (l (Swap (App j)))
- (r (Swap (App j))))
-instance Matchable (Machine inp) where
- conditional ps bs (Machine m) (Machine default_) = Machine $ \k ->
- makeJoin k $ \j ->
- m (Choices (InstrPure Functor.<$> ps)
- ((\b -> unMachine b j) Functor.<$> bs)
- (default_ j))
-instance
- ( Ord (InputToken inp)
- , Cursorable (Cursor inp)
- ) => Lookable (Machine inp) where
- look (Machine x) = Machine $ \k ->
- PushInput (x (Swap (LoadInput k)))
- eof = negLook (satisfy [{-discarded by negLook-}] (H.const H..@ H.bool True))
- -- Set a better failure message
- <|> (Machine $ \_k -> Fail [ErrorItemEnd])
- negLook (Machine x) = Machine $ \k ->
- CatchFail
- -- On x success, discard the result,
- -- and replace this 'CatchFail''s failure handler
- -- by a 'Fail'ure whose 'farthestExpecting' is negated,
- -- then a failure is raised from the input
- -- when entering 'negLook', to avoid odd cases:
- -- - where the failure that made (negLook x)
- -- succeed can get the blame for the overall
- -- failure of the grammar.
- -- - where the overall failure of
- -- the grammar might be blamed on something in x
- -- that, if corrected, still makes x succeed and
- -- (negLook x) fail.
- (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
- -- On x failure, reset the input,
- -- and go on with the next 'Instr'uctions.
- (LoadInput (Push (InstrPure H.unit) k))
-instance Letable TH.Name (Machine inp) where
- def n v = Machine $ \k ->
- Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
- ref _isRec n = Machine $ \case
- Ret -> Jump (LetName n)
- k -> Call (LetName n) k
-instance Cursorable (Cursor inp) => Foldable (Machine inp) where
- {-
- chainPre op p = go <*> p
- where go = (H..) <$> op <*> go <|> pure H.id
- chainPost p op = p <**> go
- where go = (H..) <$> op <*> go <|> pure H.id
- -}
+ TermInstr (tok -> Bool) ->
+ repr inp (tok ': vs) a ->
+ repr inp vs a
sourcephile / git / haskell / symantic-parser.git / blobdiff