module Agda.Syntax.Concrete.Operators.Parser where
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Concrete.Name
import Agda.Utils.ReadP
import Agda.Utils.Monad
#include "../../../undefined.h"
import Agda.Utils.Impossible
data ExprView e
= LocalV Name
| OtherV e
| AppV e (NamedArg e)
| OpAppV Name [e]
| HiddenArgV (Named String e)
| ParenV e
deriving (Show)
class HasRange e => IsExpr e where
exprView :: e -> ExprView e
unExprView :: ExprView e -> e
recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok a
recursive f = p0
where
fs = f p0
p0 = foldr ( $ ) p0 fs
partP :: IsExpr e => String -> ReadP e (Range, NamePart)
partP s = do
tok <- get
case isLocal s tok of
Just p -> return p
Nothing -> pfail
where
isLocal x e = case exprView e of
LocalV (Name r [Id y]) | x == y -> Just (r, Id y)
_ -> Nothing
binop :: IsExpr e => ReadP e e -> ReadP e (e -> e -> e)
binop opP = do
OpAppV (Name r ps) es <- exprView <$> opP
return $ \x y -> unExprView $
OpAppV (Name r ([Hole] ++ ps ++ [Hole])) ([x] ++ es ++ [y])
preop :: IsExpr e => ReadP e e -> ReadP e (e -> e)
preop opP = do
OpAppV (Name r ps) es <- exprView <$> opP
return $ \x -> unExprView $
OpAppV (Name r (ps ++ [Hole])) (es ++ [x])
postop :: IsExpr e => ReadP e e -> ReadP e (e -> e)
postop opP = do
OpAppV (Name r ps) es <- exprView <$> opP
return $ \x -> unExprView $
OpAppV (Name r ([Hole] ++ ps)) ([x] ++ es)
opP :: IsExpr e => ReadP e e -> Name -> ReadP e e
opP p (NoName _ _) = pfail
opP p (Name _ xs) = do
(r, ps, es) <- mix [ x | Id x <- xs ]
return $ unExprView $ OpAppV (Name r ps) es
where
mix [] = __IMPOSSIBLE__
mix [x] = do (r, part) <- partP x; return (r, [part], [])
mix (x:xs) = do
(r1, part) <- partP x
e <- p
(r2 , ps, es) <- mix xs
return (fuseRanges r1 r2, part : Hole : ps, e : es)
prefixP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
prefixP op p = do
fs <- many (preop op)
e <- p
return $ foldr ( $ ) e fs
postfixP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
postfixP op p = do
e <- p
fs <- many (postop op)
return $ foldl (flip ( $ )) e fs
infixP, infixrP, infixlP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
infixlP op p = chainl1 p (binop op)
infixrP op p = chainr1 p (binop op)
infixP op p = do
e <- p
f <- restP
return $ f e
where
restP = return id +++ do
f <- binop op
e <- p
return $ flip f e
nonfixP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
nonfixP op p = op +++ p
appP :: IsExpr e => ReadP e e -> ReadP e e -> ReadP e e
appP top p = do
h <- p
es <- many (nothidden +++ hidden)
return $ foldl app h es
where
app e arg = unExprView $ AppV e arg
isHidden (HiddenArgV _) = True
isHidden _ = False
nothidden = Arg NotHidden . unnamed <$> do
e <- p
case exprView e of
HiddenArgV _ -> pfail
_ -> return e
hidden = do
HiddenArgV e <- exprView <$> satisfy (isHidden . exprView)
return $ Arg Hidden e
atomP :: IsExpr e => (Name -> Bool) -> ReadP e e
atomP p = do
e <- get
case exprView e of
LocalV x | not (p x) -> pfail
_ -> return e