{-# LANGUAGE CPP, PatternGuards #-}
module Idris.Elab.Data(elabData) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Delaborate
import Idris.Docstrings
import Idris.Elab.Rewrite
import Idris.Elab.Type
import Idris.Elab.Utils
import Idris.Elab.Value
import Idris.Error
import Idris.Output (iWarn, sendHighlighting)
import Util.Pretty
#if (MIN_VERSION_base(4,11,0))
import Prelude hiding (id, (.), (<>))
#else
import Prelude hiding (id, (.))
#endif
import Control.Category
import Control.Monad
import Data.List
import qualified Data.Set as S
warnLC :: FC -> Name -> Idris ()
warnLC :: FC -> Name -> Idris ()
warnLC FC
fc Name
n
= FC -> OutputDoc -> Idris ()
iWarn FC
fc forall a b. (a -> b) -> a -> b
$ Name -> OutputDoc
annName Name
n forall a. Doc a -> Doc a -> Doc a
<+> forall a. String -> Doc a
text String
"has a name which may be implicitly bound."
forall a. Doc a -> Doc a -> Doc a
<> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text String
"This is likely to lead to problems!"
elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()
elabData :: ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData
-> Idris ()
elabData ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
fc DataOpts
opts (PLaterdecl Name
n FC
nfc PTerm
t_in)
= do Int -> String -> Idris ()
logElab Int
1 (forall a. Show a => a -> String
show (FC
fc, Docstring (Either Err PTerm)
doc))
FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
(Type
cty, Type
_, PTerm
t, [(Int, Name)]
inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Type, Type, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc [] Name
n PTerm
t_in
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
(Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> NameType
TCon Int
0 Int
0) Type
cty)
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, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)]
elabData ElabInfo
info SyntaxInfo
syn Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
fc DataOpts
opts (PDatadecl Name
n FC
nfc PTerm
t_in [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
dcons)
= do let codata :: Bool
codata = DataOpt
Codata forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataOpts
opts
Int -> String -> Idris ()
logElab Int
1 (forall a. Show a => a -> String
show FC
fc)
Bool
undef <- FC -> Name -> Idris Bool
isUndefined FC
fc Name
n
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
(Type
cty, Type
ckind, PTerm
t, [(Int, Name)]
inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Type, Type, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc [] Name
n PTerm
t_in
IState
i <- Idris IState
getIState
FC -> Name -> Type -> IState -> Idris ()
checkDefinedAs FC
fc Name
n Type
cty IState
i
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
undef forall a b. (a -> b) -> a -> b
$ (Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> NameType
TCon Int
0 Int
0) Type
cty)
let cnameinfo :: ElabInfo
cnameinfo = ElabInfo -> [Name] -> ElabInfo
cinfo ElabInfo
info (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {d} {e} {f} {g}. (a, b, c, d, e, f, g) -> c
cname [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
dcons)
Bool
unique <- case forall n. TT n -> TT n
getRetTy (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
i) [] Type
cty) of
UType Universe
UniqueType -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
UType Universe
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
TType UExp
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Type
rt -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"type constructor " Name
n forall a. Maybe a
Nothing (forall t. String -> Err' t
Msg String
"Not a valid type constructor")))
[(Name, Type)]
cons <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ElabInfo
-> SyntaxInfo
-> Name
-> Bool
-> Type
-> Type
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> Idris (Name, Type)
elabCon ElabInfo
cnameinfo SyntaxInfo
syn Name
n Bool
codata (forall n. TT n -> TT n
getRetTy Type
cty) Type
ckind) [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
dcons
Int
ttag <- Idris Int
getName
Context
ctxt <- Idris Context
getContext
let params :: [Int]
params = Name -> Type -> [Type] -> [Int]
findParams Name
n (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cty) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, Type)]
cons)
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"Parameters : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Int]
params
FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints FC
fc [Int]
params Type
cty [(Name, Type)]
cons
IState
i <- Idris IState
getIState
IState -> Idris ()
putIState (IState
i { idris_datatypes :: Ctxt TypeInfo
idris_datatypes =
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n ([Name] -> Bool -> DataOpts -> [Int] -> [Name] -> Bool -> TypeInfo
TI (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Type)]
cons) Bool
codata DataOpts
opts [Int]
params [Name
n]
(forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
linearArg (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Name, Type)]
cons)))
(IState -> Ctxt TypeInfo
idris_datatypes IState
i) })
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCData Name
n)
forall a. FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs FC
fc [(Name, Docstring (Either Err PTerm))]
argDocs PTerm
t
Docstring DocTerm
doc' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
doc
[(Name, Docstring DocTerm)]
argDocs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Name
n, Docstring (Either Err PTerm)
d) -> do Docstring DocTerm
d' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
d
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Docstring DocTerm
d')) [(Name, Docstring (Either Err PTerm))]
argDocs
Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n Docstring DocTerm
doc' [(Name, Docstring DocTerm)]
argDocs'
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDoc Name
n)
let metainf :: MetaInformation
metainf = [Int] -> MetaInformation
DataMI [Int]
params
IBCWrite -> Idris ()
addIBC (Name -> MetaInformation -> IBCWrite
IBCMetaInformation Name
n MetaInformation
metainf)
(Context -> Context) -> Idris ()
updateContext (Datatype Name -> Context -> Context
addDatatype (forall n. n -> Int -> TT n -> Bool -> [(n, TT n)] -> Datatype n
Data Name
n Int
ttag Type
cty Bool
unique [(Name, Type)]
cons))
(Context -> Context) -> Idris ()
updateContext (Name -> MetaInformation -> Context -> Context
setMetaInformation Name
n MetaInformation
metainf)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
totcheck (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. a -> [a]
repeat FC
fc) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Type)]
cons))
case [(Name, Type)]
cons of
[(Name
cn,Type
ct)] -> Name -> Idris ()
setDetaggable Name
cn forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Name -> Idris ()
setDetaggable Name
n
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
cn) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
[(Name, Type)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
n forall a. Eq a => a -> a -> Bool
/= String -> Name
sUN String
"=") forall a b. (a -> b) -> a -> b
$
ElabInfo -> Name -> Type -> Idris ()
elabRewriteLemma ElabInfo
info Name
n Type
cty
Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ [(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing)] forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (\(Docstring (Either Err PTerm)
_, [(Name, Docstring (Either Err PTerm))]
_, Name
n, FC
nfc, PTerm
_, FC
_, [Name]
_) ->
(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n forall a. Maybe a
Nothing forall a. Maybe a
Nothing forall a. Maybe a
Nothing))
[(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
dcons
where
checkDefinedAs :: FC -> Name -> Type -> IState -> Idris ()
checkDefinedAs FC
fc Name
n Type
t IState
i
= let defined :: Idris a
defined = forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. Name -> Err' t
AlreadyDefined Name
n))
ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
i in
case Name -> Context -> [Def]
lookupDef Name
n Context
ctxt of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[TyDecl NameType
_ Type
ty] ->
case Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt [] Type
t Type
ty of
OK () -> case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
Maybe TypeInfo
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Maybe TypeInfo
_ -> forall {a}. Idris a
defined
TC ()
_ -> forall {a}. Idris a
defined
[Def]
_ -> forall {a}. Idris a
defined
cname :: (a, b, c, d, e, f, g) -> c
cname (a
_, b
_, c
n, d
_, e
_, f
_, g
_) = c
n
cinfo :: ElabInfo -> [Name] -> ElabInfo
cinfo :: ElabInfo -> [Name] -> ElabInfo
cinfo ElabInfo
info [Name]
ds
= let newps :: [(Name, PTerm)]
newps = ElabInfo -> [(Name, PTerm)]
params ElabInfo
info
dsParams :: [(Name, [a])]
dsParams = forall a b. (a -> b) -> [a] -> [b]
map (\Name
n -> (Name
n, [])) [Name]
ds
newb :: Ctxt [Name]
newb = forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist forall {a}. [(Name, [a])]
dsParams (ElabInfo -> Ctxt [Name]
inblock ElabInfo
info) in
ElabInfo
info { params :: [(Name, PTerm)]
params = [(Name, PTerm)]
newps,
inblock :: Ctxt [Name]
inblock = Ctxt [Name]
newb,
liftname :: Name -> Name
liftname = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
}
elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->
Type ->
Type ->
(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) ->
Idris (Name, Type)
elabCon :: ElabInfo
-> SyntaxInfo
-> Name
-> Bool
-> Type
-> Type
-> (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> Idris (Name, Type)
elabCon ElabInfo
info SyntaxInfo
syn Name
tn Bool
codata Type
expkind Type
dkind (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Name
n, FC
nfc, PTerm
t_in, FC
fc, [Name]
forcenames)
= do FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
":Constructor " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
t_in
(Type
cty, Type
ckind, PTerm
t, [(Int, Name)]
inacc) <- ElabInfo
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris (Type, Type, PTerm, [(Int, Name)])
buildType ElabInfo
info SyntaxInfo
syn FC
fc [FnOpt
Constructor] Name
n (if Bool
codata then PTerm -> PTerm
mkLazy PTerm
t_in else PTerm
t_in)
Context
ctxt <- Idris Context
getContext
let cty' :: Type
cty' = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
cty
forall {n} {n}. TT n -> TT n -> Idris ()
checkUniqueKind Type
ckind Type
expkind
Name -> Type -> Idris ()
tyIs Name
n Type
cty'
let force :: [Int]
force = if Name
tn forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"Delayed"
then []
else Context -> Name -> Type -> [Int]
forceArgs Context
ctxt Name
tn Type
cty
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FC
fc forall a. [a] -> [a] -> [a]
++ String
":Constructor " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" elaborated : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show PTerm
t
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Inaccessible args: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Int, Name)]
inacc
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Forceable args: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Int]
force
Int -> String -> Idris ()
logElab Int
2 forall a b. (a -> b) -> a -> b
$ String
"---> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Type
cty
(Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> Bool -> NameType
DCon Int
0 Int
0 Bool
False) Type
cty)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
forall a. FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs FC
fc [(Name, Docstring (Either Err PTerm))]
argDocs PTerm
t
Docstring DocTerm
doc' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
doc
[(Name, Docstring DocTerm)]
argDocs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Name
n, Docstring (Either Err PTerm)
d) -> do Docstring DocTerm
d' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms ElabInfo
info Docstring (Either Err PTerm)
d
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Docstring DocTerm
d')) [(Name, Docstring (Either Err PTerm))]
argDocs
Name
-> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()
addDocStr Name
n Docstring DocTerm
doc' [(Name, Docstring DocTerm)]
argDocs'
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDoc Name
n)
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [(Int, Name)]
opt_inaccessible forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n) [(Int, Name)]
inacc
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [Int]
opt_forceable forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n) [Int]
force
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Type
cty)
where
tyIs :: Name -> Type -> Idris ()
tyIs Name
con (Bind Name
n Binder Type
b Type
sc) = Name -> Type -> Idris ()
tyIs Name
con (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) Type
sc)
tyIs Name
con Type
t | (P NameType
Bound Name
n' Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
t
= if Name
n' forall a. Eq a => a -> a -> Bool
/= Name
tn then
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"constructor " Name
con forall a. Maybe a
Nothing
(forall t. String -> Err' t
Msg (String
"Type level variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n' forall a. [a] -> [a] -> [a]
++ String
" is not " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
tn))))
else forall (m :: * -> *) a. Monad m => a -> m a
return ()
tyIs Name
con Type
t | (P NameType
_ Name
n' Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
t
= if Name
n' forall a. Eq a => a -> a -> Bool
/= Name
tn then forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"constructor " Name
con forall a. Maybe a
Nothing (forall t. String -> Err' t
Msg (forall a. Show a => a -> String
show Name
n' forall a. [a] -> [a] -> [a]
++ String
" is not " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
tn))))
else forall (m :: * -> *) a. Monad m => a -> m a
return ()
tyIs Name
con Type
t = forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
"constructor " Name
con forall a. Maybe a
Nothing (forall t. String -> Err' t
Msg (forall a. Show a => a -> String
show Type
t forall a. [a] -> [a] -> [a]
++ String
" is not " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
tn))))
mkLazy :: PTerm -> PTerm
mkLazy (PPi Plicity
pl Name
n FC
nfc PTerm
ty PTerm
sc)
= let ty' :: PTerm
ty' = if PTerm -> Bool
getTyName PTerm
ty
then FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"Delayed"))
[forall {t}. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"Infinite")),
forall {t}. t -> PArg' t
pexp PTerm
ty]
else PTerm
ty in
Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
pl Name
n FC
nfc PTerm
ty' (PTerm -> PTerm
mkLazy PTerm
sc)
mkLazy PTerm
t = PTerm
t
getTyName :: PTerm -> Bool
getTyName (PApp FC
_ (PRef FC
_ [FC]
_ Name
n) [PArg]
_) = Name
n forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
tn
getTyName (PRef FC
_ [FC]
_ Name
n) = Name
n forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
tn
getTyName PTerm
_ = Bool
False
checkUniqueKind :: TT n -> TT n -> Idris ()
checkUniqueKind (UType Universe
NullType) (UType Universe
NullType) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType Universe
NullType) TT n
_
= forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. Universe -> Name -> Err' t
UniqueKindError Universe
NullType Name
n))
checkUniqueKind (UType Universe
UniqueType) (UType Universe
UniqueType) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType Universe
UniqueType) (UType Universe
AllTypes) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType Universe
UniqueType) TT n
_
= forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. Universe -> Name -> Err' t
UniqueKindError Universe
UniqueType Name
n))
checkUniqueKind (UType Universe
AllTypes) (UType Universe
AllTypes) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType Universe
AllTypes) (UType Universe
UniqueType) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType Universe
AllTypes) TT n
_
= forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. Universe -> Name -> Err' t
UniqueKindError Universe
AllTypes Name
n))
checkUniqueKind TT n
_ TT n
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
forceArgs :: Context -> Name -> Type -> [Int]
forceArgs :: Context -> Name -> Type -> [Int]
forceArgs Context
ctxt Name
tn Type
ty = Int -> Type -> [Int]
forceFrom Int
0 Type
ty
where
forceFrom :: Int -> Type -> [Int]
forceFrom :: Int -> Type -> [Int]
forceFrom Int
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc)
= Int -> Type -> [Int]
forceFrom (Int
i forall a. Num a => a -> a -> a
+ Int
1) (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Int -> String -> Name
sMN Int
i String
"FF") forall n. TT n
Erased) Type
sc)
forceFrom Int
i Type
sc
| (P NameType
_ Name
ty Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
sc,
Name
ty forall a. Eq a => a -> a -> Bool
== Name
tn
= if forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> Type -> [Int]
findNonForcePos Bool
True) [Type]
args)
then forall a. Eq a => [a] -> [a]
nub (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Int]
findForcePos [Type]
args)
else []
forceFrom Int
i Type
sc = []
findForcePos :: Type -> [Int]
findForcePos (P NameType
_ (MN Int
i Text
ff) Type
_)
| Text
ff forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"FF" = [Int
i]
findForcePos ap :: Type
ap@(App AppStatus Name
_ Type
f Type
a)
| (P NameType
_ Name
con Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Name -> Context -> Bool
isDConName Name
con Context
ctxt
= forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Int]
findForcePos [Type]
args
findForcePos Type
_ = []
findNonForcePos :: Bool -> Type -> [Int]
findNonForcePos Bool
fok (P NameType
_ (MN Int
i Text
ff) Type
_)
| Text
ff forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"FF" = if Bool
fok then [] else [Int
i]
findNonForcePos Bool
fok ap :: Type
ap@(App AppStatus Name
_ Type
f Type
a)
| (P NameType
_ Name
con Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
ap
= forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> Type -> [Int]
findNonForcePos (Bool
fok Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
con Context
ctxt)) [Type]
args
findNonForcePos Bool
_ Type
_ = []
addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints FC
fc [Int]
ps Type
cty [(Name, Type)]
cons
= case forall n. TT n -> TT n
getRetTy Type
cty of
TType UExp
cvar -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall {t :: * -> *} {n} {p}.
(Foldable t, Eq n) =>
p -> UExp -> (TT n, t n) -> Idris ()
addConConstraint [Int]
ps UExp
cvar)
(forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (a, TT a) -> (TT a, [a])
getParamNames [(Name, Type)]
cons)
Type
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
getParamNames :: (a, TT a) -> (TT a, [a])
getParamNames (a
n, TT a
ty) = (TT a
ty, forall {a}. TT a -> [a]
getPs TT a
ty)
getPs :: TT a -> [a]
getPs (Bind a
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT a
_ TT a
_) TT a
sc)
= TT a -> [a]
getPs (forall n. TT n -> TT n -> TT n
substV (forall n. NameType -> n -> TT n -> TT n
P NameType
Ref a
n forall n. TT n
Erased) TT a
sc)
getPs TT a
t | (TT a
f, [TT a]
args) <- forall n. TT n -> (TT n, [TT n])
unApply TT a
t
= forall {a}. Int -> [TT a] -> [a]
paramArgs Int
0 [TT a]
args
paramArgs :: Int -> [TT a] -> [a]
paramArgs Int
i (P NameType
_ a
n TT a
_ : [TT a]
args) | Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = a
n forall a. a -> [a] -> [a]
: Int -> [TT a] -> [a]
paramArgs (Int
i forall a. Num a => a -> a -> a
+ Int
1) [TT a]
args
paramArgs Int
i (TT a
_ : [TT a]
args) = Int -> [TT a] -> [a]
paramArgs (Int
i forall a. Num a => a -> a -> a
+ Int
1) [TT a]
args
paramArgs Int
i [] = []
addConConstraint :: p -> UExp -> (TT n, t n) -> Idris ()
addConConstraint p
ps UExp
cvar (TT n
ty, t n
pnames) = TT n -> Idris ()
constraintTy TT n
ty
where
constraintTy :: TT n -> Idris ()
constraintTy (Bind n
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT n
ty TT n
_) TT n
sc)
= case forall n. TT n -> TT n
getRetTy TT n
ty of
TType UExp
avar -> do Bool
tit <- Idris Bool
typeInType
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
tit) forall a b. (a -> b) -> a -> b
$ do
Context
ctxt <- Idris Context
getContext
let tv :: Int
tv = Context -> Int
next_tvar Context
ctxt
let con :: UConstraint
con = if n
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t n
pnames
then UExp -> UExp -> UConstraint
ULE UExp
avar UExp
cvar
else UExp -> UExp -> UConstraint
ULT UExp
avar UExp
cvar
FC -> (Int, [UConstraint]) -> Idris ()
addConstraints FC
fc (Int
tv, [UConstraint
con])
IBCWrite -> Idris ()
addIBC (FC -> UConstraint -> IBCWrite
IBCConstraint FC
fc UConstraint
con)
TT n
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
constraintTy TT n
t = forall (m :: * -> *) a. Monad m => a -> m a
return ()