Skip to content

Commit

Permalink
[ tests ] Use proper putStrLn compiled pragmas.
Browse files Browse the repository at this point in the history
Necessary because Agda Strings are now compiled
as Haskell Text in MAlonzo.
  • Loading branch information
phile314 committed Nov 8, 2015
1 parent fba5459 commit 05b533a
Showing 1 changed file with 6 additions and 25 deletions.
31 changes: 6 additions & 25 deletions test/Compiler/simple/CompilingCoinduction.agda
Original file line number Diff line number Diff line change
Expand Up @@ -2,30 +2,8 @@
module CompilingCoinduction where

open import Common.Coinduction

data List (A : Set) : Set where
[] : List A
_∷_ : (x : A) (xs : List A) List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _∷_ #-}

{-# COMPILED_DATA List [] [] (:) #-}

postulate
Char : Set

{-# BUILTIN CHAR Char #-}
{-# COMPILED_TYPE Char Char #-}

-- Strings --

postulate
String : Set

{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}
open import Common.Char
open import Common.String

data Unit : Set where
unit : Unit
Expand All @@ -38,9 +16,12 @@ postulate
{-# COMPILED_TYPE IO IO #-}
{-# BUILTIN IO IO #-}

{-# IMPORT Data.Text.IO #-}

postulate
putStrLn : ∞ String IO Unit

{-# COMPILED putStrLn putStrLn #-}
{-# COMPILED putStrLn Data.Text.IO.putStrLn #-}
{-# COMPILED_UHC putStrLn (UHC.Agda.Builtins.primPutStrLn) #-}

main = putStrLn (♯ "a")

0 comments on commit 05b533a

Please sign in to comment.