module Agda.Compiler.MAlonzo.Compiler where
#if __GLASGOW_HASKELL__ <= 708
import Prelude hiding (mapM_, mapM, sequence, concat)
#endif
import Control.Applicative
import Control.Monad.Reader hiding (mapM_, forM_, mapM, forM, sequence)
import Control.Monad.State hiding (mapM_, forM_, mapM, forM, sequence)
import Data.Generics.Geniplate
import Data.Foldable
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable hiding (for)
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.Datatypes
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.CompiledClause
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.IO.UTF8 as UTF8
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Singleton
import Agda.Utils.Tuple
#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 . List.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 Nothing $
functionFromClauses cls
Function{ funCompiled = Just cc } | not (hasCatchAll cc) ->
function (exportHaskell compiled) $ functionFromCaseTree q cc
Function{ funClauses = cls } ->
function (exportHaskell compiled) $ functionFromClauses cls
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs }
| Just (HsType ty) <- compiledHaskell compiled -> do
ccs <- List.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) (List.maximum (np:ars) np) (np + ni) cds cl
Constructor{} -> return []
Record{ recClause = cl, recConHead = con, recFields = flds } -> do
let c = conName con
let noFields = length flds
let ar = I.arity ty
cd <- snd <$> condecl c
return $ tvaldecl q Inductive noFields ar [cd] cl
where
function :: Maybe HaskellExport -> TCM [HS.Decl] -> TCM [HS.Decl]
function mhe fun = do
ccls <- mkwhere <$> fun
case mhe of
Nothing -> return ccls
Just (HsExport t name) -> do
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)
functionFromClauses :: [Clause] -> TCM [HS.Decl]
functionFromClauses cls = mapM (clause q Nothing) (tag 0 cls)
functionFromCaseTree :: QName -> CompiledClauses -> TCM [HS.Decl]
functionFromCaseTree q cc = do
e <- casetree cc `runReaderT` initCCEnv (Just q)
return $ [HS.FunBind [HS.Match dummy (dsubname q 0) [] Nothing (HS.UnGuardedRhs e) (HS.BDecls [])]]
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)
data CCEnv = CCEnv
{ ccFunName :: Maybe QName
, ccNameSupply :: NameSupply
, ccCxt :: CCContext
, ccCatchAll :: Maybe CompiledClauses
}
type NameSupply = [HS.Name]
type CCContext = [HS.Name]
mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv
mapNameSupply f e = e { ccNameSupply = f (ccNameSupply e) }
mapContext :: (CCContext -> CCContext) -> CCEnv -> CCEnv
mapContext f e = e { ccCxt = f (ccCxt e) }
initCCEnv :: Maybe QName -> CCEnv
initCCEnv q = CCEnv
{ ccFunName = q
, ccNameSupply = map (ihname "v") [0..]
, ccCxt = []
, ccCatchAll = Nothing
}
lookupIndex :: Int -> CCContext -> HS.Name
lookupIndex i xs = fromMaybe __IMPOSSIBLE__ $ xs !!! i
lookupLevel :: Int -> CCContext -> HS.Name
lookupLevel l xs = fromMaybe __IMPOSSIBLE__ $ xs !!! (length xs 1 l)
type CC = ReaderT CCEnv TCM
casetree :: CompiledClauses -> CC HS.Exp
casetree cc = do
case cc of
Fail -> return $ rtmError $ "Impossible Clause Body"
Done xs v -> lambdasUpTo (length xs) $ hsCast <$> term v
Case n (Branches True conBrs _ _) -> lambdasUpTo n $ do
mkRecord =<< mapM casetree (content <$> conBrs)
Case n (Branches False conBrs litBrs catchAll) -> lambdasUpTo (n + 1) $ do
x <- lookupLevel n <$> asks ccCxt
HS.Case (hsCast $ hsVarUQ x) <$> do
updateCatchAll catchAll $ do
br1 <- conAlts n conBrs
br2 <- litAlts litBrs
br3 <- catchAllAlts =<< asks ccCatchAll
return (br1 ++ br2 ++ br3)
updateCatchAll :: Maybe CompiledClauses -> CC a -> CC a
updateCatchAll Nothing = id
updateCatchAll (Just cc) = local $ \ e -> e { ccCatchAll = Just cc }
conAlts :: Int -> Map QName (WithArity CompiledClauses) -> CC [HS.Alt]
conAlts x br = forM (Map.toList br) $ \ (c, WithArity n cc) -> do
c <- lift $ conhqn c
replaceVar x n $ \ xs -> do
branch (HS.PApp c $ map HS.PVar xs) cc
litAlts :: Map Literal CompiledClauses -> CC [HS.Alt]
litAlts br = forM (Map.toList br) $ \ (l, cc) ->
branch (HS.PLit HS.Signless $ hslit l) cc
catchAllAlts :: Maybe CompiledClauses -> CC [HS.Alt]
catchAllAlts (Just cc) = mapM (branch HS.PWildCard) [cc]
catchAllAlts Nothing = do
q <- fromMaybe __IMPOSSIBLE__ <$> asks ccFunName
return [ HS.Alt dummy HS.PWildCard (HS.UnGuardedRhs $ rtmIncompleteMatch q) (HS.BDecls []) ]
branch :: HS.Pat -> CompiledClauses -> CC HS.Alt
branch pat cc = do
e <- casetree cc
return $ HS.Alt dummy pat (HS.UnGuardedRhs e) (HS.BDecls [])
replaceVar :: Int -> Int -> ([HS.Name] -> CC a) -> CC a
replaceVar x n cont = do
(xs, rest) <- splitAt n <$> asks ccNameSupply
let upd cxt = ys ++ reverse xs ++ zs
where
i = length cxt 1 x
(ys, _:zs) = splitAt i cxt
local (mapNameSupply (const rest) . mapContext upd) $
cont xs
mkRecord :: Map QName HS.Exp -> CC HS.Exp
mkRecord fs = lift $ do
let p1 = fst $ fromMaybe __IMPOSSIBLE__ $ headMaybe $ Map.toList fs
ConHead c _ind xs <- recConFromProj p1
c <- conhqn c
let (args :: [HS.Exp]) = for xs $ \ x -> fromMaybe __IMPOSSIBLE__ $ Map.lookup x fs
return $ hsCast $ List.foldl HS.App (HS.Con c) args
recConFromProj :: QName -> TCM I.ConHead
recConFromProj q = do
caseMaybeM (isProjection q) __IMPOSSIBLE__ $ \ proj -> do
let d = projFromType proj
getRecordConstructor d
lambdasUpTo :: Int -> CC HS.Exp -> CC HS.Exp
lambdasUpTo n cont = do
diff <- (n ) . length <$> asks ccCxt
lambdas diff cont
lambdas :: Int -> CC HS.Exp -> CC HS.Exp
lambdas diff cont = intros diff $ \ xs -> mkLams xs <$> cont
intros :: Int -> ([HS.Name] -> CC HS.Exp) -> CC HS.Exp
intros diff cont = do
if diff <= 0 then cont [] else do
(xs, rest) <- splitAt diff <$> asks ccNameSupply
local (mapNameSupply (const rest) . mapContext (reverse xs ++)) $
cont xs
mkLams :: [HS.Name] -> HS.Exp -> HS.Exp
mkLams [] e = e
mkLams xs e = HS.Lambda dummy (map HS.PVar xs) e
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) $ replicate 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 = length (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 && List.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 .. length 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 (List.concat <$> mapM pat' ps0) bvs
where
pat :: Pattern -> StateT [HS.Pat] TCM [HS.Pat]
pat (ProjP p ) = do
kit <- lift coinductionKit
if Just p == fmap nameOfFlat kit then return [] else
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) <*> (List.concat <$> 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 = go 0 b0 where
go n (Body tm ) = hsCast <$> do
runReaderT (intros n $ const $ term tm) (initCCEnv Nothing)
go n (Bind (Abs _ b)) = go (n+1) b
go n (Bind (NoAbs _ b)) = go n b
go n NoBody = return $ rtmError $ "Impossible Clause Body"
closedTerm :: Term -> TCM HS.Exp
closedTerm v = term v `runReaderT` initCCEnv Nothing
term :: Term -> CC HS.Exp
term tm0 = case unSpine $ ignoreSharing tm0 of
Var i es -> do
x <- lookupIndex i <$> asks ccCxt
apps (hsVarUQ x) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
Lam _ at -> lambdas 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 -> CC 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