-{-# 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,
import Data.Eq (Eq(..))
import Data.Function ((.))
import Data.Kind (Type)
--- import GHC.TypeLits (Symbol)
+import Data.Set (Set)
import Text.Show (Show(..))
import qualified Language.Haskell.TH as TH
-import qualified Symantic.Parser.Haskell as H
import Symantic.Parser.Grammar
import Symantic.Parser.Machine.Input
+import qualified Symantic.Typed.Lang as Prod
+import qualified Symantic.Typed.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
- )
+-- | 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 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 a ->
- repr inp vs n a
- pop ::
- repr inp vs n a ->
- repr inp (v ': vs) n a
- liftI2 ::
- TermInstr (x -> y -> z) ->
- repr inp (z ': vs) es a ->
- repr inp (y ': x ': vs) es a
- swap ::
- repr inp (x ': y ': vs) n r ->
- repr inp (y ': x ': vs) n r
- -- | @('mapI' f k)@.
- mapI ::
- TermInstr (x -> y) ->
- repr inp (y ': vs) es a ->
- repr inp (x ': vs) es a
- mapI f = push f . liftI2 (H.flip H..@ (H.$))
- -- | @('appI' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
+-- ** Class 'InstrValuable'
+class InstrValuable (repr::ReprInstr) where
+ -- | @('pushValue' x k)@ pushes @(x)@ on the 'valueStack'
+ -- and continues with the next 'Instr'uction @(k)@.
+ 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.
+ 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)@.
+ 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)@.
- appI ::
- repr inp (y ': vs) es a ->
- repr inp (x ': (x -> y) ': vs) es a
- appI = liftI2 (H.$)
+ applyValue ::
+ repr inp (y ': vs) a ->
+ repr inp (x ': (x -> y) ': vs) a
+ applyValue = lift2Value (Prod.$)
--- ** Class 'Routinable'
-class Routinable (repr::ReprInstr) where
- subroutine ::
- LetName v -> repr inp '[] ('Succ 'Zero) v ->
- repr inp vs ('Succ es) a ->
- repr inp vs ('Succ es) a
- call ::
- LetName v -> repr inp (v ': vs) ('Succ es) a ->
- repr inp vs ('Succ es) a
- ret ::
- repr inp '[a] es a
- jump ::
- LetName a ->
- repr inp '[] ('Succ es) a
+-- ** 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 'catchStackByLabel' 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',
+ -- and the control flow goes on with the @(r)@ 'Instr'uction.
+ catch ::
+ Exception ->
+ {-scope-}repr inp vs ret ->
+ {-catcher-}repr inp (Cursor inp ': vs) ret ->
+ repr inp vs 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 a] ->
- repr inp vs es a ->
- repr inp (v ': vs) es a
- -- | @('ifI' ok ko)@ pops a 'Bool' from the 'valueStack'
+-- ** 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.
- ifI ::
- repr inp vs es a ->
- repr inp vs es a ->
- repr inp (Bool ': vs) es a
- ifI ok ko = choices [H.id] [ok] ko
-
--- ** Class 'Failable'
-class Failable (repr::ReprInstr) where
- fail ::
- [ErrorItem (InputToken inp)] ->
- repr inp vs ('Succ es) a
- popFail ::
- repr inp vs es a ->
- repr inp vs ('Succ es) a
- catchFail ::
- repr inp vs ('Succ es) a ->
- repr inp (Cursor inp ': vs) es a ->
- repr inp vs es a
+ ifBranch ::
+ repr inp vs a ->
+ repr inp vs a ->
+ repr inp (Bool ': vs) a
+ ifBranch ok ko = choicesBranch [Prod.id] [ok] ko
--- ** 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
+-- ** 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' 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) a ->
+ repr inp vs a
+ -- | @('ret')@ returns the value stored in a singleton 'valueStack'.
+ ret ::
+ repr inp '[a] a
+ -- | @('jump' n k)@ pass the control-flow to the 'DefLet' named @(n)@.
+ jump ::
+ LetName a ->
+ 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
+ repr inp (v ': vs) a
+
+-- ** Class 'InstrInputable'
+class InstrInputable (repr::ReprInstr) where
+ -- | @('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
+ -- | @('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
--- ** Class 'Readable'
-class Readable (tok::Type) (repr::ReprInstr) where
+-- ** 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) a ->
- repr inp vs ('Succ es) a
+ Set SomeFailure ->
+ Splice (tok -> Bool) ->
+ repr inp (tok ': vs) a ->
+ repr inp vs a
sourcephile / git / haskell / symantic-parser.git / blobdiff