{-|
Module      : Idris.Elab.Provider
Description : Code to elaborate type providers.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE PatternGuards #-}
module Idris.Elab.Provider(elabProvider) where

import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.Execute
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Clause
import Idris.Elab.Term
import Idris.Elab.Type
import Idris.Elab.Value
import Idris.Error
import Idris.Options
import Idris.Providers

import Prelude hiding (id, (.))

import Control.Category
import Control.Monad

-- | Elaborate a type provider
elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()
elabProvider :: Docstring (Either Err PTerm)
-> ElabInfo
-> SyntaxInfo
-> FC
-> FC
-> ProvideWhat
-> Name
-> Idris ()
elabProvider Docstring (Either Err PTerm)
doc ElabInfo
info SyntaxInfo
syn FC
fc FC
nfc ProvideWhat
what Name
n
    = do IState
i <- Idris IState
getIState
         -- Ensure that the experimental extension is enabled
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
TypeProviders forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [LanguageExt]
idris_language_extensions IState
i) forall a b. (a -> b) -> a -> b
$
           forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"Failed to define type provider \"" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++
                   String
"\".\nYou must turn on the TypeProviders extension."

         Context
ctxt <- Idris Context
getContext

         -- First elaborate the expected type (and check that it's a type)
         -- The goal type for a postulate is always Type.
         (Term
ty', Term
typ) <- case ProvideWhat
what of
                         ProvTerm PTerm
ty PTerm
p   -> ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
ERHS PTerm
ty
                         ProvPostulate PTerm
_ -> ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
ERHS (FC -> PTerm
PType FC
fc)
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term -> Bool
isTType Term
typ) forall a b. (a -> b) -> a -> b
$
           forall a. String -> Idris a
ifail (String
"Expected a type, got " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
ty' forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
typ)

         -- Elaborate the provider term to TT and check that the type matches
         (Term
e, Term
et) <- case ProvideWhat
what of
                      ProvTerm PTerm
_ PTerm
tm    -> ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
ERHS PTerm
tm
                      ProvPostulate PTerm
tm -> ElabInfo
-> ElabMode -> PTerm -> StateT IState (ExceptT Err IO) (Term, Term)
elabVal ElabInfo
info ElabMode
ERHS PTerm
tm
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Context -> Term -> Term -> Bool
isProviderOf Context
ctxt Term
ty' Term
et) forall a b. (a -> b) -> a -> b
$
           forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"Expected provider type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Term -> Term
providerOf Term
ty') forall a. [a] -> [a] -> [a]
++
                   String
", got " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
et forall a. [a] -> [a] -> [a]
++ String
" instead."

         -- Execute the type provider and normalise the result
         -- use 'run__provider' to convert to a primitive IO action

         Term
rhs <- Term -> Idris Term
execute (forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"run__provider") forall n. TT n
Erased)
                                          [forall n. TT n
Erased, Term
e])
         let rhs' :: Term
rhs' = Context -> Env -> Term -> Term
normalise Context
ctxt [] Term
rhs
         Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Normalised " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"'s RHS to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
rhs

         -- Extract the provided term or postulate from the type provider
         Provided Term
provided <- FC -> Term -> Idris (Provided Term)
getProvided FC
fc Term
rhs'

         case Provided Term
provided of
           Provide Term
tm
             | ProvTerm PTerm
ty PTerm
_ <- ProvideWhat
what ->
               do -- Finally add a top-level definition of the provided term
                  ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [] FC
fc [] Name
n FC
NoFC PTerm
ty
                  ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
elabClauses ElabInfo
info FC
fc [] Name
n [forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) []) [] (IState -> Term -> PTerm
delab IState
i Term
tm) []]
                  Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Elaborated provider " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" as: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term
tm
             | ProvPostulate PTerm
_ <- ProvideWhat
what ->
               do -- Add the postulate
                  ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabPostulate ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc FC
fc FC
nfc [] Name
n (IState -> Term -> PTerm
delab IState
i Term
tm)
                  Int -> String -> Idris ()
logElab Int
3 forall a b. (a -> b) -> a -> b
$ String
"Elaborated provided postulate " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
             | Bool
otherwise ->
               forall a. Err -> Idris a
ierror forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Attempted to provide a postulate where a term was expected."

    where isTType :: TT Name -> Bool
          isTType :: Term -> Bool
isTType (TType UExp
_) = Bool
True
          isTType Term
_ = Bool
False

          -- Note: IO (Providers.Provider ty) is used instead of IO'
          -- (MkFFI C_FFI) (Providers.Provider ty) in hopes of better
          -- error messages with less normalisation
          providerOf :: Type -> Type
          providerOf :: Term -> Term
providerOf Term
ty = forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"IO") forall n. TT n
Erased) forall a b. (a -> b) -> a -> b
$
                            forall n. AppStatus n -> TT n -> TT n -> TT n
App forall n. AppStatus n
Complete (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Provider") [String
"Providers", String
"Prelude"]) forall n. TT n
Erased)
                              Term
ty

          isProviderOf :: Context -> TT Name -> TT Name -> Bool
          isProviderOf :: Context -> Term -> Term -> Bool
isProviderOf Context
ctxt Term
tp Term
prov =
            case Context -> Env -> Term -> Term -> TC ()
converts Context
ctxt [] (Term -> Term
providerOf Term
tp) Term
prov of
              OK ()
_ -> Bool
True
              TC ()
_    -> Bool
False