-{-# LANGUAGE ConstraintKinds #-} -- For Executable
+{-# LANGUAGE ConstraintKinds #-} -- For Machine
+{-# LANGUAGE DeriveLift #-} -- For TH.Lift (Failure tok)
{-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
+-- | 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.Maybe (Maybe(..))
import Data.Function ((.))
-import Data.Kind (Constraint, Type)
-import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
+import Data.Kind (Type)
+import Data.Set (Set)
import Text.Show (Show(..))
-import qualified Data.Functor as Functor
+import Data.String (String)
import qualified Language.Haskell.TH as TH
-import qualified Symantic.Parser.Haskell as H
import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input
-import Symantic.Univariant.Trans
+import qualified Symantic.Lang as Prod
+import qualified Symantic.Data as Sym
--- * Type 'TermInstr'
-type TermInstr = H.Term TH.CodeQ
+-- * Type 'Splice'
+type Splice = Sym.SomeData TH.CodeQ
--- * Type 'Peano'
--- | Type-level natural numbers,
--- using the Peano recursive encoding.
-data Peano = Zero | Succ Peano
-
--- * Class 'Executable'
--- | All the 'Instr'uctions.
-type Executable tok repr =
- ( Branchable repr
- , Failable repr
- , Inputable repr
- , Joinable repr
- , Routinable repr
- , Stackable repr
- , Readable tok repr
- )
-
--- * Data family 'Instr'
--- | 'Instr'uctions for the 'Machine'.
--- This is an extensible data-type.
-data family Instr
- (instr :: ReprInstr -> Constraint)
- (repr :: ReprInstr)
- :: ReprInstr
-
--- | @(isInstr @instr i)@ returns a proof
--- that @(i)@ is within the extension @(instr)@
--- of the 'Instr' data-type, or 'Nothing' if it is not.
-isInstr ::
- forall (instr0 :: ReprInstr -> Constraint) instr1 repr inp vs es a.
- Typeable instr0 =>
- Typeable instr1 =>
- Instr instr1 repr inp vs es a -> Maybe (instr0:~~:instr1)
-isInstr _i = eqTypeRep (typeRep @instr0) (typeRep @instr1)
+-- | Lift a 'TH.CodeQ' into a 'Sym.SomeData'.
+splice :: TH.CodeQ a -> Splice a
+splice x = Sym.SomeData (Sym.Var x)
-- ** Type 'ReprInstr'
-type ReprInstr = Type -> [Type] -> Peano -> Type -> Type
-
--- ** Type 'SomeInstr'
--- | Some 'Instr'uction existentialized over the actual instruction data-type.
--- Useful to handle a list of 'Instr'uctions
--- without requiring impredicative quantification.
--- Must be used by pattern-matching
--- on the 'SomeInstr' data-constructor,
--- to bring the constraints in scope.
-data SomeInstr repr inp vs es a =
- forall instr.
- (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
- SomeInstr (Instr instr repr inp vs es a)
-
-instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
- trans (SomeInstr x) = trans x
+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 Eq
deriving newtype Show
--- ** Class 'Stackable'
-class Stackable (repr::ReprInstr) where
- push ::
- TermInstr 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 ::
- TermInstr (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
-data instance Instr Stackable repr inp vs fs a where
- -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
+-- ** Class 'InstrComment'
+class InstrComment (repr::ReprInstr) where
+ comment :: String -> repr inp vs a -> repr inp vs a
+
+-- ** Class 'InstrValuable'
+class InstrValuable (repr::ReprInstr) where
+ -- | @('pushValue' x k)@ pushes @(x)@ on the 'valueStack'
-- and continues with the next 'Instr'uction @(k)@.
- Push ::
- TermInstr v ->
- SomeInstr repr inp (v ': vs) es a ->
- Instr Stackable repr inp vs es a
- -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
- Pop ::
- SomeInstr repr inp vs es a ->
- Instr Stackable repr inp (v ': vs) es a
- -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
+ pushValue ::
+ Splice v ->
+ repr inp (v ': vs) a ->
+ repr inp vs a
+ -- | @('popValue' k)@ pushes @(x)@ on the 'valueStack'.
+ popValue ::
+ repr inp vs a ->
+ repr inp (v ': vs) a
+ -- | @('lift2Value' f k)@ pops two values from the 'valueStack',
-- and pushes the result of @(f)@ applied to them.
- LiftI2 ::
- TermInstr (x -> y -> z) ->
- SomeInstr repr inp (z : vs) es a ->
- Instr Stackable repr inp (y : x : vs) es a
- -- | @('Swap' k)@ pops two values on the 'valueStack',
+ lift2Value ::
+ Splice (x -> y -> z) ->
+ repr inp (z ': vs) a ->
+ repr inp (y ': x ': vs) a
+ -- | @('swapValue' k)@ pops two values on the 'valueStack',
-- pushes the first popped-out, then the second,
-- and continues with the next 'Instr'uction @(k)@.
- Swap ::
- SomeInstr repr inp (x ': y ': vs) es a ->
- Instr Stackable repr inp (y ': x ': vs) es a
-instance Stackable repr => Trans (Instr Stackable repr 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)
- Swap k -> swap (trans k)
-instance Stackable repr => Stackable (SomeInstr repr) where
- push v = SomeInstr . Push v
- pop = SomeInstr . Pop
- liftI2 f = SomeInstr . LiftI2 f
- swap = SomeInstr . Swap
-
--- | @('mapI' f k)@.
-mapI ::
- Stackable repr =>
- TermInstr (x -> y) ->
- SomeInstr repr inp (y ': vs) es ret ->
- SomeInstr repr inp (x ': vs) es ret
-mapI f = push f . liftI2 (H.flip H..@ (H.$))
-
--- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
--- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
-appI ::
- Stackable repr =>
- SomeInstr repr inp (y ': vs) es a ->
- SomeInstr repr inp (x ': (x -> y) ': vs) es a
-appI = liftI2 (H.$)
-
--- ** Class 'Routinable'
-class Routinable (repr::ReprInstr) where
- subroutine ::
- LetName v -> repr inp '[] ('Succ 'Zero) v ->
- repr inp vs ('Succ es) ret ->
- repr inp vs ('Succ es) ret
+ swapValue ::
+ repr inp (x ': y ': vs) a ->
+ repr inp (y ': x ': vs) a
+ -- | @('mapValue' f k)@.
+ mapValue ::
+ Splice (x -> y) ->
+ repr inp (y ': vs) a ->
+ repr inp (x ': vs) a
+ mapValue f = pushValue f . lift2Value (Prod.flip Prod..@ (Prod.$))
+ -- | @('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 (Prod.$)
+
+-- ** Class 'InstrExceptionable'
+class InstrExceptionable (repr::ReprInstr) where
+ -- | @('raise' exn)@ raises 'ExceptionLabel' @(exn)@.
+ raise :: ExceptionLabel -> repr inp vs a
+ -- | @('fail' fs)@ raises 'ExceptionFailure' @(exn)@.
+ -- As a special case, giving an empty 'Set' of failures
+ -- raises 'ExceptionFailure' without using the current position
+ -- to update the farthest error.
+ fail :: Set SomeFailure -> repr inp vs a
+ -- | @('commit' exn k)@ removes the 'Catcher'
+ -- from the 'onExceptionStackByLabel' for the given 'Exception' @(exn)@,
+ -- and continues with the next 'Instr'uction @(k)@.
+ commit :: Exception -> repr inp vs a -> repr inp vs a
+ -- | @('catch' exn l r)@ tries the @(l)@ 'Instr'uction
+ -- in a new failure scope such that if @(l)@ raises an exception within @(exn)@, it is caught,
+ -- then the input (and its 'Horizon') is pushed
+ -- as it was before trying @(l)@ on the 'valueStack' (resp. on the 'horizonStack'),
+ -- and the control flow goes on with the @(r)@ 'Instr'uction.
+ catch ::
+ Exception ->
+ {-scope-}repr inp vs ret ->
+ {-onException-}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 ::
+ [(Splice (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 [(Prod.id, ok)] ko
+
+-- ** Class 'InstrCallable'
+class InstrCallable (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)@.
+ defLet ::
+ LetBindings TH.Name (repr inp '[]) ->
+ repr inp vs a ->
+ repr inp vs a
+ -- | @('call' isRec 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 -> repr inp (v ': vs) ('Succ es) ret ->
- repr inp vs ('Succ es) ret
+ Bool ->
+ 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' isRec n k)@ pass the control-flow to the 'DefLet' named @(n)@.
jump ::
- LetName ret ->
- repr inp '[] ('Succ es) ret
-data instance Instr Routinable repr inp vs fs a where
- -- | @('Subroutine' 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 -> SomeInstr repr inp '[] ('Succ 'Zero) v ->
- SomeInstr repr inp vs ('Succ es) a ->
- Instr Routinable repr inp vs ('Succ es) a
- -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
- Jump ::
+ Bool ->
LetName a ->
- Instr Routinable repr inp '[] ('Succ es) a
- -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
- -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
- Call ::
- LetName v ->
- SomeInstr repr inp (v ': vs) ('Succ es) a ->
- Instr Routinable repr inp vs ('Succ es) a
- -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
- Ret ::
- Instr Routinable repr inp '[a] es a
-instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
- trans = \case
- Subroutine n sub k -> subroutine n (trans sub) (trans k)
- Jump n -> jump n
- Call n k -> call n (trans k)
- Ret -> ret
-instance Routinable repr => Routinable (SomeInstr repr) where
- subroutine n sub = SomeInstr . Subroutine n sub
- jump = SomeInstr . Jump
- call n = SomeInstr . Call n
- ret = SomeInstr Ret
-
--- ** Class 'Branchable'
-class Branchable (repr::ReprInstr) where
- caseI ::
- repr inp (x ': vs) n r ->
- repr inp (y ': vs) n r ->
- repr inp (Either x y ': vs) n r
- choices ::
- [TermInstr (v -> Bool)] ->
- [repr inp vs es ret] ->
- repr inp vs es ret ->
- repr inp (v ': vs) es ret
-data instance Instr Branchable repr inp vs fs a where
- -- | @('Case' l r)@.
- Case ::
- SomeInstr repr inp (x ': vs) es a ->
- SomeInstr repr inp (y ': vs) es a ->
- Instr Branchable repr inp (Either x y ': vs) es a
- -- | @('Choices' ps bs d)@.
- Choices ::
- [TermInstr (v -> Bool)] ->
- [SomeInstr repr inp vs es a] ->
- SomeInstr repr inp vs es a ->
- Instr Branchable repr inp (v ': vs) es a
-instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
- trans = \case
- Case l r -> caseI (trans l) (trans r)
- Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
-instance Branchable repr => Branchable (SomeInstr repr) where
- caseI l = SomeInstr . Case l
- choices ps bs = SomeInstr . Choices ps bs
-
--- | @('ifI' ok ko)@ pops a 'Bool' from the 'valueStack'
--- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
--- or @(ko)@ otherwise.
-ifI ::
- Branchable repr =>
- SomeInstr repr inp vs es a ->
- SomeInstr repr inp vs es a ->
- SomeInstr repr inp (Bool ': vs) es a
-ifI ok ko = SomeInstr (Choices [H.id] [ok] ko)
-
--- ** Class 'Failable'
-class Failable (repr::ReprInstr) 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
-data instance Instr Failable repr inp vs fs a where
- -- | @('Fail')@ raises an error from the 'failStack'.
- Fail ::
- [ErrorItem (InputToken inp)] ->
- Instr Failable repr inp vs ('Succ es) a
- -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
- -- and continues with the next 'Instr'uction @(k)@.
- PopFail ::
- SomeInstr repr inp vs es ret ->
- Instr Failable repr inp vs ('Succ es) ret
- -- | @('CatchFail' 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 ::
- SomeInstr repr inp vs ('Succ es) ret ->
- SomeInstr repr inp (Cursor inp ': vs) es ret ->
- Instr Failable repr inp vs es ret
-instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
- trans = \case
- Fail err -> fail err
- PopFail k -> popFail (trans k)
- CatchFail l r -> catchFail (trans l) (trans r)
-instance Failable repr => Failable (SomeInstr repr) where
- fail = SomeInstr . Fail
- popFail = SomeInstr . PopFail
- catchFail x = SomeInstr . CatchFail x
-
--- ** Class 'Inputable'
-class Inputable (repr::ReprInstr) where
- loadInput ::
- repr inp vs es a ->
- repr inp (Cursor inp ': vs) es a
- pushInput ::
- repr inp (Cursor inp ': vs) es a ->
- repr inp vs es a
-data instance Instr Inputable repr inp vs fs a where
- -- | @('LoadInput' k)@ removes the input from the 'valueStack'
- -- and continues with the next 'Instr'uction @(k)@ using that input.
- LoadInput ::
- SomeInstr repr inp vs es a ->
- Instr Inputable repr inp (Cursor inp : vs) es a
- -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
- -- and continues with the next 'Instr'uction @(k)@.
- PushInput ::
- SomeInstr repr inp (Cursor inp ': vs) es a ->
- Instr Inputable repr inp vs es a
-instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
- trans = \case
- LoadInput k -> loadInput (trans k)
- PushInput k -> pushInput (trans k)
-instance Inputable repr => Inputable (SomeInstr repr) where
- loadInput = SomeInstr . LoadInput
- pushInput = SomeInstr . PushInput
+ repr inp '[] a
--- ** Class 'Joinable'
-class Joinable (repr::ReprInstr) where
+-- ** Class 'InstrJoinable'
+class InstrJoinable (repr::ReprInstr) where
defJoin ::
- LetName v ->
- repr inp (v ': vs) es a ->
- repr inp vs es a ->
- repr inp vs es a
+ LetName v -> repr inp (v ': vs) a ->
+ repr inp vs a ->
+ repr inp vs a
refJoin ::
LetName v ->
- repr inp (v ': vs) es a
-data instance Instr Joinable repr inp vs fs a where
- DefJoin ::
- LetName v -> SomeInstr repr inp (v ': vs) es a ->
- SomeInstr repr inp vs es a ->
- Instr Joinable repr inp vs es a
- RefJoin ::
- LetName v ->
- Instr Joinable repr inp (v ': vs) es a
-instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
- trans = \case
- DefJoin n sub k -> defJoin n (trans sub) (trans k)
- RefJoin n -> refJoin n
-instance Joinable repr => Joinable (SomeInstr repr) where
- defJoin n sub = SomeInstr . DefJoin n sub
- refJoin = SomeInstr . RefJoin
+ repr inp (v ': vs) a
--- ** Class 'Readable'
-class Readable (tok::Type) (repr::ReprInstr) where
+-- ** Class 'InstrInputable'
+class InstrInputable (repr::ReprInstr) where
+ -- | @('saveInput' k)@ pushes the input @(inp)@ on the 'valueStackHead'
+ -- and continues with the next 'Instr'uction @(k)@.
+ saveInput ::
+ repr inp (Cursor inp ': vs) a ->
+ repr inp vs a
+ -- | @('loadInput' k)@ removes the input from the 'valueStackHead'
+ -- and continues with the next 'Instr'uction @(k)@ using that input.
+ loadInput ::
+ repr inp vs a ->
+ repr inp (Cursor inp ': vs) a
+
+-- ** Class 'InstrReadable'
+class InstrReadable (tok::Type) (repr::ReprInstr) where
+ -- | @('read' fs p k)@ reads a 'Char' @(c)@ from the input,
+ -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@,
+ -- otherwise 'fail'.
read ::
tok ~ InputToken inp =>
- [ErrorItem tok] ->
- TermInstr (tok -> Bool) ->
- repr inp (tok ': vs) ('Succ es) ret ->
- repr inp vs ('Succ es) ret
-data instance Instr (Readable tok) repr inp vs fs a 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 'Fail'.
- Read ::
- [ErrorItem (InputToken inp)] ->
- TermInstr (InputToken inp -> Bool) ->
- SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
- Instr (Readable tok) repr inp vs ('Succ es) a
-instance
- ( Readable tok repr, tok ~ InputToken inp ) =>
- Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
- trans = \case
- Read es p k -> read es p (trans k)
-instance
- ( Readable tok repr, Typeable tok ) =>
- Readable tok (SomeInstr repr) where
- read es p = SomeInstr . Read es p
+ Set SomeFailure ->
+ Splice (tok -> Bool) ->
+ repr inp (tok ': vs) a ->
+ repr inp vs a
+
+-- ** Class 'InstrIterable'
+class InstrIterable (repr::ReprInstr) where
+ -- | @('iter' loop done)@.
+ iter ::
+ LetName a ->
+ repr inp '[] a ->
+ repr inp (Cursor inp ': vs) a ->
+ repr inp vs a
+
+-- ** Class 'InstrRegisterable'
+class InstrRegisterable (repr::ReprInstr) where
+ newRegister ::
+ UnscopedRegister v ->
+ repr inp vs a ->
+ repr inp (v : vs) a
+ readRegister ::
+ UnscopedRegister v ->
+ repr inp (v : vs) a ->
+ repr inp vs a
+ writeRegister ::
+ UnscopedRegister v ->
+ repr inp vs a ->
+ repr inp (v : vs) a
+
+-- | @('modifyRegister' reg k)@
+-- modifies the content of register @(reg)@
+-- with the function at the 'valueStackHead',
+-- then continues with @(k)@.
+modifyRegister ::
+ InstrRegisterable repr =>
+ InstrValuable repr =>
+ UnscopedRegister v -> repr inp vs a -> repr inp ((v -> v) : vs) a
+modifyRegister r = readRegister r . applyValue . writeRegister r
sourcephile / git / haskell / symantic-parser.git / blobdiff