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
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 ""
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 ++ "\""