module Agda.Compiler.MAlonzo.Compiler where
import Control.Applicative
import Control.Monad.Reader
import Control.Monad.State
import Data.Generics.Geniplate
import Data.List as List
import Data.Map as Map
import Data.Set as Set
import qualified Language.Haskell.Exts.Extension as HS
import qualified Language.Haskell.Exts.Parser as HS
import qualified Language.Haskell.Exts.Pretty as HS
import qualified Language.Haskell.Exts.Syntax as HS
import System.Directory (createDirectoryIfMissing)
import System.FilePath hiding (normalise)
import Agda.Compiler.CallCompiler
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.Options
import Agda.Syntax.Common
import qualified Agda.Syntax.Abstract.Name as A
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.IO.UTF8 as UTF8
import qualified Agda.Utils.HashMap as HMap
#include "undefined.h"
import Agda.Utils.Impossible
compilerMain :: Bool -> Interface -> TCM ()
compilerMain modIsMain mainI =
localTCState $ do
opts <- commandLineOptions
compileDir <- case optCompileDir opts of
Just dir -> return dir
Nothing -> do
let tm = toTopLevelModuleName $ iModuleName mainI
f <- findFile tm
return $ filePath $ C.projectRoot f tm
setCommandLineOptions $
opts { optCompileDir = Just compileDir }
ignoreAbstractMode $ do
mapM_ (compile . miInterface) =<< (Map.elems <$> getVisitedModules)
writeModule rteModule
callGHC modIsMain mainI
compile :: Interface -> TCM ()
compile i = do
setInterface i
ifM uptodate noComp $ do
yesComp
writeModule =<< decl <$> curHsMod <*> (definitions =<< curDefs) <*> imports
where
decl mn ds imp = HS.Module dummy mn [] Nothing Nothing imp ds
uptodate = liftIO =<< (isNewerThan <$> outFile_ <*> ifile)
ifile = maybe __IMPOSSIBLE__ filePath <$>
(findInterfaceFile . toTopLevelModuleName =<< curMName)
noComp = reportSLn "" 1 . (++ " : no compilation is needed.") . show . A.mnameToConcrete =<< curMName
yesComp = reportSLn "" 1 . (`repl` "Compiling <<0>> in <<1>> to <<2>>") =<<
sequence [show . A.mnameToConcrete <$> curMName, ifile, outFile_] :: TCM ()
imports :: TCM [HS.ImportDecl]
imports = (++) <$> hsImps <*> imps where
hsImps :: TCM [HS.ImportDecl]
hsImps = (List.map decl . Set.toList .
Set.insert mazRTE . Set.map HS.ModuleName) <$>
getHaskellImports
imps :: TCM [HS.ImportDecl]
imps = List.map decl . uniq <$>
((++) <$> importsForPrim <*> (List.map mazMod <$> mnames))
decl :: HS.ModuleName -> HS.ImportDecl
decl m = HS.ImportDecl dummy m True False False Nothing Nothing Nothing
mnames :: TCM [ModuleName]
mnames = (++) <$> (Set.elems <$> use stImportedModules)
<*> (List.map fst . iImportedModules <$> curIF)
uniq :: [HS.ModuleName] -> [HS.ModuleName]
uniq = List.map head . group . List.sort
definitions :: Definitions -> TCM [HS.Decl]
definitions defs = do
kit <- coinductionKit
HMap.foldr (liftM2 (++) . (definition kit <=< instantiateFull))
declsForPrim defs
definition :: Maybe CoinductionKit -> Definition -> TCM [HS.Decl]
definition kit Defn{defArgInfo = info, defName = q} | isIrrelevant info = do
reportSDoc "malonzo.definition" 10 $
text "Not compiling" <+> prettyTCM q <> text "."
return []
definition kit Defn{defName = q, defType = ty, defCompiledRep = compiled, theDef = d} = do
reportSDoc "malonzo.definition" 10 $ vcat
[ text "Compiling" <+> prettyTCM q <> text ":"
, nest 2 $ text (show d)
]
checkTypeOfMain q ty $ do
(infodecl q :) <$> case d of
_ | Just (HsDefn ty hs) <- compiledHaskell compiled ->
return $ fbWithType ty (fakeExp hs)
Datatype{} | Just q == (nameOfInf <$> kit) -> do
let infT = unqhname "T" q
infV = unqhname "d" q
a = ihname "a" 0
b = ihname "a" 1
vars = [a, b]
return [ HS.TypeDecl dummy infT
(List.map HS.UnkindedVar vars)
(HS.TyVar b)
, HS.FunBind [HS.Match dummy infV
(List.map HS.PVar vars) Nothing
(HS.UnGuardedRhs HS.unit_con)
(HS.BDecls [])]
]
Constructor{} | Just q == (nameOfSharp <$> kit) -> do
let sharp = unqhname "d" q
x = ihname "x" 0
return $
[ HS.TypeSig dummy [sharp] $ fakeType $
"forall a. a -> a"
, HS.FunBind [HS.Match dummy sharp
[HS.PVar x]
Nothing
(HS.UnGuardedRhs (HS.Var (HS.UnQual x)))
(HS.BDecls [])]
]
Function{} | Just q == (nameOfFlat <$> kit) -> do
let flat = unqhname "d" q
x = ihname "x" 0
return $
[ HS.TypeSig dummy [flat] $ fakeType $
"forall a. a -> a"
, HS.FunBind [HS.Match dummy flat
[HS.PVar x]
Nothing
(HS.UnGuardedRhs (HS.Var (HS.UnQual x)))
(HS.BDecls [])]
]
Axiom{} -> return $ fb axiomErr
Primitive{ primClauses = [], primName = s } -> fb <$> primBody s
Primitive{ primClauses = cls } -> function cls Nothing
Function{ funClauses = cls } -> function cls (exportHaskell compiled)
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs }
| Just (HsType ty) <- compiledHaskell compiled -> 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 } -> 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, recConHead = con, recFields = flds } -> do
let c = conName con
let noFields = genericLength flds
let ar = arity ty
cd <- snd <$> condecl c
return $ tvaldecl q Inductive noFields ar [cd] cl
where
function :: [Clause] -> Maybe HaskellExport -> TCM [HS.Decl]
function cls (Just (HsExport t name)) =
do ccls <- functionStdName cls
let tsig :: HS.Decl
tsig = HS.TypeSig dummy [HS.Ident name] (fakeType t)
def :: HS.Decl
def = HS.FunBind [HS.Match dummy (HS.Ident name) [] Nothing (HS.UnGuardedRhs (hsVarUQ $ dsubname q 0)) (HS.BDecls [])]
return ([tsig,def] ++ ccls)
function cls Nothing = functionStdName cls
functionStdName :: [Clause] -> TCM [HS.Decl]
functionStdName cls = mkwhere <$> mapM (clause q Nothing) (tag 0 cls)
tag :: Nat -> [Clause] -> [(Nat, Bool, Clause)]
tag _ [] = []
tag i [cl] = (i, True , cl) : []
tag i (cl:cls) = (i, False, cl) : tag (i + 1) cls
mkwhere :: [HS.Decl] -> [HS.Decl]
mkwhere (HS.FunBind [m0, HS.Match _ dn ps mt rhs (HS.BDecls [])] :
fbs@(_:_)) =
[HS.FunBind [m0, HS.Match dummy dn ps mt rhs (HS.BDecls fbs)]]
mkwhere fbs = fbs
fbWithType :: HaskellType -> HS.Exp -> [HS.Decl]
fbWithType ty e =
[ HS.TypeSig dummy [unqhname "d" q] $ fakeType ty ] ++ fb e
fb :: HS.Exp -> [HS.Decl]
fb e = [HS.FunBind [HS.Match dummy (unqhname "d" q) [] Nothing
(HS.UnGuardedRhs $ e) (HS.BDecls [])]]
axiomErr :: HS.Exp
axiomErr = rtmError $ "postulate evaluated: " ++ show (A.qnameToConcrete q)
checkConstructorType :: QName -> TCM [HS.Decl]
checkConstructorType q = do
Just (HsDefn ty hs) <- compiledHaskell . defCompiledRep <$> getConstInfo q
return [ HS.TypeSig dummy [unqhname "check" q] $ fakeType ty
, HS.FunBind [HS.Match dummy (unqhname "check" q) [] Nothing
(HS.UnGuardedRhs $ fakeExp hs) (HS.BDecls [])]
]
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HS.Decl]
checkCover q ty n cs = do
let tvs = [ "a" ++ show i | i <- [1..n] ]
makeClause c = do
(a, _) <- conArityAndPars c
Just (HsDefn _ hsc) <- compiledHaskell . defCompiledRep <$> getConstInfo c
let pat = HS.PApp (HS.UnQual $ HS.Ident hsc) $ genericReplicate a HS.PWildCard
return $ HS.Alt dummy pat (HS.UnGuardedRhs $ HS.unit_con) (HS.BDecls [])
cs <- mapM makeClause cs
let rhs = case cs of
[] -> fakeExp "()"
_ -> HS.Case (HS.Var $ HS.UnQual $ HS.Ident "x") cs
return [ HS.TypeSig dummy [unqhname "cover" q] $ fakeType $ unwords (ty : tvs) ++ " -> ()"
, HS.FunBind [HS.Match dummy (unqhname "cover" q) [HS.PVar $ HS.Ident "x"]
Nothing (HS.UnGuardedRhs rhs) (HS.BDecls [])]
]
conArityAndPars :: QName -> TCM (Nat, Nat)
conArityAndPars q = do
def <- getConstInfo q
TelV tel _ <- telView $ defType def
let Constructor{ conPars = np } = theDef def
n = genericLength (telToList tel)
return (n np, np)
clause :: QName -> Maybe String -> (Nat, Bool, Clause) -> TCM HS.Decl
clause q maybeName (i, isLast, Clause{ namedClausePats = ps, clauseBody = b }) =
HS.FunBind . (: cont) <$> main where
main = match <$> argpatts ps (bvars b (0::Nat)) <*> clausebody b
cont | isLast && any isCon ps = [match (List.map HS.PVar cvs) failrhs]
| isLast = []
| otherwise = [match (List.map HS.PVar cvs) crhs]
cvs = List.map (ihname "v") [0 .. genericLength ps 1]
crhs = hsCast$ List.foldl HS.App (hsVarUQ $ dsubname q (i + 1)) (List.map hsVarUQ cvs)
failrhs = rtmIncompleteMatch q
match hps rhs = HS.Match dummy (maybe (dsubname q i) HS.Ident maybeName) hps Nothing
(HS.UnGuardedRhs rhs) (HS.BDecls [])
bvars (Body _) _ = []
bvars (Bind (Abs _ b')) n = HS.PVar (ihname "v" n) : bvars b' (n + 1)
bvars (Bind (NoAbs _ b)) n = HS.PWildCard : bvars b n
bvars NoBody _ = repeat HS.PWildCard
isCon (Arg _ (Named _ ConP{})) = True
isCon _ = False
argpatts :: [I.NamedArg Pattern] -> [HS.Pat] -> TCM [HS.Pat]
argpatts ps0 bvs = evalStateT (mapM pat' ps0) bvs
where
pat :: Pattern -> StateT [HS.Pat] TCM HS.Pat
pat (ProjP _ ) = lift $ typeError $ NotImplemented $ "Compilation of copatterns"
pat (VarP _ ) = do v <- gets head; modify tail; return v
pat (DotP _ ) = pat (VarP dummy)
pat (LitP (LitQName _ x)) = return $ litqnamepat x
pat (LitP l ) = return $ HS.PLit HS.Signless $ hslit l
pat p@(ConP c _ ps) = do
irrefutable <- lift $ irr p
let tilde :: HS.Pat -> HS.Pat
tilde = if tildesEnabled && irrefutable
then HS.PParen . HS.PIrrPat
else id
(tilde . HS.PParen) <$>
(HS.PApp <$> lift (conhqn $ conName c) <*> mapM pat' ps)
pat' :: I.NamedArg Pattern -> StateT [HS.Pat] TCM HS.Pat
pat' a = pat $ namedArg a
tildesEnabled = False
irr :: Pattern -> TCM Bool
irr (ProjP {}) = __IMPOSSIBLE__
irr (VarP {}) = return True
irr (DotP {}) = return True
irr (LitP {}) = return False
irr (ConP c _ ps) =
(&&) <$> singleConstructorType (conName c)
<*> (andM $ List.map irr' ps)
irr' :: I.NamedArg Pattern -> TCM Bool
irr' a | isIrrelevant a = return $ True
irr' a = irr $ namedArg a
clausebody :: ClauseBody -> TCM HS.Exp
clausebody b0 = runReaderT (go b0) 0 where
go (Body tm ) = hsCast <$> term tm
go (Bind (Abs _ b)) = local (1+) $ go b
go (Bind (NoAbs _ b)) = go b
go NoBody = return $ rtmError $ "Impossible Clause Body"
term :: Term -> ReaderT Nat TCM HS.Exp
term tm0 = case unSpine $ ignoreSharing tm0 of
Var i es -> do
let Just as = allApplyElims es
n <- ask
apps (hsVarUQ $ ihname "v" (n i 1)) as
Lam _ at -> do n <- ask; HS.Lambda dummy [HS.PVar $ ihname "v" n] <$>
local (1+) (term $ absBody at)
Lit l -> lift $ literal l
Def q es -> do
let Just as = allApplyElims es
q <- lift $ xhqn "d" q
HS.Var q `apps` as
Con c as -> do
let q = conName c
kit <- lift coinductionKit
if Just q == (nameOfSharp <$> kit)
then (`apps` as) . HS.Var =<< lift (xhqn "d" q)
else (`apps` as) . HS.Con =<< lift (conhqn q)
Level l -> term =<< lift (reallyUnLevelView l)
Pi _ _ -> return HS.unit_con
Sort _ -> return HS.unit_con
MetaV _ _ -> mazerror "hit MetaV"
DontCare _ -> return $ rtmError $ "hit DontCare"
Shared{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
where apps = foldM (\h a -> HS.App h <$> term' a)
term' :: I.Arg Term -> ReaderT Nat TCM HS.Exp
term' a | isIrrelevant a = return HS.unit_con
term' a = term $ unArg a
literal :: Literal -> TCM HS.Exp
literal l = case l of
LitInt _ _ -> do toN <- bltQual "NATURAL" mazIntegerToNat
return $ HS.Var toN `HS.App` typed "Integer"
LitFloat _ _ -> return $ typed "Double"
LitQName _ x -> return $ litqname x
_ -> return $ l'
where l' = HS.Lit $ hslit l
typed = HS.ExpTypeSig dummy l' . HS.TyCon . rtmQual
hslit :: Literal -> HS.Literal
hslit l = case l of LitInt _ x -> HS.Int x
LitFloat _ x -> HS.Frac (toRational x)
LitString _ x -> HS.String x
LitChar _ x -> HS.Char x
LitQName _ x -> __IMPOSSIBLE__
litqname :: QName -> HS.Exp
litqname x =
HS.Con (HS.Qual mazRTE $ HS.Ident "QName") `HS.App`
HS.Lit (HS.Int n) `HS.App`
HS.Lit (HS.Int m) `HS.App`
(rtmError "primQNameType: not implemented") `HS.App`
(rtmError "primQNameDefinition: not implemented") `HS.App`
HS.Lit (HS.String $ show x )
where
NameId n m = nameId $ qnameName x
litqnamepat :: QName -> HS.Pat
litqnamepat x =
HS.PApp (HS.Qual mazRTE $ HS.Ident "QName")
[ HS.PLit HS.Signless (HS.Int n)
, HS.PLit HS.Signless (HS.Int m)
, HS.PWildCard
, HS.PWildCard
, HS.PWildCard]
where
NameId n m = nameId $ qnameName x
condecl :: QName -> TCM (Nat, HS.ConDecl)
condecl q = do
(ar, np) <- conArityAndPars q
return $ (ar + np, cdecl q ar)
cdecl :: QName -> Nat -> HS.ConDecl
cdecl q n = HS.ConDecl (unqhname "C" q)
[ HS.TyVar $ ihname "a" i | i <- [0 .. n 1] ]
tvaldecl :: QName
-> Induction
-> Nat -> Nat -> [HS.ConDecl] -> Maybe Clause -> [HS.Decl]
tvaldecl q ind ntv npar cds cl =
HS.FunBind [HS.Match dummy vn pvs Nothing
(HS.UnGuardedRhs HS.unit_con) (HS.BDecls [])] :
maybe [HS.DataDecl dummy kind [] tn tvs
(List.map (HS.QualConDecl dummy [] []) cds) []]
(const []) cl
where
(tn, vn) = (unqhname "T" q, unqhname "d" q)
tvs = [ HS.UnkindedVar $ ihname "a" i | i <- [0 .. ntv 1]]
pvs = [ HS.PVar $ ihname "a" i | i <- [0 .. npar 1]]
kind = case (ind, cds) of
(Inductive, [HS.ConDecl _ [_]]) -> HS.NewType
(Inductive, [HS.RecDecl _ [_]]) -> HS.NewType
_ -> HS.DataType
infodecl :: QName -> HS.Decl
infodecl q = fakeD (unqhname "name" q) $ show $ prettyShow q
hsCast :: HS.Exp -> HS.Exp
hsCast e = mazCoerce `HS.App` hsCast' e
hsCast' :: HS.Exp -> HS.Exp
hsCast' (HS.App e1 e2) = hsCast' e1 `HS.App` (hsCoerce $ hsCast' e2)
hsCast' (HS.Lambda _ ps e) = HS.Lambda dummy ps $ hsCast' e
hsCast' e = e
hsCoerce :: HS.Exp -> HS.Exp
hsCoerce e@(HS.ExpTypeSig _ (HS.Lit (HS.Int{})) _) = e
hsCoerce e = HS.App mazCoerce e
writeModule :: HS.Module -> TCM ()
writeModule (HS.Module l m ps w ex imp ds) = do
out <- outFile m
liftIO $ UTF8.writeFile out $ prettyPrint $
HS.Module l m (p : ps) w ex imp ds
where
p = HS.LanguagePragma dummy $ List.map HS.Ident $
[ "EmptyDataDecls"
, "ExistentialQuantification"
, "ScopedTypeVariables"
, "NoMonomorphismRestriction"
, "Rank2Types"
]
rteModule :: HS.Module
rteModule = ok $ parse $ unlines
[ "module " ++ prettyPrint mazRTE ++ " where"
, "import Unsafe.Coerce"
, ""
, "-- Special version of coerce that plays well with rules."
, "{-# INLINE [1] mazCoerce #-}"
, "mazCoerce = Unsafe.Coerce.unsafeCoerce"
, "{-# RULES \"coerce-id\" forall (x :: a) . mazCoerce x = x #-}"
, ""
, "-- Builtin QNames, the third field is for the type."
, "data QName a b = QName { nameId, moduleId :: Integer, qnameType :: a, qnameDefinition :: b, qnameString :: String}"
, "instance Eq (QName a b) where"
, " QName a b _ _ _ == QName c d _ _ _ = (a, b) == (c, d)"
, ""
, "mazIncompleteMatch :: String -> a"
, "mazIncompleteMatch s = error (\"MAlonzo Runtime Error: incomplete pattern matching: \" ++ s)"
]
where
parse :: String -> HS.ParseResult HS.Module
parse = HS.parseModuleWithMode
HS.defaultParseMode
{ HS.extensions = [ HS.EnableExtension HS.ExplicitForAll ] }
ok :: HS.ParseResult HS.Module -> HS.Module
ok (HS.ParseOk d) = d
ok HS.ParseFailed{} = __IMPOSSIBLE__
compileDir :: TCM FilePath
compileDir = do
mdir <- optCompileDir <$> commandLineOptions
case mdir of
Just dir -> return dir
Nothing -> __IMPOSSIBLE__
outFile' :: (HS.Pretty a, TransformBi HS.ModuleName (Wrap a)) =>
a -> TCM (FilePath, FilePath)
outFile' m = do
mdir <- compileDir
let (fdir, fn) = splitFileName $ repldot pathSeparator $
prettyPrint m
let dir = mdir </> fdir
fp = dir </> replaceExtension fn "hs"
liftIO $ createDirectoryIfMissing True dir
return (mdir, fp)
where
repldot c = List.map $ \ c' -> if c' == '.' then c else c'
outFile :: HS.ModuleName -> TCM FilePath
outFile m = snd <$> outFile' m
outFile_ :: TCM FilePath
outFile_ = outFile =<< curHsMod
callGHC :: Bool -> Interface -> TCM ()
callGHC modIsMain i = do
setInterface i
mdir <- compileDir
hsmod <- prettyPrint <$> curHsMod
MName agdaMod <- curMName
let outputName = case agdaMod of
[] -> __IMPOSSIBLE__
ms -> last ms
(mdir, fp) <- outFile' =<< curHsMod
opts <- optGhcFlags <$> commandLineOptions
let overridableArgs =
[ "-O"] ++
(if modIsMain then ["-o", mdir </> show (nameConcrete outputName)] else []) ++
[ "-Werror"]
otherArgs =
[ "-i" ++ mdir] ++
(if modIsMain then ["-main-is", hsmod] else []) ++
[ fp
, "--make"
, "-fwarn-incomplete-patterns"
, "-fno-warn-overlapping-patterns"
]
args = overridableArgs ++ opts ++ otherArgs
compiler = "ghc"
callCompiler compiler args