← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Compiler/MAlonzo/Compiler.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Compiler/MAlonzo/Compiler.hs
3
3
module Agda.Compiler.MAlonzo.Compiler where
4
4
 
5
5
import Control.Applicative
6
 
import qualified Control.Exception as E
 
6
import Control.Monad ((<=<))
7
7
import Control.Monad.Reader
8
8
import Control.Monad.State
9
9
import Data.Char
14
14
import qualified Language.Haskell.Exts.Parser as HS
15
15
import qualified Language.Haskell.Exts.Syntax as HS
16
16
import System.Cmd
17
 
import System.Directory
18
 
import System.Exit
19
 
import System.IO
20
 
import System.Time
21
 
import System.Process
22
 
import System.FilePath hiding (normalise, (<.>))
 
17
import System.Directory (createDirectoryIfMissing)
 
18
import System.FilePath hiding (normalise)
23
19
 
 
20
import Agda.Compiler.CallCompiler
24
21
import Agda.Compiler.MAlonzo.Misc
25
22
import Agda.Compiler.MAlonzo.Pretty
26
23
import Agda.Compiler.MAlonzo.Primitives
32
29
import Agda.Syntax.Internal
33
30
import Agda.Syntax.Literal
34
31
import Agda.TypeChecking.Monad
 
32
import Agda.TypeChecking.Monad.Builtin
35
33
import Agda.TypeChecking.Monad.Options
36
34
import Agda.TypeChecking.Reduce
37
 
import Agda.TypeChecking.Rules.Builtin.Coinduction
 
35
-- import Agda.TypeChecking.Rules.Builtin.Coinduction
38
36
import Agda.TypeChecking.Pretty
39
37
import Agda.TypeChecking.Substitute
 
38
import Agda.TypeChecking.Telescope
40
39
import Agda.TypeChecking.Level (reallyUnLevelView)
41
40
import Agda.Utils.FileName
42
41
import Agda.Utils.Monad
43
 
import qualified Agda.Utils.IO.Locale as LocIO
44
42
import qualified Agda.Utils.IO.UTF8 as UTF8
45
43
import Agda.Utils.Impossible
 
44
import qualified Agda.Utils.HashMap as HMap
46
45
 
47
46
#include "../../undefined.h"
48
47
 
49
48
compilerMain :: Interface -> TCM ()
50
49
compilerMain mainI =
51
50
  -- Preserve the state (the compiler modifies the state).
52
 
  bracket get put $ \_ -> do
 
51
  localState $ do
53
52
 
54
53
    -- Compute the output directory.
55
54
    opts <- commandLineOptions
107
106
definitions :: Definitions -> TCM [HS.Decl]
108
107
definitions defs = do
109
108
  kit <- coinductionKit
110
 
  M.fold (liftM2 (++) . (definition kit <.> instantiateFull))
111
 
         declsForPrim
112
 
         defs
 
109
  HMap.foldr (liftM2 (++) . (definition kit <=< instantiateFull))
 
110
             declsForPrim defs
113
111
 
114
112
-- | Note that the INFINITY, SHARP and FLAT builtins are translated as
115
113
-- follows (if a 'CoinductionKit' is given):
120
118
--   sharp :: a -> a
121
119
--   sharp x = x
122
120
--
 
121
--   flat :: a -> a
 
122
--   flat x = x
123
123
-- @
124
124
 
125
125
definition :: Maybe CoinductionKit -> Definition -> TCM [HS.Decl]
126
126
-- ignore irrelevant definitions
127
 
definition kit (Defn Forced     _ _  _ _ _ _) = __IMPOSSIBLE__
128
 
definition kit (Defn NonStrict  _ _  _ _ _ _) = __IMPOSSIBLE__
129
 
definition kit (Defn Irrelevant _ _  _ _ _ _) = return []
130
 
definition kit (Defn Relevant   q ty _ _ compiled d) = do
131
 
  checkTypeOfMain q ty
 
127
{- Andreas, 2012-10-02: Invariant no longer holds
 
128
definition kit (Defn Forced     _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
 
129
definition kit (Defn UnusedArg  _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
 
130
definition kit (Defn NonStrict  _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
 
131
-}
 
132
definition kit (Defn Irrelevant _ _  _ _ _ _ _ _) = return []
 
133
definition kit (Defn _          q ty _ _ _ _ compiled d) = do
 
134
  checkTypeOfMain q ty $ do
132
135
  (infodecl q :) <$> case d of
133
136
 
134
137
    _ | Just (HsDefn ty hs) <- compiledHaskell compiled ->
168
169
          x    = ihname "x" 0
169
170
      return $
170
171
        [ HS.TypeSig dummy [flat] $ fakeType $
171
 
            "forall a. () -> forall b. () -> b -> b"
 
172
            "forall a. a -> a"
172
173
        , HS.FunBind [HS.Match dummy flat
173
 
                               [HS.PWildCard, HS.PWildCard, HS.PVar x]
 
174
                               [HS.PVar x]
174
175
                               Nothing
175
176
                               (HS.UnGuardedRhs (HS.Var (HS.UnQual x)))
176
177
                               (HS.BDecls [])]
242
243
conArityAndPars :: QName -> TCM (Nat, Nat)
243
244
conArityAndPars q = do
244
245
  def <- getConstInfo q
245
 
  TelV tel _ <- telViewM $ defType def
 
246
  TelV tel _ <- telView $ defType def
246
247
  let Constructor{ conPars = np } = theDef def
247
248
      n = genericLength (telToList tel)
248
249
  return (n - np, np)
301
302
  irr (LitP {})   = return False
302
303
  irr (ConP q _ ps) =
303
304
    (&&) <$> singleConstructorType q
304
 
         <*> (and <$> mapM irr' ps)
 
305
         <*> (andM $ L.map irr' ps)
305
306
 
306
307
  -- | Irrelevant patterns are naturally irrefutable.
307
308
  irr' (Arg _ Irrelevant _) = return $ True
319
320
--   Types are extracted as @()@.
320
321
--   @DontCare@ outside of irrelevant arguments is extracted as @error@.
321
322
term :: Term -> ReaderT Nat TCM HS.Exp
322
 
term tm0 = case tm0 of
 
323
term tm0 = case ignoreSharing tm0 of
323
324
  Var   i as -> do n <- ask; apps (hsVarUQ $ ihname "v" (n - i - 1)) as
324
325
  Lam   _ at -> do n <- ask; HS.Lambda dummy [HS.PVar $ ihname "v" n] <$>
325
326
                              local (1+) (term $ absBody at)
335
336
  Sort  _    -> return HS.unit_con
336
337
  MetaV _ _  -> mazerror "hit MetaV"
337
338
  DontCare _ -> return $ rtmError $ "hit DontCare"
 
339
  Shared{}   -> __IMPOSSIBLE__
338
340
  where apps =  foldM (\h a -> HS.App h <$> term' a)
339
341
 
340
342
-- | Irrelevant arguments are replaced by Haskells' ().
444
446
        , "ExistentialQuantification"
445
447
        , "ScopedTypeVariables"
446
448
        , "NoMonomorphismRestriction"
 
449
        , "Rank2Types"
447
450
        ]
448
451
 
449
452
rteModule :: HS.Module
466
469
  ]
467
470
  where
468
471
    parse = HS.parseWithMode
469
 
              HS.defaultParseMode{HS.extensions = [HS.ExplicitForall]}
470
 
 
 
472
              HS.defaultParseMode{HS.extensions = [explicitForAll]}
471
473
    ok (HS.ParseOk d)   = d
472
474
    ok HS.ParseFailed{} = __IMPOSSIBLE__
473
475
 
 
476
explicitForAll :: HS.Extension
 
477
explicitForAll =
 
478
-- GHC 7.0.1 cannot parse the following CPP conditional
 
479
-- error: missing binary operator before token "("
 
480
#if MIN_VERSION_haskell_src_exts(1,12,0)
 
481
  HS.ExplicitForAll
 
482
#else
 
483
  HS.ExplicitForall
 
484
#endif
474
485
 
475
486
compileDir :: TCM FilePath
476
487
compileDir = do
511
522
  let overridableArgs =
512
523
        [ "-O"
513
524
        , "-o", mdir </> show outputName
 
525
        , "-Werror"
514
526
        ]
515
527
      otherArgs       =
516
528
        [ "-i" ++ mdir
519
531
        , "--make"
520
532
        , "-fwarn-incomplete-patterns"
521
533
        , "-fno-warn-overlapping-patterns"
522
 
        , "-Werror"
523
534
        ]
524
535
      args     = overridableArgs ++ opts ++ otherArgs
525
536
      compiler = "ghc"
527
538
  -- Note: Some versions of GHC use stderr for progress reports. For
528
539
  -- those versions of GHC we don't print any progress information
529
540
  -- unless an error is encountered.
530
 
 
531
 
  reportSLn "" 1 $ "calling: " ++ L.intercalate " " (compiler : args)
532
 
  (_, _, err, p) <-
533
 
    liftIO $ createProcess (proc compiler args){ std_err = CreatePipe }
534
 
 
535
 
  errors <- liftIO $ case err of
536
 
    Nothing  -> __IMPOSSIBLE__
537
 
    Just err -> do
538
 
      -- The handle should be in text mode.
539
 
      hSetBinaryMode err False
540
 
      liftIO $ LocIO.hGetContents err
541
 
 
542
 
  exitcode <- liftIO $ do
543
 
    -- Ensure that the output has been read before waiting for the
544
 
    -- process.
545
 
    E.evaluate (length errors)
546
 
    waitForProcess p
547
 
  case exitcode of
548
 
    ExitFailure _ -> typeError (CompilationError errors)
549
 
    _             -> return ()
 
541
  callCompiler compiler args