{-# 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 = [(Name, PTerm)]
-> Ctxt [Name]
-> (Name -> Name)
-> [String]
-> Maybe FC
-> String
-> Int
-> [Name]
-> (PTerm -> PTerm)
-> (ElabWhat -> ElabInfo -> PDecl -> Idris ())
-> ElabInfo
EInfo [] forall {k} {a}. Map k a
emptyContext forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] (forall a. a -> Maybe a
Just FC
fc) (FC -> String
fc_fname FC
fc) Int
0 [] 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 (Term
m, Term
_) <- 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 String
"run__IO"))
[forall {t}. t -> PArg' t
pexp forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN String
"main") [String
"Main"])])
forall (m :: * -> *) a. Monad m => a -> m a
return Term
m
where fc :: FC
fc = String -> FC
fileFC String
"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 DataOpts
opt PData' t
decl Docstring (Either Err t)
docs [(Name, Docstring (Either Err t))]
argdocs =
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 String
"builtin")
DataOpts
opt PData' t
decl
LanguageExt -> Idris ()
addLangExt LanguageExt
LinearTypes
ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo FC
primfc) (forall {t}.
DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec forall a. [a]
inferOpts PData' PTerm
inferDecl forall a. Docstring a
emptyDocstring [])
LanguageExt -> Idris ()
dropLangExt LanguageExt
LinearTypes
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState 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) (forall {t}.
DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec forall a. [a]
eqOpts PData' PTerm
eqDecl forall {t} {b}. Docstring (Either (Err' t) b)
eqDoc forall {t} {b}. [(Name, Docstring (Either (Err' t) b))]
eqParamDoc)
Name -> Name -> Idris ()
addNameHint Name
eqTy (String -> Name
sUN String
"prf")
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 Name
n Term
ty Int
i [Const] -> Maybe Const
def (Int, PrimFn)
sc 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) forall a. a -> [a] -> [a]
: IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i }
primfc :: FC
primfc = String -> FC
fileFC String
"primitive"
valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim [Const] -> Maybe Const
prim [Value]
vals = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Const -> Value
VConstant (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Value -> Maybe Const
getConst [Value]
vals forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Const] -> Maybe Const
prim)
getConst :: Value -> Maybe Const
getConst (VConstant Const
c) = forall a. a -> Maybe a
Just Const
c
getConst Value
_ = forall a. Maybe a
Nothing
p_believeMe :: [a] -> Maybe a
p_believeMe [a
_,a
_,a
x] = forall a. a -> Maybe a
Just a
x
p_believeMe [a]
_ = forall a. Maybe a
Nothing
believeTy :: Term
believeTy = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"a") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
1))))
(forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"b") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
1))))
(forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"x") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. Int -> TT n
V Int
1) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
1)))) (forall n. Int -> TT n
V Int
1)))
elabBelieveMe :: Idris ()
elabBelieveMe
= do let prim__believe_me :: Name
prim__believe_me = String -> Name
sUN String
"prim__believe_me"
(Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
prim__believe_me Term
believeTy Int
3 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, (Int
3, PrimFn
LNoOp)) forall a. a -> [a] -> [a]
: IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i
}
p_synEq :: [Value] -> Maybe Value
p_synEq [Value
t,Value
_,Value
x,Value
y]
| Value
x forall a. Eq a => a -> a -> Bool
== Value
y = 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 = forall a. a -> Maybe a
Just (Value -> Value -> Value
VApp Value
vnNothing Value
VErased)
p_synEq [Value]
args = forall a. Maybe a
Nothing
nMaybe :: Term
nMaybe = forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> NameType
TCon Int
0 Int
2) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Maybe") [String
"Maybe", String
"Prelude"]) forall n. TT n
Erased
vnJust :: Value
vnJust = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon Int
1 Int
2 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Just") [String
"Maybe", String
"Prelude"]) Value
VErased
vnNothing :: Value
vnNothing = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
1 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nothing") [String
"Maybe", String
"Prelude"]) Value
VErased
vnRefl :: Value
vnRefl = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
2 Bool
False) Name
eqCon Value
VErased
synEqTy :: Term
synEqTy = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"a") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
3))) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
(forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"b") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
3))) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
(forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"x") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. Int -> TT n
V Int
1) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
(forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"y") (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW forall a. Maybe a
Nothing (forall n. Int -> TT n
V Int
1) (forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
(forall n. TT n -> [TT n] -> TT n
mkApp Term
nMaybe [forall n. TT n -> [TT n] -> TT n
mkApp (forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> NameType
TCon Int
0 Int
4) Name
eqTy forall n. TT n
Erased)
[forall n. Int -> TT n
V Int
3, forall n. Int -> TT n
V Int
2, forall n. Int -> TT n
V Int
1, forall n. Int -> TT n
V Int
0]]))))
elabSynEq :: Idris ()
elabSynEq
= do let synEq :: Name
synEq = String -> Name
sUN String
"prim__syntactic_eq"
(Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
synEq Term
synEqTy Int
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, (Int
4, PrimFn
LNoOp)) forall a. a -> [a] -> [a]
: IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i
}
elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecls ElabInfo
info [PDecl]
ds = do 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 ElabWhat
what ElabInfo
info PDecl
d
= let info' :: ElabInfo
info' = ElabInfo
info { rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl = ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' } in
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (forall a. Idris a -> Idris a
withErrorReflection 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' ElabWhat
_ ElabInfo
info (PFix FC
_ Fixity
_ [String]
_)
= forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
_ ElabInfo
info (PSyntax FC
_ Syntax
p)
= forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
what ElabInfo
info (PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
s FC
f FnOpts
o Name
n FC
nfc PTerm
ty)
| ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating type decl " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ 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
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
what ElabInfo
info (PPostulate Bool
b Docstring (Either Err PTerm)
doc SyntaxInfo
s FC
f FC
nfc FnOpts
o Name
n PTerm
ty)
| ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating postulate " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ 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' ElabWhat
what ElabInfo
info (PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
s FC
f DataOpts
co PData' PTerm
d)
| ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating [type of] " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 (forall t. Name -> FC -> t -> PData' t
PLaterdecl (forall t. PData' t -> Name
d_name PData' PTerm
d) (forall t. PData' t -> FC
d_name_fc PData' PTerm
d) (forall t. PData' t -> t
d_tcon PData' PTerm
d))
elabDecl' ElabWhat
what ElabInfo
info d :: PDecl
d@(PClauses FC
f FnOpts
o Name
n [PClause' PTerm]
ps)
| ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating clause " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
IState
i <- Idris IState
getIState
let o' :: FnOpts
o' = case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt FnOpts
idris_flags IState
i) of
[FnOpts
fs] -> FnOpts
fs
[] -> []
ElabInfo -> FC -> FnOpts -> Name -> [PClause' PTerm] -> Idris ()
elabClauses ElabInfo
info FC
f (FnOpts
o forall a. [a] -> [a] -> [a]
++ FnOpts
o') Name
n [PClause' PTerm]
ps
elabDecl' ElabWhat
what ElabInfo
info (PMutual FC
f [PDecl]
ps)
= do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
let ([Name]
ufnames, [[Name]]
umethss) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (IState -> PDecl -> Maybe (Name, [Name])
findTCImpl IState
i) [PDecl]
ps)
case [PDecl]
ps of
[PDecl
p] -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
what ElabInfo
info PDecl
p
[PDecl]
_ -> do 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
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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
declared (forall {t}. [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl]
ps)
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 Int
1 forall a b. (a -> b) -> a -> b
$ String
"Rechecking for positivity " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Name]
datans
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
x -> do Name -> Totality -> Idris ()
setTotality Name
x Totality
Unchecked) [Name]
datans
IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Simplifying " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
Context
ctxt' <- do Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
forall a. TC a -> Idris a
tclift 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')
(forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (IState -> [(FC, Name)]
idris_totcheck IState
i))
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)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris Totality
checkDeclTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
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 Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ DataOpts
_ PData' t
_) = Bool
True
isDataDecl PDecl' t
_ = Bool
False
findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])
findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])
findTCImpl IState
ist (PImplementation Docstring (Either Err PTerm)
_ [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
_ FC
_ [(Name, PTerm)]
_ [Name]
_ Accessibility
_ FnOpts
_ Name
n_in FC
_ [PTerm]
ps [(Name, PTerm)]
_ PTerm
_ Maybe Name
expn [PDecl]
_)
= let (Name
n, [Name]
meths)
= case forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n_in (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
[(Name
n', InterfaceInfo
ci)] -> (Name
n', forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))
[(Name, InterfaceInfo)]
_ -> (Name
n_in, [])
iname :: Name
iname = forall {a}. Show a => Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n (ElabInfo -> [String]
namespace ElabInfo
info) [PTerm]
ps Maybe Name
expn in
forall a. a -> Maybe a
Just (Name
iname, [Name]
meths)
findTCImpl IState
ist PDecl
_ = forall a. Maybe a
Nothing
mkiname :: Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n' [String]
ns [a]
ps' Maybe Name
expn' =
case Maybe Name
expn' of
Maybe Name
Nothing -> case [String]
ns of
[] -> SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [a]
ps'))
[String]
m -> Name -> [String] -> Name
sNS (SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [a]
ps'))) [String]
m
Just Name
nm -> Name
nm
getDataDecls :: [PDecl' t] -> [PDecl' t]
getDataDecls (PNamespace String
_ FC
_ [PDecl' t]
ds : [PDecl' t]
decls)
= [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
ds forall a. [a] -> [a] -> [a]
++ [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
getDataDecls (PDecl' t
d : [PDecl' t]
decls)
| forall {t}. PDecl' t -> Bool
isDataDecl PDecl' t
d = PDecl' t
d 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 [Name]
ns Name
n
= do IState
i <- Idris IState
getIState
case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
[TypeInfo
x] -> do let x' :: TypeInfo
x' = TypeInfo
x { mutual_types :: [Name]
mutual_types = [Name]
ns }
IState -> Idris ()
putIState forall a b. (a -> b) -> a -> b
$ IState
i { idris_datatypes :: Ctxt TypeInfo
idris_datatypes
= forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n TypeInfo
x' (IState -> Ctxt TypeInfo
idris_datatypes IState
i) }
[TypeInfo]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
what ElabInfo
info (PParams FC
f [(Name, PTerm)]
ns [PDecl]
ps)
= do IState
i <- Idris IState
getIState
Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Expanding params block with " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Name, PTerm)]
ns forall a. [a] -> [a] -> [a]
++ String
" decls " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show (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
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 IState
i = forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl
-> PDecl
expandParamsD Bool
False IState
i forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [(Name, PTerm)]
ns
(forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
tldeclared [PDecl]
ps)) [PDecl]
ps
elabDecl' ElabWhat
what ElabInfo
info (POpenInterfaces FC
f [Name]
ns [PDecl]
ds)
= do [Name]
open <- [Name] -> Idris [Name]
addOpenImpl [Name]
ns
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' ElabWhat
what ElabInfo
info (PNamespace String
n FC
nfc [PDecl]
ps) =
do 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 = forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
newNS)
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
nfc, [Text] -> Maybe String -> OutputAnnotation
AnnNamespace [Text]
ns forall a. Maybe a
Nothing)]
where
newNS :: [String]
newNS = String
n forall a. a -> [a] -> [a]
: ElabInfo -> [String]
namespace ElabInfo
info
ninfo :: ElabInfo
ninfo = ElabInfo
info { namespace :: [String]
namespace = [String]
newNS }
elabDecl' ElabWhat
what ElabInfo
info (PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
s 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)
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating interface " forall a. [a] -> [a] -> [a]
++ 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' ElabWhat
what ElabInfo
info (PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
s 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)
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating implementation " forall a. [a] -> [a] -> [a]
++ 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' ElabWhat
what ElabInfo
info (PRecord 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)
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating record " forall a. [a] -> [a] -> [a]
++ 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' ElabWhat
_ ElabInfo
info (PDSL Name
n DSL' PTerm
dsl)
= do IState
i <- Idris IState
getIState
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
DSLNotation 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 String
"You must turn on the DSLNotation extension to use a dsl block"
IState -> Idris ()
putIState (IState
i { idris_dsls :: Ctxt (DSL' PTerm)
idris_dsls = 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' ElabWhat
what ElabInfo
info (PDirective i :: Directive
i@(DLogging Integer
_))
= Directive -> Idris ()
directiveAction Directive
i
elabDecl' ElabWhat
what ElabInfo
info (PDirective Directive
i)
| ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns = Directive -> Idris ()
directiveAction Directive
i
elabDecl' ElabWhat
what ElabInfo
info (PProvider Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc FC
nfc ProvideWhat' PTerm
provWhat Name
n)
| ElabWhat
what forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
= do Int -> String -> Idris ()
logElab Int
1 forall a b. (a -> b) -> a -> b
$ String
"Elaborating type provider " forall a. [a] -> [a] -> [a]
++ 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' ElabWhat
what ElabInfo
info (PTransform FC
fc Bool
safety PTerm
old PTerm
new)
= do ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
elabTransform ElabInfo
info FC
fc Bool
safety PTerm
old PTerm
new
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
what ElabInfo
info (PRunElabDecl FC
fc PTerm
script [String]
ns)
= do IState
i <- Idris IState
getIState
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
ElabReflection 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. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Err' t
Msg String
"You must turn on the ElabReflection extension to use %runElab")
ElabInfo -> FC -> PTerm -> [String] -> Idris ()
elabRunElab ElabInfo
info FC
fc PTerm
script [String]
ns
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
_ ElabInfo
_ PDecl
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()