{-# LANGUAGE UndecidableInstances #-} module Data.Type.Symbol.Parser.Parser.Take ( Take ) where import Data.Type.Symbol.Parser.Types import Data.Type.Symbol.Parser.Common import GHC.TypeLits import DeFun.Core ( type (~>), type App ) type Take :: Natural -> Parser (Natural, [Char]) Symbol type family Take n where Take 0 = '( FailChSym "Take" (ErrParserLimitation "can't take 0") , TakeEndSym, '(0, '[])) Take n = '(TakeChSym, TakeEndSym, '(n, '[])) type TakeCh :: ParserCh (Natural, [Char]) Symbol type family TakeCh ch s where TakeCh ch '(1, chs) = Done (RevCharsToSymbol (ch : chs)) TakeCh ch '(n, chs) = Cont '(n-1, ch : chs) type TakeEnd :: ParserEnd (Natural, [Char]) Symbol type family TakeEnd s where TakeEnd '(0, chs) = Right (RevCharsToSymbol chs) TakeEnd '(n, _) = Left (EBase "Take" ( Text "tried to take " :<>: ShowType n :<>: Text " chars from empty symbol")) type RevCharsToSymbol chs = RevCharsToSymbol' "" chs type family RevCharsToSymbol' sym chs where RevCharsToSymbol' sym '[] = sym RevCharsToSymbol' sym (ch : chs) = RevCharsToSymbol' (ConsSymbol ch sym) chs type TakeChSym :: ParserChSym (Natural, [Char]) Symbol data TakeChSym f type instance App TakeChSym f = TakeChSym1 f type TakeChSym1 :: Char -> (Natural, [Char]) ~> Result (Natural, [Char]) Symbol data TakeChSym1 ch s type instance App (TakeChSym1 ch) s = TakeCh ch s type TakeEndSym :: ParserEndSym (Natural, [Char]) Symbol data TakeEndSym s type instance App TakeEndSym s = TakeEnd s