1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- A simple example of a program using the foreign function interface
------------------------------------------------------------------------
{-# OPTIONS --guardedness #-}
module README.Foreign.Haskell where
-- In order to be considered safe by Agda, the standard library cannot
-- add COMPILE pragmas binding the inductive types it defines to concrete
-- Haskell types.
-- To work around this limitation, we have defined FFI-friendly versions
-- of these types together with a zero-cost coercion `coerce`.
open import Level using (Level)
open import Agda.Builtin.Int
open import Agda.Builtin.Nat
open import Data.Bool.Base using (Bool; if_then_else_)
open import Data.Char as Char
open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Data.Product.Base using (_×_; _,_)
open import Function
open import Relation.Nullary.Decidable
import Foreign.Haskell as FFI
open import Foreign.Haskell.Coerce
private
variable
a : Level
A : Set a
-- Here we use the FFI version of Pair.
postulate
primUncons : List A → Maybe (FFI.Pair A (List A))
primCatMaybes : List (Maybe A) → List A
primTestChar : Char → Bool
primIntEq : Int → Int → Bool
{-# COMPILE GHC primUncons = \ _ _ xs -> case xs of
{ [] -> Nothing
; (x : xs) -> Just (x, xs)
}
#-}
{-# FOREIGN GHC import Data.Maybe #-}
{-# COMPILE GHC primCatMaybes = \ _ _ -> catMaybes #-}
{-# COMPILE GHC primTestChar = ('-' /=) #-}
{-# COMPILE GHC primIntEq = (==) #-}
-- We however want to use the notion of Pair internal to the standard library.
-- For this we use `coerce` to take use back to the types we are used to.
-- The typeclass mechanism uses the coercion rules for Pair, as well as the
-- knowledge that natural numbers are represented as integers.
-- We additionally benefit from the congruence rules for List, Maybe, Char,
-- Bool, and a reflexivity principle for variable A.
uncons : List A → Maybe (A × List A)
uncons = coerce primUncons
catMaybes : List (Maybe A) → List A
catMaybes = primCatMaybes
testChar : Char → Bool
testChar = coerce primTestChar
-- note that coerce is useless here but the proof could come from
-- either `coerce-fun coerce-refl coerce-refl` or `coerce-refl` alone
-- We (and Agda) do not care which proof we got.
eqNat : Nat → Nat → Bool
eqNat = coerce primIntEq
-- We can coerce `Nat` to `Int` but not `Int` to `Nat`. This fundamentally
-- relies on the fact that `Coercible` understands that functions are
-- contravariant.
open import IO
open import Codata.Musical.Notation
open import Data.String.Base using (toList; fromList; unlines; _++_)
open import Relation.Nullary.Negation
-- example program using uncons, catMaybes, and testChar
main = run $ do
content ← readFiniteFile "README/Foreign/Haskell.agda"
let chars = toList content
let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing)
let cleaned = dropWhile ('\n' ≟_) $ cleanup chars
case uncons cleaned of λ where
nothing → putStrLn "I cannot believe this file is filed with dashes only!"
(just (c , cs)) → putStrLn $ unlines
$ ("First (non dash) character: " ++ Char.show c)
∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≟_)) cs))
∷ []
-- You can compile and run this test by writing:
-- agda -c Haskell.agda
-- ../../Haskell
-- You should see the following text (without the indentation on the left):
-- First (non dash) character: ' '
-- Rest (dash free) of the line: The Agda standard library
|
