{-|
Module      : Idris.Providers
Description : Idris' 'Type Provider' implementation.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE DeriveFunctor, PatternGuards #-}
module Idris.Providers (
    providerTy
  , getProvided
  , Provided(..)
  ) where

import Idris.AbsSyntax
import Idris.Core.TT
import Idris.Error

-- | Wrap a type provider in the type of type providers
providerTy :: FC -> PTerm -> PTerm
providerTy :: FC -> PTerm -> PTerm
providerTy FC
fc PTerm
tm
  = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS (String -> Name
sUN String
"Provider" ) [String
"Providers", String
"Prelude"]) [forall t. Int -> [ArgOpt] -> Name -> t -> PArg' t
PExp Int
0 [] (Int -> String -> Name
sMN Int
0 String
"pvarg") PTerm
tm]

ioret :: Name
ioret :: Name
ioret = String -> Name
sUN String
"prim_io_pure"

ermod :: Name
ermod :: Name
ermod = Name -> [String] -> Name
sNS (String -> Name
sUN String
"Error") [String
"Providers", String
"Prelude"]

prmod :: Name
prmod :: Name
prmod = Name -> [String] -> Name
sNS (String -> Name
sUN String
"Provide") [String
"Providers", String
"Prelude"]

data Provided a = Provide a
  deriving (Int -> Provided a -> ShowS
forall a. Show a => Int -> Provided a -> ShowS
forall a. Show a => [Provided a] -> ShowS
forall a. Show a => Provided a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Provided a] -> ShowS
$cshowList :: forall a. Show a => [Provided a] -> ShowS
show :: Provided a -> String
$cshow :: forall a. Show a => Provided a -> String
showsPrec :: Int -> Provided a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Provided a -> ShowS
Show, Provided a -> Provided a -> Bool
forall a. Eq a => Provided a -> Provided a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Provided a -> Provided a -> Bool
$c/= :: forall a. Eq a => Provided a -> Provided a -> Bool
== :: Provided a -> Provided a -> Bool
$c== :: forall a. Eq a => Provided a -> Provided a -> Bool
Eq, forall a b. a -> Provided b -> Provided a
forall a b. (a -> b) -> Provided a -> Provided b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Provided b -> Provided a
$c<$ :: forall a b. a -> Provided b -> Provided a
fmap :: forall a b. (a -> b) -> Provided a -> Provided b
$cfmap :: forall a b. (a -> b) -> Provided a -> Provided b
Functor)

-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.
getProvided :: FC -> TT Name -> Idris (Provided (TT Name))
getProvided :: FC -> TT Name -> Idris (Provided (TT Name))
getProvided FC
fc TT Name
tm | (P NameType
_ Name
pioret TT Name
_, [TT Name
tp, TT Name
result]) <- forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm
                  , (P NameType
_ Name
nm TT Name
_, [TT Name
_, TT Name
err]) <- forall n. TT n -> (TT n, [TT n])
unApply TT Name
result
                  , Name
pioret forall a. Eq a => a -> a -> Bool
== Name
ioret Bool -> Bool -> Bool
&& Name
nm forall a. Eq a => a -> a -> Bool
== Name
ermod
                      = case TT Name
err of
                          Constant (Str String
msg) -> forall a. Err -> Idris a
ierror forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FC -> Err' t -> Err' t
At FC
fc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
ProviderError forall a b. (a -> b) -> a -> b
$ String
msg
                          TT Name
_ -> forall a. String -> Idris a
ifail String
"Internal error in type provider, non-normalised error"
                  | (P NameType
_ Name
pioret TT Name
_, [TT Name
tp, TT Name
result]) <- forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm
                  , (P NameType
_ Name
nm TT Name
_, [TT Name
_, TT Name
res]) <- forall n. TT n -> (TT n, [TT n])
unApply TT Name
result
                  , Name
pioret forall a. Eq a => a -> a -> Bool
== Name
ioret Bool -> Bool -> Bool
&& Name
nm forall a. Eq a => a -> a -> Bool
== Name
prmod
                      = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Provided a
Provide forall a b. (a -> b) -> a -> b
$ TT Name
res
                  | Bool
otherwise = forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"Internal type provider error: result was not " forall a. [a] -> [a] -> [a]
++
                                        String
"IO (Provider a), or perhaps missing normalisation.\n" forall a. [a] -> [a] -> [a]
++
                                        String
"Term: " forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
take Int
1000 (forall a. Show a => a -> String
show TT Name
tm)