    {-# LANGUAGE CPP #-}

    {-| common
    -}

    module Agda.Compiler.Agate.Common where

    #include "../../undefined.h"
    import Agda.Utils.Impossible

    import Control.Monad

    import Agda.Compiler.Agate.TranslateName

    import Agda.Syntax.Common
    import Agda.Syntax.Literal
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Pretty
    import Agda.Utils.Monad

    ----------------------------------------------------------------

    psep :: [Doc] -> Doc
    psep [x] = x
    psep xs = parens $ sep xs

    dropArgs :: Int -> Type -> TCM Type
    dropArgs n (El s t) = dropArgsTm s n t
        where
    	dropArgsTm s 0 t = return (El s t)
    	dropArgsTm _ n t = do
    	    t <- reduce t
    	    case t of
    		Pi arg abs  -> dropArgs (n - 1) $ absBody abs
    		Fun arg ty  -> dropArgs (n - 1) ty
    		Var _ _	    -> __IMPOSSIBLE__
    		Def _ _	    -> __IMPOSSIBLE__
    		Con _ _	    -> __IMPOSSIBLE__
    		MetaV _ _   -> __IMPOSSIBLE__
    		Lam _ _	    -> __IMPOSSIBLE__
    		Sort _	    -> __IMPOSSIBLE__
    		Lit _	    -> __IMPOSSIBLE__

    withFunctionDomain :: Type -> (Type -> TCM a) -> ([a] -> Type -> TCM b) -> TCM b
    withFunctionDomain (El s tm) f ret = withDomain s tm
        where
    	withDomain s tm = do
    	    tm <- reduce tm
    	    case tm of
    		Pi arg abs -> do
    		    res	    <- f $ unArg arg
    		    underAbstraction arg abs $ \ty ->
    			withFunctionDomain ty f $ \ress ty ->
    			ret (res : ress) ty
    		Fun arg ty -> do
    		    res  <- f $ unArg arg
    		    withFunctionDomain ty f $ \ress ty ->
    			ret (res : ress) ty
    		Var _ _    -> ret [] (El s tm)
    		Def _ _    -> ret [] (El s tm)
    		Con _ _    -> ret [] (El s tm)
    		Sort _	   -> ret [] (El s tm)
    		Lit _	   -> __IMPOSSIBLE__
    		MetaV _ _  -> __IMPOSSIBLE__
    		Lam _ _	   -> __IMPOSSIBLE__

    splitType :: Type -> TCM ([Type], Type)
    splitType ty = withFunctionDomain ty return $ \tys ty -> return (tys,ty)

    forEachArgM :: (Type -> TCM a) -> Type -> TCM [a]
    forEachArgM f ty = withFunctionDomain ty f $ \ress _ -> return ress

    underContext :: Type -> TCM a -> TCM a
    underContext ty k = withFunctionDomain ty return $ \_ _ -> k

    --

    showOptimizedLiteral :: Literal -> Doc
    showOptimizedLiteral (LitLevel  _ i) = text $ show i
    showOptimizedLiteral (LitInt    _ i) = text $ show i
    showOptimizedLiteral (LitString _ s) = text $ show s
    showOptimizedLiteral (LitFloat  _ f) = text $ show f
    showOptimizedLiteral (LitChar   _ c) = text $ show c

    showUntypedLiteral :: Literal -> Doc
    showUntypedLiteral (LitLevel  _ i) = text "VInt"    <+> text (show i)
    showUntypedLiteral (LitInt    _ i) = text "VInt"    <+> text (show i)
    showUntypedLiteral (LitString _ s) = text "VString" <+> text (show s)
    showUntypedLiteral (LitFloat  _ f) = text "VFloat"  <+> text (show f)
    showUntypedLiteral (LitChar   _ c) = text "VChar"   <+> text (show c)

    showClause :: (Term -> TCM Doc) ->
    	      (QName -> [Doc] -> TCM Doc) ->
    	      ([Doc] -> Term -> TCM Doc) -> Clause -> TCM Doc
    showClause fTerm fCon fBody (Clause{ clauseBody = NoBody }) = return empty
    showClause fTerm fCon fBody (Clause{ clausePats = pats, clauseBody = body })   = go 0 [] body
        where
        go :: Int -> [Doc] -> ClauseBody -> TCM Doc
        go n dvars NoBody        = return empty
        go n dvars (NoBind body) = go n (dvars ++ [text "_"]) body
        go n dvars (Bind abs)    =
    	underAbstraction_ abs{absName = show (n + 1)} $ \body -> do
    	    dvar <- fTerm $ Var 0 []
    	    go (n + 1) (dvars ++ [dvar]) body
        go n dvars (Body term)   = do
    	(_,dpats) <- showPatterns dvars $ map unArg pats
    	fBody dpats term

        showPatterns :: [Doc] -> [Pattern] -> TCM ([Doc], [Doc])
        showPatterns dvars []           = return (dvars,[])
        showPatterns dvars (pat : pats) = do
    	(dvars', dpat)  <- showPattern  dvars  pat
    	(dvars'',dpats) <- showPatterns dvars' pats
    	return (dvars'', (dpat : dpats))

        showPattern :: [Doc] -> Pattern -> TCM ([Doc], Doc)
        showPattern (dvar : dvars) (VarP s) = return (dvars, dvar)
        showPattern []             (VarP s) = __IMPOSSIBLE__
        showPattern (dvar : dvars) (DotP _) = return (dvars, dvar)
        showPattern []             (DotP _) = __IMPOSSIBLE__
        showPattern dvars (ConP name args) = do
    	(dvars',dargs) <- showPatterns dvars (map unArg args)
    	dcon <- fCon name dargs
    	return (dvars', dcon)
        showPattern dvars (LitP lit) = do
    	dlit <- fTerm $ Lit lit
    	return (dvars, dlit)

    --