← 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/Primitives.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/Primitives.hs
 
1
{-# LANGUAGE CPP #-}
1
2
module Agda.Compiler.MAlonzo.Primitives where
2
3
 
3
4
import Control.Monad.Reader
18
19
import Agda.TypeChecking.Substitute
19
20
import Agda.TypeChecking.Pretty
20
21
import Agda.Utils.Monad
21
 
 
 
22
import Agda.Utils.Impossible
 
23
import qualified Agda.Utils.HashMap as HMap
 
24
 
 
25
#include "../../undefined.h"
 
26
 
 
27
{- OLD
22
28
-- | Check that the main function has type IO a, for some a.
23
29
checkTypeOfMain :: QName -> Type -> TCM ()
24
30
checkTypeOfMain q ty
25
31
  | show (qnameName q) /= "main" = return ()
26
32
  | otherwise = do
27
 
    Def io _ <- primIO
 
33
    Def io _ <- ignoreSharing <$> primIO
28
34
    ty <- normalise ty
29
 
    case unEl ty of
 
35
    case ignoreSharing $ unEl ty of
30
36
      Def d _ | d == io -> return ()
31
37
      _                 -> do
32
38
        err <- fsep $
33
39
          pwords "The type of main should be" ++
34
40
          [prettyTCM io] ++ pwords " A, for some A. The given type is" ++ [prettyTCM ty]
35
41
        typeError $ GenericError $ show err
 
42
-}
 
43
 
 
44
-- | Check that the main function has type IO a, for some a.
 
45
checkTypeOfMain :: QName -> Type -> TCM [HS.Decl] -> TCM [HS.Decl]
 
46
checkTypeOfMain q ty ret
 
47
  | show (qnameName q) /= "main" = ret
 
48
  | otherwise = do
 
49
    Def io _ <- ignoreSharing <$> primIO
 
50
    ty <- normalise ty
 
51
    case ignoreSharing $ unEl ty of
 
52
      Def d _ | d == io -> (mainAlias :) <$> ret
 
53
      _                 -> do
 
54
        err <- fsep $
 
55
          pwords "The type of main should be" ++
 
56
          [prettyTCM io] ++ pwords " A, for some A. The given type is" ++ [prettyTCM ty]
 
57
        typeError $ GenericError $ show err
 
58
  where
 
59
    mainAlias = HS.FunBind [HS.Match dummy mainLHS [] Nothing mainRHS $ HS.BDecls [] ]
 
60
    mainLHS   = HS.Ident "main"
 
61
    mainRHS   = HS.UnGuardedRhs $ HS.Var $ HS.UnQual $ unqhname "d" q
36
62
 
37
63
-- Haskell modules to be imported for BUILT-INs
38
64
importsForPrim :: TCM [HS.ModuleName]
39
65
importsForPrim =
40
66
  xForPrim $
41
67
  L.map (\(s, ms) -> (s, return (L.map HS.ModuleName ms))) $
42
 
  [ "CHAR" |-> ["Data.Char"]
43
 
  -- , "IO" |-> ["System.IO"]
 
68
  [ "CHAR"           |-> ["Data.Char"]
 
69
  , "primIsDigit"    |-> ["Data.Char"]
 
70
  , "primIsLower"    |-> ["Data.Char"]
 
71
  , "primIsDigit"    |-> ["Data.Char"]
 
72
  , "primIsAlpha"    |-> ["Data.Char"]
 
73
  , "primIsSpace"    |-> ["Data.Char"]
 
74
  , "primIsAscii"    |-> ["Data.Char"]
 
75
  , "primIsLatin1"   |-> ["Data.Char"]
 
76
  , "primIsPrint"    |-> ["Data.Char"]
 
77
  , "primIsHexDigit" |-> ["Data.Char"]
 
78
  , "primToUpper"    |-> ["Data.Char"]
 
79
  , "primToLower"    |-> ["Data.Char"]
44
80
  ]
45
81
  where (|->) = (,)
46
82
 
107
143
 
108
144
xForPrim :: [(String, TCM [a])] -> TCM [a]
109
145
xForPrim table = do
110
 
  qs <- keys   <$> curDefs
 
146
  qs <- HMap.keys <$> curDefs
111
147
  bs <- toList <$> gets stBuiltinThings
 
148
  let getName (Builtin (Def q _))    = q
 
149
      getName (Builtin (Con q _))    = q
 
150
      getName (Builtin (Shared p))   = getName (Builtin $ derefPtr p)
 
151
      getName (Builtin _)            = __IMPOSSIBLE__
 
152
      getName (Prim (PrimFun q _ _)) = q
112
153
  concat <$> sequence [ maybe (return []) id $ L.lookup s table
113
 
                        | (s, Builtin (Def q _)) <- bs, q `elem` qs ]
 
154
                        | (s, def) <- bs, getName def `elem` qs ]
114
155
 
115
156
 
116
157
-- Definition bodies for primitive functions
165
206
  , "primIsAscii"        |-> pred "Data.Char.isAscii"
166
207
  , "primIsLatin1"       |-> pred "Data.Char.isLatin1"
167
208
  , "primIsPrint"        |-> pred "Data.Char.isPrint"
168
 
  , "primIsHExDigit"     |-> pred "Data.Char.isHexDigit"
 
209
  , "primIsHexDigit"     |-> pred "Data.Char.isHexDigit"
169
210
  , "primToUpper"        |-> return "Data.Char.toUpper"
170
211
  , "primToLower"        |-> return "Data.Char.toLower"
171
212
  , "primCharToNat" |-> do toN <- bltQual' "NATURAL" mazIntToNat
218
259
  unimplemented = typeError $ NotImplemented s
219
260
 
220
261
  lam x t = Lam Hidden (Abs x t)
 
262
{- UNUSED
221
263
  var x   = Arg Hidden Relevant (Var x [])
 
264
-}
222
265
 
223
266
----------------------
224
267