module Agda.Compiler.MAlonzo.Compiler where
import Control.Applicative
import qualified Control.Exception as E
import Control.Monad.Reader
import Control.Monad.State
import Data.Char
import Data.List as L
import Data.Map as M
import Data.Set as S
import Language.Haskell.Syntax
import System.Cmd
import System.Directory
import System.Exit
import System.IO
import System.Time
import System.Process
import System.FilePath hiding (normalise, (<.>))
import Agda.Compiler.MAlonzo.Misc
import Agda.Compiler.MAlonzo.Pretty
import Agda.Compiler.MAlonzo.Primitives
import Agda.Interaction.FindFile
import Agda.Interaction.Imports
import Agda.Interaction.Monad
import Agda.Interaction.Options
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete.Name as CN
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.Utils.FileName
import Agda.Utils.Monad
import qualified Agda.Utils.IO.Locale as LocIO
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Impossible
#include "../../undefined.h"
compilerMain :: Interface -> TCM ()
compilerMain mainI =
bracket get put $ \_ -> do
opts <- commandLineOptions
malonzoDir <- case optMAlonzoDir opts of
Just dir -> return dir
Nothing -> do
let tm = toTopLevelModuleName $ iModuleName mainI
f <- findFile tm
return $ filePath $ CN.projectRoot f tm
setCommandLineOptions PersistentOptions $
opts { optMAlonzoDir = Just malonzoDir }
ignoreAbstractMode $ do
mapM_ (compile . miInterface) =<< (M.elems <$> getVisitedModules)
callGHC mainI
compile :: Interface -> TCM ()
compile i = do
setInterface i
ifM uptodate noComp $ (yesComp >>) $ do
writeModule =<< decl <$> curHsMod <*> (definitions =<< curDefs) <*> imports
where
decl mn ds imp = HsModule dummy mn Nothing imp ds
uptodate = liftIO =<< (isNewerThan <$> outFile <*> ifile)
ifile = maybe __IMPOSSIBLE__ filePath <$>
(findInterfaceFile . toTopLevelModuleName =<< curMName)
noComp = reportSLn "" 1 . (++ " : no compilation is needed.").show =<< curMName
yesComp = reportSLn "" 1 . (`repl` "Compiling <<0>> in <<1>> to <<2>>") =<<
sequence [show <$> curMName, ifile, outFile] :: TCM ()
imports :: TCM [HsImportDecl]
imports = (++) <$> hsImps <*> imps where
hsImps = (L.map decl . S.toList .
S.insert unsafeCoerceMod . S.map Module) <$>
getHaskellImports
imps = L.map decl . uniq <$>
((++) <$> importsForPrim <*> (L.map mazMod <$> mnames))
decl m = HsImportDecl dummy m True Nothing Nothing
mnames = (++) <$> (S.elems <$> gets stImportedModules)
<*> (iImportedModules <$> curIF)
uniq = L.map head . group . L.sort
definitions :: Definitions -> TCM [HsDecl]
definitions = M.fold (liftM2(++).(definition<.>instantiateFull)) declsForPrim
definition :: Definition -> TCM [HsDecl]
definition (Defn q ty _ _ d) = do
checkTypeOfMain q ty
(infodecl q :) <$> case d of
Axiom{ axHsDef = Just (HsDefn ty hs) } -> return $ fbWithType ty (fakeExp hs)
Axiom{} -> return $ fb axiomErr
Function{ funClauses = cls } -> function cls
Primitive{ primClauses = Just cls } -> function cls
Primitive{ primClauses = Nothing, primName = s } -> fb <$> primBody s
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs, dataHsType = Just ty } -> do
ccs <- concat <$> mapM checkConstructorType cs
cov <- checkCover q ty np cs
return $ tvaldecl q (dataInduction d) 0 (np + ni) [] (Just __IMPOSSIBLE__) ++ ccs ++ cov
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs, dataHsType = Nothing } -> do
(ars, cds) <- unzip <$> mapM condecl cs
return $ tvaldecl q (dataInduction d) (maximum (np:ars) np) (np + ni) cds cl
Constructor{} -> return []
Record{ recClause = cl, recCon = c, recFields = flds } -> do
let noFields = genericLength flds
ar <- arity <$> normalise ty
cd <- case c of
Nothing -> return $ cdecl q noFields
Just c -> snd <$> condecl c
return $ tvaldecl q Inductive noFields ar [cd] cl
where
function cls = mkwhere <$> mapM (clause q) (tag 0 cls)
tag _ [] = []
tag i [cl] = (i, True , cl): []
tag i (cl:cls) = (i, False, cl): tag (i + 1) cls
mkwhere (HsFunBind [m0, HsMatch _ dn ps rhs [] ] : fbs@(_:_)) =
[HsFunBind [m0, HsMatch dummy dn ps rhs fbs]]
mkwhere fbs = fbs
fbWithType ty e =
[ HsTypeSig dummy [unqhname "d" q] $ fakeType ty ] ++ fb e
fb e =[HsFunBind[HsMatch dummy (unqhname "d" q)[] (HsUnGuardedRhs $ e) []]]
axiomErr = rtmError $ "postulate evaluated: " ++ show q
checkConstructorType :: QName -> TCM [HsDecl]
checkConstructorType q = do
Constructor{ conHsCode = Just (ty, hs) } <- theDef <$> getConstInfo q
return [ HsTypeSig dummy [unqhname "check" q] $ fakeType ty
, HsFunBind [HsMatch dummy (unqhname "check" q) [] (HsUnGuardedRhs $ fakeExp hs) []]
]
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HsDecl]
checkCover q ty n cs = do
let tvs = [ "a" ++ show i | i <- [1..n] ]
makeClause c = do
a <- constructorArity c
Just (_, hsc) <- conHsCode . theDef <$> getConstInfo c
let pat = HsPApp (UnQual $ HsIdent hsc) $ genericReplicate a HsPWildCard
return $ HsAlt dummy pat (HsUnGuardedAlt $ HsTuple []) []
cs <- mapM makeClause cs
let rhs = case cs of
[] -> fakeExp "()"
_ -> HsCase (HsVar $ UnQual $ HsIdent "x") cs
return [ HsTypeSig dummy [unqhname "cover" q] $ fakeType $ unwords (ty : tvs) ++ " -> ()"
, HsFunBind [HsMatch dummy (unqhname "cover" q) [HsPVar $ HsIdent "x"]
(HsUnGuardedRhs rhs) []]
]
constructorArity :: MonadTCM tcm => QName -> tcm Nat
constructorArity q = do
def <- getConstInfo q
a <- normalise $ defType def
case theDef def of
Constructor{ conPars = np } -> return $ arity a np
_ -> fail $ "constructorArity: non constructor: " ++ show q
clause :: QName -> (Nat, Bool, Clause) -> TCM HsDecl
clause q (i, isLast, Clause{ clausePats = ps, clauseBody = b }) =
HsFunBind . (: cont) <$> main where
main = match <$> argpatts ps (bvars b (0::Nat)) <*> clausebody b
cont | isLast && any isCon ps = [match (L.map HsPVar cvs) failrhs]
| isLast = []
| otherwise = [match (L.map HsPVar cvs) crhs]
cvs = L.map (ihname "v") [0 .. genericLength ps 1]
crhs = hsCast$ foldl HsApp (hsVarUQ $ dsubname q (i + 1)) (L.map hsVarUQ cvs)
failrhs = rtmError $ "incomplete pattern matching: " ++ show q
match hps rhs = HsMatch dummy (dsubname q i) hps (HsUnGuardedRhs rhs) []
bvars (Body _) _ = []
bvars (Bind (Abs _ b')) n = HsPVar (ihname "v" n) : bvars b' (n + 1)
bvars (NoBind b' ) n = HsPWildCard : bvars b' n
bvars NoBody _ = repeat HsPWildCard
isCon (Arg _ ConP{}) = True
isCon _ = False
argpatts :: [Arg Pattern] -> [HsPat] -> TCM [HsPat]
argpatts ps0 bvs = evalStateT (mapM pat' ps0) bvs
where
pat (VarP _ ) = do v <- gets head; modify tail; return v
pat (DotP _ ) = pat (VarP dummy)
pat (LitP l ) = return $ HsPLit $ hslit l
pat p@(ConP q ps) = do
irrefutable <- lift $ irr p
let tilde = if tildesEnabled && irrefutable
then HsPParen . HsPIrrPat
else id
(tilde . HsPParen) <$>
(HsPApp <$> lift (conhqn q) <*> mapM pat' ps)
pat' = pat . unArg
tildesEnabled = False
irr :: Pattern -> TCM Bool
irr (VarP {}) = return True
irr (DotP {}) = return True
irr (LitP {}) = return False
irr (ConP q ps) =
(&&) <$> singleConstructorType q
<*> (and <$> mapM (irr . unArg) ps)
clausebody :: ClauseBody -> TCM HsExp
clausebody b0 = runReaderT (go b0) 0 where
go (Body tm ) = hsCast <$> term tm
go (Bind (Abs _ b)) = local (1+) $ go b
go (NoBind b ) = go b
go NoBody = return$ rtmError$ "Impossible Clause Body"
term :: Term -> ReaderT Nat TCM HsExp
term tm0 = case tm0 of
Var i as -> do n <- ask; apps (hsVarUQ $ ihname "v" (n i 1)) as
Lam _ at -> do n <- ask; HsLambda dummy [HsPVar $ ihname "v" n] <$>
local (1+) (term $ absBody at)
Lit l -> lift $ literal l
Def q as -> (`apps` as) . HsVar =<< lift (xhqn "d" q)
Con q as -> (`apps` as) . HsCon =<< lift (conhqn q)
Pi _ _ -> return unit_con
Fun _ _ -> return unit_con
Sort _ -> return unit_con
MetaV _ _ -> mazerror "hit MetaV"
where apps = foldM (\h a -> HsApp h <$> term (unArg a))
literal :: Literal -> TCM HsExp
literal l = case l of
LitInt _ _ -> do toN <- bltQual "NATURAL" mazIntegerToNat
return $ HsVar toN `HsApp` typed "Integer"
LitFloat _ _ -> return $ typed "Double"
_ -> return $ l'
where l' = HsLit $ hslit l
typed = HsExpTypeSig dummy l' . HsQualType [] . HsTyCon . rtmQual
hslit :: Literal -> HsLiteral
hslit l = case l of LitInt _ x -> HsInt x
LitLevel _ x -> HsInt x
LitFloat _ x -> HsFrac (toRational x)
LitString _ x -> HsString x
LitChar _ x -> HsChar x
condecl :: QName -> TCM (Nat, HsConDecl)
condecl q = getConstInfo q >>= \d -> case d of
Defn _ ty _ _ (Constructor {conPars = np}) -> do ar <- arity <$> normalise ty
return $ (ar, cdecl q (ar np))
_ -> mazerror $ "condecl:" ++ gshow' (q, d)
cdecl :: QName -> Nat -> HsConDecl
cdecl q n = HsConDecl dummy (unqhname "C" q)
[ HsUnBangedTy $ HsTyVar $ ihname "a" i | i <- [0 .. n 1]]
tvaldecl :: QName
-> Induction
-> Nat -> Nat -> [HsConDecl] -> Maybe Clause -> [HsDecl]
tvaldecl q ind ntv npar cds cl =
HsFunBind [HsMatch dummy vn pvs (HsUnGuardedRhs unit_con) []] :
maybe [datatype] (const []) cl
where
(tn, vn) = (unqhname "T" q, unqhname "d" q)
tvs = [ ihname "a" i | i <- [0 .. ntv 1]]
pvs = [ HsPVar $ ihname "a" i | i <- [0 .. npar 1]]
datatype = case (ind, cds) of
(Inductive, [c@(HsConDecl _ _ [_])]) -> newtyp c
(Inductive, [c@(HsRecDecl _ _ [_])]) -> newtyp c
_ -> datatyp
newtyp c = HsNewTypeDecl dummy [] tn tvs c []
datatyp = HsDataDecl dummy [] tn tvs cds []
infodecl :: QName -> HsDecl
infodecl q = fakeD (unqhname "name" q) $ show (show q)
hsCast :: HsExp -> HsExp
hsCast e = mazCoerce `HsApp` hsCast' e
hsCast' (HsApp e1 e2) = hsCast' e1 `HsApp` (mazCoerce `HsApp` hsCast' e2)
hsCast' (HsLambda _ ps e) = HsLambda dummy ps $ hsCast' e
hsCast' e = e
writeModule :: HsModule -> TCM ()
writeModule m =
liftIO . (`UTF8.writeFile` (preamble ++ prettyPrint m)) =<< outFile
where
preamble = unlines $ [ "{-# LANGUAGE EmptyDataDecls"
, " , ExistentialQuantification"
, " , ScopedTypeVariables"
, " , NoMonomorphismRestriction"
, " #-}"
]
malonzoDir :: TCM FilePath
malonzoDir = do
mdir <- optMAlonzoDir <$> commandLineOptions
case mdir of
Just dir -> return dir
Nothing -> __IMPOSSIBLE__
outFile' = do
mdir <- malonzoDir
(fdir, fn) <- splitFileName . repldot pathSeparator .
prettyPrint <$> curHsMod
let dir = mdir </> fdir
fp = dir </> replaceExtension fn "hs"
liftIO $ createDirectoryIfMissing True dir
return (mdir, fp)
where
repldot c = L.map (\c' -> if c' == '.' then c else c')
outFile :: TCM FilePath
outFile = snd <$> outFile'
callGHC :: Interface -> TCM ()
callGHC i = do
setInterface i
mdir <- malonzoDir
hsmod <- prettyPrint <$> curHsMod
MName agdaMod <- curMName
let outputName = case agdaMod of
[] -> __IMPOSSIBLE__
ms -> last ms
(mdir, fp) <- outFile'
opts <- optGhcFlags <$> commandLineOptions
let overridableArgs =
[ "-O"
, "-o", mdir </> show outputName
]
otherArgs =
[ "-i" ++ mdir
, "-main-is", hsmod
, fp
, "--make"
, "-fwarn-incomplete-patterns"
, "-fno-warn-overlapping-patterns"
, "-Werror"
]
args = overridableArgs ++ opts ++ otherArgs
compiler = "ghc"
reportSLn "" 1 $ "calling: " ++ L.intercalate " " (compiler : args)
(inn, out, err, p) <-
liftIO $ runInteractiveProcess compiler args Nothing Nothing
liftIO $ do
hClose inn
hSetBinaryMode out False
hSetBinaryMode err False
s <- liftIO $ join <$> LocIO.hGetContents err <*> LocIO.hGetContents out
reportSLn "" 1 s
exitcode <- liftIO $ do
E.evaluate (length s)
waitForProcess p
case exitcode of
ExitFailure _ -> typeError (CompilationError s)
_ -> return ()
where
join s1 s2 =
s1 ++ (if L.null s1 || last s1 == '\n' then "" else "\n") ++ s2