{-# LANGUAGE CPP #-}

{-| main module.
-}

module Agda.Compiler.Agate.Main where

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

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

import Agda.Syntax.Internal
import Text.PrettyPrint
import Agda.Syntax.Common

import Control.Monad.State
import Control.Monad.Error

import Data.List as List
import qualified Data.Map as Map
import Data.Map (Map)

import Agda.Syntax.Abstract.Name

import Agda.Interaction.Options
import Agda.Interaction.Monad

import Agda.TypeChecker
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce

import Agda.Utils.Monad

import Agda.Version

-- | The main function
compilerMain :: TCM () -> TCM ()
compilerMain typeCheck = do
	typeCheck
	sig <- gets stSignature
	let definitions = sigDefinitions sig
	let defs = Map.toList definitions
	maxconargs <- computeMaxArity definitions
	liftIO $ do
	    putStrLn "{-# OPTIONS -fglasgow-exts -cpp #-}"
	    putStrLn ""
	    putStrLn "-- Generated by Agate 2"
	    putStrLn ""
	    printConstants definitions
	    putStrLn ""
	    putStrLn "data Value = VAbs (Value -> Value)"
	    putStrLn "           | VCon0 !Nat"
	    mapM_ (\k -> putStrLn $ "           | VCon" ++ show k ++ " !Nat"
	 			 ++ concat (genericReplicate k " Value") )
	    	  [1..maxconargs]
	    putStrLn "           | VNonData"
	    putStrLn "           | VIO      !(IO Value)"
	    putStrLn "           | VInt     !Integer"
	    putStrLn "           | VFloat   !Double"
	    putStrLn "           | VString  !String"
	    putStrLn "           | VChar    !Char"
	    putStrLn ""
	    putStrLn "instance Show Value where"
	    putStrLn "  show v = case v of"
	    putStrLn "    VAbs     f     -> \"<func>\""
	    putStrLn "    VCon0    c     -> getConString c"
	    mapM_ (\k -> putStrLn $ "    VCon" ++ show k ++ "    c"
	 			 ++ concatMap (\i -> " a" ++ show i) [1..k]
	 			 ++ "\t-> showCons c [a1"
	 			 ++ concatMap (\i -> ",a" ++ show i) [2..k]
	 			 ++ "]" )
	    	  [1..maxconargs]
	    putStrLn "    VNonData       -> \"<nondata>\""
	    putStrLn "    VIO      m     -> \"<IO>\""
	    putStrLn "    VInt     i     -> show i"
	    putStrLn "    VFloat   f     -> show f"
	    putStrLn "    VString  s     -> show s"
	    putStrLn "    VChar    c     -> show c"
	    putStrLn ""
	    --putStrLn "join sep []     = \"\""
	    --putStrLn "join sep [a]    = a"
	    --putStrLn "join sep (a:as) = a ++ sep ++ join sep as"
	    putStrLn ""
	    putStrLn "showCons c as = \"(\" ++ unwords (getConString c : map show as) ++ \")\""
	    putStrLn "showBind (f,v) = show v"
	    putStrLn ""
	    printShowConstants definitions
	    putStrLn "getConString c = show c"
	    putStrLn ""
    	    putStrLn "(|$|) :: Value -> Value -> Value"
	    putStrLn "(VAbs f) |$| x = f x"
	    putStrLn ""
	    putStrLn "class Trans a where"
	    putStrLn "    unbox :: Value -> a"
	    putStrLn "    box   :: a -> Value"
	    putStrLn ""
	    putStrLn "instance Trans () where"
	    putStrLn "    unbox VNonData = ()"
	    putStrLn "    box () = VNonData"
	    putStrLn ""
	    putStrLn "instance (Trans a, Trans b) => Trans (a -> b) where"
	    putStrLn "    unbox (VAbs f) = unbox . f . box"
	    putStrLn "    box f = VAbs ( box . f . unbox )"
	    putStrLn ""
	    putStrLn "instance Trans Integer where"
	    putStrLn "    unbox (VInt i) = i"
	    putStrLn "    box i = VInt i"
	    putStrLn ""
	    putStrLn "instance Trans Double where"
	    putStrLn "    unbox (VFloat f) = f"
	    putStrLn "    box f = VFloat f"
	    putStrLn ""
	    putStrLn "instance Trans String where"
	    putStrLn "    unbox (VString s) = s"
	    putStrLn "    box s = VString s"
	    putStrLn ""
	    putStrLn "instance Trans Char where"
	    putStrLn "    unbox (VChar c) = c"
	    putStrLn "    box c = VChar c"
	    putStrLn ""
	    putStrLn "main = putStrLn $ show x_Main__main"
	liftIO $ putStrLn $ "--"
	ddefs <- mapM showUntypedDefinition defs
	liftIO $ putStrLn $ render $ vcat ddefs
	showOptimizedDefinitions definitions

enumConstructors :: Definitions -> [QName]
enumConstructors = concatMap f . Map.toList where
    f (name, d) = case theDef d of
			Constructor{} -> [name]
                        Record{}      -> [name]
                        _             -> []

computeMaxArity :: Definitions -> TCM Nat
computeMaxArity dd =
    fmap maximum $ mapM getConstructorArity $ map snd $ Map.toList dd

getConstructorArity :: Definition -> TCM Nat
getConstructorArity defn = case theDef defn of
    Record{recFields = flds} -> return $ genericLength flds
    Constructor{conPars = np} -> do
	ty <- normalise $ defType defn
	(args,_) <- splitType ty
	return $ genericLength args - np
    _ -> return 0

printConstants :: Definitions -> IO ()
printConstants dd = mapM_ go $ zip (enumConstructors dd) [1..] where
    go (name,n) = let cname = translateNameAsUntypedConstructor $ show name in
		  putStrLn $ "#define " ++ cname ++ " " ++ show n

printShowConstants :: Definitions -> IO ()
printShowConstants dd = mapM_ go $ zip (enumConstructors dd) [1..] where
    go (name,n) = let pname = show $ qnameName name in
		  putStrLn $ "getConString " ++ show n ++ " = \"" ++ pname ++ "\""

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