module Agda.Compiler.Alonzo.Main where
#include "../../undefined.h"
import Agda.Utils.Impossible
import Debug.Trace(trace)
import Language.Haskell.Syntax
import Language.Haskell.Pretty
import System.FilePath (pathSeparator)
import Agda.Compiler.Alonzo.Haskell
import Agda.Compiler.Alonzo.Names
import Agda.Compiler.Alonzo.PatternMonad
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Internal
import Agda.Syntax.Literal
import Text.PrettyPrint
import Agda.Syntax.Common
import Control.Applicative
import Control.Monad.State
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.List as List
import Data.Set (Set)
import Data.Map (Map, (!))
import Data.Generics.Text
import Agda.Syntax.Abstract.Name
import qualified Agda.Syntax.Concrete.Name as CN
import Agda.Interaction.Options
import Agda.Interaction.Monad
import Agda.TypeChecker
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Reduce
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import System.IO
compilerMain :: TCM () -> TCM ()
compilerMain typeCheck = ignoreAbstractMode $ do
typeCheck
sig <- gets stSignature
let (moduleName:_) = Map.keys $ sigSections sig
withCurrentModule moduleName $ do
builtinMap <- getBuiltinThings
let definitions = sigDefinitions sig
let defs = Map.toList definitions
let names = List.map fst defs
hsdefs <- mapM processDefWithDebug defs
allImps <- map (render . pretty) . Map.keys <$> getVisitedModules
verboseS "comp.alonzo.import" 20 $ liftIO $ mapM_ (\m -> putStrLn $ "import " ++ m) allImps
hImps <- getHaskellImports
let mainNum = (numOfMainS names)
let fileBase = map pathSep (show moduleName)
where
pathSep '.' = pathSeparator
pathSep c = c
let moduleString = show moduleName
let hsmod = hsModuleImporting moduleString (Set.toList hImps) allImps (concat hsdefs)
liftIO $ outputHsModule fileBase hsmod mainNum
fromCurrentModule :: QName -> TCM Bool
fromCurrentModule q = do
m <- qnameFromList . mnameToList <$> currentModule
return $ moduleId q == moduleId m
where
moduleId q = mi
where NameId _ mi = nameId $ qnameName q
flattenSubmodules :: QName -> TCM QName
flattenSubmodules q = do
ifM (fromCurrentModule q)
(return q)
$ do
topModules <- map (iModuleName . miInterface) . Map.elems <$>
getVisitedModules
case filter (isInModule q) topModules of
[top] -> return $ q { qnameModule = top }
[] -> error $ "flattenSubmodules: " ++ show q ++ " </- " ++ show topModules
_ : _ : _ -> __IMPOSSIBLE__
maybeQualName :: (QName -> HsQName) -> (Name -> HsName) -> QName -> PM HsQName
maybeQualName qual unqual q = lift $ do
ifM (fromCurrentModule q)
(return $ UnQual (unqual $ qnameName q))
(qual <$> flattenSubmodules q)
maybeQualConName = maybeQualName conQName conName
maybeQualDefName = maybeQualName dfQName dfName
numOfMainS :: [QName] -> Maybe Nat
numOfMainS [] = Nothing
numOfMainS (n:ns) | isMain (qnameName n) = Just $ numOfQName n
| otherwise = numOfMainS ns
isMain n = (show n == "main")
processDefWithDebug :: (QName,Definition) -> TCM [HsDecl]
processDefWithDebug (qname,def) = do
def <- instantiateFull def
hsdecls <- processDef (qname,def)
return (nameInfo:hsdecls) where
nameInfo = infoDecl infoName (show name)
infoName = "name" ++ (show $ numOfName name)
name = qnameName qname
infoDecl :: String -> String -> HsDecl
infoDecl name val = HsFunBind [ HsMatch dummyLoc hsname [] rhs []] where
rhs = HsUnGuardedRhs $ HsLit $ HsString val
hsname = HsIdent name
processDef :: (QName,Definition) -> TCM [HsDecl]
processDef (qname,Defn { theDef = Function { funClauses = clauses } }) = do
hsDecls <- foldClauses name 1 clauses
return [HsFunBind [HsMatch dummyLoc (dfName name) [] rhs hsDecls]] where
rhs = HsUnGuardedRhs $ HsVar $ UnQual $ dfNameSub name 1
name = qnameName qname
processDef (qname,Defn { theDef = Datatype{ dataPars = n, dataClause = Nothing, dataCons = [] } }) = do
return [ddecl,vdecl] where
name = qnameName qname
ddecl = HsDataDecl dummyLoc [] (dataName name) tvars cons []
tvars = []
cons = [HsConDecl dummyLoc (conName name) [] ]
vdecl = HsFunBind [ HsMatch dummyLoc hsname (nDummyArgs n) rhs []]
rhs = HsUnGuardedRhs $ HsVar $ unit_con_name
hsname = dfName name
nDummyArgs :: Nat -> [HsPat]
nDummyArgs 0 = []
nDummyArgs k = (HsPVar $ HsIdent ("v" ++ (show k))) : nDummyArgs (k1)
processDef (qname,Defn { theDef = Datatype{ dataPars = n, dataIxs = nind, dataClause = Nothing, dataCons = cs }}) = do
cons <- consForName name cs
arities <- getConArities cs
return [ddecl cons arities,vdecl] where
name = qnameName qname
dataname = dataName name
ddecl cs arities = HsDataDecl dummyLoc [] dataname (tvars arities) cs []
tvars arities = genericTake (List.maximum arities) $ List.map HsIdent letters
vdecl = HsFunBind [ HsMatch dummyLoc hsname (nDummyArgs (n+nind)) rhs []]
rhs = HsUnGuardedRhs $ HsVar $ unit_con_name
hsname = dfName name
nDummyArgs 0 = []
nDummyArgs k = (HsPVar $ HsIdent ("v" ++ (show k))) : nDummyArgs (k1)
processDef (qname, Defn { theDef =
Record { recPars = n, recFields = fields, recTel = tel } }) = do
return [ddecl arity tel,vdecl tel] where
name = qnameName qname
arity = genericLength fields
ddecl n tel = HsDataDecl dummyLoc [] dataname (tvars n) [con n] []
dataname = (dataName name)
tvars n = genericTake n idents
con n = HsConDecl dummyLoc (conName name) args
idents = List.map HsIdent letters
args = List.map (HsUnBangedTy . HsTyVar) $ genericTake arity idents
vdecl tel = HsFunBind [ HsMatch dummyLoc hsname (nDummyArgs 0) rhs []]
rhs = HsUnGuardedRhs $ HsVar $ unit_con_name
hsname = dfName name
nDummyArgs 0 = []
nDummyArgs k = (HsPVar $ HsIdent ("v" ++ (show k))) : nDummyArgs (k1)
processDef def@(qname,Defn { theDef = Constructor{} }) =
return []
processDef def@(qname,Defn { theDef = Axiom{axHsDef = mhs} }) = return
[HsFunBind [HsMatch dummyLoc hsid [] rhs decls]] where
rhs = HsUnGuardedRhs $ case mhs of
Just (HsDefn _ hs) -> hsVar hs
_ -> hsError $ "axiom: " ++ show qname
decls = []
hsid = dfName name
name = qnameName qname
processDef (qname,Defn { theDef = Primitive info prim expr }) = return $
[HsFunBind [HsMatch dummyLoc hsid [] rhs decls]] where
rhs = HsUnGuardedRhs $ HsVar $ rtpQName prim
decls = []
hsid = dfName name
name = qnameName qname
processDef (qname, (Defn { theDef = Datatype{dataClause = Just clause} })) = do
mkSynonym (clauseBod clause) where
name = qnameName qname
mkSynonym (Lam _ (Abs _ t)) = mkSynonym t
mkSynonym (Def rhsqname args) = return [ddecl, vdecl] where
ddecl = HsTypeDecl loc dname [] typ
moduleName = qnameModule rhsqname
hsModuleName = Module $ moduleStr moduleName
vdecl = HsFunBind [ HsMatch dummyLoc hsname (nDummyArgs 0) rhs []]
rhs = HsUnGuardedRhs $ HsVar $ unit_con_name
hsname = dfName name
loc = dummyLoc
nDummyArgs 0 = []
nDummyArgs k = (HsPVar $ HsIdent ("v" ++ (show k))) : nDummyArgs (k1)
dname = dataName name
typ = HsTyCon $ Qual hsModuleName $ dataName $ qnameName rhsqname
mkSynonym t = __IMPOSSIBLE__
consForName dname qns = mapM (processCon dname) qns
times :: Nat -> a -> [a]
times 0 x = []
times n x = x:(times (n1) x)
processCon dname qn = do
arity <- getConArity qn
let arg = HsUnBangedTy $ HsTyVar $ HsIdent "a"
let idents = List.map HsIdent letters
let args = List.map (HsUnBangedTy . HsTyVar) $ genericTake arity idents
return $ HsConDecl dummyLoc (conName $ qnameName qn) args
consDefs :: [QName] -> TCM [Definition]
consDefs qns = do
definitions <- getDefinitions
return [definitions ! qn | qn <- qns]
processClause :: Name -> Nat -> Clause -> TCM HsDecl
processClause name number clause@(Clause{ clausePerm = perm
, clausePats = args
, clauseBody = body
}) = do
reportSLn "comp.alonzo.clause" 20 $
"processClause " ++ show name ++ "\n" ++
" perm = " ++ show perm ++ "\n" ++
" args = " ++ show args ++ "\n"
ldefs <- getDefinitions
let bodyPM = processBody body
pst0 = initPState clause ldefs
(exp, pst) <- runStateT bodyPM pst0
let rhs = HsUnGuardedRhs exp
(pats, pst2) <- runStateT (processArgPats args) pst
return $ HsFunBind $ [HsMatch dummyLoc hsid pats rhs decls]
where
decls = []
hsid = dfNameSub name $ fromIntegral number
contClause :: Name -> Nat -> Clause -> TCM HsDecl
contClause name number (Clause{ clausePats = args, clauseBody = body }) = do
return $ HsFunBind $ [HsMatch dummyLoc hsid pats rhs decls] where
decls = []
hsid = dfNameSub name (fromIntegral number)
rightLetters = genericTake (length args) letters
pats = List.map (HsPVar . HsIdent) rightLetters
rhs = HsUnGuardedRhs exp
exp = vecApp expfun expargs
expfun = hsCast$ HsVar $ UnQual $ dfNameSub name (fromIntegral $ number+1)
expargs = List.map (HsVar . UnQual . HsIdent) rightLetters
foldClauses :: Name -> Nat -> [Clause] -> TCM [HsDecl]
foldClauses name n [] = return []
foldClauses name n [c] = do
decl <- processClause name n c
return [decl]
foldClauses name n (c:cs) = do
head <- processClause name n c
cont <- contClause name n c
tail <- foldClauses name (n+1) cs
return (head:cont:tail)
processArgPats :: [Arg Pattern] -> PM [HsPat]
processArgPats args = mapM processArgPat args
processArgPat :: (Arg Pattern) -> PM HsPat
processArgPat (Arg hid pat) = processPat pat
processPat :: Pattern -> PM HsPat
processPat (VarP _) = do
pats <- getPlst
case pats of
[] -> do
c <- getPclause
error $ "Oops! empty pattern list in\n" ++ (gshow c)
(p:ps) -> do
putPlst ps
return p
processPat (DotP _) = return HsPWildCard
processPat (ConP qname args) = do
hsCode <- do
def <- lift $ theDef <$> getConstInfo qname
case def of
Constructor{conHsCode = c} -> return c
Record{} -> return Nothing
_ -> __IMPOSSIBLE__
cname <- case hsCode of
Just (_, h) -> return $ UnQual $ HsIdent h
Nothing -> maybeQualConName qname
hspats <- mapM processArgPat args
return $ HsPParen $ HsPApp cname hspats
processPat (LitP (LitInt _ i)) = return $ HsPLit (HsInt i)
processPat (LitP (LitChar _ c)) =
return $ HsPParen $ HsPApp (rtpCon "CharT") [HsPLit (HsChar c)]
processPat (LitP _) = error "Unimplemented literal patttern"
processBody :: ClauseBody -> PM HsExp
processBody (NoBind cb) = do
addWildcard
processBody cb
processBody (Bind (Abs name cb)) = do
addVar
incPcnt
processBody cb
processBody (Body t) = processTerm t >>= (return . hsCast)
processBody NoBody = do
putPlst (repeat HsPWildCard)
return hsUndefined
processTerm :: Term -> PM HsExp
processTerm (Var n ts) = do
cnt <- getPcnt
processVap (hsVar $ "v" ++ (show (cnt fromIntegral n 1))) ts
processTerm (Def qn ts) = do
x <- maybeQualDefName qn
processVap (HsVar x) ts
processTerm (Con qn ts) = do
def <- lift $ theDef <$> getConstInfo qn
case def of
Constructor{conHsCode = Just (_, hs)} ->
processVap (HsCon $ UnQual $ HsIdent hs) ts
_ -> do
ldefs <- getPDefs
if (Map.member qn ldefs)
then do
definiens <- case theDef <$> Map.lookup qn ldefs of
Just df -> return df
Nothing -> fail $ "Alonzo: No such definition: " ++ show qn
case definiens of
Constructor{conSrcCon = origqn} -> do
x <- maybeQualConName origqn
processVap (HsCon x) ts
_ -> do
x <- maybeQualConName qn
processVap (HsCon x) ts
else do
x <- maybeQualConName qn
processVap (HsCon x) ts
processTerm (Lam h (Abs n t)) = do
cnt <- getPcnt
incPcnt
exp <- processTerm t
return $ hsLam ("v" ++ show cnt) exp
processTerm (Lit l) = return $ (processLit l)
processTerm (Pi arg abs) = return $ HsVar unit_con_name
processTerm (Fun arg typ) = return $ HsVar unit_con_name
processTerm (Sort s) = return $ HsVar unit_con_name
processTerm (MetaV _ _) = error "Can't have metavariables"
processLit :: Literal -> HsExp
processLit (LitLevel r i) = processLit (LitInt r i)
processLit (LitInt _ i) = HsApp toNat $ intLit i where
intLit i = HsParen $ hsPreludeTypedExp "Integer" $ HsLit $ HsInt i
toNat = HsVar $ Qual (Module "RTP") $ HsIdent "_primIntegerToNat"
processLit (LitFloat _ f) = hsPreludeTypedExp "Double" $
HsLit $ HsFrac $ toRational f
processLit (LitString _ s) = HsLit $ HsString s
processLit (LitChar _ c) = HsApp (HsVar $ rtpCon "CharT")
(HsLit $ HsChar c)
processVap :: HsExp -> [Arg Term] -> PM HsExp
processVap e ts = do
p <- get
lift $ unfoldVap p e ts
unfoldVap :: PState -> HsExp -> [Arg Term] -> TCM HsExp
unfoldVap _ e [] = return e
unfoldVap p e ((Arg NotHidden t):ts) = do
e1 <- evalStateT (processTerm t) p
unfoldVap p (hsAp e e1) ts
unfoldVap p e ((Arg Hidden t):ts) = do
e1 <- evalStateT (processTerm t) p
unfoldVap p (hsAp e e1) ts
getDefinitions :: TCM Definitions
getDefinitions = do
sig <- gets stSignature
let definitions = sigDefinitions sig
idefs <- sigDefinitions <$> getImportedSignature
return (definitions `Map.union` idefs)
getConArities cs = mapM getConArity cs
getConArity :: QName -> TCM Nat
getConArity qn = do
Defn _ ty _ _ Constructor{conPars = np} <- getConstInfo qn
ty' <- normalise ty
return $ typeArity ty' np
typeArity :: Type -> Nat
typeArity (El s t) = ar t where
ar (Pi _ (Abs _ t2)) = typeArity t2 + 1
ar (Fun a t2) = typeArity t2 + 1
ar _ = 0
clauseBod :: Clause -> Term
clauseBod c = stripBinds (clauseBody c) where
stripBinds (Bind (Abs _ r)) = stripBinds r
stripBinds (NoBind r) = stripBinds r
stripBinds (Body r) = r
stripBinds (NoBody) = __IMPOSSIBLE__
letters = ["a", "b", "c", "d", "e", "f", "g", "h", "i", "k", "m", "n", "p","q"]
vecApp :: HsExp -> [HsExp] -> HsExp
vecApp e [] = e
vecApp e (a:as) = vecApp (HsApp e a) as