← 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/Primitive.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/Primitive.hs
1
 
{-# LANGUAGE CPP, FlexibleInstances, UndecidableInstances,
2
 
             GeneralizedNewtypeDeriving, ScopedTypeVariables
3
 
  #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE FlexibleInstances #-}
 
3
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
4
{-# LANGUAGE ScopedTypeVariables #-}
 
5
{-# LANGUAGE TypeSynonymInstances #-}
 
6
{-# LANGUAGE UndecidableInstances #-}
4
7
 
5
8
{-| Primitive functions, such as addition on builtin integers.
6
9
-}
7
10
module Agda.TypeChecking.Primitive where
8
11
 
9
12
import Control.Monad
10
 
import Control.Monad.Error
 
13
import Control.Applicative
 
14
 
 
15
import Data.Char
11
16
import Data.Map (Map)
12
17
import qualified Data.Map as Map
13
 
import Data.Char
14
18
 
15
19
import Agda.Interaction.Options
16
20
 
17
21
import Agda.Syntax.Position
18
22
import Agda.Syntax.Common hiding (Nat)
19
 
import Agda.Syntax.Internal
 
23
import Agda.Syntax.Internal as I
20
24
import Agda.Syntax.Literal
21
25
import Agda.Syntax.Concrete.Pretty ()
22
 
import Agda.Syntax.Abstract.Name
23
 
import qualified Agda.Syntax.Concrete.Name as C
24
26
 
25
 
import Agda.TypeChecking.Monad
 
27
import Agda.TypeChecking.Monad hiding (getConstInfo, typeOfConst)
 
28
import qualified Agda.TypeChecking.Monad as TCM
26
29
import Agda.TypeChecking.Monad.Builtin
27
30
import Agda.TypeChecking.Reduce
 
31
import Agda.TypeChecking.Reduce.Monad
28
32
import Agda.TypeChecking.Substitute
29
33
import Agda.TypeChecking.Errors
30
 
import Agda.TypeChecking.Quote (quoteType, quotingKit)
 
34
import Agda.TypeChecking.Level
 
35
import Agda.TypeChecking.Quote (quotingKit)
31
36
import Agda.TypeChecking.Pretty ()  -- instances only
32
 
import {-# SOURCE #-} Agda.TypeChecking.Conversion
33
 
import Agda.TypeChecking.Constraints
34
 
import Agda.TypeChecking.Level
35
37
 
36
38
import Agda.Utils.Monad
37
39
import Agda.Utils.Pretty (pretty)
 
40
import Agda.Utils.Maybe
38
41
 
39
42
#include "../undefined.h"
40
43
import Agda.Utils.Impossible
41
 
 
42
 
constructorForm :: Term -> TCM Term
43
 
constructorForm v = case ignoreSharing v of
44
 
{- 2012-04-02 changed semantics of DontCare
45
 
    DontCare v                  -> constructorForm v
46
 
-}
47
 
    Lit (LitInt r n)            -> cons primZero primSuc (Lit . LitInt r) n
48
 
    _                           -> return v
49
 
  where
50
 
    cons pZero pSuc lit n
51
 
      | n == 0  = pZero
52
 
      | n > 0   = do
53
 
        s <- pSuc
54
 
        return $ s `apply` [defaultArg $ lit $ n - 1]
55
 
      | otherwise       = return v
 
44
import Debug.Trace
56
45
 
57
46
---------------------------------------------------------------------------
58
47
-- * Primitive functions
70
55
    deriving (Eq, Ord)
71
56
 
72
57
newtype Nat = Nat { unNat :: Integer }
73
 
    deriving (Eq, Ord, Num, Integral, Enum, Real)
 
58
    deriving (Eq, Ord, Num, Enum, Real)
 
59
 
 
60
-- TODO: ghc-7.7 bug: deriving Integral causes an unnecessary toInteger
 
61
-- warning. Once 7.8 is out check if we can go back to deriving.
 
62
instance Integral Nat where
 
63
  toInteger = unNat
 
64
  quotRem (Nat a) (Nat b) = (Nat q, Nat r)
 
65
    where (q, r) = quotRem a b
74
66
 
75
67
newtype Lvl = Lvl { unLvl :: Integer }
76
68
  deriving (Eq, Ord)
147
139
 
148
140
-- From Haskell value to Agda term
149
141
 
150
 
type FromTermFunction a = Arg Term -> TCM (Reduced (MaybeReduced (Arg Term)) a)
 
142
type FromTermFunction a = I.Arg Term -> ReduceM (Reduced (MaybeReduced (I.Arg Term)) a)
151
143
 
152
144
class FromTerm a where
153
145
    fromTerm :: TCM (FromTermFunction a)
213
205
    where
214
206
      isCon (Lam _ b)  = isCon $ absBody b
215
207
      isCon (Con c _)  = return c
216
 
      isCon (Shared p) = isCon (derefPtr p)
217
 
      isCon v          = do
218
 
        d <- prettyTCM v
219
 
        typeError $ GenericError $ "expected constructor in built-in binding to " ++ show d
220
 
                        -- TODO: check this when binding the things
 
208
      isCon (Shared p) = __IMPOSSIBLE__ -- isCon (derefPtr p)
 
209
      isCon v          = __IMPOSSIBLE__
221
210
 
222
211
      mkList nil cons toA fromA t = do
223
 
        b <- reduceB t
 
212
        b <- reduceB' t
224
213
        let t = ignoreBlocking b
225
 
        let arg = Arg (argHiding t) (argRelevance t)
 
214
        let arg = Arg (ArgInfo { argInfoHiding = getHiding t
 
215
                               , argInfoRelevance = getRelevance t
 
216
                               , argInfoColors = argColors t
 
217
                               })
226
218
        case unArg t of
227
219
          Con c []
228
 
            | c == nil  -> return $ YesReduction []
 
220
            | c == nil  -> return $ YesReduction NoSimplification []
229
221
          Con c [x,xs]
230
222
            | c == cons ->
231
223
              redBind (toA x)
237
229
          _ -> return $ NoReduction (reduced b)
238
230
 
239
231
-- | Conceptually: @redBind m f k = either (return . Left . f) k =<< m@
240
 
redBind :: TCM (Reduced a a') -> (a -> b) ->
241
 
             (a' -> TCM (Reduced b b')) -> TCM (Reduced b b')
 
232
redBind :: ReduceM (Reduced a a') -> (a -> b) ->
 
233
             (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
242
234
redBind ma f k = do
243
235
    r <- ma
244
236
    case r of
245
 
        NoReduction x   -> return $ NoReduction $ f x
246
 
        YesReduction y  -> k y
 
237
        NoReduction x    -> return $ NoReduction $ f x
 
238
        YesReduction _ y -> k y
247
239
 
248
 
redReturn :: a -> TCM (Reduced a' a)
249
 
redReturn = return . YesReduction
 
240
redReturn :: a -> ReduceM (Reduced a' a)
 
241
redReturn = return . YesReduction YesSimplification
250
242
 
251
243
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
252
244
fromReducedTerm f = return $ \t -> do
253
 
    b <- reduceB t
 
245
    b <- reduceB' t
254
246
    case f $ ignoreSharing $ unArg (ignoreBlocking b) of
255
 
        Just x  -> return $ YesReduction x
 
247
        Just x  -> return $ YesReduction NoSimplification x
256
248
        Nothing -> return $ NoReduction (reduced b)
257
249
 
258
250
fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
272
264
          El (varSort 3) <$>
273
265
            primEquality <#> varM 3 <#> varM 2 <@> varM 1 <@> varM 0
274
266
  Con rf [] <- ignoreSharing <$> primRefl
275
 
  n         <- conPars . theDef <$> getConstInfo rf
276
 
  let refl x | n == 2    = Con rf [Arg Hidden Forced x]
 
267
  n         <- conPars . theDef <$> getConInfo rf
 
268
  let refl x | n == 2    = Con rf [setRelevance Forced $ hide $ defaultArg x]
277
269
             | n == 3    = Con rf []
278
270
             | otherwise = __IMPOSSIBLE__
279
271
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 4 $ \ts ->
280
272
      case ts of
281
 
        [a, t, x, y] -> liftTCM $ do
 
273
        [a, t, u, v] -> do
 
274
            -- Andreas, 2013-07-22.
 
275
            -- Note that we cannot call the conversion checker here,
 
276
            -- because 'reduce' might be called in a context where
 
277
            -- some bound variables do not have a type (just 'Prop),
 
278
            -- and the conversion checker for eliminations does not
 
279
            -- like this.
 
280
            -- We can only do untyped equality, e.g., by normalisation.
 
281
            (u', v') <- normalise' (u, v)
 
282
            if (u' == v') then redReturn (refl $ unArg u) else
 
283
              return (NoReduction $ map notReduced [a, t, u, v])
 
284
{- OLD:
 
285
 
 
286
              -- BAD:
282
287
              noConstraints $
283
 
                equalTerm (El (Type $ lvlView $ unArg a) (unArg t))
284
 
                          (unArg x) (unArg y)
285
 
              redReturn (refl $ unArg x)
286
 
            `catchError` \_ -> return (NoReduction $ map notReduced [a, t, x, y])
 
288
                equalTerm (El (Type $ lvlView $ unArg a) (unArg t)) (unArg u) (unArg v)
 
289
              redReturn (refl $ unArg u)
 
290
            `catchError` \_ -> return (NoReduction $ map notReduced [a, t, u, v])
 
291
-}
287
292
        _ -> __IMPOSSIBLE__
288
293
 
289
294
primQNameType :: TCM PrimitiveImpl
290
 
primQNameType = mkPrimFun1TCM (el primQName --> el primAgdaType) typeOfConst
 
295
primQNameType = mkPrimFun1TCM (el primQName --> el primAgdaType)
 
296
                              (\q -> defType <$> getConstInfo q)
 
297
  -- Note: gets the top-level type! All bounds variables have been lifted.
291
298
 
292
299
primQNameDefinition :: TCM PrimitiveImpl
293
300
primQNameDefinition = do
 
301
  agdaFunDef                    <- primAgdaDefinitionFunDef
 
302
  agdaDefinitionFunDef          <- primAgdaDefinitionFunDef
 
303
  agdaDefinitionDataDef         <- primAgdaDefinitionDataDef
 
304
  agdaDefinitionRecordDef       <- primAgdaDefinitionRecordDef
 
305
  agdaDefinitionPostulate       <- primAgdaDefinitionPostulate
 
306
  agdaDefinitionPrimitive       <- primAgdaDefinitionPrimitive
 
307
  agdaDefinitionDataConstructor <- primAgdaDefinitionDataConstructor
 
308
 
294
309
  let argQName qn = [defaultArg (Lit (LitQName noRange qn))]
295
 
      app mt xs = do t <- mt
296
 
                     return $ apply t xs
297
 
 
298
 
      con qn Function{}    = app primAgdaDefinitionFunDef    (argQName qn)
299
 
      con qn Datatype{}    = app primAgdaDefinitionDataDef   (argQName qn)
300
 
      con qn Record{}      = app primAgdaDefinitionRecordDef (argQName qn)
301
 
      con _  Axiom{}       = app primAgdaDefinitionPostulate []
302
 
      con _  Primitive{}   = app primAgdaDefinitionPrimitive []
303
 
      con _  Constructor{} = app primAgdaDefinitionDataConstructor []
 
310
      con qn Function{}    = apply agdaDefinitionFunDef    (argQName qn)
 
311
      con qn Datatype{}    = apply agdaDefinitionDataDef   (argQName qn)
 
312
      con qn Record{}      = apply agdaDefinitionRecordDef (argQName qn)
 
313
      con _  Axiom{}       = apply agdaDefinitionPostulate []
 
314
      con _  Primitive{}   = apply agdaDefinitionPrimitive []
 
315
      con _  Constructor{} = apply agdaDefinitionDataConstructor []
304
316
 
305
317
  unquoteQName <- fromTerm
306
318
  t <- el primQName --> el primAgdaDefinition
307
319
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 1 $ \ts ->
308
320
    case ts of
309
 
      [v] -> liftTCM $
 
321
      [v] ->
310
322
        redBind (unquoteQName v)
311
323
            (\v' -> [v']) $ \x ->
312
 
        redReturn =<< con x . theDef =<< getConstInfo x
 
324
        redReturn =<< (con x . theDef <$> getConstInfo x)
313
325
      _ -> __IMPOSSIBLE__
314
326
 
315
327
primDataConstructors :: TCM PrimitiveImpl
316
 
primDataConstructors = mkPrimFun1TCM (el primAgdaDataDef --> el (list primQName))
317
 
                                     (fmap (dataCons . theDef) . getConstInfo)
 
328
primDataConstructors =
 
329
  mkPrimFun1TCM (el primAgdaDataDef --> el (list primQName))
 
330
                (fmap (dataCons . theDef) . getConstInfo)
318
331
 
319
332
mkPrimLevelZero :: TCM PrimitiveImpl
320
333
mkPrimLevelZero = do
324
337
mkPrimLevelSuc :: TCM PrimitiveImpl
325
338
mkPrimLevelSuc = do
326
339
  t <- primType (id :: Lvl -> Lvl)
327
 
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 1 $ \ ~[a] -> liftTCM $ do
328
 
    l <- levelView $ unArg a
 
340
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 1 $ \ ~[a] -> do
 
341
    l <- levelView' $ unArg a
329
342
    redReturn $ Level $ levelSuc l
330
343
 
331
344
mkPrimLevelMax :: TCM PrimitiveImpl
332
345
mkPrimLevelMax = do
333
346
  t <- primType (max :: Op Lvl)
334
 
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 2 $ \ ~[a, b] -> liftTCM $ do
335
 
    Max as <- levelView $ unArg a
336
 
    Max bs <- levelView $ unArg b
 
347
  return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 2 $ \ ~[a, b] -> do
 
348
    Max as <- levelView' $ unArg a
 
349
    Max bs <- levelView' $ unArg b
337
350
    redReturn $ Level $ levelMax $ as ++ bs
338
351
 
339
 
mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> TCM b) -> TCM PrimitiveImpl
 
352
mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
340
353
mkPrimFun1TCM mt f = do
341
354
    toA   <- fromTerm
342
355
    fromB <- toTerm
343
356
    t     <- mt
344
357
    return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 1 $ \ts ->
345
358
      case ts of
346
 
        [v] -> liftTCM $
 
359
        [v] ->
347
360
          redBind (toA v)
348
361
              (\v' -> [v']) $ \x ->
349
362
          redReturn . fromB =<< f x
358
371
    t     <- primType f
359
372
    return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 1 $ \ts ->
360
373
      case ts of
361
 
        [v] -> liftTCM $
 
374
        [v] ->
362
375
          redBind (toA v)
363
376
              (\v' -> [v']) $ \x ->
364
377
          redReturn $ fromB $ f x
374
387
    t     <- primType f
375
388
    return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 2 $ \ts ->
376
389
      case ts of
377
 
        [v,w] -> liftTCM $
 
390
        [v,w] ->
378
391
          redBind (toA v)
379
392
              (\v' -> [v', notReduced w]) $ \x ->
380
393
          redBind (toB w)
381
 
              (\w' -> [ reduced $ notBlocked $ Arg (argHiding v) (argRelevance v) (fromA x)
 
394
              (\w' -> [ reduced $ notBlocked $ Arg (argInfo v) (fromA x)
382
395
                      , w']) $ \y ->
383
396
          redReturn $ fromC $ f x y
384
397
        _ -> __IMPOSSIBLE__
398
411
    t <- primType f
399
412
    return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 4 $ \ts ->
400
413
      let argFrom fromX a x =
401
 
            reduced $ notBlocked $ Arg (argHiding a) (argRelevance a) (fromX x)
 
414
            reduced $ notBlocked $ Arg (argInfo a) (fromX x)
402
415
      in case ts of
403
 
        [a,b,c,d] -> liftTCM $
 
416
        [a,b,c,d] ->
404
417
          redBind (toA a)
405
418
              (\a' -> a' : map notReduced [b,c,d]) $ \x ->
406
419
          redBind (toB b)
425
438
a --> b = do
426
439
    a' <- a
427
440
    b' <- b
428
 
    return $ El (getSort a' `sLub` getSort b') $ Pi (Dom NotHidden Relevant a') (NoAbs "_" b')
 
441
    return $ El (getSort a' `sLub` getSort b') $ Pi (Dom defaultArgInfo a') (NoAbs "_" b')
429
442
 
430
443
infixr 4 .-->
431
444
 
433
446
a .--> b = do
434
447
    a' <- a
435
448
    b' <- b
436
 
    return $ El (getSort a' `sLub` getSort b') $ Pi (Dom NotHidden Irrelevant a') (NoAbs "_" b')
 
449
    return $ El (getSort a' `sLub` getSort b') $
 
450
             Pi (Dom (setRelevance Irrelevant defaultArgInfo) a') (NoAbs "_" b')
437
451
 
438
 
gpi :: Hiding -> Relevance -> String -> TCM Type -> TCM Type -> TCM Type
439
 
gpi h r name a b = do
 
452
gpi :: I.ArgInfo -> String -> TCM Type -> TCM Type -> TCM Type
 
453
gpi info name a b = do
440
454
  a <- a
441
 
  x <- freshName_ name
442
 
  b <- addCtx x (Dom h r a) b
443
 
  return $ El (getSort a `dLub` Abs name (getSort b))
444
 
              (Pi (Dom h r a) (Abs name b))
 
455
  b <- addContext (name, Dom info a) b
 
456
  let y = stringToArgName name
 
457
  return $ El (getSort a `dLub` Abs y (getSort b))
 
458
              (Pi (Dom info a) (Abs y b))
445
459
 
446
460
hPi, nPi :: String -> TCM Type -> TCM Type -> TCM Type
447
 
hPi = gpi Hidden Relevant
448
 
nPi = gpi NotHidden Relevant
 
461
hPi = gpi $ setHiding Hidden $ defaultArgInfo
 
462
nPi = gpi defaultArgInfo
449
463
 
450
464
varM :: Int -> TCM Term
451
465
varM = return . var
456
470
gApply h a b = do
457
471
    x <- a
458
472
    y <- b
459
 
    return $ x `apply` [Arg h Relevant y]
 
473
    return $ x `apply` [Arg (setHiding h defaultArgInfo) y]
460
474
 
461
475
(<@>),(<#>) :: TCM Term -> TCM Term -> TCM Term
462
476
(<@>) = gApply NotHidden
474
488
tset :: TCM Type
475
489
tset = return $ sort (mkType 0)
476
490
 
477
 
 
478
 
argN = Arg NotHidden Relevant
479
 
domN = Dom NotHidden Relevant
480
 
 
481
 
 
482
 
argH = Arg Hidden Relevant
483
 
domH = Dom Hidden Relevant
 
491
-- | Abbreviation: @argN = 'Arg' 'defaultArgInfo'@.
 
492
 
 
493
argN = Arg defaultArgInfo
 
494
domN = Dom defaultArgInfo
 
495
 
 
496
-- | Abbreviation: @argH = 'hide' 'Arg' 'defaultArgInfo'@.
 
497
 
 
498
argH = Arg $ setHiding Hidden defaultArgInfo
 
499
domH = Dom $ setHiding Hidden defaultArgInfo
484
500
 
485
501
---------------------------------------------------------------------------
486
502
-- * The actual primitive functions
569
583
 
570
584
    -- Other stuff
571
585
    , "primTrustMe"         |-> primTrustMe
572
 
    , "primQNameEquality"  |-> mkPrimFun2 ((==) :: Rel QName)
 
586
    , "primQNameEquality"   |-> mkPrimFun2 ((==) :: Rel QName)
 
587
    , "primShowQName"       |-> mkPrimFun1 (Str . show :: QName -> Str)
573
588
    ]
574
589
    where
575
590
        (|->) = (,)
577
592
lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
578
593
lookupPrimitiveFunction x =
579
594
    case Map.lookup x primitiveFunctions of
580
 
        Just p  -> liftTCM p
 
595
        Just p  -> p
581
596
        Nothing -> typeError $ NoSuchPrimitiveFunction x
582
597
 
583
598
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)
586
601
            Name _ x _ _ -> show x
587
602
  PrimImpl t pf <- lookupPrimitiveFunction s
588
603
  return (s, PrimImpl t $ pf { primFunName = q })
589