[ Issue 1428 ] Size BUILTINs no longer need postulates.

CHANGELOG

@@ -30,6 +30,15 @@ Language
 
     {xs {ys zs} : List A} → ...
 
+* The builtins for sized types no longer need accompanying postulates.
+  The BUILTIN pragmas for size stuff now also declare the identifiers
+  they bind to.
+
+    {-# BUILTIN SIZE     Size     #-}  --  Size   : Set
+    {-# BUILTIN SIZELT   Size<_   #-}  --  Size<_ : Size → Set
+    {-# BUILTIN SIZESUC  ↑_       #-}  --  ↑_     : Size → Size
+    {-# BUILTIN SIZEINF  ∞        #-}  --  ∞      : Size
+
 Type checking
 =============
 

src/full/Agda/Syntax/Abstract.hs

@@ -170,6 +170,9 @@ data ModuleApplication
 data Pragma
   = OptionsPragma [String]
   | BuiltinPragma String Expr
+  | BuiltinNoDefPragma String QName
+    -- ^ Builtins that do not come with a definition,
+    --   but declare a name for an Agda concept.
   | RewritePragma QName
   | CompiledPragma QName String
   | CompiledExportPragma QName String

src/full/Agda/Syntax/Scope/Monad.hs

@@ -198,7 +198,7 @@ data ResolvedName = VarName A.Name
                   | ConstructorName [AbstractName]
                   | PatternSynResName AbstractName
                   | UnknownName
-  deriving (Show)
+  deriving (Show, Eq)
 
 -- | Look up the abstract name referred to by a given concrete name.
 resolveName :: C.QName -> ScopeM ResolvedName

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

@@ -795,8 +795,10 @@ data RangeAndPragma = RangeAndPragma Range A.Pragma
 instance ToConcrete RangeAndPragma C.Pragma where
     toConcrete (RangeAndPragma r p) = case p of
         A.OptionsPragma xs  -> return $ C.OptionsPragma r xs
-        A.BuiltinPragma b x -> C.BuiltinPragma r b <$> toConcrete x
-        A.RewritePragma x   -> C.RewritePragma r <$> toConcrete x
+        A.BuiltinPragma b e      -> C.BuiltinPragma r b <$> toConcrete e
+        A.BuiltinNoDefPragma b x -> C.BuiltinPragma r b . C.Ident <$>
+          toConcrete x
+        A.RewritePragma x        -> C.RewritePragma r <$> toConcrete x
         A.CompiledTypePragma x hs -> do
           x <- toConcrete x
           return $ C.CompiledTypePragma r x hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP                    #-}
+{-# LANGUAGE DoAndIfThenElse        #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
@@ -63,6 +64,7 @@ import Agda.TypeChecking.Monad.Base
   )
 import Agda.TypeChecking.Monad.Benchmark (billTo, billTop, reimburseTop)
 import qualified Agda.TypeChecking.Monad.Benchmark as Bench
+import Agda.TypeChecking.Monad.Builtin
 import Agda.TypeChecking.Monad.Trace (traceCall, setCurrentRange)
 import Agda.TypeChecking.Monad.State
 import Agda.TypeChecking.Monad.MetaVars (registerInteractionPoint)
@@ -1392,6 +1394,22 @@ instance ToAbstract C.Pragma [A.Pragma] where
             _       -> __IMPOSSIBLE__
         return [ A.StaticPragma y ]
     toAbstract (C.BuiltinPragma _ b e) = do
+      -- Andreas, 2015-02-14
+      -- Some builtins cannot be given a valid Agda type,
+      -- thus, they do not come with accompanying postulate or definition.
+      if b `elem` builtinsNoDef then do
+        case e of
+          C.Ident q@(C.QName x) -> do
+            unlessM ((UnknownName ==) <$> resolveName q) $ genericError $
+              "BUILTIN " ++ b ++ " declares an identifier " ++
+              "(no longer expects an already defined identifier)"
+            y <- freshAbstractQName defaultFixity' x
+            bindName PublicAccess DefName x y
+            return [ A.BuiltinNoDefPragma b y ]
+          _ -> genericError $
+            "Pragma BUILTIN " ++ b ++ ": expected unqualified identifier, " ++
+            "but found expression " ++ prettyShow e
+      else do
         e <- toAbstract e
         return [ A.BuiltinPragma b e ]
     toAbstract (C.ImportPragma _ i) = do

src/full/Agda/TypeChecking/Monad/Builtin.hs

@@ -109,12 +109,12 @@ primInteger, primFloat, primChar, primString, primBool, primTrue, primFalse,
     primList, primNil, primCons, primIO, primNat, primSuc, primZero,
     primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
     primNatEquality, primNatLess,
-    primSize, primSizeLt, primSizeSuc, primSizeInf,
+    primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
     primInf, primSharp, primFlat,
     primEquality, primRefl,
     primRewrite, -- Name of rewrite relation
     primLevel, primLevelZero, primLevelSuc, primLevelMax,
-    primIrrAxiom, primSizeMax,
+    primIrrAxiom,
     -- builtins for reflection:
     primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAgdaTerm, primAgdaTermVar,
     primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
@@ -153,6 +153,7 @@ primNatDivSucAux = getBuiltin builtinNatDivSucAux
 primNatModSucAux = getBuiltin builtinNatModSucAux
 primNatEquality  = getBuiltin builtinNatEquals
 primNatLess      = getBuiltin builtinNatLess
+primSizeUniv     = getBuiltin builtinSizeUniv
 primSize         = getBuiltin builtinSize
 primSizeLt       = getBuiltin builtinSizeLt
 primSizeSuc      = getBuiltin builtinSizeSuc
@@ -228,9 +229,11 @@ primAgdaDefinition                = getBuiltin builtinAgdaDefinition
 builtinNat, builtinSuc, builtinZero, builtinNatPlus, builtinNatMinus,
   builtinNatTimes, builtinNatDivSucAux, builtinNatModSucAux, builtinNatEquals,
   builtinNatLess, builtinInteger, builtinFloat, builtinChar, builtinString,
-  builtinBool, builtinTrue, builtinFalse, builtinList, builtinNil,
-  builtinCons, builtinIO, builtinSize, builtinSizeLt, builtinSizeSuc,
-  builtinSizeInf, builtinSizeMax, builtinInf, builtinSharp, builtinFlat,
+  builtinBool, builtinTrue, builtinFalse,
+  builtinList, builtinNil, builtinCons, builtinIO,
+  builtinSizeUniv, builtinSize, builtinSizeLt,
+  builtinSizeSuc, builtinSizeInf, builtinSizeMax,
+  builtinInf, builtinSharp, builtinFlat,
   builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
   builtinLevel, builtinLevelZero, builtinLevelSuc, builtinIrrAxiom,
   builtinQName, builtinAgdaSort, builtinAgdaSortSet, builtinAgdaSortLit,
@@ -274,6 +277,7 @@ builtinList                          = "LIST"
 builtinNil                           = "NIL"
 builtinCons                          = "CONS"
 builtinIO                            = "IO"
+builtinSizeUniv                      = "SIZEUNIV"
 builtinSize                          = "SIZE"
 builtinSizeLt                        = "SIZELT"
 builtinSizeSuc                       = "SIZESUC"
@@ -346,6 +350,27 @@ builtinAgdaDefinitionPostulate       = "AGDADEFINITIONPOSTULATE"
 builtinAgdaDefinitionPrimitive       = "AGDADEFINITIONPRIMITIVE"
 builtinAgdaDefinition                = "AGDADEFINITION"
 
+-- | Builtins that come without a definition in Agda syntax.
+--   These are giving names to Agda internal concepts which
+--   cannot be assigned an Agda type.
+--
+--   An example would be a user-defined name for @Set@.
+--
+--     {-# BUILTIN TYPE Type #-}
+--
+--   The type of @Type@ would be @Type : Level → Setω@
+--   which is not valid Agda.
+
+builtinsNoDef :: [String]
+builtinsNoDef =
+  [ builtinSizeUniv
+  , builtinSize
+  , builtinSizeLt
+  , builtinSizeSuc
+  , builtinSizeInf
+  , builtinSizeMax
+  ]
+
 -- | The coinductive primitives.
 
 data CoinductionKit = CoinductionKit

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

@@ -85,8 +85,8 @@ haveSizedTypes = do
   `catchError` \_ -> return False
 
 -- | Add polarity info to a SIZE builtin.
-builtinSizeHook :: String -> QName -> Term -> Type -> TCM ()
-builtinSizeHook s q e' t = do
+builtinSizeHook :: String -> QName -> Type -> TCM ()
+builtinSizeHook s q t = do
   when (s `elem` [builtinSizeLt, builtinSizeSuc]) $ do
     modifySignature $ updateDefinition q
       $ updateDefPolarity       (const [Covariant])

src/full/Agda/TypeChecking/Rules/Builtin.hs

@@ -1,10 +1,15 @@
-{-# LANGUAGE CPP           #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
-
-module Agda.TypeChecking.Rules.Builtin (bindBuiltin, bindPostulatedName) where
-
-import Control.Applicative
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE PatternGuards       #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TupleSections       #-}
+
+module Agda.TypeChecking.Rules.Builtin
+  ( bindBuiltin
+  , bindBuiltinNoDef
+  , bindPostulatedName
+  ) where
+
+import Control.Applicative hiding (empty)
 import Control.Monad
 import Data.List (find)
 
@@ -32,6 +37,7 @@ import {-# SOURCE #-} Agda.TypeChecking.Rewriting
 import Agda.Utils.Except ( MonadError(catchError) )
 import Agda.Utils.Maybe
 import Agda.Utils.Monad
+import Agda.Utils.Null
 import Agda.Utils.Size
 
 #include "undefined.h"
@@ -117,6 +123,7 @@ coreBuiltins = map (\ (x, z) -> BuiltinInfo x z)
   , (builtinVisible            |-> BuiltinDataCons thiding)
   , (builtinRelevant           |-> BuiltinDataCons trelevance)
   , (builtinIrrelevant         |-> BuiltinDataCons trelevance)
+  , (builtinSizeUniv           |-> builtinPostulate tset)
   , (builtinSize               |-> builtinPostulate tset)
   , (builtinSizeLt             |-> builtinPostulate (tsize --> tset))
   , (builtinSizeSuc            |-> builtinPostulate (tsize --> tsize))
@@ -435,7 +442,7 @@ bindBuiltinInfo (BuiltinInfo s d) e = do
             def <- ignoreAbstractMode $ getConstInfo q
             case theDef def of
               Axiom {} -> do
-                builtinSizeHook s q e' t'
+                builtinSizeHook s q t'
                 bindBuiltinName s e'
               _        -> err
           _ -> err
@@ -463,3 +470,26 @@ bindBuiltin b e = do
     nowNat b = genericError $
       "Builtin " ++ b ++ " does no longer exist. " ++
       "It is now bound by BUILTIN " ++ builtinNat
+
+
+-- | Bind a builtin thing to a new name.
+bindBuiltinNoDef :: String -> A.QName -> TCM ()
+bindBuiltinNoDef b q = do
+  unlessM ((0 ==) <$> getContextSize) $ typeError $ BuiltinInParameterisedModule b
+  case lookup b $ map (\ (BuiltinInfo b i) -> (b, i)) coreBuiltins of
+    Just (BuiltinPostulate rel mt) -> do
+      t <- mt
+      addConstant q $ defaultDefn (setRelevance rel defaultArgInfo) q t def
+      builtinSizeHook b q t
+      bindBuiltinName b $ Def q []
+      where
+        -- Andreas, 2015-02-14
+        -- Special treatment of SizeUniv, should maybe be a primitive.
+        def | b == builtinSizeUniv = emptyFunction
+                { funClauses = [ (empty :: Clause) { clauseBody = Body $ Sort SizeUniv } ]
+                , funTerminates = Just True
+                }
+            | otherwise = Axiom
+
+    Just{}  -> __IMPOSSIBLE__
+    Nothing -> __IMPOSSIBLE__ -- typeError $ NoSuchBuiltinName b

src/full/Agda/TypeChecking/Rules/Decl.hs

@@ -54,7 +54,7 @@ import Agda.TypeChecking.Rules.Term
 import Agda.TypeChecking.Rules.Data    ( checkDataDef )
 import Agda.TypeChecking.Rules.Record  ( checkRecDef )
 import Agda.TypeChecking.Rules.Def     ( checkFunDef, useTerPragma )
-import Agda.TypeChecking.Rules.Builtin ( bindBuiltin )
+import Agda.TypeChecking.Rules.Builtin
 
 import Agda.Termination.TermCheck
 
@@ -400,6 +400,7 @@ checkPragma :: Range -> A.Pragma -> TCM ()
 checkPragma r p =
     traceCall (CheckPragma r p) $ case p of
         A.BuiltinPragma x e -> bindBuiltin x e
+        A.BuiltinNoDefPragma b x -> bindBuiltinNoDef b x
         A.RewritePragma q   -> addRewriteRule q
         A.CompiledTypePragma x hs -> do
           def <- getConstInfo x

test/Common/Size.agda

@@ -6,13 +6,8 @@
 
 module Common.Size where
 
-postulate
-  Size   : Set
-  Size<_ : Size → Set
-  ↑_     : Size → Size
-  ∞      : Size
-
-{-# BUILTIN SIZE    Size   #-}
-{-# BUILTIN SIZELT  Size<_ #-}
-{-# BUILTIN SIZESUC ↑_     #-}
-{-# BUILTIN SIZEINF ∞      #-}
+{-# BUILTIN SIZEUNIV SizeUniv #-}  --  sort SizeUniv
+{-# BUILTIN SIZE     Size     #-}  --  Size   : SizeUniv
+{-# BUILTIN SIZELT   Size<_   #-}  --  Size<_ : Size → SizeUniv
+{-# BUILTIN SIZESUC  ↑_       #-}  --  ↑_     : Size → Size
+{-# BUILTIN SIZEINF  ∞        #-}  --  ∞      : Size

test/interaction/GiveSize.agda

@@ -1,11 +1,8 @@
 -- {-# OPTIONS -v tc.meta:30 #-}
-{-# OPTIONS --sized-types #-}
+
 module GiveSize where
 
-postulate Size : Set
-postulate ∞ : Size
 {-# BUILTIN SIZE Size #-}
--- {-# BUILTIN SIZEINF ∞ #-}
 
 id : Size → Size
 id i = {!i!}