← 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/SizedTypes.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Monad/SizedTypes.hs
1
 
{-# LANGUAGE CPP #-}
 
1
{-# LANGUAGE CPP           #-}
2
2
{-# LANGUAGE DeriveFunctor #-}
3
3
{-# LANGUAGE TupleSections #-}
4
4
 
9
9
module Agda.TypeChecking.Monad.SizedTypes where
10
10
 
11
11
import Control.Applicative
12
 
import Control.Monad.Error
13
12
 
14
13
import Agda.Interaction.Options
15
14
 
20
19
import Agda.TypeChecking.Monad.Options
21
20
import Agda.TypeChecking.Monad.Builtin
22
21
import Agda.TypeChecking.Monad.Signature
 
22
import Agda.TypeChecking.Monad.State
23
23
import Agda.TypeChecking.Substitute ()
24
24
 
 
25
import Agda.Utils.Except ( MonadError(catchError) )
25
26
import Agda.Utils.Monad
26
27
 
27
 
#include "../../undefined.h"
 
28
#include "undefined.h"
28
29
import Agda.Utils.Impossible
29
30
 
30
31
------------------------------------------------------------------------
105
106
-- * Constructors
106
107
------------------------------------------------------------------------
107
108
 
 
109
-- | The sort of built-in types @SIZE@ and @SIZELT@.
 
110
sizeSort :: Sort
 
111
sizeSort = mkType 0
 
112
 
 
113
-- | The type of built-in types @SIZE@ and @SIZELT@.
 
114
sizeUniv :: Type
 
115
sizeUniv = sort $ sizeSort
 
116
 
 
117
-- | The built-in type @SIZE@ with user-given name.
108
118
sizeType_ :: QName -> Type
109
 
sizeType_ size = El (mkType 0) $ Def size []
 
119
sizeType_ size = El sizeSort $ Def size []
110
120
 
 
121
-- | The built-in type @SIZE@.
111
122
sizeType :: TCM Type
112
 
sizeType = El (mkType 0) <$> primSize
 
123
sizeType = El sizeSort <$> primSize
113
124
 
 
125
-- | The name of @SIZESUC@.
114
126
sizeSucName :: TCM (Maybe QName)
115
127
sizeSucName = liftTCM $
116
128
  ifM (not . optSizedTypes <$> pragmaOptions) (return Nothing) $ do