SParser.idr

module SParser

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)

Rule : Bool -> Type -> Type
Rule c ty = SParser () Char c ty

-- match : (Eq k, TokType k) => (kind : k) -> Rule True (TokType kind)
-- match p = lift $ mapToken match p -- mapToken tok (match p)

data SToken : Type where
  AddOp : SToken
  MulOp : SToken
  IntConst : SToken
  LP : SToken
  RP : SToken

TokenKind SToken where
  TokType IntConst = Integer
  TokType AddOp = ()
  TokType MulOp = ()
  TokType LP = ()
  TokType RP = ()

  tokValue IntConst s = (cast s)
  tokValue AddOp _ = ()
  tokValue MulOp _ = ()
  tokValue LP _ = ()
  tokValue RP _ = ()

Eq SToken where
  (==) AddOp AddOp = True
  (==) MulOp MulOp = True
  (==) IntConst IntConst = True
  (==) LP LP = True
  (==) RP RP = True
  (==) _ _ = False

-- namespace Expr
--   data Expr : Type where
--     IntConst : Integer -> Expr
--     Add : Expr -> Expr -> Expr
--     Mul : Expr -> Expr -> Expr

-- gchainl1 : Grammar t True (a -> a -> a) -> Grammar t True a -> Grammar t True a
-- gchainl1 op p = p >>= rest op p
--   where rest : Grammar t True (a -> a -> a) -> Grammar t True a -> (a -> Grammar t False a)
--         rest op p a = (do f <- op
--                           b <- p
--                           rest op p (f a b)) <|> pure a

-- intConst : Grammar (TokenData (Token SToken)) True Integer
-- intConst = do i <- mapToken tok $ match SParser.IntConst
--               pure i

-- mutual
--   factor : Grammar (TokenData (Token SToken)) True Expr
--   factor = (do i <- intConst
--                pure (IntConst i)) <|> (between (mapToken tok $ match LP) (mapToken tok $ match RP) expr)

--   mulOp : Grammar (TokenData (Token SToken)) True (Expr -> Expr -> Expr)
--   mulOp = mapToken tok $ match MulOp *> pure Mul

--   term : Grammar (TokenData (Token SToken)) True Expr
--   term = gchainl1 mulOp factor

--   addOp : Grammar (TokenData (Token SToken)) True (Expr -> Expr -> Expr)
--   addOp = mapToken tok $ match AddOp *> pure Add

--   expr : Grammar (TokenData (Token SToken)) True Expr
--   expr = gchainl1 addOp term

-- test : IO ()
-- test = case (parse expr [ MkToken 0 0 (Tok IntConst "123")
--                         , MkToken 0 5 (Tok AddOp "+")
--                         , MkToken 0 7 (Tok IntConst "345")
--                         ]) of
--             Left l => print "fail"
--             Right (t, _) => print "success"


data Operator = Add | Mul

Eq Operator where
  Add == Add = True
  Mul == Mul = True
  _ == _ = False

data Bracket = Open | Close

Eq Bracket where
  Open == Open = True
  Close == Close = True
  _ == _ = False

data MToken = IntLiteral |
              Paren Bracket |
              Op Operator |
              Ignored

Eq MToken where
  IntLiteral == IntLiteral = True
  (Paren a) == (Paren b) = a == b
  (Op a) == (Op b) = a == b
  _ == _ = False

TokenKind MToken where
  TokType IntLiteral = Integer
  TokType (Paren _) = ()
  TokType (Op _) = ()
  TokType Ignored = ()

  tokValue IntLiteral str = cast str
  tokValue (Paren _) _ = ()
  tokValue (Op _) _ = ()
  tokValue Ignored _ = ()


data Expr = Constant Integer |
            Binary Operator Expr Expr

MRule : Type -> Type
MRule ty = Grammar (Token MToken) True ty


intLiteral : MRule Expr
intLiteral = do v <- match IntLiteral
                pure $ Constant v

mutual
  factor : MRule Expr
  factor = intLiteral <|>
           do match (Paren Open)
              commit
              res <- expr
              match (Paren Close)
              pure res

  term : MRule Expr
  term = do x <- factor
            (do match (Op Mul)
                commit
                y <- term
                pure $ Binary Mul x y) <|> pure x

  expr : MRule Expr
  expr = do x <- term
            (do match (Op Add)
                commit
                y <- expr
                pure $ Binary Add x y) <|> pure x

test : IO ()
test = case (parse expr [ Tok IntLiteral "123"
                        , Tok (Op Add) "+"
                        , Tok IntLiteral "345"
                        ]) of
            Left l => print "fail"
            Right (t, _) => print "success"