[ builtins ] Char, String and Float now get COMPILED_TYPE for free

agda · Oct 28, 2015 · 7997e8e · 7997e8e
1 parent 988141b
commit 7997e8e
Show file tree

Hide file tree

Showing 11 changed files with 14 additions and 11 deletions.
diff --git a/doc/release-notes/2-4-4.txt b/doc/release-notes/2-4-4.txt
@@ -785,7 +785,8 @@ Compiler backends
 
     Since builtin naturals are compiled to Integer you can no longer
     give a {-# COMPILED_DATA #-} pragma for Nat. The same goes for
-    builtin booleans which are now hard-wired to Haskell booleans.
+    builtin booleans, integers, floats, characters and strings which are now
+    hard-wired to appropriate Haskell types.
 
 
 * UHC compiler backend

diff --git a/examples/simple-lib/Lib/Prelude.agda b/examples/simple-lib/Lib/Prelude.agda
@@ -19,7 +19,6 @@ data Unit : Set where
 
 postulate String : Set
 
-{-# COMPILED_TYPE String String #-}
 {-# BUILTIN STRING String #-}
 
 data _×_ (A B : Set) : Set where

diff --git a/src/full/Agda/TypeChecking/Monad/Signature.hs b/src/full/Agda/TypeChecking/Monad/Signature.hs
@@ -96,7 +96,7 @@ ensureNoCompiledHaskell :: QName -> TCM ()
 ensureNoCompiledHaskell q =
   whenM (isJust . compiledHaskell . defCompiledRep <$> getConstInfo q) $
     typeError $ GenericError $ "Multiple Haskell bindings for " ++ show q ++ ". " ++
-                               "Note that builtin natural numbers and booleans don't need " ++
+                               "Note that builtin numbers, booleans, chars and strings don't need " ++
                                "COMPILED pragmas."
 
 addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()

diff --git a/src/full/Agda/TypeChecking/Rules/Builtin.hs b/src/full/Agda/TypeChecking/Rules/Builtin.hs
@@ -397,6 +397,8 @@ bindBuiltinBool = bindAndSetHaskellType builtinBool "Bool"
 bindBuiltinInt :: Term -> TCM ()
 bindBuiltinInt = bindAndSetHaskellType builtinInteger "Either Integer Integer"
 
+bindBuiltinString :: Term -> TCM ()
+bindBuiltinString = bindAndSetHaskellType builtinString "String"
 
 bindBuiltinNat :: Term -> TCM ()
 bindBuiltinNat t = do
@@ -485,6 +487,9 @@ bindBuiltinInfo (BuiltinInfo s d) e = do
             case theDef def of
               Axiom {} -> do
                 builtinSizeHook s q t'
+                when (s == builtinChar)   $ addHaskellType q "Char"
+                when (s == builtinString) $ addHaskellType q "String"
+                when (s == builtinFloat)  $ addHaskellType q "Double"
                 bindBuiltinName s e'
               _        -> err
           _ -> err

diff --git a/std-lib b/std-lib
diff --git a/test/Common/Char.agda b/test/Common/Char.agda
@@ -6,7 +6,6 @@ postulate
   Char : Set
 
 {-# BUILTIN CHAR Char #-}
-{-# COMPILED_TYPE Char Char #-}
 
 private
   primitive

diff --git a/test/Common/String.agda b/test/Common/String.agda
@@ -10,7 +10,6 @@ postulate
   String : Set
 
 {-# BUILTIN STRING String #-}
-{-# COMPILED_TYPE String String #-}
 
 primitive
   primStringAppend   : String → String → String

diff --git a/test/Fail/CompiledBuiltinBool.err b/test/Fail/CompiledBuiltinBool.err
@@ -1,4 +1,5 @@
 CompiledBuiltinBool.agda:12,1-43
 Multiple Haskell bindings for CompiledBuiltinBool.Bool. Note that
-builtin natural numbers and booleans don't need COMPILED pragmas.
+builtin numbers, booleans, chars and strings don't need COMPILED
+pragmas.
 when checking the pragma COMPILED_DATA Bool Bool True False
diff --git a/test/Fail/DuplicateBuiltinBinding.err b/test/Fail/DuplicateBuiltinBinding.err
@@ -1,4 +1,5 @@
 DuplicateBuiltinBinding.agda:6,1-30
-Duplicate binding for built-in thing STRING, previous binding to
-String
+Multiple Haskell bindings for DuplicateBuiltinBinding.String. Note
+that builtin numbers, booleans, chars and strings don't need
+COMPILED pragmas.
 when checking the pragma BUILTIN STRING String
diff --git a/test/interaction/Issue373.agda b/test/interaction/Issue373.agda
@@ -25,7 +25,6 @@ postulate
   String : Set
 
 {-# BUILTIN STRING String #-}
-{-# COMPILED_TYPE String String #-}
 
 postulate
   IO : Set → Set

diff --git a/test/succeed/UniversePolymorphicIO.agda b/test/succeed/UniversePolymorphicIO.agda
@@ -19,7 +19,6 @@ postulate
   String : Set
 
 {-# BUILTIN STRING String #-}
-{-# COMPILED_TYPE String String #-}
 
 {-# COMPILED return (\_ _ -> return :: a -> IO a) #-}
 {-# COMPILED _>>=_  (\_ _ _ _ ->