3
3
module Agda.Compiler.MAlonzo.Compiler where
5
5
import Control.Applicative
6
import qualified Control.Exception as E
6
7
import Control.Monad.Reader
7
8
import Control.Monad.State
14
15
import System.Directory
17
import qualified System.IO.UTF8 as UTF8
19
19
import System.Process
20
import System.FilePath ((</>))
20
import System.FilePath hiding (normalise, (<.>))
22
22
import Agda.Compiler.MAlonzo.Misc
23
23
import Agda.Compiler.MAlonzo.Pretty
24
24
import Agda.Compiler.MAlonzo.Primitives
25
import Agda.Interaction.FindFile
25
26
import Agda.Interaction.Imports
26
27
import Agda.Interaction.Monad
27
28
import Agda.Interaction.Options
28
29
import Agda.Syntax.Common
30
import qualified Agda.Syntax.Concrete.Name as CN
29
31
import Agda.Syntax.Internal
30
32
import Agda.Syntax.Literal
31
33
import Agda.TypeChecking.Monad
34
36
import Agda.TypeChecking.Pretty
35
37
import Agda.Utils.FileName
36
38
import Agda.Utils.Monad
39
import qualified Agda.Utils.IO.Locale as LocIO
40
import qualified Agda.Utils.IO.UTF8 as UTF8
37
41
import Agda.Utils.Impossible
39
43
#include "../../undefined.h"
41
compilerMain :: TCM Interface -> TCM ()
42
compilerMain typecheck = do
44
ignoreAbstractMode $ do
45
t <- liftIO getClockTime
47
mapM_ compile =<< ((mainICT :) . M.elems <$> getVisitedModules)
50
compile :: (Interface, ClockTime) -> TCM ()
45
compilerMain :: Interface -> TCM ()
47
-- Preserve the state (the compiler modifies the state).
48
bracket get put $ \_ -> do
50
-- Compute the output directory.
51
opts <- commandLineOptions
52
malonzoDir <- case optMAlonzoDir opts of
53
Just dir -> return dir
55
-- The default output directory is the project root.
56
let tm = toTopLevelModuleName $ iModuleName mainI
58
return $ filePath $ CN.projectRoot f tm
59
setCommandLineOptions PersistentOptions $
60
opts { optMAlonzoDir = Just malonzoDir }
62
ignoreAbstractMode $ do
63
mapM_ (compile . miInterface) =<< (M.elems <$> getVisitedModules)
66
compile :: Interface -> TCM ()
53
69
ifM uptodate noComp $ (yesComp >>) $ do
54
70
writeModule =<< decl <$> curHsMod <*> (definitions =<< curDefs) <*> imports
56
72
decl mn ds imp = HsModule dummy mn Nothing imp ds
57
73
uptodate = liftIO =<< (isNewerThan <$> outFile <*> ifile)
58
ifile = findFile InterfaceFile =<< curMName
74
ifile = maybe __IMPOSSIBLE__ filePath <$>
75
(findInterfaceFile . toTopLevelModuleName =<< curMName)
59
76
noComp = reportSLn "" 1 . (++ " : no compilation is needed.").show =<< curMName
60
77
yesComp = reportSLn "" 1 . (`repl` "Compiling <<0>> in <<1>> to <<2>>") =<<
61
78
sequence [show <$> curMName, ifile, outFile] :: TCM ()
67
84
--------------------------------------------------
69
86
imports :: TCM [HsImportDecl]
70
imports = (++) <$> unqualImps <*> qualImps where
71
unqualImps = (L.map (decl False) . (unsafeCoerceMod :) . L.map Module) <$>
73
qualImps = L.map (decl True) . uniq <$>
74
((++) <$> importsForPrim <*> (L.map mazMod <$> mnames))
75
decl qual m = HsImportDecl dummy m qual Nothing Nothing
76
mnames = (++) <$> (S.elems <$> gets stImportedModules)
77
<*> (iImportedModules <$> curIF)
78
uniq = L.map head . group . L.sort
87
imports = (++) <$> hsImps <*> imps where
88
hsImps = (L.map decl . S.toList .
89
S.insert unsafeCoerceMod . S.map Module) <$>
91
imps = L.map decl . uniq <$>
92
((++) <$> importsForPrim <*> (L.map mazMod <$> mnames))
93
decl m = HsImportDecl dummy m True Nothing Nothing
94
mnames = (++) <$> (S.elems <$> gets stImportedModules)
95
<*> (iImportedModules <$> curIF)
96
uniq = L.map head . group . L.sort
80
98
--------------------------------------------------
81
99
-- Main compiling clauses
90
108
(infodecl q :) <$> case d of
91
109
Axiom{ axHsDef = Just (HsDefn ty hs) } -> return $ fbWithType ty (fakeExp hs)
92
110
Axiom{} -> return $ fb axiomErr
93
Function{ funClauses = cls } -> mkwhere <$> mapM (clause q) (tag 0 cls)
111
Function{ funClauses = cls } -> function cls
112
Primitive{ primClauses = Just cls } -> function cls
113
Primitive{ primClauses = Nothing, primName = s } -> fb <$> primBody s
94
114
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs, dataHsType = Just ty } -> do
95
115
ccs <- concat <$> mapM checkConstructorType cs
96
116
cov <- checkCover q ty np cs
97
return $ tvaldecl q 0 (np + ni) [] (Just __IMPOSSIBLE__) ++ ccs ++ cov
117
return $ tvaldecl q (dataInduction d) 0 (np + ni) [] (Just __IMPOSSIBLE__) ++ ccs ++ cov
98
118
Datatype{ dataPars = np, dataIxs = ni, dataClause = cl, dataCons = cs, dataHsType = Nothing } -> do
99
119
(ars, cds) <- unzip <$> mapM condecl cs
100
return $ tvaldecl q (maximum (np:ars) - np) (np + ni) cds cl
120
return $ tvaldecl q (dataInduction d) (maximum (np:ars) - np) (np + ni) cds cl
101
121
Constructor{} -> return []
102
Record{ recClause = cl, recFields = flds } -> do
122
Record{ recClause = cl, recCon = c, recFields = flds } -> do
123
let noFields = genericLength flds
103
124
ar <- arity <$> normalise ty
104
return $ tvaldecl q (genericLength flds) ar [cdecl q (genericLength flds)] cl
105
Primitive{ primName = s } -> fb <$> primBody s
126
Nothing -> return $ cdecl q noFields
127
Just c -> snd <$> condecl c
128
return $ tvaldecl q Inductive noFields ar [cd] cl
130
function cls = mkwhere <$> mapM (clause q) (tag 0 cls)
108
132
tag i [cl] = (i, True , cl): []
109
133
tag i (cl:cls) = (i, False, cl): tag (i + 1) cls
171
195
argpatts :: [Arg Pattern] -> [HsPat] -> TCM [HsPat]
172
argpatts ps0 bvs = evalStateT (mapM pat' ps0) bvs where
173
pat (VarP _ ) = do v <- gets head; modify tail; return v
174
pat (DotP _ ) = pat (VarP dummy)
175
pat (ConP q ps) = (HsPParen .).HsPApp <$> lift (conhqn q) <*> mapM pat' ps
176
pat (LitP l ) = return $ HsPLit $ hslit l
196
argpatts ps0 bvs = evalStateT (mapM pat' ps0) bvs
198
pat (VarP _ ) = do v <- gets head; modify tail; return v
199
pat (DotP _ ) = pat (VarP dummy)
200
pat (LitP l ) = return $ HsPLit $ hslit l
201
pat p@(ConP q ps) = do
202
-- Note that irr is applied once for every subpattern, so in the
203
-- worst case it is quadratic in the size of the pattern. I
204
-- suspect that this will not be a problem in practice, though.
205
irrefutable <- lift $ irr p
206
let tilde = if tildesEnabled && irrefutable
207
then HsPParen . HsPIrrPat
209
(tilde . HsPParen) <$>
210
(HsPApp <$> lift (conhqn q) <*> mapM pat' ps)
177
212
pat' = pat . unArg
214
tildesEnabled = False
216
-- | Is the pattern irrefutable?
217
irr :: Pattern -> TCM Bool
218
irr (VarP {}) = return True
219
irr (DotP {}) = return True
220
irr (LitP {}) = return False
222
(&&) <$> singleConstructorType q
223
<*> (and <$> mapM (irr . unArg) ps)
179
225
clausebody :: ClauseBody -> TCM HsExp
180
226
clausebody b0 = runReaderT (go b0) 0 where
181
227
go (Body tm ) = hsCast <$> term tm
222
269
cdecl q n = HsConDecl dummy (unqhname "C" q)
223
270
[ HsUnBangedTy $ HsTyVar $ ihname "a" i | i <- [0 .. n - 1]]
225
tvaldecl :: QName -> Nat -> Nat -> [HsConDecl] -> Maybe Clause -> [HsDecl]
226
tvaldecl q ntv npar cds cl = let
227
(tn, vn) = (unqhname "T" q, unqhname "d" q)
228
tvs = [ ihname "a" i | i <- [0 .. ntv - 1]]
229
pvs = [ HsPVar $ ihname "a" i | i <- [0 .. npar - 1]]
230
in HsFunBind [HsMatch dummy vn pvs (HsUnGuardedRhs unit_con) []] :
231
maybe [HsDataDecl dummy [] tn tvs cds []] (const []) cl
274
-- ^ Is the type inductive or coinductive?
275
-> Nat -> Nat -> [HsConDecl] -> Maybe Clause -> [HsDecl]
276
tvaldecl q ind ntv npar cds cl =
277
HsFunBind [HsMatch dummy vn pvs (HsUnGuardedRhs unit_con) []] :
278
maybe [datatype] (const []) cl
280
(tn, vn) = (unqhname "T" q, unqhname "d" q)
281
tvs = [ ihname "a" i | i <- [0 .. ntv - 1]]
282
pvs = [ HsPVar $ ihname "a" i | i <- [0 .. npar - 1]]
284
-- Inductive data types consisting of a single constructor with a
285
-- single argument are translated into newtypes.
286
datatype = case (ind, cds) of
287
(Inductive, [c@(HsConDecl _ _ [_])]) -> newtyp c
288
(Inductive, [c@(HsRecDecl _ _ [_])]) -> newtyp c
291
newtyp c = HsNewTypeDecl dummy [] tn tvs c []
292
datatyp = HsDataDecl dummy [] tn tvs cds []
233
294
infodecl :: QName -> HsDecl
234
295
infodecl q = fakeD (unqhname "name" q) $ show (show q)
260
321
writeModule :: HsModule -> TCM ()
323
-- Note that GHC assumes that sources use ASCII or UTF-8.
262
324
liftIO . (`UTF8.writeFile` (preamble ++ prettyPrint m)) =<< outFile
264
326
preamble = unlines $ [ "{-# LANGUAGE EmptyDataDecls"
265
327
, " , ExistentialQuantification"
266
328
, " , ScopedTypeVariables"
268
329
, " , NoMonomorphismRestriction"
333
malonzoDir :: TCM FilePath
335
mdir <- optMAlonzoDir <$> commandLineOptions
337
Just dir -> return dir
338
Nothing -> __IMPOSSIBLE__
273
mdir <- gets (optMAlonzoDir . stOptions)
274
(fdir, fn, _) <- splitFilePath . repldot slash . prettyPrint <$> curHsMod
275
let (dir, fp) = (addSlash mdir ++ fdir, addSlash dir ++ fn ++ ".hs")
342
(fdir, fn) <- splitFileName . repldot pathSeparator .
343
prettyPrint <$> curHsMod
344
let dir = mdir </> fdir
345
fp = dir </> replaceExtension fn "hs"
276
346
liftIO $ createDirectoryIfMissing True dir
277
347
return (mdir, fp)
281
351
outFile :: TCM FilePath
282
352
outFile = snd <$> outFile'
284
callGHC :: (Interface, ClockTime) -> TCM ()
287
mdir <- optMAlonzoDir <$> commandLineOptions
354
callGHC :: Interface -> TCM ()
288
358
hsmod <- prettyPrint <$> curHsMod
289
359
MName agdaMod <- curMName
290
360
let outputName = case agdaMod of
291
361
[] -> __IMPOSSIBLE__
293
363
(mdir, fp) <- outFile'
294
opts <- gets (optGhcFlags . stOptions)
364
opts <- optGhcFlags <$> commandLineOptions
295
366
let overridableArgs =
297
368
, "-o", mdir </> show outputName
308
379
args = overridableArgs ++ opts ++ otherArgs
310
382
reportSLn "" 1 $ "calling: " ++ L.intercalate " " (compiler : args)
311
(exitcode, out, err) <- liftIO $ readProcessWithExitCode compiler args ""
383
(inn, out, err, p) <-
384
liftIO $ runInteractiveProcess compiler args Nothing Nothing
388
-- The handles should be in text mode.
389
hSetBinaryMode out False
390
hSetBinaryMode err False
392
-- GHC seems to use stderr for progress reports.
393
s <- liftIO $ join <$> LocIO.hGetContents err <*> LocIO.hGetContents out
396
exitcode <- liftIO $ do
397
-- Ensure that the output has been read before waiting for the
399
E.evaluate (length s)
313
ExitFailure _ -> typeError $ CompilationError $ out ++ "\n" ++ err
402
ExitFailure _ -> typeError (CompilationError s)
406
-- Note that this function returns s1 before inspecting its input.
408
s1 ++ (if L.null s1 || last s1 == '\n' then "" else "\n") ++ s2
added
removed
src/full/Agda/Compiler/MAlonzo/Compiler.hs
