1
{-# LANGUAGE CPP, FlexibleInstances, UndecidableInstances,
2
GeneralizedNewtypeDeriving, ScopedTypeVariables
5
{-| Primitive functions, such as addition on builtin integers.
7
module Agda.TypeChecking.Primitive where
11
import qualified Data.Map as Map
14
import Agda.Syntax.Position
15
import Agda.Syntax.Common hiding (Nat)
16
import Agda.Syntax.Internal
17
import Agda.Syntax.Literal
18
import Agda.Syntax.Concrete.Pretty ()
19
import Agda.Syntax.Abstract.Name
20
import qualified Agda.Syntax.Concrete.Name as C
22
import Agda.TypeChecking.Monad
23
import Agda.TypeChecking.Monad.Builtin
24
import Agda.TypeChecking.Reduce
25
import Agda.TypeChecking.Substitute
26
import Agda.TypeChecking.Errors
27
import Agda.TypeChecking.Pretty () -- instances only
29
import Agda.Utils.Monad
30
import Agda.Utils.Pretty (pretty)
32
#include "../undefined.h"
33
import Agda.Utils.Impossible
35
-- | Rewrite a literal to constructor form if possible.
36
constructorForm :: MonadTCM tcm => Term -> tcm Term
37
constructorForm v@(Lit (LitInt r n))
41
return $ s `apply` [Arg NotHidden $ Lit $ LitInt r $ n - 1]
42
| otherwise = return v
43
constructorForm v = return v
45
---------------------------------------------------------------------------
46
-- * Primitive functions
47
---------------------------------------------------------------------------
49
data PrimitiveImpl = PrimImpl Type PrimFun
51
-- Haskell type to Agda type
53
newtype Str = Str { unStr :: String }
56
newtype Nat = Nat { unNat :: Integer }
57
deriving (Eq, Ord, Num, Integral, Enum, Real)
59
instance Show Nat where
62
class PrimType a where
63
primType :: MonadTCM tcm => a -> tcm Type
65
instance (PrimType a, PrimType b) => PrimTerm (a -> b) where
66
primTerm _ = unEl <$> (primType (undefined :: a) --> primType (undefined :: b))
68
instance PrimTerm a => PrimType a where
69
primType _ = el $ primTerm (undefined :: a)
71
class PrimTerm a where primTerm :: MonadTCM tcm => a -> tcm Term
72
instance PrimTerm Integer where primTerm _ = primInteger
73
instance PrimTerm Bool where primTerm _ = primBool
74
instance PrimTerm Char where primTerm _ = primChar
75
instance PrimTerm Double where primTerm _ = primFloat
76
instance PrimTerm Str where primTerm _ = primString
77
instance PrimTerm Nat where primTerm _ = primNat
79
instance PrimTerm a => PrimTerm [a] where
80
primTerm _ = list (primTerm (undefined :: a))
82
instance PrimTerm a => PrimTerm (IO a) where
83
primTerm _ = io (primTerm (undefined :: a))
85
-- From Agda term to Haskell value
88
toTerm :: MonadTCM tcm => tcm (a -> Term)
90
instance ToTerm Integer where toTerm = return $ Lit . LitInt noRange
91
instance ToTerm Nat where toTerm = return $ Lit . LitInt noRange . unNat
92
instance ToTerm Double where toTerm = return $ Lit . LitFloat noRange
93
instance ToTerm Char where toTerm = return $ Lit . LitChar noRange
94
instance ToTerm Str where toTerm = return $ Lit . LitString noRange . unStr
96
instance ToTerm Bool where
100
return $ \b -> if b then true else false
102
-- | @buildList A ts@ builds a list of type @List A@. Assumes that the terms
103
-- @ts@ all have type @A@.
104
buildList :: MonadTCM tcm => Term -> tcm ([Term] -> Term)
108
let nil = nil' `apply` [Arg Hidden a]
109
cons x xs = cons' `apply` [Arg Hidden a, Arg NotHidden x, Arg NotHidden xs]
110
return $ foldr cons nil
112
instance (PrimTerm a, ToTerm a) => ToTerm [a] where
114
a <- primTerm (undefined :: a)
115
mkList <- buildList a
117
return $ mkList . map fromA
119
-- From Haskell value to Agda term
121
type FromTermFunction a = Arg Term -> TCM (Reduced (Arg Term) a)
123
class FromTerm a where
124
fromTerm :: MonadTCM tcm => tcm (FromTermFunction a)
126
instance FromTerm Integer where
127
fromTerm = fromLiteral $ \l -> case l of
131
instance FromTerm Nat where
132
fromTerm = fromLiteral $ \l -> case l of
133
LitInt _ n -> Just $ Nat n
136
instance FromTerm Double where
137
fromTerm = fromLiteral $ \l -> case l of
138
LitFloat _ x -> Just x
141
instance FromTerm Char where
142
fromTerm = fromLiteral $ \l -> case l of
143
LitChar _ c -> Just c
146
instance FromTerm Str where
147
fromTerm = fromLiteral $ \l -> case l of
148
LitString _ s -> Just $ Str s
151
instance FromTerm Bool where
155
fromReducedTerm $ \t -> case t of
156
_ | t === true -> Just True
157
| t === false -> Just False
158
| otherwise -> Nothing
160
Def x [] === Def y [] = x == y
161
Con x [] === Con y [] = x == y
162
Var n [] === Var m [] = n == m
165
instance (ToTerm a, FromTerm a) => FromTerm [a] where
173
return $ mkList nil cons toA fromA
175
isCon (Lam _ b) = isCon $ absBody b
176
isCon (Con c _) = return c
179
typeError $ GenericError $ "expected constructor in built-in binding to " ++ show d
180
-- TODO: check this when binding the things
182
mkList nil cons toA fromA t = do
184
let arg = Arg (argHiding t)
187
| c == nil -> return $ YesReduction []
191
(\x' -> arg $ Con c [x',xs]) $ \y ->
193
(mkList nil cons toA fromA xs)
194
(\xs' -> arg $ Con c [Arg NotHidden $ fromA y, xs']) $ \ys ->
196
_ -> return $ NoReduction t
198
-- | Conceptually: @redBind m f k = either (return . Left . f) k =<< m@
199
redBind :: MonadTCM tcm => tcm (Reduced a a') -> (a -> b) ->
200
(a' -> tcm (Reduced b b')) -> tcm (Reduced b b')
204
NoReduction x -> return $ NoReduction $ f x
205
YesReduction y -> k y
207
redReturn :: MonadTCM tcm => a -> tcm (Reduced a' a)
208
redReturn = return . YesReduction
210
fromReducedTerm :: MonadTCM tcm => (Term -> Maybe a) -> tcm (FromTermFunction a)
211
fromReducedTerm f = return $ \t -> do
214
Just x -> return $ YesReduction x
215
Nothing -> return $ NoReduction t
217
fromLiteral :: MonadTCM tcm => (Literal -> Maybe a) -> tcm (FromTermFunction a)
218
fromLiteral f = fromReducedTerm $ \t -> case t of
223
mkPrimFun1 :: (MonadTCM tcm, PrimType a, PrimType b, FromTerm a, ToTerm b) =>
224
(a -> b) -> tcm PrimitiveImpl
229
return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 1 $ \[v] -> liftTCM $
231
(\v' -> [v']) $ \x ->
232
redReturn $ fromB $ f x
234
mkPrimFun2 :: (MonadTCM tcm, PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) =>
235
(a -> b -> c) -> tcm PrimitiveImpl
242
return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 2 $ \[v,w] -> liftTCM $
244
(\v' -> [v',w]) $ \x ->
246
(\w' -> [Arg (argHiding v) (fromA x), w']) $ \y ->
247
redReturn $ fromC $ f x y
249
mkPrimFun4 :: ( MonadTCM tcm
250
, PrimType a, FromTerm a, ToTerm a
251
, PrimType b, FromTerm b, ToTerm b
252
, PrimType c, FromTerm c, ToTerm c
253
, PrimType d, FromTerm d
254
, PrimType e, ToTerm e) =>
255
(a -> b -> c -> d -> e) -> tcm PrimitiveImpl
257
(toA, fromA) <- (,) <$> fromTerm <*> toTerm
258
(toB, fromB) <- (,) <$> fromTerm <*> toTerm
259
(toC, fromC) <- (,) <$> fromTerm <*> toTerm
263
return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ 4 $ \[a,b,c,d] -> liftTCM $
265
(\a' -> [a',b,c,d]) $ \x ->
267
(\b' -> [Arg (argHiding a) (fromA x), b', c, d]) $ \y ->
269
(\c' -> [ Arg (argHiding a) (fromA x)
270
, Arg (argHiding b) (fromB y), c', d]) $ \z ->
272
(\d' -> [ Arg (argHiding a) (fromA x)
273
, Arg (argHiding b) (fromB y)
274
, Arg (argHiding c) (fromC z)
276
redReturn $ fromE $ f x y z w
278
-- Abstract primitive functions
279
abstractPrim :: (MonadTCM tcm, PrimType a) => a -> tcm PrimitiveImpl
280
abstractPrim x = abstractFromType (primType x)
282
abstractFromType :: MonadTCM tcm => tcm Type -> tcm PrimitiveImpl
283
abstractFromType mt = do
285
return $ PrimImpl t $ PrimFun __IMPOSSIBLE__ (arity t) $ \args -> NoReduction <$> normalise args
290
(-->) :: MonadTCM tcm => tcm Type -> tcm Type -> tcm Type
294
return $ El (getSort a' `sLub` getSort b') $ Fun (Arg NotHidden a') b'
296
gpi :: MonadTCM tcm => Hiding -> String -> tcm Type -> tcm Type -> tcm Type
300
b' <- addCtx x (Arg h a') b
301
return $ El (getSort a' `sLub` getSort b') $ Pi (Arg h a') (Abs name b')
303
hPi, nPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm Type
307
var :: MonadTCM tcm => Integer -> tcm Term
308
var n = return $ Var n []
312
gApply :: MonadTCM tcm => Hiding -> tcm Term -> tcm Term -> tcm Term
316
return $ x `apply` [Arg h y]
318
(<@>),(<#>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm Term
319
(<@>) = gApply NotHidden
320
(<#>) = gApply Hidden
322
list :: MonadTCM tcm => tcm Term -> tcm Term
323
list t = primList <@> t
325
io :: MonadTCM tcm => tcm Term -> tcm Term
328
el :: MonadTCM tcm => tcm Term -> tcm Type
329
el t = El (Type 0) <$> t
331
tset :: MonadTCM tcm => tcm Type
332
tset = return $ sort (Type 0)
334
---------------------------------------------------------------------------
335
-- * The actual primitive functions
336
---------------------------------------------------------------------------
338
type Op a = a -> a -> a
340
type Rel a = a -> a -> Bool
341
type Pred a = a -> Bool
343
primitiveFunctions :: Map String (TCM PrimitiveImpl)
344
primitiveFunctions = Map.fromList
347
[ "primIntegerPlus" |-> mkPrimFun2 ((+) :: Op Integer)
348
, "primIntegerMinus" |-> mkPrimFun2 ((-) :: Op Integer)
349
, "primIntegerTimes" |-> mkPrimFun2 ((*) :: Op Integer)
350
, "primIntegerDiv" |-> mkPrimFun2 (div :: Op Integer) -- partial
351
, "primIntegerMod" |-> mkPrimFun2 (mod :: Op Integer) -- partial
352
, "primIntegerEquality" |-> mkPrimFun2 ((==) :: Rel Integer)
353
, "primIntegerLess" |-> mkPrimFun2 ((<) :: Rel Integer)
354
, "primIntegerAbs" |-> mkPrimFun1 (Nat . abs :: Integer -> Nat)
355
, "primNatToInteger" |-> mkPrimFun1 (unNat :: Nat -> Integer)
356
, "primShowInteger" |-> mkPrimFun1 (Str . show :: Integer -> Str)
358
-- Natural number functions
359
, "primNatPlus" |-> mkPrimFun2 ((+) :: Op Nat)
360
, "primNatMinus" |-> mkPrimFun2 ((\x y -> max 0 (x - y)) :: Op Nat)
361
, "primNatTimes" |-> mkPrimFun2 ((*) :: Op Nat)
362
, "primNatDivSucAux" |-> mkPrimFun4 ((\k m n j -> k + div (n + m - j) (m + 1)) :: Nat -> Nat -> Nat -> Nat -> Nat)
363
, "primNatModSucAux" |->
364
let aux :: Nat -> Nat -> Nat -> Nat -> Nat
365
aux k m n j | n > j = mod (n - j - 1) (m + 1)
368
, "primNatEquality" |-> mkPrimFun2 ((==) :: Rel Nat)
369
, "primNatLess" |-> mkPrimFun2 ((<) :: Rel Nat)
371
-- Floating point functions
372
, "primIntegerToFloat" |-> mkPrimFun1 (fromIntegral :: Integer -> Double)
373
, "primFloatPlus" |-> mkPrimFun2 ((+) :: Op Double)
374
, "primFloatMinus" |-> mkPrimFun2 ((-) :: Op Double)
375
, "primFloatTimes" |-> mkPrimFun2 ((*) :: Op Double)
376
, "primFloatDiv" |-> mkPrimFun2 ((/) :: Op Double)
377
, "primFloatLess" |-> mkPrimFun2 ((<) :: Rel Double)
378
, "primRound" |-> mkPrimFun1 (round :: Double -> Integer)
379
, "primFloor" |-> mkPrimFun1 (floor :: Double -> Integer)
380
, "primCeiling" |-> mkPrimFun1 (ceiling :: Double -> Integer)
381
, "primExp" |-> mkPrimFun1 (exp :: Fun Double)
382
, "primLog" |-> mkPrimFun1 (log :: Fun Double) -- partial
383
, "primSin" |-> mkPrimFun1 (sin :: Fun Double)
384
, "primShowFloat" |-> mkPrimFun1 (Str . show :: Double -> Str)
386
-- Character functions
387
, "primCharEquality" |-> mkPrimFun2 ((==) :: Rel Char)
388
, "primIsLower" |-> mkPrimFun1 isLower
389
, "primIsDigit" |-> mkPrimFun1 isDigit
390
, "primIsAlpha" |-> mkPrimFun1 isAlpha
391
, "primIsSpace" |-> mkPrimFun1 isSpace
392
, "primIsAscii" |-> mkPrimFun1 isAscii
393
, "primIsLatin1" |-> mkPrimFun1 isLatin1
394
, "primIsPrint" |-> mkPrimFun1 isPrint
395
, "primIsHexDigit" |-> mkPrimFun1 isHexDigit
396
, "primToUpper" |-> mkPrimFun1 toUpper
397
, "primToLower" |-> mkPrimFun1 toLower
398
, "primCharToNat" |-> mkPrimFun1 (fromIntegral . fromEnum :: Char -> Nat)
399
, "primNatToChar" |-> mkPrimFun1 (toEnum . fromIntegral :: Nat -> Char)
400
, "primShowChar" |-> mkPrimFun1 (Str . show . pretty . LitChar noRange)
403
, "primStringToList" |-> mkPrimFun1 unStr
404
, "primStringFromList" |-> mkPrimFun1 Str
405
, "primStringAppend" |-> mkPrimFun2 (\s1 s2 -> Str $ unStr s1 ++ unStr s2)
406
, "primStringEquality" |-> mkPrimFun2 ((==) :: Rel Str)
407
, "primShowString" |-> mkPrimFun1 (Str . show . pretty . LitString noRange . unStr)
412
lookupPrimitiveFunction :: MonadTCM tcm => String -> tcm PrimitiveImpl
413
lookupPrimitiveFunction x =
414
case Map.lookup x primitiveFunctions of
416
Nothing -> typeError $ NoSuchPrimitiveFunction x
418
-- | Rebind a primitive. Assumes everything is type correct. Used when
419
-- importing a module with primitives.
420
rebindPrimitive :: MonadTCM tcm => String -> tcm PrimFun
421
rebindPrimitive x = do
422
PrimImpl _ pf <- lookupPrimitiveFunction x
added
removed
src/full/Agda/TypeChecking/Primitive.hs
