← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Monad/Builtin.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Monad/Builtin.hs
 
1
{-# LANGUAGE CPP #-}
1
2
 
2
3
module Agda.TypeChecking.Monad.Builtin where
3
4
 
 
5
import Control.Applicative
4
6
import Control.Monad.Error
5
7
import Control.Monad.State
6
8
 
7
9
import Data.Functor
8
10
import qualified Data.Map as Map
9
11
 
 
12
import Agda.Syntax.Common
10
13
import Agda.Syntax.Position
11
14
import Agda.Syntax.Literal
12
15
import Agda.Syntax.Internal
13
16
import Agda.TypeChecking.Monad.Base
 
17
import Agda.TypeChecking.Substitute
14
18
 
15
19
import Agda.Utils.Monad (when_)
 
20
import Agda.Utils.Maybe
 
21
import Agda.Utils.Tuple
 
22
 
 
23
#include "../../undefined.h"
 
24
import Agda.Utils.Impossible
 
25
 
 
26
class (Functor m, Applicative m, Monad m) => HasBuiltins m where
 
27
  getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))
16
28
 
17
29
litType :: Literal -> TCM Type
18
30
litType l = case l of
27
39
  where
28
40
    el t = El (mkType 0) t
29
41
 
30
 
getBuiltinThing :: String -> TCM (Maybe (Builtin PrimFun))
31
 
getBuiltinThing b = liftM2 mplus (Map.lookup b <$> gets stLocalBuiltins)
32
 
                    (Map.lookup b <$> gets stImportedBuiltins)
 
42
instance MonadIO m => HasBuiltins (TCMT m) where
 
43
  getBuiltinThing b = liftM2 mplus (Map.lookup b <$> gets stLocalBuiltins)
 
44
                      (Map.lookup b <$> gets stImportedBuiltins)
33
45
 
34
46
setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
35
47
setBuiltinThings b = modify $ \s -> s { stLocalBuiltins = b }
50
62
  builtin <- gets stLocalBuiltins
51
63
  setBuiltinThings $ Map.insert b (Prim pf) builtin
52
64
 
53
 
 
54
65
getBuiltin :: String -> TCM Term
55
 
getBuiltin x = do
56
 
    mt <- getBuiltin' x
57
 
    case mt of
58
 
        Nothing -> typeError $ NoBindingForBuiltin x
59
 
        Just t  -> return t
 
66
getBuiltin x =
 
67
  fromMaybeM (typeError $ NoBindingForBuiltin x) $ getBuiltin' x
60
68
 
61
 
getBuiltin' :: String -> TCM (Maybe Term)
 
69
getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
62
70
getBuiltin' x = do
63
71
    builtin <- getBuiltinThing x
64
72
    case builtin of
65
73
        Just (Builtin t) -> return $ Just (killRange t)
66
74
        _                -> return Nothing
67
75
 
 
76
getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
 
77
getPrimitive' x = (getPrim =<<) <$> getBuiltinThing x
 
78
  where
 
79
    getPrim (Prim pf) = return pf
 
80
    getPrim _         = Nothing
 
81
 
68
82
getPrimitive :: String -> TCM PrimFun
69
 
getPrimitive x = do
70
 
    builtin <- getBuiltinThing x
71
 
    case builtin of
72
 
        Just (Prim pf) -> return pf
73
 
        _              -> typeError $ NoSuchPrimitiveFunction x
 
83
getPrimitive x =
 
84
  fromMaybeM (typeError $ NoSuchPrimitiveFunction x) $ getPrimitive' x
 
85
 
 
86
-- | Rewrite a literal to constructor form if possible.
 
87
constructorForm :: Term -> TCM Term
 
88
constructorForm v = constructorForm' primZero primSuc v
 
89
 
 
90
constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
 
91
constructorForm' pZero pSuc v = case ignoreSharing v of
 
92
{- 2012-04-02 changed semantics of DontCare
 
93
-- Andreas, 2011-10-03, the following line restores IrrelevantLevel
 
94
    DontCare v                  -> constructorForm v
 
95
-}
 
96
    Lit (LitInt r n)            -> cons (Lit . LitInt r) n
 
97
--     Level (Max [])              -> primLevelZero
 
98
--     Level (Max [ClosedLevel n]) -> cons primLevelZero primLevelSuc (Level . Max . (:[]) . ClosedLevel) n
 
99
    _                           -> pure v
 
100
  where
 
101
    cons lit n
 
102
      | n == 0    = pZero
 
103
      | n > 0     = (`apply` [defaultArg $ lit $ n - 1]) <$> pSuc
 
104
      | otherwise = pure v
74
105
 
75
106
---------------------------------------------------------------------------
76
107
-- * The names of built-in things
84
115
    primInf, primSharp, primFlat,
85
116
    primEquality, primRefl,
86
117
    primLevel, primLevelZero, primLevelSuc, primLevelMax,
87
 
    primIrrAxiom,
 
118
    primIrrAxiom, primSizeMax,
88
119
    -- builtins for reflection:
89
 
    primQName, primArg, primArgArg, primAgdaTerm, primAgdaTermVar,
 
120
    primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAgdaTerm, primAgdaTermVar,
90
121
    primAgdaTermLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
91
122
    primAgdaTermSort, primAgdaTermUnsupported,
92
123
    primAgdaType, primAgdaTypeEl,
146
177
primRelevance    = getBuiltin builtinRelevance
147
178
primRelevant     = getBuiltin builtinRelevant
148
179
primIrrelevant   = getBuiltin builtinIrrelevant
 
180
primArgInfo      = getBuiltin builtinArgInfo
 
181
primArgArgInfo   = getBuiltin builtinArgArgInfo
149
182
primAgdaSortSet  = getBuiltin builtinAgdaSortSet
150
183
primAgdaSortLit  = getBuiltin builtinAgdaSortLit
151
184
primAgdaSortUnsupported = getBuiltin builtinAgdaSortUnsupported
218
251
builtinRelevant     = "RELEVANT"
219
252
builtinIrrelevant   = "IRRELEVANT"
220
253
builtinArg          = "ARG"
 
254
builtinArgInfo      = "ARGINFO"
 
255
builtinArgArgInfo   = "ARGARGINFO"
221
256
builtinArgArg       = "ARGARG"
222
257
builtinAgdaTerm         = "AGDATERM"
223
258
builtinAgdaTermVar      = "AGDATERMVAR"
259
294
    , nameOfFlat  = flat
260
295
    })
261
296
    `catchError` \_ -> return Nothing
 
297
 
 
298
------------------------------------------------------------------------
 
299
-- * Builtin equality
 
300
------------------------------------------------------------------------
 
301
 
 
302
-- | Get the name of the equality type.
 
303
primEqualityName :: TCM QName
 
304
primEqualityName = do
 
305
  eq <- primEquality
 
306
  -- Andreas, 2014-05-17 moved this here from TC.Rules.Def
 
307
  -- Don't know why up to 2 hidden lambdas need to be stripped,
 
308
  -- but I left the code in place.
 
309
  -- Maybe it was intended that equality could be declared
 
310
  -- in three different ways:
 
311
  -- 1. universe and type polymorphic
 
312
  -- 2. type polymorphic only
 
313
  -- 3. monomorphic.
 
314
  let lamV (Lam i b)  = mapFst (getHiding i :) $ lamV (unAbs b)
 
315
      lamV (Shared p) = lamV (derefPtr p)
 
316
      lamV v          = ([], v)
 
317
  return $ case lamV eq of
 
318
    ([Hidden, Hidden], Def equality _) -> equality
 
319
    ([Hidden],         Def equality _) -> equality
 
320
    ([],               Def equality _) -> equality
 
321
    _                                  -> __IMPOSSIBLE__
 
322