diff --git a/src/data/lib/prim/Agda/Builtin/Char.agda b/src/data/lib/prim/Agda/Builtin/Char.agda
index 245c0a4e385..e9f6cbe6502 100644
--- a/src/data/lib/prim/Agda/Builtin/Char.agda
+++ b/src/data/lib/prim/Agda/Builtin/Char.agda
@@ -5,7 +5,6 @@ module Agda.Builtin.Char where
open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
-postulate Char : Set
{-# BUILTIN CHAR Char #-}
primitive
diff --git a/src/data/lib/prim/Agda/Builtin/Coinduction.agda b/src/data/lib/prim/Agda/Builtin/Coinduction.agda
index 0d5fb098f0d..3359341b69e 100644
--- a/src/data/lib/prim/Agda/Builtin/Coinduction.agda
+++ b/src/data/lib/prim/Agda/Builtin/Coinduction.agda
@@ -4,11 +4,6 @@ module Agda.Builtin.Coinduction where
infix 1000 ♯_
-postulate
- ∞ : ∀ {a} (A : Set a) → Set a
- ♯_ : ∀ {a} {A : Set a} → A → ∞ A
- ♭ : ∀ {a} {A : Set a} → ∞ A → A
-
{-# BUILTIN INFINITY ∞ #-}
{-# BUILTIN SHARP ♯_ #-}
{-# BUILTIN FLAT ♭ #-}
diff --git a/src/data/lib/prim/Agda/Builtin/Float.agda b/src/data/lib/prim/Agda/Builtin/Float.agda
index f9c0e25cd56..fc7cdc79f9b 100644
--- a/src/data/lib/prim/Agda/Builtin/Float.agda
+++ b/src/data/lib/prim/Agda/Builtin/Float.agda
@@ -7,7 +7,6 @@ open import Agda.Builtin.Nat
open import Agda.Builtin.Int
open import Agda.Builtin.String
-postulate Float : Set
{-# BUILTIN FLOAT Float #-}
primitive
diff --git a/src/data/lib/prim/Agda/Builtin/String.agda b/src/data/lib/prim/Agda/Builtin/String.agda
index 3a76e833fa0..229f333be40 100644
--- a/src/data/lib/prim/Agda/Builtin/String.agda
+++ b/src/data/lib/prim/Agda/Builtin/String.agda
@@ -6,7 +6,6 @@ open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Char
-postulate String : Set
{-# BUILTIN STRING String #-}
primitive
diff --git a/src/data/lib/prim/Agda/Builtin/Word.agda b/src/data/lib/prim/Agda/Builtin/Word.agda
index 124fb8ea7cd..e5ffb411288 100644
--- a/src/data/lib/prim/Agda/Builtin/Word.agda
+++ b/src/data/lib/prim/Agda/Builtin/Word.agda
@@ -4,7 +4,6 @@ module Agda.Builtin.Word where
open import Agda.Builtin.Nat
-postulate Word64 : Set
{-# BUILTIN WORD64 Word64 #-}
primitive
diff --git a/src/full/Agda/Syntax/Abstract.hs b/src/full/Agda/Syntax/Abstract.hs
index f0028ebceca..99c1523855b 100644
--- a/src/full/Agda/Syntax/Abstract.hs
+++ b/src/full/Agda/Syntax/Abstract.hs
@@ -33,14 +33,18 @@ import Agda.Syntax.Concrete.Name (NumHoles(..))
import Agda.Syntax.Concrete (FieldAssignment'(..), exprFieldA, HoleContent'(..))
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Pretty ()
-import Agda.Syntax.Info
-import Agda.Syntax.Common
-import Agda.Syntax.Position
+
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Abstract.Name as A (QNamed)
+
+import qualified Agda.Syntax.Internal as I
+
+import Agda.Syntax.Common
+import Agda.Syntax.Info
+import Agda.Syntax.Fixity ( Fixity' )
import Agda.Syntax.Literal
+import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
-import qualified Agda.Syntax.Internal as I
import Agda.TypeChecking.Positivity.Occurrence
diff --git a/src/full/Agda/Syntax/Concrete.hs b/src/full/Agda/Syntax/Concrete.hs
index 99fd73af701..628498c73c7 100644
--- a/src/full/Agda/Syntax/Concrete.hs
+++ b/src/full/Agda/Syntax/Concrete.hs
@@ -393,7 +393,9 @@ data OpenShortHand = DoOpen | DontOpen
data Pragma
= OptionsPragma Range [String]
- | BuiltinPragma Range String QName
+ | BuiltinPragma Range String QName Fixity'
+ -- ^ BUILTIN pragmas with no associated definition can have a fixity
+ -- default value: @noFixity'@.
| RewritePragma Range [QName]
| CompiledDataPragma Range QName String [String]
| CompiledTypePragma Range QName String
@@ -664,7 +666,7 @@ instance HasRange DoStmt where
instance HasRange Pragma where
getRange (OptionsPragma r _) = r
- getRange (BuiltinPragma r _ _) = r
+ getRange (BuiltinPragma r _ _ _) = r
getRange (RewritePragma r _) = r
getRange (CompiledDataPragma r _ _ _) = r
getRange (CompiledTypePragma r _ _) = r
@@ -865,7 +867,7 @@ instance KillRange Pattern where
instance KillRange Pragma where
killRange (OptionsPragma _ s) = OptionsPragma noRange s
- killRange (BuiltinPragma _ s e) = killRange1 (BuiltinPragma noRange s) e
+ killRange (BuiltinPragma _ s e f) = killRange2 (BuiltinPragma noRange s) e f
killRange (RewritePragma _ qs) = killRange1 (RewritePragma noRange) qs
killRange (CompiledDataPragma _ q s ss) = killRange1 (\q -> CompiledDataPragma noRange q s ss) q
killRange (CompiledTypePragma _ q s) = killRange1 (\q -> CompiledTypePragma noRange q s) q
@@ -1008,7 +1010,7 @@ instance NFData Declaration where
instance NFData Pragma where
rnf (OptionsPragma _ a) = rnf a
- rnf (BuiltinPragma _ a b) = rnf a `seq` rnf b
+ rnf (BuiltinPragma _ a b f) = rnf a `seq` rnf b `seq` rnf f
rnf (RewritePragma _ a) = rnf a
rnf (CompiledDataPragma _ a b c) = rnf a `seq` rnf b `seq` rnf c
rnf (CompiledTypePragma _ a b) = rnf a `seq` rnf b
diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs
index 76f723755e3..43a01cfaf78 100644
--- a/src/full/Agda/Syntax/Concrete/Definitions.hs
+++ b/src/full/Agda/Syntax/Concrete/Definitions.hs
@@ -73,6 +73,7 @@ import Agda.Syntax.Concrete.Pretty ()
import Agda.Interaction.Options.Warnings
import Agda.TypeChecking.Positivity.Occurrence
+import {-# SOURCE #-} Agda.TypeChecking.Monad.Builtin ( builtinsNoDef )
import Agda.Utils.AffineHole
import Agda.Utils.Except ( MonadError(throwError,catchError) )
@@ -866,6 +867,10 @@ niceDeclarations ds = do
Module{} -> []
UnquoteDecl _ xs _ -> xs
UnquoteDef{} -> []
+ -- BUILTIN pragmas which do not require an accompanying definition declare
+ -- the (unqualified) name they mention.
+ Pragma (BuiltinPragma _ b (QName x) _)
+ | b `elem` builtinsNoDef -> [x]
Pragma{} -> []
inferMutualBlocks :: [NiceDeclaration] -> Nice [NiceDeclaration]
@@ -1113,6 +1118,10 @@ niceDeclarations ds = do
nicePragma (PolarityPragma{}) ds = return ([], ds)
+ nicePragma (BuiltinPragma r str qn@(QName x) _) ds = do
+ fx <- getFixity x
+ return ([NicePragma r (BuiltinPragma r str qn fx)], ds)
+
nicePragma p ds = return ([NicePragma (getRange p) p], ds)
canHaveTerminationMeasure :: [Declaration] -> Bool
diff --git a/src/full/Agda/Syntax/Concrete/Pretty.hs b/src/full/Agda/Syntax/Concrete/Pretty.hs
index 4c144c2d013..98d825ffcf3 100644
--- a/src/full/Agda/Syntax/Concrete/Pretty.hs
+++ b/src/full/Agda/Syntax/Concrete/Pretty.hs
@@ -513,7 +513,7 @@ instance Pretty OpenShortHand where
instance Pretty Pragma where
pretty (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts
- pretty (BuiltinPragma _ b x) = hsep [ text "BUILTIN", text b, pretty x ]
+ pretty (BuiltinPragma _ b x _) = hsep [ text "BUILTIN", text b, pretty x ]
pretty (RewritePragma _ xs) =
hsep [ text "REWRITE", hsep $ map pretty xs ]
pretty (CompiledPragma _ x hs) =
diff --git a/src/full/Agda/Syntax/Parser/Parser.y b/src/full/Agda/Syntax/Parser/Parser.y
index adc4aed9ea9..6b4e2fbbb07 100644
--- a/src/full/Agda/Syntax/Parser/Parser.y
+++ b/src/full/Agda/Syntax/Parser/Parser.y
@@ -1575,10 +1575,10 @@ OptionsPragma : '{-#' 'OPTIONS' PragmaStrings '#-}' { OptionsPragma (getRange ($
BuiltinPragma :: { Pragma }
BuiltinPragma
: '{-#' 'BUILTIN' string PragmaQName '#-}'
- { BuiltinPragma (getRange ($1,$2,fst $3,$4,$5)) (snd $3) $4 }
- -- Extra rule to accept keword REWRITE also as built-in:
+ { BuiltinPragma (getRange ($1,$2,fst $3,$4,$5)) (snd $3) $4 __IMPOSSIBLE__ }
+ -- Extra rule to accept keyword REWRITE also as built-in:
| '{-#' 'BUILTIN' 'REWRITE' PragmaQName '#-}'
- { BuiltinPragma (getRange ($1,$2,$3,$4,$5)) "REWRITE" $4 }
+ { BuiltinPragma (getRange ($1,$2,$3,$4,$5)) "REWRITE" $4 __IMPOSSIBLE__ }
RewritePragma :: { Pragma }
RewritePragma
diff --git a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
index 4a4b6f13aa6..00356cf69f2 100644
--- a/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
+++ b/src/full/Agda/Syntax/Translation/AbstractToConcrete.hs
@@ -952,9 +952,9 @@ 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.BuiltinNoDefPragma b x -> C.BuiltinPragma r b <$> toConcrete x
- A.RewritePragma x -> C.RewritePragma r . singleton <$> toConcrete x
+ A.BuiltinPragma b x -> C.BuiltinPragma r b <$> toConcrete x <*> pure noFixity'
+ A.BuiltinNoDefPragma b x -> C.BuiltinPragma r b <$> toConcrete x <*> pure (nameFixity $ qnameName x)
+ A.RewritePragma x -> C.RewritePragma r . singleton <$> toConcrete x
A.CompiledTypePragma x hs -> do
x <- toConcrete x
return $ C.CompiledTypePragma r x hs
diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
index b3095ec0293..82502e25e91 100644
--- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
+++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
@@ -1902,20 +1902,25 @@ instance ToAbstract C.Pragma [A.Pragma] where
sINLINE ++ " used on ambiguous name " ++ prettyShow x
_ -> genericError $ "Target of " ++ sINLINE ++ " pragma should be a function"
return [ A.InlinePragma b y ]
- toAbstract (C.BuiltinPragma _ b q) | isUntypedBuiltin b = do
+ toAbstract (C.BuiltinPragma _ b q _) | isUntypedBuiltin b = do
bindUntypedBuiltin b =<< toAbstract (ResolveQName q)
return []
- toAbstract (C.BuiltinPragma _ b q) = do
+ toAbstract (C.BuiltinPragma _ b q f) = 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 q of
C.QName x -> do
- unlessM ((UnknownName ==) <$> resolveName q) $ genericError $
- "BUILTIN " ++ b ++ " declares an identifier " ++
- "(no longer expects an already defined identifier)"
- y <- freshAbstractQName noFixity' x
+ -- The name shouldn't exist yet. If it does, we raise a warning
+ -- and drop the existing definition.
+ unlessM ((UnknownName ==) <$> resolveName q) $ do
+ genericWarning $ P.text $
+ "BUILTIN " ++ b ++ " declares an identifier " ++
+ "(no longer expects an already defined identifier)"
+ modifyCurrentScope $ removeNameFromScope PublicNS x
+ -- We then happily bind the name
+ y <- freshAbstractQName f x
kind <- fromMaybe __IMPOSSIBLE__ <$> builtinKindOfName b
bindName PublicAccess kind x y
return [ A.BuiltinNoDefPragma b y ]
diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs b/src/full/Agda/TypeChecking/Monad/Builtin.hs
index d3a90b7de48..640e90b6307 100644
--- a/src/full/Agda/TypeChecking/Monad/Builtin.hs
+++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs
@@ -60,11 +60,11 @@ setBuiltinThings b = stLocalBuiltins .= b
bindBuiltinName :: String -> Term -> TCM ()
bindBuiltinName b x = do
- builtin <- getBuiltinThing b
- case builtin of
- Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
- Just (Prim _) -> typeError $ NoSuchBuiltinName b
- Nothing -> stLocalBuiltins %= Map.insert b (Builtin x)
+ builtin <- getBuiltinThing b
+ case builtin of
+ Just (Builtin y) -> typeError $ DuplicateBuiltinBinding b y x
+ Just (Prim _) -> typeError $ NoSuchBuiltinName b
+ Nothing -> stLocalBuiltins %= Map.insert b (Builtin x)
bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive b pf = do
@@ -612,6 +612,13 @@ builtinsNoDef =
, builtinIZero
, builtinIOne
, builtinSetOmega
+ , builtinString
+ , builtinChar
+ , builtinFloat
+ , builtinWord64
+ , builtinInf
+ , builtinSharp
+ , builtinFlat
]
-- | The coinductive primitives.
diff --git a/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot b/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot
new file mode 100644
index 00000000000..e110b945613
--- /dev/null
+++ b/src/full/Agda/TypeChecking/Monad/Builtin.hs-boot
@@ -0,0 +1,3 @@
+module Agda.TypeChecking.Monad.Builtin where
+
+builtinsNoDef :: [String]
diff --git a/src/full/Agda/TypeChecking/Rules/Builtin.hs b/src/full/Agda/TypeChecking/Rules/Builtin.hs
index c67945c50cb..f36fc00dcc8 100644
--- a/src/full/Agda/TypeChecking/Rules/Builtin.hs
+++ b/src/full/Agda/TypeChecking/Rules/Builtin.hs
@@ -52,8 +52,8 @@ import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.NonemptyList
import Agda.Utils.Null
-import Agda.Utils.Size
import Agda.Utils.Permutation
+import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
@@ -96,6 +96,9 @@ coreBuiltins =
, (builtinFloat |-> builtinPostulate tset)
, (builtinChar |-> builtinPostulate tset)
, (builtinString |-> builtinPostulate tset)
+ , (builtinInf |-> builtinPostulate typeOfInf)
+ , (builtinSharp |-> builtinPostulate typeOfSharp)
+ , (builtinFlat |-> builtinPostulate typeOfFlat)
, (builtinQName |-> builtinPostulate tset)
, (builtinAgdaMeta |-> builtinPostulate tset)
, (builtinIO |-> builtinPostulate (tset --> tset))
@@ -134,12 +137,12 @@ coreBuiltins =
nPi' "i" (cl tinterval) $ \ i ->
nPi' "j" (cl tinterval) $ \ j ->
nPi' "i1" (elInf $ cl primIsOne <@> i) $ \ i1 ->
- (elInf $ cl primIsOne <@> (cl (getPrimitiveTerm "primIMax") <@> i <@> j))))
+ (elInf $ cl primIsOne <@> (cl primIMax <@> i <@> j))))
, (builtinIsOne2 |-> builtinPostulate (runNamesT [] $
nPi' "i" (cl tinterval) $ \ i ->
nPi' "j" (cl tinterval) $ \ j ->
nPi' "j1" (elInf $ cl primIsOne <@> j) $ \ j1 ->
- (elInf $ cl primIsOne <@> (cl (getPrimitiveTerm "primIMax") <@> i <@> j))))
+ (elInf $ cl primIsOne <@> (cl primIMax <@> i <@> j))))
, (builtinIsOneEmpty |-> builtinPostulate (runNamesT [] $
hPi' "l" (el $ cl primLevel) $ \ l ->
hPi' "A" (pPi' "o" (cl primIZero) $ \ _ ->
@@ -788,10 +791,6 @@ bindBuiltinInfo (BuiltinInfo s d) e = do
case theDef def of
Axiom {} -> do
builtinSizeHook s q t'
- when (s == builtinChar) $ addHaskellPragma q "= type Char"
- when (s == builtinString) $ addHaskellPragma q "= type Data.Text.Text"
- when (s == builtinFloat) $ addHaskellPragma q "= type Double"
- when (s == builtinWord64) $ addHaskellPragma q "= type MAlonzo.RTE.Word64"
bindBuiltinName s v
_ -> err
_ -> err
@@ -854,11 +853,37 @@ bindUntypedBuiltin b = \case
-- We simply ignore the parameters.
bindBuiltinNoDef :: String -> A.QName -> TCM ()
bindBuiltinNoDef b q = inTopContext $ do
+ if | b == builtinInf -> ax typeOfInf >> bindBuiltinInf r
+ | b == builtinSharp -> ax typeOfSharp >> bindBuiltinSharp r
+ | b == builtinFlat -> ax typeOfFlat >> bindBuiltinFlat r
+ | otherwise -> bindBuiltinNoDef' b q
+
+ where
+
+ r :: ResolvedName
+ r = DefinedName PublicAccess (AbsName q DefName Defined)
+
+ ax :: TCM Type -> TCM ()
+ ax mty = do
+ ty <- mty
+ addConstant q $ defaultDefn defaultArgInfo q ty Axiom
+
+bindBuiltinNoDef' :: String -> A.QName -> TCM ()
+bindBuiltinNoDef' b q = do
case builtinDesc <$> findBuiltinInfo b of
Just (BuiltinPostulate rel mt) -> do
+ -- We start by adding the corresponding postulate
t <- mt
addConstant q $ defaultDefn (setRelevance rel defaultArgInfo) q t def
+ -- And we then *modify* the definition based on our needs:
+ -- We add polarity information for SIZE-related definitions
builtinSizeHook b q t
+ -- And compilation pragmas for base types
+ when (b == builtinChar) $ addHaskellPragma q "= type Char"
+ when (b == builtinString) $ addHaskellPragma q "= type Data.Text.Text"
+ when (b == builtinFloat) $ addHaskellPragma q "= type Double"
+ when (b == builtinWord64) $ addHaskellPragma q "= type MAlonzo.RTE.Word64"
+ -- Finally, bind the BUILTIN in the environment.
bindBuiltinName b $ Def q []
where
-- Andreas, 2015-02-14
diff --git a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot
index abe1a03a8cf..fa0508e0677 100644
--- a/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot
+++ b/src/full/Agda/TypeChecking/Rules/Builtin/Coinduction.hs-boot
@@ -1,8 +1,13 @@
module Agda.TypeChecking.Rules.Builtin.Coinduction where
import Agda.Syntax.Scope.Base
+import Agda.Syntax.Internal (Type)
import Agda.TypeChecking.Monad
+typeOfInf :: TCM Type
+typeOfSharp :: TCM Type
+typeOfFlat :: TCM Type
+
bindBuiltinInf :: ResolvedName -> TCM ()
bindBuiltinSharp :: ResolvedName -> TCM ()
bindBuiltinFlat :: ResolvedName -> TCM ()
diff --git a/test/Compiler/simple/Issue2821.out b/test/Compiler/simple/Issue2821.out
index 7c29ade3b1b..ff7499f33ec 100644
--- a/test/Compiler/simple/Issue2821.out
+++ b/test/Compiler/simple/Issue2821.out
@@ -1,6 +1,26 @@
EXECUTED_PROGRAM
ret > ExitSuccess
+out > /Issue2821.agda:24,1-30
+out > BUILTIN STRING declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN STRING String #-}
+out > /Issue2821.agda:25,1-28
+out > BUILTIN CHAR declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN CHAR Char #-}
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /Issue2821.agda:24,1-30
+out > BUILTIN STRING declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN STRING String #-}
+out >
+out > /Issue2821.agda:25,1-28
+out > BUILTIN CHAR declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN CHAR Char #-}
out > ALSE
out > RUE
out >
diff --git a/test/Compiler/simple/Issue2909-5.out b/test/Compiler/simple/Issue2909-5.out
index b6706a6362e..7ba731a0391 100644
--- a/test/Compiler/simple/Issue2909-5.out
+++ b/test/Compiler/simple/Issue2909-5.out
@@ -1,6 +1,35 @@
COMPILE_FAILED
ret > ExitFailure 1
+out > /Issue2909-5.agda:6,1-28
+out > BUILTIN INFINITY declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN INFINITY ∞ #-}
+out > /Issue2909-5.agda:7,1-28
+out > BUILTIN SHARP declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN SHARP ♯_ #-}
+out > /Issue2909-5.agda:8,1-28
+out > BUILTIN FLAT declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN FLAT ♭ #-}
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /Issue2909-5.agda:6,1-28
+out > BUILTIN INFINITY declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN INFINITY ∞ #-}
+out >
+out > /Issue2909-5.agda:7,1-28
+out > BUILTIN SHARP declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN SHARP ♯_ #-}
+out >
+out > /Issue2909-5.agda:8,1-28
+out > BUILTIN FLAT declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN FLAT ♭ #-}
out > /Issue2909-5.agda:8,22-23
out > "COMPILE GHC as" pragmas are not allowed for the FLAT builtin.
out >
diff --git a/test/Compiler/simple/Issue2909-6.out b/test/Compiler/simple/Issue2909-6.out
index 5924934d627..d2bc696ed2f 100644
--- a/test/Compiler/simple/Issue2909-6.out
+++ b/test/Compiler/simple/Issue2909-6.out
@@ -1,6 +1,35 @@
COMPILE_FAILED
ret > ExitFailure 1
+out > /Issue2909-6.agda:6,1-28
+out > BUILTIN INFINITY declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN INFINITY ∞ #-}
+out > /Issue2909-6.agda:7,1-28
+out > BUILTIN SHARP declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN SHARP ♯_ #-}
+out > /Issue2909-6.agda:8,1-28
+out > BUILTIN FLAT declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN FLAT ♭ #-}
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /Issue2909-6.agda:6,1-28
+out > BUILTIN INFINITY declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN INFINITY ∞ #-}
+out >
+out > /Issue2909-6.agda:7,1-28
+out > BUILTIN SHARP declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN SHARP ♯_ #-}
+out >
+out > /Issue2909-6.agda:8,1-28
+out > BUILTIN FLAT declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN FLAT ♭ #-}
out > /Issue2909-6.agda:8,22-23
out > "COMPILE GHC" pragmas are not allowed for the FLAT builtin.
out >
diff --git a/test/Compiler/simple/UniversePolymorphicIO.out b/test/Compiler/simple/UniversePolymorphicIO.out
index 09fc54d9afe..f40f700ae11 100644
--- a/test/Compiler/simple/UniversePolymorphicIO.out
+++ b/test/Compiler/simple/UniversePolymorphicIO.out
@@ -1,5 +1,16 @@
EXECUTED_PROGRAM
ret > ExitSuccess
+out > /UniversePolymorphicIO.agda:21,1-30
+out > BUILTIN STRING declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN STRING String #-}
+out >
+out > ———— All done; warnings encountered ————————————————————————
+out >
+out > /UniversePolymorphicIO.agda:21,1-30
+out > BUILTIN STRING declares an identifier (no longer expects an already defined identifier)
+out > when scope checking the declaration
+out > {-# BUILTIN STRING String #-}
out > ok
out >
diff --git a/test/Fail/AbstractGuardednessPreservingTypeConstructors.agda b/test/Fail/AbstractGuardednessPreservingTypeConstructors.agda
index e057cda29d8..5f8e106c24d 100644
--- a/test/Fail/AbstractGuardednessPreservingTypeConstructors.agda
+++ b/test/Fail/AbstractGuardednessPreservingTypeConstructors.agda
@@ -7,13 +7,6 @@
module AbstractGuardednessPreservingTypeConstructors where
-infix 1000 ♯_
-
-postulate
- ∞ : ∀ {a} (A : Set a) → Set a
- ♯_ : ∀ {a} {A : Set a} → A → ∞ A
- ♭ : ∀ {a} {A : Set a} → ∞ A → A
-
{-# BUILTIN INFINITY ∞ #-}
{-# BUILTIN SHARP ♯_ #-}
{-# BUILTIN FLAT ♭ #-}
diff --git a/test/Fail/DuplicateBuiltinBinding.err b/test/Fail/DuplicateBuiltinBinding.err
index ee7b940eb09..96faf9871df 100644
--- a/test/Fail/DuplicateBuiltinBinding.err
+++ b/test/Fail/DuplicateBuiltinBinding.err
@@ -1,4 +1,4 @@
DuplicateBuiltinBinding.agda:6,1-30
Duplicate binding for built-in thing STRING, previous binding to
-String
+;DuplicateBuiltinBinding.String
when checking the pragma BUILTIN STRING String
diff --git a/test/Fail/PatternMatchingOnCodata.err b/test/Fail/PatternMatchingOnCodata.err
index 722a811d590..0d6a762ddbc 100644
--- a/test/Fail/PatternMatchingOnCodata.err
+++ b/test/Fail/PatternMatchingOnCodata.err
@@ -1,6 +1,6 @@
PatternMatchingOnCodata.agda:31,1-11
Could not parse the left-hand side my-♭ (♯ x)
Operators used in the grammar:
- ♯ (prefix operator, level 1000) [♯_ (PatternMatchingOnCodata.agda:23,3-5)]
+ ♯ (prefix operator, level 1000) [♯_ (PatternMatchingOnCodata.agda:27,22-24)]
when scope checking the left-hand side my-♭ (♯ x) in the definition
of my-♭
diff --git a/test/LaTeXAndHTML/succeed/Issue2019.html b/test/LaTeXAndHTML/succeed/Issue2019.html
index 5d6cb7f1746..ddc9cfc0013 100644
--- a/test/LaTeXAndHTML/succeed/Issue2019.html
+++ b/test/LaTeXAndHTML/succeed/Issue2019.html
@@ -19,7 +19,7 @@
-various-whitespace-characters : String
+various-whitespace-characters : String
various-whitespace-characters = " "
\end{code}\begin{code}
open import Agda.Builtin.String
-argh : String
+argh : String
argh = "Hello,\
\World!"
\end{code}