{-# 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 Control.Monad.State.Strict as State
import Data.Char (isLetter, toLower)
import Data.List
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T
warnLC :: FC -> Name -> Idris ()
warnLC :: FC -> Name -> Idris ()
warnLC fc :: FC
fc n :: Name
n
= FC -> OutputDoc -> Idris ()
iWarn FC
fc (OutputDoc -> Idris ()) -> OutputDoc -> Idris ()
forall a b. (a -> b) -> a -> b
$ Name -> OutputDoc
annName Name
n OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<+> String -> OutputDoc
forall a. String -> Doc a
text "has a name which may be implicitly bound."
OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> OutputDoc
forall a. Doc a
line OutputDoc -> OutputDoc -> OutputDoc
forall a. Doc a -> Doc a -> Doc a
<> String -> OutputDoc
forall a. String -> Doc a
text "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 info :: ElabInfo
info syn :: SyntaxInfo
syn doc :: Docstring (Either Err PTerm)
doc argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs fc :: FC
fc opts :: DataOpts
opts (PLaterdecl n :: Name
n nfc :: FC
nfc t_in :: PTerm
t_in)
= do Int -> String -> Idris ()
logElab 1 ((FC, Docstring (Either Err PTerm)) -> String
forall a. Show a => a -> String
show (FC
fc, Docstring (Either Err PTerm)
doc))
FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
(cty :: Type
cty, _, t :: PTerm
t, inacc :: [(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 0 0) Type
cty)
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, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)]
elabData info :: ElabInfo
info syn :: SyntaxInfo
syn doc :: Docstring (Either Err PTerm)
doc argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs fc :: FC
fc opts :: DataOpts
opts (PDatadecl n :: Name
n nfc :: FC
nfc t_in :: PTerm
t_in dcons :: [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
dcons)
= do let codata :: Bool
codata = DataOpt
Codata DataOpt -> DataOpts -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` DataOpts
opts
Int -> String -> Idris ()
logElab 1 (FC -> String
forall a. Show a => a -> String
show FC
fc)
Bool
undef <- FC -> Name -> Idris Bool
isUndefined FC
fc Name
n
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
(cty :: Type
cty, ckind :: Type
ckind, t :: PTerm
t, inacc :: [(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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
undef (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ (Context -> Context) -> Idris ()
updateContext (Name -> NameType -> Type -> Context -> Context
addTyDecl Name
n (Int -> Int -> NameType
TCon 0 0) Type
cty)
let cnameinfo :: ElabInfo
cnameinfo = ElabInfo -> [Name] -> ElabInfo
cinfo ElabInfo
info (((Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> Name)
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> Name
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 Type -> Type
forall n. TT n -> TT n
getRetTy (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
i) [] Type
cty) of
UType UniqueType -> Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
UType _ -> Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
TType _ -> Bool -> Idris Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
rt :: Type
rt -> TC Bool -> Idris Bool
forall a. TC a -> Idris a
tclift (TC Bool -> Idris Bool) -> TC Bool -> Idris Bool
forall a b. (a -> b) -> a -> b
$ Err -> TC Bool
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "type constructor " Name
n Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
Msg "Not a valid type constructor")))
[(Name, Type)]
cons <- ((Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> StateT IState (ExceptT Err IO) (Name, Type))
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> StateT IState (ExceptT Err IO) [(Name, Type)]
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])
-> StateT IState (ExceptT Err IO) (Name, Type)
elabCon ElabInfo
cnameinfo SyntaxInfo
syn Name
n Bool
codata (Type -> Type
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) (((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
forall a b. (a, b) -> b
snd [(Name, Type)]
cons)
Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Parameters : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
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 =
Name -> TypeInfo -> Ctxt TypeInfo -> Ctxt TypeInfo
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n ([Name] -> Bool -> DataOpts -> [Int] -> [Name] -> Bool -> TypeInfo
TI (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
cons) Bool
codata DataOpts
opts [Int]
params [Name
n]
((Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
linearArg (((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
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)
FC -> [(Name, Docstring (Either Err PTerm))] -> PTerm -> Idris ()
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' <- ((Name, Docstring (Either Err PTerm))
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm))
-> [(Name, Docstring (Either Err PTerm))]
-> StateT IState (ExceptT Err IO) [(Name, Docstring DocTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(n :: Name
n, d :: 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
(Name, Docstring DocTerm)
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm)
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 (Name -> Int -> Type -> Bool -> [(Name, Type)] -> Datatype Name
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)
((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 ()
totcheck ([FC] -> [Name] -> [(FC, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip (FC -> [FC]
forall a. a -> [a]
repeat FC
fc) (((Name, Type) -> Name) -> [(Name, Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Type)]
cons))
case [(Name, Type)]
cons of
[(cn :: Name
cn,ct :: Type
ct)] -> Name -> Idris ()
setDetaggable Name
cn Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Name -> Idris ()
setDetaggable Name
n
Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
cn) Idris () -> Idris () -> Idris ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCOpt Name
n)
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Name
sUN "=") (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
ElabInfo -> Name -> Type -> Idris ()
elabRewriteLemma ElabInfo
info Name
n Type
cty
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', OutputAnnotation)] -> Set (FC', OutputAnnotation))
-> [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a b. (a -> b) -> a -> b
$ [(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing)] [(FC', OutputAnnotation)]
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
forall a. [a] -> [a] -> [a]
++
((Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])
-> (FC', OutputAnnotation))
-> [(Docstring (Either Err PTerm),
[(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC,
[Name])]
-> [(FC', OutputAnnotation)]
forall a b. (a -> b) -> [a] -> [b]
map (\(_, _, n :: Name
n, nfc :: FC
nfc, _, _, _) ->
(FC -> FC'
FC' FC
nfc, Name
-> Maybe NameOutput
-> Maybe String
-> Maybe String
-> OutputAnnotation
AnnName Name
n Maybe NameOutput
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing Maybe String
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
fc n :: Name
n t :: Type
t i :: IState
i
= let defined :: Idris a
defined = TC a -> Idris a
forall a. TC a -> Idris a
tclift (TC a -> Idris a) -> TC a -> Idris a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Err
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
[] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[TyDecl _ ty :: Type
ty] ->
case Context -> Env -> Type -> Type -> TC ()
converts Context
ctxt [] Type
t Type
ty of
OK () -> case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
_ -> Idris ()
forall a. Idris a
defined
_ -> Idris ()
forall a. Idris a
defined
_ -> Idris ()
forall a. Idris a
defined
cname :: (a, b, c, d, e, f, g) -> c
cname (_, _, n :: c
n, _, _, _, _) = c
n
cinfo :: ElabInfo -> [Name] -> ElabInfo
cinfo :: ElabInfo -> [Name] -> ElabInfo
cinfo info :: ElabInfo
info ds :: [Name]
ds
= let newps :: [(Name, PTerm)]
newps = ElabInfo -> [(Name, PTerm)]
params ElabInfo
info
dsParams :: [(Name, [a])]
dsParams = (Name -> (Name, [a])) -> [Name] -> [(Name, [a])]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Name
n -> (Name
n, [])) [Name]
ds
newb :: Ctxt [Name]
newb = [(Name, [Name])] -> Ctxt [Name] -> Ctxt [Name]
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, [Name])]
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 = Name -> Name
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])
-> StateT IState (ExceptT Err IO) (Name, Type)
elabCon info :: ElabInfo
info syn :: SyntaxInfo
syn tn :: Name
tn codata :: Bool
codata expkind :: Type
expkind dkind :: Type
dkind (doc :: Docstring (Either Err PTerm)
doc, argDocs :: [(Name, Docstring (Either Err PTerm))]
argDocs, n :: Name
n, nfc :: FC
nfc, t_in :: PTerm
t_in, fc :: FC
fc, forcenames :: [Name]
forcenames)
= do FC -> Name -> Idris ()
checkUndefined FC
fc Name
n
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name -> Bool
implicitable (Name -> Name
nsroot Name
n)) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Name -> Idris ()
warnLC FC
fc Name
n
Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":Constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
t_in
(cty :: Type
cty, ckind :: Type
ckind, t :: PTerm
t, inacc :: [(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
Type -> Type -> Idris ()
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "Delayed"
then []
else Context -> Name -> Type -> [Int]
forceArgs Context
ctxt Name
tn Type
cty
Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> String
forall a. Show a => a -> String
show FC
fc String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":Constructor " 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]
++ " elaborated : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
forall a. Show a => a -> String
show PTerm
t
Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Inaccessible args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Int, Name)] -> String
forall a. Show a => a -> String
show [(Int, Name)]
inacc
Int -> String -> Idris ()
logElab 5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Forceable args: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
forall a. Show a => a -> String
show [Int]
force
Int -> String -> Idris ()
logElab 2 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ "---> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
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 0 0 Bool
False) Type
cty)
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
FC -> [(Name, Docstring (Either Err PTerm))] -> PTerm -> Idris ()
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' <- ((Name, Docstring (Either Err PTerm))
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm))
-> [(Name, Docstring (Either Err PTerm))]
-> StateT IState (ExceptT Err IO) [(Name, Docstring DocTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(n :: Name
n, d :: 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
(Name, Docstring DocTerm)
-> StateT IState (ExceptT Err IO) (Name, Docstring DocTerm)
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)
Field IState [(Int, Name)] -> [(Int, Name)] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [(Int, Name)]
opt_inaccessible Field OptInfo [(Int, Name)]
-> Field IState OptInfo -> Field IState [(Int, Name)]
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
Field IState [Int] -> [Int] -> Idris ()
forall s (m :: * -> *) a. MonadState s m => Field s a -> a -> m ()
fputState (Field OptInfo [Int]
opt_forceable Field OptInfo [Int] -> Field IState OptInfo -> Field IState [Int]
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)
(Name, Type) -> StateT IState (ExceptT Err IO) (Name, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Type
cty)
where
tyIs :: Name -> Type -> Idris ()
tyIs con :: Name
con (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = Name -> Type -> Idris ()
tyIs Name
con (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
forall n. TT n
Erased) Type
sc)
tyIs con :: Name
con t :: Type
t | (P Bound n' :: Name
n' _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t
= if Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
tn then
TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "constructor " Name
con Maybe Type
forall a. Maybe a
Nothing
(String -> Err
forall t. String -> Err' t
Msg ("Type level variable " 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]
++ " is not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tn))))
else () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
tyIs con :: Name
con t :: Type
t | (P _ n' :: Name
n' _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t
= if Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
tn then TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "constructor " Name
con Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
Msg (Name -> String
forall a. Show a => a -> String
show Name
n' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tn))))
else () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
tyIs con :: Name
con t :: Type
t = TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Name -> Maybe Type -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating "constructor " Name
con Maybe Type
forall a. Maybe a
Nothing (String -> Err
forall t. String -> Err' t
Msg (Type -> String
forall a. Show a => a -> String
show Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
tn))))
mkLazy :: PTerm -> PTerm
mkLazy (PPi pl :: Plicity
pl n :: Name
n nfc :: FC
nfc ty :: PTerm
ty sc :: 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 "Delayed"))
[PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "Infinite")),
PTerm -> PArg
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 t :: PTerm
t = PTerm
t
getTyName :: PTerm -> Bool
getTyName (PApp _ (PRef _ _ n :: Name
n) _) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
tn
getTyName (PRef _ _ n :: Name
n) = Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Name
nsroot Name
tn
getTyName _ = Bool
False
checkUniqueKind :: TT n -> TT n -> Idris ()
checkUniqueKind (UType NullType) (UType NullType) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType NullType) _
= TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
NullType Name
n))
checkUniqueKind (UType UniqueType) (UType UniqueType) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType UniqueType) (UType AllTypes) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType UniqueType) _
= TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
UniqueType Name
n))
checkUniqueKind (UType AllTypes) (UType AllTypes) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType AllTypes) (UType UniqueType) = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkUniqueKind (UType AllTypes) _
= TC () -> Idris ()
forall a. TC a -> Idris a
tclift (TC () -> Idris ()) -> TC () -> Idris ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Universe -> Name -> Err
forall t. Universe -> Name -> Err' t
UniqueKindError Universe
AllTypes Name
n))
checkUniqueKind _ _ = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
forceArgs :: Context -> Name -> Type -> [Int]
forceArgs :: Context -> Name -> Type -> [Int]
forceArgs ctxt :: Context
ctxt tn :: Name
tn ty :: Type
ty = Int -> Type -> [Int]
forceFrom 0 Type
ty
where
forceFrom :: Int -> Type -> [Int]
forceFrom :: Int -> Type -> [Int]
forceFrom i :: Int
i (Bind n :: Name
n (Pi _ _ _ _) sc :: Type
sc)
= Int -> Type -> [Int]
forceFrom (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
substV (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (Int -> String -> Name
sMN Int
i "FF") Type
forall n. TT n
Erased) Type
sc)
forceFrom i :: Int
i sc :: Type
sc
| (P _ ty :: Name
ty _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
sc,
Name
ty Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tn
= if [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ((Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> Type -> [Int]
findNonForcePos Bool
True) [Type]
args)
then [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ((Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Int]
findForcePos [Type]
args)
else []
forceFrom i :: Int
i sc :: Type
sc = []
findForcePos :: Type -> [Int]
findForcePos (P _ (MN i :: Int
i ff :: Text
ff) _)
| Text
ff Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "FF" = [Int
i]
findForcePos ap :: Type
ap@(App _ f :: Type
f a :: Type
a)
| (P _ con :: Name
con _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Name -> Context -> Bool
isDConName Name
con Context
ctxt
= [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Type -> [Int]) -> [Type] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Int]
findForcePos [Type]
args
findForcePos _ = []
findNonForcePos :: Bool -> Type -> [Int]
findNonForcePos fok :: Bool
fok (P _ (MN i :: Int
i ff :: Text
ff) _)
| Text
ff Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "FF" = if Bool
fok then [] else [Int
i]
findNonForcePos fok :: Bool
fok ap :: Type
ap@(App _ f :: Type
f a :: Type
a)
| (P _ con :: Name
con _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap
= [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Type -> [Int]) -> [Type] -> [Int]
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 _ _ = []
addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()
addParamConstraints fc :: FC
fc ps :: [Int]
ps cty :: Type
cty cons :: [(Name, Type)]
cons
= case Type -> Type
forall n. TT n -> TT n
getRetTy Type
cty of
TType cvar :: UExp
cvar -> ((Type, [Name]) -> Idris ()) -> [(Type, [Name])] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Int] -> UExp -> (Type, [Name]) -> Idris ()
forall (t :: * -> *) n p.
(Foldable t, Eq n) =>
p -> UExp -> (TT n, t n) -> Idris ()
addConConstraint [Int]
ps UExp
cvar)
(((Name, Type) -> (Type, [Name]))
-> [(Name, Type)] -> [(Type, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> (Type, [Name])
forall a a. (a, TT a) -> (TT a, [a])
getParamNames [(Name, Type)]
cons)
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
getParamNames :: (a, TT a) -> (TT a, [a])
getParamNames (n :: a
n, ty :: TT a
ty) = (TT a
ty, TT a -> [a]
forall a. TT a -> [a]
getPs TT a
ty)
getPs :: TT a -> [a]
getPs (Bind n :: a
n (Pi _ _ _ _) sc :: TT a
sc)
= TT a -> [a]
getPs (TT a -> TT a -> TT a
forall n. TT n -> TT n -> TT n
substV (NameType -> a -> TT a -> TT a
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref a
n TT a
forall n. TT n
Erased) TT a
sc)
getPs t :: TT a
t | (f :: TT a
f, args :: [TT a]
args) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
t
= Int -> [TT a] -> [a]
forall a. Int -> [TT a] -> [a]
paramArgs 0 [TT a]
args
paramArgs :: Int -> [TT a] -> [a]
paramArgs i :: Int
i (P _ n :: a
n _ : args :: [TT a]
args) | Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps = a
n a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Int -> [TT a] -> [a]
paramArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [TT a]
args
paramArgs i :: Int
i (_ : args :: [TT a]
args) = Int -> [TT a] -> [a]
paramArgs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [TT a]
args
paramArgs i :: Int
i [] = []
addConConstraint :: p -> UExp -> (TT n, t n) -> Idris ()
addConConstraint ps :: p
ps cvar :: UExp
cvar (ty :: TT n
ty, pnames :: t n
pnames) = TT n -> Idris ()
constraintTy TT n
ty
where
constraintTy :: TT n -> Idris ()
constraintTy (Bind n :: n
n (Pi _ _ ty :: TT n
ty _) sc :: TT n
sc)
= case TT n -> TT n
forall n. TT n -> TT n
getRetTy TT n
ty of
TType avar :: UExp
avar -> do Bool
tit <- Idris Bool
typeInType
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
tit) (Idris () -> Idris ()) -> Idris () -> Idris ()
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 n -> t n -> Bool
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)
_ -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
constraintTy t :: TT n
t = () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()