{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
PatternGuards #-}
module Idris.ElabDecls(elabDecl, elabDecl', elabDecls, elabMain, elabPrims,
recinfo) where
import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Directives
import Idris.Docstrings hiding (Unchecked)
import Idris.Elab.Clause
import Idris.Elab.Data
import Idris.Elab.Implementation
import Idris.Elab.Interface
import Idris.Elab.Provider
import Idris.Elab.Record
import Idris.Elab.RunElab
import Idris.Elab.Term
import Idris.Elab.Transform
import Idris.Elab.Type
import Idris.Elab.Value
import Idris.Error
import Idris.Options
import Idris.Output (sendHighlighting)
import Idris.Primitives
import Idris.Termination
import IRTS.Lang
import Prelude hiding (id, (.))
import Control.Category
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
recinfo :: FC -> ElabInfo
recinfo :: FC -> ElabInfo
recinfo fc :: FC
fc = [(Name, PTerm)]
-> Ctxt [Name]
-> (Name -> Name)
-> [String]
-> Maybe FC
-> String
-> Int
-> [Name]
-> (PTerm -> PTerm)
-> (ElabWhat -> ElabInfo -> PDecl -> Idris ())
-> ElabInfo
EInfo [] Ctxt [Name]
forall k a. Map k a
emptyContext Name -> Name
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] (FC -> Maybe FC
forall a. a -> Maybe a
Just FC
fc) (FC -> String
fc_fname FC
fc) 0 [] PTerm -> PTerm
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl'
elabMain :: Idris Term
elabMain :: Idris Term
elabMain = do (m :: Term
m, _) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo FC
fc) ElabMode
ERHS
(FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "run__IO"))
[PTerm -> PArg
forall t. t -> PArg' t
pexp (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN "main") ["Main"])])
Term -> Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
m
where fc :: FC
fc = String -> FC
fileFC "toplevel"
elabPrims :: Idris ()
elabPrims :: Idris ()
elabPrims = do IState
i <- Idris IState
getIState
let cs_in :: Set ConstraintFC
cs_in = IState -> Set ConstraintFC
idris_constraints IState
i
let mkdec :: DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec opt :: DataOpts
opt decl :: PData' t
decl docs :: Docstring (Either Err t)
docs argdocs :: [(Name, Docstring (Either Err t))]
argdocs =
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> DataOpts
-> PData' t
-> PDecl' t
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> DataOpts
-> PData' t
-> PDecl' t
PData Docstring (Either Err t)
docs [(Name, Docstring (Either Err t))]
argdocs SyntaxInfo
defaultSyntax (String -> FC
fileFC "builtin")
DataOpts
opt PData' t
decl
LanguageExt -> Idris ()
addLangExt LanguageExt
LinearTypes
ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo FC
primfc) (DataOpts
-> PData' PTerm
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> PDecl
forall t.
DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec DataOpts
forall a. [a]
inferOpts PData' PTerm
inferDecl Docstring (Either Err PTerm)
forall a. Docstring a
emptyDocstring [])
LanguageExt -> Idris ()
dropLangExt LanguageExt
LinearTypes
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_constraints :: Set ConstraintFC
idris_constraints = Set ConstraintFC
cs_in }
ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo FC
primfc) (DataOpts
-> PData' PTerm
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> PDecl
forall t.
DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec DataOpts
forall a. [a]
eqOpts PData' PTerm
eqDecl Docstring (Either Err PTerm)
forall t b. Docstring (Either (Err' t) b)
eqDoc [(Name, Docstring (Either Err PTerm))]
forall t b. [(Name, Docstring (Either (Err' t) b))]
eqParamDoc)
Name -> Name -> Idris ()
addNameHint Name
eqTy (String -> Name
sUN "prf")
(Prim -> Idris ()) -> [Prim] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prim -> Idris ()
elabPrim [Prim]
primitives
Idris ()
elabBelieveMe
Idris ()
elabSynEq
where elabPrim :: Prim -> Idris ()
elabPrim :: Prim -> Idris ()
elabPrim (Prim n :: Name
n ty :: Term
ty i :: Int
i def :: [Const] -> Maybe Const
def sc :: (Int, PrimFn)
sc tot :: Totality
tot)
= do (Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
n Term
ty Int
i (([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim [Const] -> Maybe Const
def))
Name -> Totality -> Idris ()
setTotality Name
n Totality
tot
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState IState
i { idris_scprims :: [(Name, (Int, PrimFn))]
idris_scprims = (Name
n, (Int, PrimFn)
sc) (Name, (Int, PrimFn))
-> [(Name, (Int, PrimFn))] -> [(Name, (Int, PrimFn))]
forall a. a -> [a] -> [a]
: IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i }
primfc :: FC
primfc = String -> FC
fileFC "primitive"
valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim prim :: [Const] -> Maybe Const
prim vals :: [Value]
vals = (Const -> Value) -> Maybe Const -> Maybe Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Const -> Value
VConstant ((Value -> Maybe Const) -> [Value] -> Maybe [Const]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Maybe Const
getConst [Value]
vals Maybe [Const] -> ([Const] -> Maybe Const) -> Maybe Const
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Const] -> Maybe Const
prim)
getConst :: Value -> Maybe Const
getConst (VConstant c :: Const
c) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
getConst _ = Maybe Const
forall a. Maybe a
Nothing
p_believeMe :: [a] -> Maybe a
p_believeMe [_,_,x :: a
x] = a -> Maybe a
forall a. a -> Maybe a
Just a
x
p_believeMe _ = Maybe a
forall a. Maybe a
Nothing
believeTy :: Term
believeTy = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "a") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-2))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-1))))
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "b") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-2))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-1))))
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "x") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Int -> Term
forall n. Int -> TT n
V 1) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-1)))) (Int -> Term
forall n. Int -> TT n
V 1)))
elabBelieveMe :: Idris ()
elabBelieveMe
= do let prim__believe_me :: Name
prim__believe_me = String -> Name
sUN "prim__believe_me"
(Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
prim__believe_me Term
believeTy 3 [Value] -> Maybe Value
forall a. [a] -> Maybe a
p_believeMe)
Name -> Totality -> Idris ()
setTotality Name
prim__believe_me ([Int] -> Totality
Total [])
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState IState
i {
idris_scprims :: [(Name, (Int, PrimFn))]
idris_scprims = (Name
prim__believe_me, (3, PrimFn
LNoOp)) (Name, (Int, PrimFn))
-> [(Name, (Int, PrimFn))] -> [(Name, (Int, PrimFn))]
forall a. a -> [a] -> [a]
: IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i
}
p_synEq :: [Value] -> Maybe Value
p_synEq [t :: Value
t,_,x :: Value
x,y :: Value
y]
| Value
x Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
y = Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value -> Value
VApp (Value -> Value -> Value
VApp Value
vnJust Value
VErased)
(Value -> Value -> Value
VApp (Value -> Value -> Value
VApp Value
vnRefl Value
t) Value
x))
| Bool
otherwise = Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value -> Value
VApp Value
vnNothing Value
VErased)
p_synEq args :: [Value]
args = Maybe Value
forall a. Maybe a
Nothing
nMaybe :: Term
nMaybe = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> NameType
TCon 0 2) (Name -> [String] -> Name
sNS (String -> Name
sUN "Maybe") ["Maybe", "Prelude"]) Term
forall n. TT n
Erased
vnJust :: Value
vnJust = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon 1 2 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN "Just") ["Maybe", "Prelude"]) Value
VErased
vnNothing :: Value
vnNothing = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon 0 1 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN "Nothing") ["Maybe", "Prelude"]) Value
VErased
vnRefl :: Value
vnRefl = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon 0 2 Bool
False) Name
eqCon Value
VErased
synEqTy :: Term
synEqTy = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "a") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-3))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-2))))
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "b") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-3))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-2))))
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "x") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Int -> Term
forall n. Int -> TT n
V 1) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-2))))
(Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN "y") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Int -> Term
forall n. Int -> TT n
V 1) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-2))))
(Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
nMaybe [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 (Int -> Int -> NameType
TCon 0 4) Name
eqTy Term
forall n. TT n
Erased)
[Int -> Term
forall n. Int -> TT n
V 3, Int -> Term
forall n. Int -> TT n
V 2, Int -> Term
forall n. Int -> TT n
V 1, Int -> Term
forall n. Int -> TT n
V 0]]))))
elabSynEq :: Idris ()
elabSynEq
= do let synEq :: Name
synEq = String -> Name
sUN "prim__syntactic_eq"
(Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
synEq Term
synEqTy 4 [Value] -> Maybe Value
p_synEq)
Name -> Totality -> Idris ()
setTotality Name
synEq ([Int] -> Totality
Total [])
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState IState
i {
idris_scprims :: [(Name, (Int, PrimFn))]
idris_scprims = (Name
synEq, (4, PrimFn
LNoOp)) (Name, (Int, PrimFn))
-> [(Name, (Int, PrimFn))] -> [(Name, (Int, PrimFn))]
forall a. a -> [a] -> [a]
: IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i
}
elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecls info :: ElabInfo
info ds :: [PDecl]
ds = do (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
EAll ElabInfo
info) [PDecl]
ds
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl what :: ElabWhat
what info :: ElabInfo
info d :: PDecl
d
= let info' :: ElabInfo
info' = ElabInfo
info { rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl = ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' } in
Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (Idris () -> Idris ()
forall a. Idris a -> Idris a
withErrorReflection (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
info' PDecl
d) (Err -> Idris ()
setAndReport)
elabDecl' :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' _ info :: ElabInfo
info (PFix _ _ _)
= () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' _ info :: ElabInfo
info (PSyntax _ p :: Syntax
p)
= () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PTy doc :: Docstring (Either Err PTerm)
doc argdocs :: [(Name, Docstring (Either Err PTerm))]
argdocs s :: SyntaxInfo
s f :: FC
f o :: FnOpts
o n :: Name
n nfc :: FC
nfc ty :: PTerm
ty)
| ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating type decl " 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]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
o
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs FC
f FnOpts
o Name
n FC
nfc PTerm
ty
() -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PPostulate b :: Bool
b doc :: Docstring (Either Err PTerm)
doc s :: SyntaxInfo
s f :: FC
f nfc :: FC
nfc o :: FnOpts
o n :: Name
n ty :: PTerm
ty)
| ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating postulate " 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]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
o
if Bool
b
then ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabExtern ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc FC
f FC
nfc FnOpts
o Name
n PTerm
ty
else ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabPostulate ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc FC
f FC
nfc FnOpts
o Name
n PTerm
ty
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PData doc :: Docstring (Either Err PTerm)
doc argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs s :: SyntaxInfo
s f :: FC
f co :: DataOpts
co d :: PData' PTerm
d)
| ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
d)
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
f DataOpts
co PData' PTerm
d
| Bool
otherwise
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating [type of] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
d)
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
f DataOpts
co (Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
d) (PData' PTerm -> FC
forall t. PData' t -> FC
d_name_fc PData' PTerm
d) (PData' PTerm -> PTerm
forall t. PData' t -> t
d_tcon PData' PTerm
d))
elabDecl' what :: ElabWhat
what info :: ElabInfo
info d :: PDecl
d@(PClauses f :: FC
f o :: FnOpts
o n :: Name
n ps :: [PClause' PTerm]
ps)
| ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating clause " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
IState
i <- Idris IState
getIState
let o' :: FnOpts
o' = case Name -> Ctxt FnOpts -> [FnOpts]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt FnOpts
idris_flags IState
i) of
[fs :: FnOpts
fs] -> FnOpts
fs
[] -> []
ElabInfo -> FC -> FnOpts -> Name -> [PClause' PTerm] -> Idris ()
elabClauses ElabInfo
info FC
f (FnOpts
o FnOpts -> FnOpts -> FnOpts
forall a. [a] -> [a] -> [a]
++ FnOpts
o') Name
n [PClause' PTerm]
ps
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PMutual f :: FC
f ps :: [PDecl]
ps)
= do IState
i <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
let (ufnames :: [Name]
ufnames, umethss :: [[Name]]
umethss) = [(Name, [Name])] -> ([Name], [[Name]])
forall a b. [(a, b)] -> ([a], [b])
unzip ((PDecl -> Maybe (Name, [Name])) -> [PDecl] -> [(Name, [Name])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (IState -> PDecl -> Maybe (Name, [Name])
findTCImpl IState
i) [PDecl]
ps)
case [PDecl]
ps of
[p :: PDecl
p] -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
what ElabInfo
info PDecl
p
_ -> do (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
ETypes ElabInfo
info) [PDecl]
ps
(PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
EDefns ElabInfo
info) [PDecl]
ps
let datans :: [Name]
datans = (PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
declared ([PDecl] -> [PDecl]
forall t. [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl]
ps)
(Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Name] -> Name -> Idris ()
setMutData [Name]
datans) [Name]
datans
Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Rechecking for positivity " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
datans
(Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\x :: Name
x -> do Name -> Totality -> Idris ()
setTotality Name
x Totality
Unchecked) [Name]
datans
IState
i <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
(Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\n :: Name
n -> do Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Simplifying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
Context
ctxt' <- do Context
ctxt <- Idris Context
getContext
TC Context -> Idris Context
forall a. TC a -> Idris a
tclift (TC Context -> Idris Context) -> TC Context -> Idris Context
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef Name
n [Name]
ufnames [[Name]]
umethss (IState -> ErasureInfo
getErasureInfo IState
i) Context
ctxt
Context -> Idris ()
setContext Context
ctxt')
(((FC, Name) -> Name) -> [(FC, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (FC, Name) -> Name
forall a b. (a, b) -> b
snd (IState -> [(FC, Name)]
idris_totcheck IState
i))
((FC, Name) -> Idris ()) -> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
buildSCG (IState -> [(FC, Name)]
idris_totcheck IState
i)
((FC, Name) -> StateT IState (ExceptT Err IO) Totality)
-> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> StateT IState (ExceptT Err IO) Totality
checkDeclTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
((FC, Name) -> Idris ()) -> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
verifyTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
Idris ()
clear_totcheck
where isDataDecl :: PDecl' t -> Bool
isDataDecl (PData _ _ _ _ _ _) = Bool
True
isDataDecl _ = Bool
False
findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])
findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])
findTCImpl ist :: IState
ist (PImplementation _ _ _ _ _ _ _ _ n_in :: Name
n_in _ ps :: [PTerm]
ps _ _ expn :: Maybe Name
expn _)
= let (n :: Name
n, meths :: [Name]
meths)
= case Name -> Ctxt InterfaceInfo -> [(Name, InterfaceInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n_in (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
[(n' :: Name
n', ci :: InterfaceInfo
ci)] -> (Name
n', ((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, FnOpts, PTerm)) -> Name
forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))
_ -> (Name
n_in, [])
iname :: Name
iname = Name -> [String] -> [PTerm] -> Maybe Name -> Name
forall a. Show a => Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n (ElabInfo -> [String]
namespace ElabInfo
info) [PTerm]
ps Maybe Name
expn in
(Name, [Name]) -> Maybe (Name, [Name])
forall a. a -> Maybe a
Just (Name
iname, [Name]
meths)
findTCImpl ist :: IState
ist _ = Maybe (Name, [Name])
forall a. Maybe a
Nothing
mkiname :: Name -> [String] -> [a] -> Maybe Name -> Name
mkiname n' :: Name
n' ns :: [String]
ns ps' :: [a]
ps' expn' :: Maybe Name
expn' =
case Maybe Name
expn' of
Nothing -> case [String]
ns of
[] -> SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
ps'))
m :: [String]
m -> Name -> [String] -> Name
sNS (SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
ps'))) [String]
m
Just nm :: Name
nm -> Name
nm
getDataDecls :: [PDecl' t] -> [PDecl' t]
getDataDecls (PNamespace _ _ ds :: [PDecl' t]
ds : decls :: [PDecl' t]
decls)
= [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
ds [PDecl' t] -> [PDecl' t] -> [PDecl' t]
forall a. [a] -> [a] -> [a]
++ [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
getDataDecls (d :: PDecl' t
d : decls :: [PDecl' t]
decls)
| PDecl' t -> Bool
forall t. PDecl' t -> Bool
isDataDecl PDecl' t
d = PDecl' t
d PDecl' t -> [PDecl' t] -> [PDecl' t]
forall a. a -> [a] -> [a]
: [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
| Bool
otherwise = [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
getDataDecls [] = []
setMutData :: [Name] -> Name -> Idris ()
setMutData ns :: [Name]
ns n :: Name
n
= do IState
i <- Idris IState
getIState
case Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
[x :: TypeInfo
x] -> do let x' :: TypeInfo
x' = TypeInfo
x { mutual_types :: [Name]
mutual_types = [Name]
ns }
IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_datatypes :: Ctxt TypeInfo
idris_datatypes
= Name -> TypeInfo -> Ctxt TypeInfo -> Ctxt TypeInfo
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n TypeInfo
x' (IState -> Ctxt TypeInfo
idris_datatypes IState
i) }
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PParams f :: FC
f ns :: [(Name, PTerm)]
ns ps :: [PDecl]
ps)
= do IState
i <- Idris IState
getIState
Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Expanding params block with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)] -> String
forall a. Show a => a -> String
show [(Name, PTerm)]
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ " decls " String -> String -> String
forall a. [a] -> [a] -> [a]
++
[Name] -> String
forall a. Show a => a -> String
show ((PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
tldeclared [PDecl]
ps)
let nblock :: [PDecl]
nblock = IState -> [PDecl]
pblock IState
i
(PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
info) [PDecl]
nblock
where
pblock :: IState -> [PDecl]
pblock i :: IState
i = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl
-> PDecl
expandParamsD Bool
False IState
i Name -> Name
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [(Name, PTerm)]
ns
((PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
tldeclared [PDecl]
ps)) [PDecl]
ps
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (POpenInterfaces f :: FC
f ns :: [Name]
ns ds :: [PDecl]
ds)
= do [Name]
open <- [Name] -> Idris [Name]
addOpenImpl [Name]
ns
(PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
info) [PDecl]
ds
[Name] -> Idris ()
setOpenImpl [Name]
open
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PNamespace n :: String
n nfc :: FC
nfc ps :: [PDecl]
ps) =
do (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
ninfo) [PDecl]
ps
let ns :: [Text]
ns = [Text] -> [Text]
forall a. [a] -> [a]
reverse ((String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
newNS)
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
nfc, [Text] -> Maybe String -> OutputAnnotation
AnnNamespace [Text]
ns Maybe String
forall a. Maybe a
Nothing)]
where
newNS :: [String]
newNS = String
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ElabInfo -> [String]
namespace ElabInfo
info
ninfo :: ElabInfo
ninfo = ElabInfo
info { namespace :: [String]
namespace = [String]
newNS }
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PInterface doc :: Docstring (Either Err PTerm)
doc s :: SyntaxInfo
s f :: FC
f cs :: [(Name, PTerm)]
cs n :: Name
n nfc :: FC
nfc ps :: [(Name, FC, PTerm)]
ps pdocs :: [(Name, Docstring (Either Err PTerm))]
pdocs fds :: [(Name, FC)]
fds ds :: [PDecl]
ds cn :: Maybe (Name, FC)
cn cd :: Docstring (Either Err PTerm)
cd)
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating interface " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> Name
-> FC
-> [(Name, FC, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC)]
-> [PDecl]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> Idris ()
elabInterface ElabInfo
info (SyntaxInfo
s { syn_params :: [(Name, PTerm)]
syn_params = [] }) Docstring (Either Err PTerm)
doc ElabWhat
what FC
f [(Name, PTerm)]
cs Name
n FC
nfc [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
fds [PDecl]
ds Maybe (Name, FC)
cn Docstring (Either Err PTerm)
cd
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PImplementation doc :: Docstring (Either Err PTerm)
doc argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs s :: SyntaxInfo
s f :: FC
f cs :: [(Name, PTerm)]
cs pnames :: [Name]
pnames acc :: Accessibility
acc fnopts :: FnOpts
fnopts n :: Name
n nfc :: FC
nfc ps :: [PTerm]
ps pextra :: [(Name, PTerm)]
pextra t :: PTerm
t expn :: Maybe Name
expn ds :: [PDecl]
ds)
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating implementation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe Name
-> [PDecl]
-> Idris ()
elabImplementation ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs ElabWhat
what FC
f [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
fnopts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
expn [PDecl]
ds
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PRecord doc :: Docstring (Either Err PTerm)
doc rsyn :: SyntaxInfo
rsyn fc :: FC
fc opts :: DataOpts
opts name :: Name
name nfc :: FC
nfc ps :: [(Name, FC, Plicity, PTerm)]
ps pdocs :: [(Name, Docstring (Either Err PTerm))]
pdocs fs :: [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fs cname :: Maybe (Name, FC)
cname cdoc :: Docstring (Either Err PTerm)
cdoc csyn :: SyntaxInfo
csyn)
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating record " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
name
ElabInfo
-> ElabWhat
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> DataOpts
-> Name
-> FC
-> [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> Idris ()
elabRecord ElabInfo
info ElabWhat
what Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc DataOpts
opts Name
name FC
nfc [(Name, FC, Plicity, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Maybe (Name, FC), Plicity, PTerm,
Maybe (Docstring (Either Err PTerm)))]
fs Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
csyn
elabDecl' _ info :: ElabInfo
info (PDSL n :: Name
n dsl :: DSL' PTerm
dsl)
= do IState
i <- Idris IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
DSLNotation LanguageExt -> [LanguageExt] -> 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 "You must turn on the DSLNotation extension to use a dsl block"
IState -> Idris ()
putIState (IState
i { idris_dsls :: Ctxt (DSL' PTerm)
idris_dsls = Name -> DSL' PTerm -> Ctxt (DSL' PTerm) -> Ctxt (DSL' PTerm)
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n DSL' PTerm
dsl (IState -> Ctxt (DSL' PTerm)
idris_dsls IState
i) })
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDSL Name
n)
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PDirective i :: Directive
i@(DLogging _))
= Directive -> Idris ()
directiveAction Directive
i
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PDirective i :: Directive
i)
| ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns = Directive -> Idris ()
directiveAction Directive
i
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PProvider doc :: Docstring (Either Err PTerm)
doc syn :: SyntaxInfo
syn fc :: FC
fc nfc :: FC
nfc provWhat :: ProvideWhat' PTerm
provWhat n :: Name
n)
| ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
= do Int -> String -> Idris ()
logElab 1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Elaborating type provider " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
Docstring (Either Err PTerm)
-> ElabInfo
-> SyntaxInfo
-> FC
-> FC
-> ProvideWhat' PTerm
-> Name
-> Idris ()
elabProvider Docstring (Either Err PTerm)
doc ElabInfo
info SyntaxInfo
syn FC
fc FC
nfc ProvideWhat' PTerm
provWhat Name
n
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PTransform fc :: FC
fc safety :: Bool
safety old :: PTerm
old new :: PTerm
new)
= do ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
elabTransform ElabInfo
info FC
fc Bool
safety PTerm
old PTerm
new
() -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' what :: ElabWhat
what info :: ElabInfo
info (PRunElabDecl fc :: FC
fc script :: PTerm
script ns :: [String]
ns)
= do IState
i <- Idris IState
getIState
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
ElabReflection LanguageExt -> [LanguageExt] -> 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
$
Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> Err -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg "You must turn on the ElabReflection extension to use %runElab")
ElabInfo -> FC -> PTerm -> [String] -> Idris ()
elabRunElab ElabInfo
info FC
fc PTerm
script [String]
ns
() -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' _ _ _ = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()