{-# 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
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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
TypeProviders LanguageExt -> [LanguageExt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [LanguageExt]
idris_language_extensions IState
i) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
String -> Idris ()
forall a. String -> Idris a
ifail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Failed to define type provider \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"\".\nYou must turn on the TypeProviders extension."
Context
ctxt <- Idris Context
getContext
(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)
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term -> Bool
isTType Term
typ) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
String -> Idris ()
forall a. String -> Idris a
ifail (String
"Expected a type, got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
ty' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
typ)
(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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Context -> Term -> Term -> Bool
isProviderOf Context
ctxt Term
ty' Term
et) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
String -> Idris ()
forall a. String -> Idris a
ifail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Expected provider type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show (Term -> Term
providerOf Term
ty') String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
", got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
et String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" instead."
Term
rhs <- Term -> Idris Term
execute (Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"run__provider") Term
forall n. TT n
Erased)
[Term
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Normalised " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'s RHS to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
rhs
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
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 [FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl' PTerm] -> PClause
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborated provider " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" as: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm
| ProvPostulate PTerm
_ <- ProvideWhat
what ->
do
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborated provided postulate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
| Bool
otherwise ->
Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (String -> Err) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. String -> Err
forall t. String -> Err' t
Msg (String -> Idris ()) -> String -> Idris ()
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
providerOf :: Type -> Type
providerOf :: Term -> Term
providerOf Term
ty = AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (String -> Name
sUN String
"IO") Term
forall n. TT n
Erased) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Provider") [String
"Providers", String
"Prelude"]) Term
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