{-|
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 [] (Name -> PTerm) -> Name -> PTerm
forall a b. (a -> b) -> a -> b
$ Name -> [String] -> Name
sNS (String -> Name
sUN String
"Provider" ) [String
"Providers", String
"Prelude"]) [Int -> [ArgOpt] -> Name -> PTerm -> PArg
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
[Provided a] -> ShowS
Provided a -> String
(Int -> Provided a -> ShowS)
-> (Provided a -> String)
-> ([Provided a] -> ShowS)
-> Show (Provided a)
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
$cshowsPrec :: forall a. Show a => Int -> Provided a -> ShowS
showsPrec :: Int -> Provided a -> ShowS
$cshow :: forall a. Show a => Provided a -> String
show :: Provided a -> String
$cshowList :: forall a. Show a => [Provided a] -> ShowS
showList :: [Provided a] -> ShowS
Show, Provided a -> Provided a -> Bool
(Provided a -> Provided a -> Bool)
-> (Provided a -> Provided a -> Bool) -> Eq (Provided a)
forall a. Eq a => Provided a -> Provided a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
/= :: Provided a -> Provided a -> Bool
Eq, (forall a b. (a -> b) -> Provided a -> Provided b)
-> (forall a b. a -> Provided b -> Provided a) -> Functor Provided
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
$cfmap :: forall a b. (a -> b) -> Provided a -> Provided b
fmap :: forall a b. (a -> b) -> Provided a -> Provided b
$c<$ :: forall a b. a -> Provided b -> Provided a
<$ :: forall a b. a -> Provided b -> Provided a
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]) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm
                  , (P NameType
_ Name
nm TT Name
_, [TT Name
_, TT Name
err]) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
result
                  , Name
pioret Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ioret Bool -> Bool -> Bool
&& Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ermod
                      = case TT Name
err of
                          Constant (Str String
msg) -> Err -> Idris (Provided (TT Name))
forall a. Err -> Idris a
ierror (Err -> Idris (Provided (TT Name)))
-> (String -> Err) -> String -> Idris (Provided (TT Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err) -> (String -> Err) -> String -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
ProviderError (String -> Idris (Provided (TT Name)))
-> String -> Idris (Provided (TT Name))
forall a b. (a -> b) -> a -> b
$ String
msg
                          TT Name
_ -> String -> Idris (Provided (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]) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm
                  , (P NameType
_ Name
nm TT Name
_, [TT Name
_, TT Name
res]) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
result
                  , Name
pioret Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ioret Bool -> Bool -> Bool
&& Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
prmod
                      = Provided (TT Name) -> Idris (Provided (TT Name))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Provided (TT Name) -> Idris (Provided (TT Name)))
-> (TT Name -> Provided (TT Name))
-> TT Name
-> Idris (Provided (TT Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TT Name -> Provided (TT Name)
forall a. a -> Provided a
Provide (TT Name -> Idris (Provided (TT Name)))
-> TT Name -> Idris (Provided (TT Name))
forall a b. (a -> b) -> a -> b
$ TT Name
res
                  | Bool
otherwise = String -> Idris (Provided (TT Name))
forall a. String -> Idris a
ifail (String -> Idris (Provided (TT Name)))
-> String -> Idris (Provided (TT Name))
forall a b. (a -> b) -> a -> b
$ String
"Internal type provider error: result was not " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        String
"IO (Provider a), or perhaps missing normalisation.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                        String
"Term: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
1000 (TT Name -> String
forall a. Show a => a -> String
show TT Name
tm)