State over Grammar

SParser.idr

module Danac.Parser

import Danac.Lexer
import Text.Lexer
import Text.Parser

data SParser : Type -> Type -> Bool -> Type -> Type where
  MkSParser : (s -> Grammar t c (a, s)) -> SParser s t c a

Functor (SParser s t b) where
  map f (MkSParser g) = MkSParser $ \s => map (\(v,s) => (f v, s)) (g s)

runSParser : SParser s t c a -> s -> Grammar t c (a, s)
runSParser (MkSParser x) y = x y

helper : (a -> SParser s t c2 b) -> (a,s) -> Grammar t c2 (b, s)
helper f (a, b) = runSParser (f a) b

(>>=) : SParser s t c1 a -> inf c1 (a -> SParser s t c2 b) -> SParser s t (c1 || c2) b
(>>=) {c1 = False} p f = MkSParser $ \s => (runSParser p s) >>= (\a => helper f a)
(>>=) {c1 = True} p (Delay f) = MkSParser $ \s => (runSParser p s) >>= (\a => helper f a)

(<|>) : SParser s t c1 a -> SParser s t c2 a -> SParser s t (c1 && c2) a
(<|>) p1 p2 = MkSParser $ \s => runSParser p1 s <|> runSParser p2 s

(<*>) : SParser s t c1 (a -> b) -> SParser s t c2 a -> SParser s t (c1 || c2) b
(<*>) p1 p2 = MkSParser $ \s => seq (runSParser p1 s) (\(f,s1) => runSParser (map f p2) s1)

(<*) : SParser s t c1 a -> SParser s t c2 b -> SParser s t (c1 || c2) a
(<*) p1 p2 = map const p1 <*> p2

(*>) : SParser s t c1 a -> SParser s t c2 b -> SParser s t (c1 || c2) b
(*>) p1 p2 = map (const id) p1 <*> p2

pure : a -> SParser s t False a
pure a = MkSParser $ \s => pure (a, s)

lift : Grammar t c a -> SParser s t c a
lift g = MkSParser $ \s => map (\v => (v, s)) g

gets : (s -> a) -> SParser s t False a
gets f = MkSParser $ \s => pure (f s, s)

get : SParser s t False s
get = gets id

puts : (s -> s) -> SParser s t False ()
puts f = MkSParser $ \s => pure ((), f s)

put : s -> SParser s t False ()
put s = puts (const s)

ext : SParser s t b a -> SParser s t False (Grammar t b a)
ext p = MkSParser $ \s => pure (map Basics.fst (runSParser p s), s)

match : (t : Token) -> Rule True (TokType t)
match p = lift $ mapToken tok (match p)