module Agda.Compiler.UHC.FromAgda where
#if __GLASGOW_HASKELL__ <= 708
import Control.Applicative
import Data.Traversable (traverse)
#endif
import Control.Monad
import Control.Monad.State
import Control.Monad.Reader
import qualified Data.Map as M
import Data.Maybe
import Data.Either
import Data.List
import qualified Data.Set as Set
import Agda.Syntax.Internal hiding (Term(..))
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Literal as TL
import Agda.Syntax.Treeless (TTerm (..), TAlt (..))
import qualified Agda.Syntax.Treeless as C
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.Utils.List
import qualified Agda.Utils.Pretty as P
import qualified Agda.Utils.HashMap as HMap
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Common
import Agda.Compiler.Common
import Agda.Compiler.ToTreeless
import Agda.Compiler.Treeless.GuardsToPrims
import Agda.Compiler.Treeless.NormalizeNames
import Agda.Compiler.Treeless.Pretty
import Agda.Compiler.UHC.Pragmas.Base
import Agda.Compiler.UHC.Pragmas.Parse (coreExprToCExpr)
import Agda.Compiler.UHC.CompileState
import Agda.Compiler.UHC.Primitives
import Agda.Compiler.UHC.MagicTypes
import Agda.Compiler.UHC.Bridge as CA
import Agda.Utils.Maybe
import Agda.Utils.Except ( MonadError (catchError) )
import Agda.Utils.Lens
#include "undefined.h"
import Agda.Utils.Impossible
opts :: EHCOpts
opts = defaultEHCOpts
fromAgdaModule :: ModuleName
-> [ModuleName]
-> Interface
-> TCM CModule
fromAgdaModule modNm curModImps iface = do
setCommandLineOptions =<< gets (stPersistentOptions . stPersistentState)
mapM_ setOptionsFromPragma (iPragmaOptions iface)
let defs = sortDefs $ iSignature iface ^. sigDefinitions
runCompileT modNm (do
lift $ reportSLn "uhc" 10 "Translate datatypes..."
funs' <- concat <$> mapM translateDefn defs
let funs = mkLetRec funs' (mkInt opts 0)
additionalImports <- lift getHaskellImportsUHC
let imps = map mkImport $ nub $
[ mkHsName1 "UHC.Base"
, mkHsName1 "UHC.Agda.Builtins" ]
++ map moduleNameToCoreName curModImps
++ map mkHsName1 (Set.toList additionalImports)
crModNm = moduleNameToCoreName modNm
mkModule crModNm
<$> getExports <*> pure imps <*> getDeclMetas <*> pure funs
)
translateDefn :: (QName, Definition) -> Compile [CBind]
translateDefn (n, defini) = do
crName <- getCoreName n
let crRep = compiledCore $ defCompiledRep defini
kit <- lift coinductionKit
case theDef defini of
d@(Datatype {}) -> do
unless (isJust crRep || Just n == (nameOfInf <$> kit)) $ do
addMetaData n (mkMetaData crName)
vars <- replicateM (dataPars d + dataIxs d) freshLocalName
addExports [crName]
return [mkBind1 crName (mkLam vars $ mkUnit opts)]
(Function{}) | Just n == (nameOfFlat <$> kit) -> do
addExports [crName]
(\x -> [x]) <$> mkIdentityFun n "coind-flat" 0
f@(Function{}) | otherwise -> do
let ty = (defType defini)
lift $ reportSDoc "uhc.fromagda" 5 $ text "compiling fun:" <+> prettyTCM n
lift $ reportSDoc "uhc.fromagda" 15 $ text "type:" <+> (text . show) ty
caseMaybeM (lift $ toTreeless n) (pure []) $ \ treeless -> do
funBody <- convertGuards <$> lift (normalizeNames treeless)
lift $ reportSDoc "uhc.fromagda" 30 $ text " compiled treeless fun:" <+> (text . show) funBody
funBody' <- runTT $ compileTerm funBody
lift $ reportSDoc "uhc.fromagda" 30 $ text " compiled UHC Core fun:" <+> (text . show) funBody'
addExports [crName]
return [mkBind1 crName funBody']
Constructor{} | Just n == (nameOfSharp <$> kit) -> do
addExports [crName]
(\x -> [x]) <$> mkIdentityFun n "coind-sharp" 0
(Constructor{}) | Nothing <- crRep -> do
n' <- lift $ canonicalName n
if (n /= n')
then return []
else do
addExports [crName]
ctag <- getConstrCTag n
addMetaCon n (fromJust $ mkMetaDataConFromCTag ctag)
vars <- replicateM (getCTagArity ctag) freshLocalName
let conWrapper = mkLam vars (mkTagTup ctag $ map mkVar vars)
return [mkBind1 crName conWrapper]
Constructor{} -> return []
r@(Record{}) -> do
unless (isJust crRep) $ do
addMetaData n (mkMetaData crName)
vars <- replicateM (recPars r) freshLocalName
addExports [crName]
return [mkBind1 crName (mkLam vars $ mkUnit opts)]
(Axiom{}) -> do
addExports [crName]
case crRep of
Nothing -> return [mkBind1 crName
(coreError $ "Axiom " ++ show n ++ " used but has no computation.")]
Just (CrDefn x) -> do
x' <- case coreExprToCExpr x of
Left err -> internalError $ "Invalid COMPILED_UHC pragma value: " ++ err
Right y -> return y
return [mkBind1 crName x']
_ -> __IMPOSSIBLE__
p@(Primitive{}) -> do
addExports [crName]
case primName p `M.lookup` primFunctions of
Nothing -> internalError $ "Primitive " ++ show (primName p) ++ " declared, but no such primitive exists."
(Just expr) -> do
expr' <- expr
return [mkBind1 crName expr']
where
mkIdentityFun :: QName
-> String
-> Int
-> Compile CBind
mkIdentityFun nm comment ignArgs = do
crName <- getCoreName nm
xs <- replicateM (ignArgs + 1) freshLocalName
return $ mkBind1 crName (mkLam xs (mkVar $ last xs))
runTT :: TT a -> Compile a
runTT r = do
r `runReaderT` (TTEnv [])
data TTEnv = TTEnv
{ nmEnv :: [HsName]
}
type TT = ReaderT TTEnv Compile
addToEnv :: [HsName] -> TT a -> TT a
addToEnv nms cont =
local (\e -> e { nmEnv = nms ++ (nmEnv e) }) cont
data BuiltinKit = BuiltinKit
{ isNat :: QName -> Bool
, isInt :: QName -> Bool
}
builtinKit :: TCM BuiltinKit
builtinKit =
BuiltinKit <$> is dat builtinNat
<*> is dat builtinInteger
where
dat (I.Def d _) = pure d
dat _ = Nothing
is a b = maybe (const False) (==) . (a =<<) <$> getBuiltin' b
compileTerm :: C.TTerm -> TT CExpr
compileTerm term = do
builtinKit' <- lift $ lift builtinKit
case term of
C.TPrim t -> return $ compilePrim t
C.TVar x -> do
nm <- fromMaybe __IMPOSSIBLE__ . (!!! x) <$> asks nmEnv
return $ mkVar nm
C.TDef nm -> do
nm' <- lift $ getCoreName nm
return $ mkVar nm'
C.TApp t xs -> do
mkApp <$> compileTerm t <*> mapM compileTerm xs
C.TLam t -> do
name <- lift freshLocalName
addToEnv [name] $ do
mkLam [name] <$> compileTerm t
C.TLit l -> return $ litToCore l
C.TCon c -> do
con <- lift $ getConstrFun c
return $ mkVar con
C.TLet x body -> do
nm <- lift freshLocalName
mkLet1Plain nm
<$> compileTerm x
<*> addToEnv [nm] (compileTerm body)
C.TCase sc (C.CTData dt) def alts | not (isNat builtinKit' dt || isInt builtinKit' dt) -> do
caseScr <- lift freshLocalName
defVar <- lift freshLocalName
def' <- compileTerm def
branches <- traverse compileConAlt alts
defBranches <- defaultBranches dt alts (mkVar defVar)
let cas = mkCase (mkVar caseScr) (branches ++ defBranches)
caseScr' <- compileTerm (C.TVar sc)
return $ mkLet1Plain defVar def' (mkLet1Strict caseScr caseScr' cas)
C.TCase sc ct def alts | otherwise -> do
sc <- compileTerm (C.TVar sc)
var <- lift freshLocalName
def <- compileTerm def
css <- buildPrimCases eq (mkVar var) alts def
return $ mkLet1Strict var sc css
where
eq :: CExpr
eq = case ct of
C.CTChar -> mkVar $ primFunNm "primCharEquality"
C.CTString -> mkVar $ primFunNm "primStringEquality"
C.CTQName -> mkVar $ primFunNm "primQNameEquality"
C.CTData nm | isNat builtinKit' nm -> mkVar $ primFunNm "primIntegerEquality"
C.CTData nm | isInt builtinKit' nm -> mkVar $ primFunNm "primIntegerEquality"
_ -> __IMPOSSIBLE__
C.TUnit -> unit
C.TSort -> unit
C.TErased -> unit
C.TError e -> return $ case e of
C.TUnreachable -> coreError $ "Unreachable code reached. This should never happen! Crashing..."
where unit = return $ mkUnit opts
buildPrimCases :: CExpr
-> CExpr
-> [C.TAlt]
-> CExpr
-> TT CExpr
buildPrimCases _ _ [] def = return def
buildPrimCases eq scr (b:brs) def = do
var <- lift freshLocalName
e' <- compileTerm (C.aBody b)
rec' <- buildPrimCases eq scr brs def
let lit = litToCore $ C.aLit b
eqTest = mkApp eq [scr, lit]
return $ mkLet1Strict var eqTest (mkIfThenElse (mkVar var) e' rec')
mkIfThenElse :: CExpr -> CExpr -> CExpr -> CExpr
mkIfThenElse c t e = mkCase c [b1, b2]
where b1 = mkAlt (mkPatCon (ctagTrue opts) mkPatRestEmpty []) t
b2 = mkAlt (mkPatCon (ctagFalse opts) mkPatRestEmpty []) e
compileConAlt :: C.TAlt -> TT CAlt
compileConAlt a =
makeConAlt (C.aCon a)
(\vars -> addToEnv (reverse vars) $ compileTerm (C.aBody a))
makeConAlt :: QName -> ([HsName] -> TT CExpr) -> TT CAlt
makeConAlt con mkBody = do
ctag <- lift $ getConstrCTag con
vars <- lift $ replicateM (getCTagArity ctag) freshLocalName
body <- mkBody vars
let patFlds = [mkPatFldBind (mkHsName [] "", mkInt opts i) (mkBind1Nm1 v) | (i, v) <- zip [0..] vars]
return $ mkAlt (mkPatCon ctag mkPatRestEmpty patFlds) body
defaultBranches :: QName -> [C.TAlt] -> CExpr -> TT [CAlt]
defaultBranches dt alts def = do
dtCons <- dataRecCons . theDef <$> (lift . lift) (getConstInfo dt)
let altCons = map C.aCon alts
missingCons = dtCons \\ altCons
mapM (\a -> makeConAlt a (\_ -> return def)) missingCons
litToCore :: Literal -> CExpr
litToCore (LitNat _ i) = mkApp (mkVar $ primFunNm "primIntegerToNat") [mkInteger opts i]
litToCore (LitString _ s) = mkString opts s
litToCore (LitChar _ c) = mkChar c
litToCore (LitFloat _ f) = mkApp (mkVar $ primFunNm "primMkFloat") [mkString opts (show f)]
litToCore (LitQName _ q) = mkApp (mkVar $ primFunNm "primMkQName")
[mkInteger opts n, mkInteger opts m, mkString opts $ P.prettyShow q]
where NameId n m = nameId $ qnameName q
litToCore LitMeta{} = __IMPOSSIBLE__
getCTagArity :: CTag -> Int
getCTagArity = destructCTag 0 (\_ _ _ ar -> ar)
coreError :: String -> CExpr
coreError msg = mkError opts $ "Fatal error: " ++ msg
compilePrim :: C.TPrim -> CExpr
compilePrim C.PQuot = mkVar $ primFunNm "primIntegerQuot"
compilePrim C.PRem = mkVar $ primFunNm "primIntegerRem"
compilePrim C.PSub = mkVar $ primFunNm "primIntegerMinus"
compilePrim C.PAdd = mkVar $ primFunNm "primIntegerPlus"
compilePrim C.PMul = mkVar $ primFunNm "primIntegerTimes"
compilePrim C.PIf = mkVar $ primFunNm "primIfThenElse"
compilePrim C.PGeq = mkVar $ primFunNm "primIntegerGreaterOrEqual"
compilePrim C.PLt = mkVar $ primFunNm "primIntegerLess"
compilePrim C.PEq = mkVar $ primFunNm "primIntegerEquality"
compilePrim C.PSeq = mkVar $ primFunNm "primSeq"
createMainModule :: ModuleName -> HsName -> CModule
createMainModule mainMod main = mkModule (mkHsName [] "Main") [] [mkImport $ mkHsName1 "UHC.Run", mkImport mainModAux] [] (mkMain main)
where mainModAux = moduleNameToCoreName mainMod