{-# LANGUAGE CPP #-}

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

---------------------------------------------------------------------------
-- * Parser combinators
---------------------------------------------------------------------------

-- | Combining a hierarchy of parsers.
recursive :: (ReadP tok a -> [ReadP tok a -> ReadP tok a]) -> ReadP tok a
recursive f = p0
    where
	fs = f p0
	p0 = foldr ( $ ) p0 fs

-- Specific combinators
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