{-# LANGUAGE CPP #-}

{-| Generate GHC code for untyped execution
-}

module Agda.Compiler.Agate.UntypedPrinter where

import Data.List

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

import Agda.Compiler.Agate.TranslateName
import Agda.Compiler.Agate.Common
import Agda.Compiler.Agate.OptimizedPrinter

import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.Utils.Pretty

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

showAsUntypedConstructor :: QName -> TCM Doc
showAsUntypedConstructor name =
    return $ text $ translateNameAsUntypedConstructor $ show name

----------------------------------------------------------------
-- implementation of the "X" function

class ShowAsUntypedTerm a where
    showAsUntypedTerm :: a -> TCM Doc

instance ShowAsUntypedTerm Name where
    showAsUntypedTerm t = return $ text $ translateNameAsUntypedTerm $ show t

instance ShowAsUntypedTerm QName where
    showAsUntypedTerm t = return $ text $ translateNameAsUntypedTerm $ show t

instance ShowAsUntypedTerm Term where
    showAsUntypedTerm (Var n args) = do
	varname <- nameOfBV n
	showUntypedApp varname args
    showAsUntypedTerm (Lam h abs) = underAbstraction_ abs $ \body -> do
	dvar <- showAsUntypedTerm $ Var 0 []
	dbody <- showAsUntypedTerm body
	return $ parens $ text "VAbs" <+>
		 parens (sep [ text "\\" <> dvar, text "->", dbody ])
    showAsUntypedTerm (Con name args) = showUntypedApp name args
    showAsUntypedTerm (Def name args) = showUntypedApp name args
    showAsUntypedTerm (Lit lit)    = return $ parens $ showUntypedLiteral lit
    showAsUntypedTerm (Pi _ _)	   = return $ text "VNonData"
    showAsUntypedTerm (Fun _ _)    = return $ text "VNonData"
    showAsUntypedTerm (Sort _)	   = return $ text "VNonData"
    showAsUntypedTerm (MetaV _ _)  = __IMPOSSIBLE__

showUntypedApp :: ShowAsUntypedTerm a => a -> [Arg Term] -> TCM Doc
showUntypedApp head args = do
    dhead <- showAsUntypedTerm head
    dargs <- mapM (showAsUntypedTerm . unArg) args
    return $ foldl (\f a -> parens (f <+> text "|$|" <+> a)) dhead dargs

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

showUntypedDefinition :: (QName, Definition) -> TCM Doc
showUntypedDefinition (name, defn) = do
    dname <- showAsUntypedTerm name
    case theDef defn of
	Axiom{} ->
	    return $ sep [ dname, equals ] <+>
		     sep [ text "undefined {- postulate -}" ]
	Function {funClauses = []} -> __IMPOSSIBLE__
	Function {funClauses = clauses} -> do
            let pats = clausePats $ head clauses
	    let dvars = map (\i -> text ("v" ++ show i)) [1 .. length pats]
	    let drhs = untypedAbs dvars $ sep (text "f" : dvars)
	    dclauses <- mapM showUntypedClause clauses
	    return $ (dname <+> equals) <+> drhs <+> text "where" $+$
		     nest 2 (vcat dclauses)
	Datatype{ dataPars = np, dataIxs = ni, dataCons = cnames } -> do
	    let dvars = map (\i -> text ("v" ++ show i)) [1 .. np + ni]
	    let drhs = untypedAbs dvars $ text "VNonData"
	    return $ sep [ dname, equals ] <+> drhs <+> text "{- datatype -}"
	Record{ recPars = np, recFields = flds } -> do
	    dcname <- showAsUntypedConstructor name
	    let arity = length flds
	    let dvars = map (\i -> text ("v" ++ show i)) [1 .. arity]
	    let drhs = untypedAbs dvars $ sep $
		       text "VCon" <> text (show arity) : dcname : dvars
	    return $ sep [ dname, equals ] <+> drhs
	Constructor{ conPars = np } -> do
	    dcname <- showAsUntypedConstructor name
	    ty <- instantiate $ defType defn
	    (args,_) <- splitType ty
	    let arity = genericLength args - np
	    let dvars = map (\i -> text ("v" ++ show i)) [1 .. arity]
	    let drhs = untypedAbs dvars $ sep $
		       text "VCon" <> text (show arity) : dcname : dvars
	    return $ sep [ dname, equals ] <+> drhs
	Primitive{ primName = pf } -> do
	    doptname <- showAsOptimizedTerm name
	    return $ sep [ dname, equals ] <+>
		     sep [ text "box", doptname, text "{- primitive -}" ]

untypedAbs :: [Doc] -> Doc -> Doc
untypedAbs dvars dtail = foldr
    (\dvar d -> sep [ text "VAbs (\\" <> dvar <+> text "->",
		      d <> text ")" ]) dtail dvars

showUntypedClause :: Clause -> TCM Doc
showUntypedClause = showClause fTerm fCon fBody where
    fTerm = showAsUntypedTerm
    fCon name dargs = do
	dname <- showAsUntypedConstructor name
	return $ parens $ (text "VCon" <> text (show (length dargs))) <+>
			  sep (dname : dargs)
    fBody dpats term = do
	dterm <- showAsUntypedTerm term
	return $ text "f" <+> sep [ sep [ sep dpats, equals ], dterm ]

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