{-# LANGUAGE CPP, FlexibleContexts, PatternGuards #-}
module Idris.Elab.Utils where
import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.WHNF
import Idris.Delaborate
import Idris.Docstrings
import Idris.Error
import Idris.Output
import Util.Pretty
#if (MIN_VERSION_base(4,11,0))
import Prelude hiding ((<>))
#endif
import Control.Monad
import Control.Monad.State
import Data.List
import qualified Data.Map as Map
import Data.Maybe
recheckC :: String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> StateT IState (ExceptT Err IO) (Type, Type)
recheckC = Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> StateT IState (ExceptT Err IO) (Type, Type)
recheckC_borrowing Bool
False Bool
True []
recheckC_borrowing :: Bool
-> Bool
-> [Name]
-> String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> StateT IState (ExceptT Err IO) (Type, Type)
recheckC_borrowing Bool
uniq_check Bool
addConstrs [Name]
bs String
tcns FC
fc Err -> Err
mkerr Env
env Type
t
= do
Context
ctxt <- Idris Context
getContext
Raw
t' <- case Type -> Maybe Raw
safeForget Type
t of
Just Raw
ft -> forall (m :: * -> *) a. Monad m => a -> m a
return Raw
ft
Maybe Raw
Nothing -> forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ forall a. Err -> TC a
tfail forall a b. (a -> b) -> a -> b
$ Err -> Err
mkerr (forall t. FC -> Err' t -> Err' t
At FC
fc (forall t. t -> Err' t
IncompleteTerm Type
t))
(Type
tm, Type
ty, UCs
cs) <- forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ case Bool
-> [Name]
-> String
-> Context
-> Env
-> Raw
-> Type
-> TC (Type, Type, UCs)
recheck_borrowing Bool
uniq_check [Name]
bs String
tcns Context
ctxt Env
env Raw
t' Type
t of
Error Err
e -> forall a. Err -> TC a
tfail (forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err
mkerr Err
e))
OK (Type, Type, UCs)
x -> forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type, UCs)
x
Int -> String -> Idris ()
logElab Int
6 forall a b. (a -> b) -> a -> b
$ String
"CONSTRAINTS ADDED: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Type
tm, Type
ty, UCs
cs)
Bool
tit <- Idris Bool
typeInType
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
tit Bool -> Bool -> Bool
&& Bool
addConstrs) forall a b. (a -> b) -> a -> b
$
do FC -> UCs -> Idris ()
addConstraints FC
fc UCs
cs
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\UConstraint
c -> IBCWrite -> Idris ()
addIBC (FC -> UConstraint -> IBCWrite
IBCConstraint FC
fc UConstraint
c)) (forall a b. (a, b) -> b
snd UCs
cs)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> Name -> Idris ()
checkDeprecated FC
fc) (forall n. Eq n => TT n -> [n]
allTTNames Type
tm)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> Name -> Idris ()
checkDeprecated FC
fc) (forall n. Eq n => TT n -> [n]
allTTNames Type
ty)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> Name -> Idris ()
checkFragile FC
fc) (forall n. Eq n => TT n -> [n]
allTTNames Type
tm)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC -> Name -> Idris ()
checkFragile FC
fc) (forall n. Eq n => TT n -> [n]
allTTNames Type
ty)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tm, Type
ty)
checkDeprecated :: FC -> Name -> Idris ()
checkDeprecated :: FC -> Name -> Idris ()
checkDeprecated FC
fc Name
n
= do Maybe String
r <- Name -> Idris (Maybe String)
getDeprecated Name
n
case Maybe String
r of
Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just String
r -> do FC -> OutputDoc -> Idris ()
iWarn FC
fc forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
text String
"Use of deprecated name " forall a. Doc a -> Doc a -> Doc a
<> Name -> OutputDoc
annName Name
n
forall a. Doc a -> Doc a -> Doc a
<> case String
r of
String
"" -> forall a. Doc a
Util.Pretty.empty
String
_ -> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text String
r
checkFragile :: FC -> Name -> Idris ()
checkFragile :: FC -> Name -> Idris ()
checkFragile FC
fc Name
n = do
Maybe String
r <- Name -> Idris (Maybe String)
getFragile Name
n
case Maybe String
r of
Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just String
r -> do
FC -> OutputDoc -> Idris ()
iWarn FC
fc forall a b. (a -> b) -> a -> b
$ forall a. String -> Doc a
text String
"Use of a fragile construct "
forall a. Doc a -> Doc a -> Doc a
<> Name -> OutputDoc
annName Name
n
forall a. Doc a -> Doc a -> Doc a
<> case String
r of
String
"" -> forall a. Doc a
Util.Pretty.empty
String
_ -> forall a. Doc a
line forall a. Doc a -> Doc a -> Doc a
<> forall a. String -> Doc a
text String
r
iderr :: Name -> Err -> Err
iderr :: Name -> Err -> Err
iderr Name
_ Err
e = Err
e
checkDef :: ElabInfo -> FC -> (Name -> Err -> Err) -> Bool ->
[(Name, (Int, Maybe Name, Type, [Name]))] ->
Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef :: ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkDef ElabInfo
info FC
fc Name -> Err -> Err
mkerr Bool
definable [(Name, (Int, Maybe Name, Type, [Name]))]
ns
= Bool
-> Bool
-> ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkAddDef Bool
False Bool
True ElabInfo
info FC
fc Name -> Err -> Err
mkerr Bool
definable [(Name, (Int, Maybe Name, Type, [Name]))]
ns
checkAddDef :: Bool -> Bool -> ElabInfo -> FC -> (Name -> Err -> Err) -> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkAddDef :: Bool
-> Bool
-> ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkAddDef Bool
add Bool
toplvl ElabInfo
info FC
fc Name -> Err -> Err
mkerr Bool
def [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
checkAddDef Bool
add Bool
toplvl ElabInfo
info FC
fc Name -> Err -> Err
mkerr Bool
definable ((Name
n, (Int
i, Maybe Name
top, Type
t, [Name]
psns)) : [(Name, (Int, Maybe Name, Type, [Name]))]
ns)
= do Context
ctxt <- Idris Context
getContext
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"Rechecking deferred name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
n, Type
t, Bool
definable)
(Type
t', Type
_) <- String
-> FC
-> (Err -> Err)
-> Env
-> Type
-> StateT IState (ExceptT Err IO) (Type, Type)
recheckC (ElabInfo -> String
constraintNS ElabInfo
info) FC
fc (Name -> Err -> Err
mkerr Name
n) [] Type
t
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
add forall a b. (a -> b) -> a -> b
$ do [(Name, (Int, Maybe Name, Type, [Name], Bool, Bool))] -> Idris ()
addDeferred [(Name
n, (Int
i, Maybe Name
top, Type
t, [Name]
psns, Bool
toplvl, Bool
definable))]
IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
[(Name, (Int, Maybe Name, Type, [Name]))]
ns' <- Bool
-> Bool
-> ElabInfo
-> FC
-> (Name -> Err -> Err)
-> Bool
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
checkAddDef Bool
add Bool
toplvl ElabInfo
info FC
fc Name -> Err -> Err
mkerr Bool
definable [(Name, (Int, Maybe Name, Type, [Name]))]
ns
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
n, (Int
i, Maybe Name
top, Type
t', [Name]
psns)) forall a. a -> [a] -> [a]
: [(Name, (Int, Maybe Name, Type, [Name]))]
ns')
inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps Int
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
sc) (Bool
inacc : [Bool]
ins)
| Bool
inacc = (Int
i, Name
n) forall a. a -> [a] -> [a]
: Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps (Int
i forall a. Num a => a -> a -> a
+ Int
1) Type
sc [Bool]
ins
| Bool
otherwise = Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps (Int
i forall a. Num a => a -> a -> a
+ Int
1) Type
sc [Bool]
ins
inaccessibleImps Int
_ Type
_ [Bool]
_ = []
inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
inaccessibleArgs Int
i (PPi Plicity
plicity Name
n FC
_ PTerm
ty PTerm
t)
| ArgOpt
InaccessibleArg forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Plicity -> [ArgOpt]
pargopts Plicity
plicity
= (Int
i,Name
n) forall a. a -> [a] -> [a]
: Int -> PTerm -> [(Int, Name)]
inaccessibleArgs (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
t
| Bool
otherwise
= Int -> PTerm -> [(Int, Name)]
inaccessibleArgs (Int
iforall a. Num a => a -> a -> a
+Int
1) PTerm
t
inaccessibleArgs Int
_ PTerm
_ = []
elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()
elabCaseBlock :: ElabInfo -> FnOpts -> PDecl -> Idris ()
elabCaseBlock ElabInfo
info FnOpts
opts d :: PDecl
d@(PClauses FC
f FnOpts
o Name
n [PClause' PTerm]
ps)
= do IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDef Name
n)
Int -> String -> Idris ()
logElab Int
5 forall a b. (a -> b) -> a -> b
$ String
"CASE BLOCK: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name
n, PDecl
d)
let opts' :: FnOpts
opts' = forall a. (a -> Bool) -> [a] -> [a]
filter FnOpt -> Bool
propagatable FnOpts
opts
Name -> FnOpts -> Idris ()
setFlags Name
n FnOpts
opts'
ElabInfo -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
rec_elabDecl ElabInfo
info ElabWhat
EAll ElabInfo
info (forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
f FnOpts
opts' Name
n [PClause' PTerm]
ps )
where
propagatable :: FnOpt -> Bool
propagatable FnOpt
AssertTotal = Bool
True
propagatable FnOpt
Inlinable = Bool
True
propagatable FnOpt
_ = Bool
False
checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred FC
fc PTerm
inf PTerm
user =
do Int -> String -> Idris ()
logElab Int
6 forall a b. (a -> b) -> a -> b
$ String
"Checked to\n" forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
inf forall a. [a] -> [a] -> [a]
++ String
"\n\nFROM\n\n" forall a. [a] -> [a] -> [a]
++
PTerm -> String
showTmImpls PTerm
user
Int -> String -> Idris ()
logElab Int
10 forall a b. (a -> b) -> a -> b
$ String
"Checking match"
IState
i <- Idris IState
getIState
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ case Bool
-> IState
-> PTerm
-> PTerm
-> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause' Bool
True IState
i PTerm
user PTerm
inf of
Either (PTerm, PTerm) [(Name, PTerm)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Int -> String -> Idris ()
logElab Int
10 forall a b. (a -> b) -> a -> b
$ String
"Checked match"
inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
inferredDiff FC
fc PTerm
inf PTerm
user =
do IState
i <- Idris IState
getIState
Int -> String -> Idris ()
logElab Int
6 forall a b. (a -> b) -> a -> b
$ String
"Checked to\n" forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
inf forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++
PTerm -> String
showTmImpls PTerm
user
forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ case Bool
-> IState
-> PTerm
-> PTerm
-> Either (PTerm, PTerm) [(Name, PTerm)]
matchClause' Bool
True IState
i PTerm
user PTerm
inf of
Right [(Name, PTerm)]
vs -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Left (PTerm
x, PTerm
y) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs :: forall a. FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
checkDocs FC
fc [(Name, Docstring a)]
args PTerm
tm = forall {a}. Map Name a -> PTerm -> Idris ()
cd (forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Name, Docstring a)]
args) PTerm
tm
where cd :: Map Name a -> PTerm -> Idris ()
cd Map Name a
as (PPi Plicity
_ Name
n FC
_ PTerm
_ PTerm
sc) = Map Name a -> PTerm -> Idris ()
cd (forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Name
n Map Name a
as) PTerm
sc
cd Map Name a
as PTerm
_ | forall k a. Map k a -> Bool
Map.null Map Name a
as = forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = forall a. Err -> Idris a
ierror forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FC -> Err' t -> Err' t
At FC
fc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
String
"There is documentation for argument(s) "
forall a. [a] -> [a] -> [a]
++ (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse String
", " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
Map.keys) Map Name a
as
forall a. [a] -> [a] -> [a]
++ String
" but they were not found."
decorateid :: (Name -> Name) -> PDecl -> PDecl
decorateid Name -> Name
decorate (PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
s FC
f FnOpts
o Name
n FC
nfc PTerm
t) = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
s FC
f FnOpts
o (Name -> Name
decorate Name
n) FC
nfc PTerm
t
decorateid Name -> Name
decorate (PClauses FC
f FnOpts
o Name
n [PClause' PTerm]
cs)
= forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
f FnOpts
o (Name -> Name
decorate Name
n) (forall a b. (a -> b) -> [a] -> [b]
map PClause' PTerm -> PClause' PTerm
dc [PClause' PTerm]
cs)
where dc :: PClause' PTerm -> PClause' PTerm
dc (PClause FC
fc Name
n PTerm
t [PTerm]
as PTerm
w [PDecl]
ds) = forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc (Name -> Name
decorate Name
n) (PTerm -> PTerm
dappname PTerm
t) [PTerm]
as PTerm
w [PDecl]
ds
dc (PWith FC
fc Name
n PTerm
t [PTerm]
as PTerm
w Maybe (Name, FC)
pn [PDecl]
ds)
= forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc (Name -> Name
decorate Name
n) (PTerm -> PTerm
dappname PTerm
t) [PTerm]
as PTerm
w Maybe (Name, FC)
pn
(forall a b. (a -> b) -> [a] -> [b]
map ((Name -> Name) -> PDecl -> PDecl
decorateid Name -> Name
decorate) [PDecl]
ds)
dappname :: PTerm -> PTerm
dappname (PApp FC
fc (PRef FC
fc' [FC]
hl Name
n) [PArg]
as) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc' [FC]
hl (Name -> Name
decorate Name
n)) [PArg]
as
dappname PTerm
t = PTerm
t
pbinds :: IState -> Term -> ElabD ()
pbinds :: IState -> Type -> ElabD ()
pbinds IState
i (Bind Name
n (PVar RigCount
rig Type
t) Type
sc)
= do forall aux. Elab' aux ()
attack; forall aux. Name -> RigCount -> Elab' aux ()
patbind Name
n RigCount
rig
Env
env <- forall aux. Elab' aux Env
get_env
case forall n. TT n -> (TT n, [TT n])
unApply (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
i) Env
env Type
t) of
(P NameType
_ Name
c Type
_, [Type]
args) -> case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
c (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
[InterfaceInfo]
_ ->
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {aux}. Type -> Elab' aux ()
setinjArg [Type]
args
(Type, [Type])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
IState -> Type -> ElabD ()
pbinds IState
i Type
sc
where setinjArg :: Type -> Elab' aux ()
setinjArg (P NameType
_ Name
n Type
_) = forall aux. Name -> Elab' aux ()
setinj Name
n
setinjArg Type
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
pbinds IState
i Type
tm = forall (m :: * -> *) a. Monad m => a -> m a
return ()
pbty :: TT n -> TT n -> TT n
pbty (Bind n
n (PVar RigCount
_ TT n
t) TT n
sc) TT n
tm = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. b -> Binder b
PVTy TT n
t) (TT n -> TT n -> TT n
pbty TT n
sc TT n
tm)
pbty TT n
_ TT n
tm = TT n
tm
getPBtys :: TT a -> [(a, TT a)]
getPBtys (Bind a
n (PVar RigCount
_ TT a
t) TT a
sc) = (a
n, TT a
t) forall a. a -> [a] -> [a]
: TT a -> [(a, TT a)]
getPBtys TT a
sc
getPBtys (Bind a
n (PVTy TT a
t) TT a
sc) = (a
n, TT a
t) forall a. a -> [a] -> [a]
: TT a -> [(a, TT a)]
getPBtys TT a
sc
getPBtys TT a
_ = []
psolve :: TT n -> StateT (ElabState aux) TC ()
psolve (Bind n
n (PVar RigCount
_ TT n
t) TT n
sc) = do forall aux. Elab' aux ()
solve; TT n -> StateT (ElabState aux) TC ()
psolve TT n
sc
psolve TT n
tm = forall (m :: * -> *) a. Monad m => a -> m a
return ()
pvars :: IState -> Type -> [(Name, PTerm)]
pvars IState
ist Type
tm = [(Name, Type)] -> Type -> [(Name, PTerm)]
pv' [] Type
tm
where
pv' :: [(Name, Type)] -> Type -> [(Name, PTerm)]
pv' [(Name, Type)]
env (Bind Name
n (PVar RigCount
_ Type
t) Type
sc)
= (Name
n, IState -> [(Name, Type)] -> Type -> PTerm
delabWithEnv IState
ist [(Name, Type)]
env Type
t) forall a. a -> [a] -> [a]
: [(Name, Type)] -> Type -> [(Name, PTerm)]
pv' ((Name
n, Type
t) forall a. a -> [a] -> [a]
: [(Name, Type)]
env) Type
sc
pv' [(Name, Type)]
env Type
_ = []
getFixedInType :: IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env (PExp Int
_ [ArgOpt]
_ Name
_ t
_ : [PArg' t]
is) (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
sc)
= forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [] Type
t forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i (Name
n forall a. a -> [a] -> [a]
: [Name]
env) [PArg' t]
is (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
forall a. [a] -> [a] -> [a]
++ case forall n. TT n -> (TT n, [TT n])
unApply Type
t of
(P NameType
_ Name
n Type
_, [Type]
_) -> if Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
env then [Name
n] else []
(Type, [Type])
_ -> []
getFixedInType IState
i [Name]
env (PArg' t
_ : [PArg' t]
is) (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
sc)
= IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i (Name
n forall a. a -> [a] -> [a]
: [Name]
env) [PArg' t]
is (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
getFixedInType IState
i [Name]
env [PArg' t]
is tm :: Type
tm@(App AppStatus Name
_ Type
f Type
a)
| (P NameType
_ Name
tn Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
tm
= case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tn (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
Just TypeInfo
t -> forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
[TT a] -> t a -> [Int] -> [a]
paramNames [Type]
args [Name]
env (TypeInfo -> [Int]
param_pos TypeInfo
t) forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
f forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
a
Maybe TypeInfo
Nothing -> forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
f forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
a
| Bool
otherwise = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
f forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
a
getFixedInType IState
i [Name]
_ [PArg' t]
_ Type
_ = []
getFlexInType :: IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
sc)
= forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ (if (Bool -> Bool
not (Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
ps)) then IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
t else []) forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i (Name
n forall a. a -> [a] -> [a]
: [Name]
env) t Name
ps (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
getFlexInType IState
i [Name]
env t Name
ps tm :: Type
tm@(App AppStatus Name
_ Type
f Type
a)
| (P NameType
nt Name
tn Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
tm, NameType
nt forall a. Eq a => a -> a -> Bool
/= NameType
Bound
= case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tn (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
Just TypeInfo
t -> forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
[TT a] -> t a -> [Int] -> [a]
paramNames [Type]
args [Name]
env [Int
x | Int
x <- [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args],
Bool -> Bool
not (Int
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TypeInfo -> [Int]
param_pos TypeInfo
t)]
forall a. [a] -> [a] -> [a]
++ IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
f forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
a
Maybe TypeInfo
Nothing -> let ppos :: [Int]
ppos = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tn (IState -> Ctxt FnInfo
idris_fninfo IState
i) of
Just FnInfo
fi -> FnInfo -> [Int]
fn_params FnInfo
fi
Maybe FnInfo
Nothing -> []
in forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
[TT a] -> t a -> [Int] -> [a]
paramNames [Type]
args [Name]
env [Int
x | Int
x <- [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args],
Bool -> Bool
not (Int
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ppos)]
forall a. [a] -> [a] -> [a]
++ IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
f forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
a
| Bool
otherwise = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
f forall a. [a] -> [a] -> [a]
++
IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
a
getFlexInType IState
i [Name]
_ t Name
_ Type
_ = []
getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getParamsInType IState
i [Name]
env [PArg]
ps Type
t = let fix :: [Name]
fix = forall {t}. IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg]
ps Type
t
flex :: [Name]
flex = forall {t :: * -> *}.
Foldable t =>
IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env [Name]
fix Type
t in
[Name
x | Name
x <- [Name]
fix, Bool -> Bool
not (Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
flex)]
getTCinj :: IState -> Type -> [Name]
getTCinj IState
i (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
sc)
= IState -> Type -> [Name]
getTCinj IState
i Type
t forall a. [a] -> [a] -> [a]
++ IState -> Type -> [Name]
getTCinj IState
i (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
getTCinj IState
i ap :: Type
ap@(App AppStatus Name
_ Type
f Type
a)
| (P NameType
_ Name
n Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
Name -> Bool
isTCName Name
n = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. TT a -> Maybe a
getInjName [Type]
args
| Bool
otherwise = []
where
isTCName :: Name -> Bool
isTCName Name
n = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
Just InterfaceInfo
_ -> Bool
True
Maybe InterfaceInfo
_ -> Bool
False
getInjName :: TT a -> Maybe a
getInjName TT a
t | (P NameType
_ a
x TT a
_, [TT a]
_) <- forall n. TT n -> (TT n, [TT n])
unApply TT a
t = forall a. a -> Maybe a
Just a
x
| Bool
otherwise = forall a. Maybe a
Nothing
getTCinj IState
_ Type
_ = []
getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getTCParamsInType :: IState -> [Name] -> [PArg] -> Type -> [Name]
getTCParamsInType IState
i [Name]
env [PArg]
ps Type
t = let params :: [Name]
params = IState -> [Name] -> [PArg] -> Type -> [Name]
getParamsInType IState
i [Name]
env [PArg]
ps Type
t
tcs :: [Name]
tcs = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ IState -> Type -> [Name]
getTCinj IState
i Type
t in
forall a. (a -> Bool) -> [a] -> [a]
filter (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [Name]
tcs) [Name]
params
paramNames :: [TT a] -> t a -> [Int] -> [a]
paramNames [TT a]
args t a
env [] = []
paramNames [TT a]
args t a
env (Int
p : [Int]
ps)
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [TT a]
args forall a. Ord a => a -> a -> Bool
> Int
p = case [TT a]
argsforall a. [a] -> Int -> a
!!Int
p of
P NameType
_ a
n TT a
_ -> if a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
env
then a
n forall a. a -> [a] -> [a]
: [TT a] -> t a -> [Int] -> [a]
paramNames [TT a]
args t a
env [Int]
ps
else [TT a] -> t a -> [Int] -> [a]
paramNames [TT a]
args t a
env [Int]
ps
TT a
_ -> [TT a] -> t a -> [Int] -> [a]
paramNames [TT a]
args t a
env [Int]
ps
| Bool
otherwise = [TT a] -> t a -> [Int] -> [a]
paramNames [TT a]
args t a
env [Int]
ps
getLinearUsed :: Context -> Term -> [Name]
getLinearUsed :: Context -> Type -> [Name]
getLinearUsed Context
ctxt Type
tm = forall s a. State s a -> s -> s
execState (Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin [] [] Type
tm) []
where
getLin :: Env -> [(Name, Bool)] -> Term -> State [Name] ()
getLin :: Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin Env
env [(Name, Bool)]
us (Bind Name
n Binder Type
b Type
sc)
= do Env -> [(Name, Bool)] -> Binder Type -> State [Name] ()
getLinB Env
env [(Name, Bool)]
us Binder Type
b
let r :: RigCount
r = Binder Type -> RigCount
getRig Binder Type
b
let lin :: Bool
lin = case RigCount
r of
RigCount
Rig1 -> Bool
True
RigCount
_ -> Bool
False
Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin ((Name
n, Binder Type -> RigCount
getRig Binder Type
b, Binder Type
b) forall a. a -> [a] -> [a]
: Env
env) ((Name
n, Bool
lin) forall a. a -> [a] -> [a]
: [(Name, Bool)]
us) Type
sc
getLin Env
env [(Name, Bool)]
us (App AppStatus Name
_ Type
f Type
a) = do Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin Env
env [(Name, Bool)]
us Type
f; Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin Env
env [(Name, Bool)]
us Type
a
getLin Env
env [(Name, Bool)]
us (V Int
i)
| Int
i forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Bool)]
us = if forall a b. (a, b) -> b
snd ([(Name, Bool)]
usforall a. [a] -> Int -> a
!!Int
i) then forall {m :: * -> *} {a}. MonadState [a] m => a -> m ()
use (forall a b. (a, b) -> a
fst ([(Name, Bool)]
usforall a. [a] -> Int -> a
!!Int
1)) else forall (m :: * -> *) a. Monad m => a -> m a
return ()
getLin Env
env [(Name, Bool)]
us (P NameType
_ Name
n Type
_)
| Just Bool
u <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Bool)]
us = if Bool
u then forall {m :: * -> *} {a}. MonadState [a] m => a -> m ()
use Name
n else forall (m :: * -> *) a. Monad m => a -> m a
return ()
getLin Env
env [(Name, Bool)]
us Type
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
getLinB :: Env -> [(Name, Bool)] -> Binder Type -> State [Name] ()
getLinB Env
env [(Name, Bool)]
us (Let RigCount
Rig0 Type
t Type
v) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
getLinB Env
env [(Name, Bool)]
us (Let RigCount
rig Type
t Type
v) = Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin Env
env [(Name, Bool)]
us Type
v
getLinB Env
env [(Name, Bool)]
us (Guess Type
t Type
v) = Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin Env
env [(Name, Bool)]
us Type
v
getLinB Env
env [(Name, Bool)]
us (NLet Type
t Type
v) = Env -> [(Name, Bool)] -> Type -> State [Name] ()
getLin Env
env [(Name, Bool)]
us Type
v
getLinB Env
env [(Name, Bool)]
us Binder Type
b = forall (m :: * -> *) a. Monad m => a -> m a
return ()
use :: a -> m ()
use a
n = do [a]
ns <- forall s (m :: * -> *). MonadState s m => m s
get; forall s (m :: * -> *). MonadState s m => s -> m ()
put (a
n forall a. a -> [a] -> [a]
: [a]
ns)
getRig :: Binder Term -> RigCount
getRig :: Binder Type -> RigCount
getRig (Pi RigCount
rig Maybe ImplicitInfo
_ Type
_ Type
_) = RigCount
rig
getRig (PVar RigCount
rig Type
_) = RigCount
rig
getRig (Lam RigCount
rig Type
_) = RigCount
rig
getRig (Let RigCount
rig Type
_ Type
_) = RigCount
rig
getRig Binder Type
_ = RigCount
RigW
getUniqueUsed :: Context -> Term -> [Name]
getUniqueUsed :: Context -> Type -> [Name]
getUniqueUsed Context
ctxt Type
tm = forall s a. State s a -> s -> s
execState (Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq [] [] Type
tm) []
where
getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()
getUniq :: Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq Env
env [(Name, Bool)]
us (Bind Name
n Binder Type
b Type
sc)
= let uniq :: Bool
uniq = case Context -> Env -> Raw -> TC (Type, Type)
check Context
ctxt Env
env ([Name] -> Type -> Raw
forgetEnv (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (forall b. Binder b -> b
binderTy Binder Type
b)) of
OK (Type
_, UType Universe
UniqueType) -> Bool
True
OK (Type
_, UType Universe
NullType) -> Bool
True
OK (Type
_, UType Universe
AllTypes) -> Bool
True
TC (Type, Type)
_ -> Bool
False in
do Env -> [(Name, Bool)] -> Binder Type -> State [Name] ()
getUniqB Env
env [(Name, Bool)]
us Binder Type
b
Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq ((Name
n, RigCount
RigW, Binder Type
b)forall a. a -> [a] -> [a]
:Env
env) ((Name
n, Bool
uniq)forall a. a -> [a] -> [a]
:[(Name, Bool)]
us) Type
sc
getUniq Env
env [(Name, Bool)]
us (App AppStatus Name
_ Type
f Type
a) = do Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq Env
env [(Name, Bool)]
us Type
f; Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq Env
env [(Name, Bool)]
us Type
a
getUniq Env
env [(Name, Bool)]
us (V Int
i)
| Int
i forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Bool)]
us = if forall a b. (a, b) -> b
snd ([(Name, Bool)]
usforall a. [a] -> Int -> a
!!Int
i) then forall {m :: * -> *} {a}. MonadState [a] m => a -> m ()
use (forall a b. (a, b) -> a
fst ([(Name, Bool)]
usforall a. [a] -> Int -> a
!!Int
i)) else forall (m :: * -> *) a. Monad m => a -> m a
return ()
getUniq Env
env [(Name, Bool)]
us (P NameType
_ Name
n Type
_)
| Just Bool
u <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Bool)]
us = if Bool
u then forall {m :: * -> *} {a}. MonadState [a] m => a -> m ()
use Name
n else forall (m :: * -> *) a. Monad m => a -> m a
return ()
getUniq Env
env [(Name, Bool)]
us Type
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
use :: a -> m ()
use a
n = do [a]
ns <- forall s (m :: * -> *). MonadState s m => m s
get; forall s (m :: * -> *). MonadState s m => s -> m ()
put (a
n forall a. a -> [a] -> [a]
: [a]
ns)
getUniqB :: Env -> [(Name, Bool)] -> Binder Type -> State [Name] ()
getUniqB Env
env [(Name, Bool)]
us (Let RigCount
rig Type
t Type
v) = Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq Env
env [(Name, Bool)]
us Type
v
getUniqB Env
env [(Name, Bool)]
us (Guess Type
t Type
v) = Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq Env
env [(Name, Bool)]
us Type
v
getUniqB Env
env [(Name, Bool)]
us (NLet Type
t Type
v) = Env -> [(Name, Bool)] -> Type -> State [Name] ()
getUniq Env
env [(Name, Bool)]
us Type
v
getUniqB Env
env [(Name, Bool)]
us Binder Type
b = forall (m :: * -> *) a. Monad m => a -> m a
return ()
getStaticNames :: IState -> Term -> [Name]
getStaticNames :: IState -> Type -> [Name]
getStaticNames IState
ist (Bind Name
n (PVar RigCount
_ Type
_) Type
sc)
= IState -> Type -> [Name]
getStaticNames IState
ist (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n forall n. TT n
Erased) Type
sc)
getStaticNames IState
ist Type
tm
| (P NameType
_ Name
fn Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
tm
= case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
fn (IState -> Ctxt [Bool]
idris_statics IState
ist) of
Just [Bool]
stpos -> forall {a}. [TT a] -> [Bool] -> [a]
getStatics [Type]
args [Bool]
stpos
Maybe [Bool]
_ -> []
where
getStatics :: [TT a] -> [Bool] -> [a]
getStatics (P NameType
_ a
n TT a
_ : [TT a]
as) (Bool
True : [Bool]
ss) = a
n forall a. a -> [a] -> [a]
: [TT a] -> [Bool] -> [a]
getStatics [TT a]
as [Bool]
ss
getStatics (TT a
_ : [TT a]
as) (Bool
_ : [Bool]
ss) = [TT a] -> [Bool] -> [a]
getStatics [TT a]
as [Bool]
ss
getStatics [TT a]
_ [Bool]
_ = []
getStaticNames IState
_ Type
_ = []
getStatics :: [Name] -> Term -> [Bool]
getStatics :: [Name] -> Type -> [Bool]
getStatics [Name]
ns (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
t)
| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns = Bool
True forall a. a -> [a] -> [a]
: [Name] -> Type -> [Bool]
getStatics [Name]
ns Type
t
| Bool
otherwise = Bool
False forall a. a -> [a] -> [a]
: [Name] -> Type -> [Bool]
getStatics [Name]
ns Type
t
getStatics [Name]
_ Type
_ = []
mkStatic :: [Name] -> PDecl -> PDecl
mkStatic :: [Name] -> PDecl -> PDecl
mkStatic [Name]
ns (PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc FnOpts
o Name
n FC
nfc PTerm
ty)
= forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
syn FC
fc FnOpts
o Name
n FC
nfc ([Name] -> PTerm -> PTerm
mkStaticTy [Name]
ns PTerm
ty)
mkStatic [Name]
ns PDecl
t = PDecl
t
mkStaticTy :: [Name] -> PTerm -> PTerm
mkStaticTy :: [Name] -> PTerm -> PTerm
mkStaticTy [Name]
ns (PPi Plicity
p Name
n FC
fc PTerm
ty PTerm
sc)
| Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
p { pstatic :: Static
pstatic = Static
Static }) Name
n FC
fc PTerm
ty ([Name] -> PTerm -> PTerm
mkStaticTy [Name]
ns PTerm
sc)
| Bool
otherwise = Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
p Name
n FC
fc PTerm
ty ([Name] -> PTerm -> PTerm
mkStaticTy [Name]
ns PTerm
sc)
mkStaticTy [Name]
ns PTerm
t = PTerm
t
checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()
checkVisibility :: FC -> Name -> Accessibility -> Accessibility -> Name -> Idris ()
checkVisibility FC
fc Name
n Accessibility
minAcc Accessibility
acc Name
ref
= do Maybe Accessibility
nvis <- Name -> Idris (Maybe Accessibility)
getFromHideList Name
ref
case Maybe Accessibility
nvis of
Maybe Accessibility
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Accessibility
acc' -> if Accessibility
acc' forall a. Ord a => a -> a -> Bool
> Accessibility
minAcc
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 -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Accessibility
acc forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++
String
" can't refer to " forall a. [a] -> [a] -> [a]
++
forall a. Show a => a -> String
show Accessibility
acc' forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
ref))
else forall (m :: * -> *) a. Monad m => a -> m a
return ()
findParams :: Name
-> Type
-> [Type]
-> [Int]
findParams :: Name -> Type -> [Type] -> [Int]
findParams Name
tyn Type
famty [Type]
ts =
let allapps :: [[[Maybe Name]]]
allapps = forall a b. (a -> b) -> [a] -> [b]
map Type -> [[Maybe Name]]
getDataApp [Type]
ts
conParams :: [[Int]]
conParams = forall a b. (a -> b) -> [a] -> [b]
map [[Maybe Name]] -> [Int]
paramPos [[[Maybe Name]]]
allapps
in [[Int]] -> [Int]
inAll [[Int]]
conParams
where
inAll :: [[Int]] -> [Int]
inAll :: [[Int]] -> [Int]
inAll [] = []
inAll ([Int]
x : [[Int]]
xs) = forall a. (a -> Bool) -> [a] -> [a]
filter (\Int
p -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Int]
ps -> Int
p forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
ps) [[Int]]
xs) [Int]
x
paramPos :: [[Maybe Name]] -> [Int]
paramPos [] = []
paramPos ([Maybe Name]
args : [[Maybe Name]]
rest)
= forall {a} {a}. [(a, Maybe a)] -> [a]
dropNothing forall a b. (a -> b) -> a -> b
$ [(Int, Maybe Name)] -> [[Maybe Name]] -> [(Int, Maybe Name)]
keepSame (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Maybe Name]
args) [[Maybe Name]]
rest
dropNothing :: [(a, Maybe a)] -> [a]
dropNothing [] = []
dropNothing ((a
x, Maybe a
Nothing) : [(a, Maybe a)]
ts) = [(a, Maybe a)] -> [a]
dropNothing [(a, Maybe a)]
ts
dropNothing ((a
x, Maybe a
_) : [(a, Maybe a)]
ts) = a
x forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [a]
dropNothing [(a, Maybe a)]
ts
keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->
[(Int, Maybe Name)]
keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] -> [(Int, Maybe Name)]
keepSame [(Int, Maybe Name)]
as [] = [(Int, Maybe Name)]
as
keepSame [(Int, Maybe Name)]
as ([Maybe Name]
args : [[Maybe Name]]
rest) = [(Int, Maybe Name)] -> [[Maybe Name]] -> [(Int, Maybe Name)]
keepSame (forall {a} {a}.
Eq a =>
[(a, Maybe a)] -> [Maybe a] -> [(a, Maybe a)]
update [(Int, Maybe Name)]
as [Maybe Name]
args) [[Maybe Name]]
rest
where
update :: [(a, Maybe a)] -> [Maybe a] -> [(a, Maybe a)]
update [] [Maybe a]
_ = []
update [(a, Maybe a)]
_ [] = []
update ((a
n, Just a
x) : [(a, Maybe a)]
as) (Just a
x' : [Maybe a]
args)
| a
x forall a. Eq a => a -> a -> Bool
== a
x' = (a
n, forall a. a -> Maybe a
Just a
x) forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [Maybe a] -> [(a, Maybe a)]
update [(a, Maybe a)]
as [Maybe a]
args
update ((a
n, Maybe a
_) : [(a, Maybe a)]
as) (Maybe a
_ : [Maybe a]
args) = (a
n, forall a. Maybe a
Nothing) forall a. a -> [a] -> [a]
: [(a, Maybe a)] -> [Maybe a] -> [(a, Maybe a)]
update [(a, Maybe a)]
as [Maybe a]
args
getDataApp :: Type -> [[Maybe Name]]
getDataApp :: Type -> [[Maybe Name]]
getDataApp f :: Type
f@(App AppStatus Name
_ Type
_ Type
_)
| (P NameType
_ Name
d Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
f
= if (Name
d forall a. Eq a => a -> a -> Bool
== Name
tyn) then [forall {a}. Eq a => [TT a] -> [TT a] -> [Maybe a]
mParam [Type]
args [Type]
args] else []
getDataApp (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
t Type
_) Type
sc)
= Type -> [[Maybe Name]]
getDataApp Type
t forall a. [a] -> [a] -> [a]
++ Type -> [[Maybe Name]]
getDataApp (forall n. TT n -> TT n -> TT n
instantiate (forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
getDataApp Type
_ = []
mParam :: [TT a] -> [TT a] -> [Maybe a]
mParam [TT a]
args [] = []
mParam [TT a]
args (P NameType
Bound a
n TT a
_ : [TT a]
rest)
| forall {a}. Eq a => Bool -> a -> [TT a] -> Bool
paramIn Bool
False a
n [TT a]
args = forall a. a -> Maybe a
Just a
n forall a. a -> [a] -> [a]
: [TT a] -> [TT a] -> [Maybe a]
mParam (forall a. (a -> Bool) -> [a] -> [a]
filter (forall {a}. Eq a => a -> TT a -> Bool
noN a
n) [TT a]
args) [TT a]
rest
where paramIn :: Bool -> a -> [TT a] -> Bool
paramIn Bool
ok a
n [] = Bool
ok
paramIn Bool
ok a
n (P NameType
_ a
t TT a
_ : [TT a]
ts)
= Bool -> a -> [TT a] -> Bool
paramIn (Bool
ok Bool -> Bool -> Bool
|| a
n forall a. Eq a => a -> a -> Bool
== a
t) a
n [TT a]
ts
paramIn Bool
ok a
n (TT a
t : [TT a]
ts)
| a
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall n. Eq n => TT n -> [n]
freeNames TT a
t = Bool
False
| Bool
otherwise = Bool -> a -> [TT a] -> Bool
paramIn Bool
ok a
n [TT a]
ts
noN :: a -> TT a -> Bool
noN a
n (P NameType
_ a
t TT a
_) = a
n forall a. Eq a => a -> a -> Bool
/= a
t
noN a
n TT a
_ = Bool
False
mParam [TT a]
args (TT a
_ : [TT a]
rest) = forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: [TT a] -> [TT a] -> [Maybe a]
mParam [TT a]
args [TT a]
rest
setDetaggable :: Name -> Idris ()
setDetaggable :: Name -> Idris ()
setDetaggable Name
n = do
IState
ist <- Idris IState
getIState
let opt :: Ctxt OptInfo
opt = IState -> Ctxt OptInfo
idris_optimisation IState
ist
case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n Ctxt OptInfo
opt of
[OptInfo
oi] -> IState -> Idris ()
putIState IState
ist { idris_optimisation :: Ctxt OptInfo
idris_optimisation = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n OptInfo
oi { detaggable :: Bool
detaggable = Bool
True } Ctxt OptInfo
opt }
[OptInfo]
_ -> IState -> Idris ()
putIState IState
ist { idris_optimisation :: Ctxt OptInfo
idris_optimisation = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
n ([(Int, Name)] -> Bool -> [Int] -> OptInfo
Optimise [] Bool
True []) Ctxt OptInfo
opt }
displayWarnings :: EState -> Idris ()
displayWarnings :: EState -> Idris ()
displayWarnings EState
est
= forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
displayImpWarning (EState -> [(FC, Name)]
implicit_warnings EState
est)
where
displayImpWarning :: (FC, Name) -> Idris ()
displayImpWarning :: (FC, Name) -> Idris ()
displayImpWarning (FC
fc, Name
n) = do
IState
ist <- Idris IState
getIState
let msg :: String
msg = forall a. Show a => a -> String
show (Name -> Name
nsroot Name
n)
forall a. [a] -> [a] -> [a]
++ String
" is bound as an implicit\n"
forall a. [a] -> [a] -> [a]
++ String
"\tDid you mean to refer to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
"?"
FC -> OutputDoc -> Idris ()
iWarn FC
fc (IState -> Err -> OutputDoc
pprintErr IState
ist (forall t. String -> Err' t
Msg String
msg))
propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
propagateParams IState
i [Name]
ps Type
t [Name]
bound tm :: PTerm
tm@(PApp FC
_ (PRef FC
fc [FC]
hls Name
n) [PArg]
args)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n) (Type -> [PArg] -> [PArg]
addP Type
t [PArg]
args)
where addP :: Type -> [PArg] -> [PArg]
addP (Bind Name
n Binder Type
_ Type
sc) (PArg
t : [PArg]
ts)
| PTerm
Placeholder <- forall t. PArg' t -> t
getTm PArg
t,
Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ps,
Bool -> Bool
not (Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
bound)
= PArg
t { getTm :: PTerm
getTm = FC -> Name -> PTerm
PPatvar FC
NoFC Name
n } forall a. a -> [a] -> [a]
: Type -> [PArg] -> [PArg]
addP Type
sc [PArg]
ts
addP (Bind Name
n Binder Type
_ Type
sc) (PArg
t : [PArg]
ts) = PArg
t forall a. a -> [a] -> [a]
: Type -> [PArg] -> [PArg]
addP Type
sc [PArg]
ts
addP Type
_ [PArg]
ts = [PArg]
ts
propagateParams IState
i [Name]
ps Type
t [Name]
bound (PApp FC
fc PTerm
ap [PArg]
args)
= FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm
propagateParams IState
i [Name]
ps Type
t [Name]
bound PTerm
ap) [PArg]
args
propagateParams IState
i [Name]
ps Type
t [Name]
bound (PRef FC
fc [FC]
hls Name
n)
= case forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
[[PArg]
is] -> let ps' :: [Name]
ps' = forall a. (a -> Bool) -> [a] -> [a]
filter (forall {t}. [PArg' t] -> Name -> Bool
isImplicit [PArg]
is) [Name]
ps in
FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n) (forall a b. (a -> b) -> [a] -> [b]
map (\Name
x -> forall {t}. Name -> t -> Bool -> PArg' t
pimp Name
x (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
x) Bool
True) [Name]
ps')
[[PArg]]
_ -> FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n
where isImplicit :: [PArg' t] -> Name -> Bool
isImplicit [] Name
n = Bool
False
isImplicit (PImp Int
_ Bool
_ [ArgOpt]
_ Name
x t
_ : [PArg' t]
is) Name
n | Name
x forall a. Eq a => a -> a -> Bool
== Name
n = Bool
True
isImplicit (PArg' t
_ : [PArg' t]
is) Name
n = [PArg' t] -> Name -> Bool
isImplicit [PArg' t]
is Name
n
propagateParams IState
i [Name]
ps Type
t [Name]
bound PTerm
x = PTerm
x
orderPats :: Term -> Term
orderPats :: Type -> Type
orderPats Type
tm = [(Name, Binder Type)] -> Type -> Type
op [] Type
tm
where
op :: [(Name, Binder Type)] -> Type -> Type
op [] (App AppStatus Name
s Type
f Type
a) = forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f ([(Name, Binder Type)] -> Type -> Type
op [] Type
a)
op [(Name, Binder Type)]
ps (Bind Name
n (PVar RigCount
r Type
t) Type
sc) = [(Name, Binder Type)] -> Type -> Type
op ((Name
n, forall b. RigCount -> b -> Binder b
PVar RigCount
r Type
t) forall a. a -> [a] -> [a]
: [(Name, Binder Type)]
ps) Type
sc
op [(Name, Binder Type)]
ps (Bind Name
n (Hole Type
t) Type
sc) = [(Name, Binder Type)] -> Type -> Type
op ((Name
n, forall b. b -> Binder b
Hole Type
t) forall a. a -> [a] -> [a]
: [(Name, Binder Type)]
ps) Type
sc
op [(Name, Binder Type)]
ps (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Type
t Type
k) Type
sc) = [(Name, Binder Type)] -> Type -> Type
op ((Name
n, forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Type
t Type
k) forall a. a -> [a] -> [a]
: [(Name, Binder Type)]
ps) Type
sc
op [(Name, Binder Type)]
ps Type
sc = forall n. [(n, Binder (TT n))] -> TT n -> TT n
bindAll ([(Name, Binder Type)] -> [(Name, Binder Type)]
sortP [(Name, Binder Type)]
ps) Type
sc
sortP :: [(Name, Binder Type)] -> [(Name, Binder Type)]
sortP [(Name, Binder Type)]
ps = let ([(Name, Binder Type)]
exps, [(Name, Binder Type)]
imps) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall {a} {b}. (a, Binder b) -> Bool
isExp [(Name, Binder Type)]
ps in
[(Name, Binder Type)]
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
pick (forall a. [a] -> [a]
reverse [(Name, Binder Type)]
exps) [(Name, Binder Type)]
imps
isExp :: (a, Binder b) -> Bool
isExp (a
_, Pi RigCount
rig Maybe ImplicitInfo
Nothing b
_ b
_) = Bool
True
isExp (a
_, Pi RigCount
rig (Just ImplicitInfo
i) b
_ b
_) = ImplicitInfo -> Bool
toplevel_imp ImplicitInfo
i Bool -> Bool -> Bool
&& Bool -> Bool
not (ImplicitInfo -> Bool
machine_gen ImplicitInfo
i)
isExp (a, Binder b)
_ = Bool
False
pick :: [(Name, Binder Type)]
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
pick [(Name, Binder Type)]
acc [] = [(Name, Binder Type)]
acc
pick [(Name, Binder Type)]
acc ((Name
n, Binder Type
t) : [(Name, Binder Type)]
ps) = [(Name, Binder Type)]
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
pick (Name
-> Binder Type -> [(Name, Binder Type)] -> [(Name, Binder Type)]
insert Name
n Binder Type
t [(Name, Binder Type)]
acc) [(Name, Binder Type)]
ps
insert :: Name
-> Binder Type -> [(Name, Binder Type)] -> [(Name, Binder Type)]
insert Name
n Binder Type
t [] = [(Name
n, Binder Type
t)]
insert Name
n Binder Type
t rest :: [(Name, Binder Type)]
rest@((Name
n', Binder Type
t') : [(Name, Binder Type)]
ps)
| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
x -> Name
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Type -> [Name]
refsIn (forall b. Binder b -> b
binderTy Binder Type
t)) (Name
n' forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, Binder Type)]
ps)
= (Name
n', Binder Type
t') forall a. a -> [a] -> [a]
: Name
-> Binder Type -> [(Name, Binder Type)] -> [(Name, Binder Type)]
insert Name
n Binder Type
t [(Name, Binder Type)]
ps
| Bool
otherwise = (Name
n, Binder Type
t) forall a. a -> [a] -> [a]
: [(Name, Binder Type)]
rest
liftPats :: Term -> Term
liftPats :: Type -> Type
liftPats Type
tm = let (Type
tm', [(Name, Type)]
ps) = forall s a. State s a -> s -> (a, s)
runState (Type -> State [(Name, Type)] Type
getPats Type
tm) [] in
Type -> Type
orderPats forall a b. (a -> b) -> a -> b
$ forall {n}. Eq n => [(n, TT n)] -> TT n -> TT n
bindPats (forall a. [a] -> [a]
reverse [(Name, Type)]
ps) Type
tm'
where
bindPats :: [(n, TT n)] -> TT n -> TT n
bindPats [] TT n
tm = TT n
tm
bindPats ((n
n, TT n
t):[(n, TT n)]
ps) TT n
tm
| n
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(n, TT n)]
ps = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (forall b. RigCount -> b -> Binder b
PVar RigCount
RigW TT n
t) ([(n, TT n)] -> TT n -> TT n
bindPats [(n, TT n)]
ps TT n
tm)
| Bool
otherwise = [(n, TT n)] -> TT n -> TT n
bindPats [(n, TT n)]
ps TT n
tm
getPats :: Term -> State [(Name, Type)] Term
getPats :: Type -> State [(Name, Type)] Type
getPats (Bind Name
n (PVar RigCount
_ Type
t) Type
sc) = do [(Name, Type)]
ps <- forall s (m :: * -> *). MonadState s m => m s
get
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, Type
t) forall a. a -> [a] -> [a]
: [(Name, Type)]
ps)
Type -> State [(Name, Type)] Type
getPats Type
sc
getPats (Bind Name
n (Guess Type
t Type
v) Type
sc) = do Type
t' <- Type -> State [(Name, Type)] Type
getPats Type
t
Type
v' <- Type -> State [(Name, Type)] Type
getPats Type
v
Type
sc' <- Type -> State [(Name, Type)] Type
getPats Type
sc
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. b -> b -> Binder b
Guess Type
t' Type
v') Type
sc')
getPats (Bind Name
n (Let RigCount
rig Type
t Type
v) Type
sc) = do Type
t' <- Type -> State [(Name, Type)] Type
getPats Type
t
Type
v' <- Type -> State [(Name, Type)] Type
getPats Type
v
Type
sc' <- Type -> State [(Name, Type)] Type
getPats Type
sc
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig Type
t' Type
v') Type
sc')
getPats (Bind Name
n (Pi RigCount
rig Maybe ImplicitInfo
i Type
t Type
k) Type
sc) = do Type
t' <- Type -> State [(Name, Type)] Type
getPats Type
t
Type
k' <- Type -> State [(Name, Type)] Type
getPats Type
k
Type
sc' <- Type -> State [(Name, Type)] Type
getPats Type
sc
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Type
t' Type
k') Type
sc')
getPats (Bind Name
n (Lam RigCount
r Type
t) Type
sc) = do Type
t' <- Type -> State [(Name, Type)] Type
getPats Type
t
Type
sc' <- Type -> State [(Name, Type)] Type
getPats Type
sc
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
Lam RigCount
r Type
t') Type
sc')
getPats (Bind Name
n (Hole Type
t) Type
sc) = do Type
t' <- Type -> State [(Name, Type)] Type
getPats Type
t
Type
sc' <- Type -> State [(Name, Type)] Type
getPats Type
sc
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. b -> Binder b
Hole Type
t') Type
sc')
getPats (App AppStatus Name
s Type
f Type
a) = do Type
f' <- Type -> State [(Name, Type)] Type
getPats Type
f
Type
a' <- Type -> State [(Name, Type)] Type
getPats Type
a
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f' Type
a')
getPats Type
t = forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool
isEmpty :: Context -> Ctxt TypeInfo -> Type -> Bool
isEmpty Context
ctxt Ctxt TypeInfo
tyctxt Type
ty
| (P NameType
_ Name
tyname Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
ty,
Just TypeInfo
tyinfo <- forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tyname Ctxt TypeInfo
tyctxt
= let neededty :: Type
neededty = forall n. TT n -> TT n
getRetTy Type
ty
contys :: [Type]
contys = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Name -> Maybe Type
getConType (TypeInfo -> [Name]
con_names TypeInfo
tyinfo) in
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Type -> Type -> Bool
findClash Type
neededty) [Type]
contys
where
getConType :: Name -> Maybe Type
getConType Name
n = do Type
t <- Name -> Context -> Maybe Type
lookupTyExact Name
n Context
ctxt
forall (m :: * -> *) a. Monad m => a -> m a
return (forall n. TT n -> TT n
getRetTy (Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
t))
findClash :: Type -> Type -> Bool
findClash Type
l Type
r
| (P NameType
_ Name
n Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
l,
(P NameType
_ Name
n' Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
r,
Name -> Context -> Bool
isConName Name
n Context
ctxt Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
n' Context
ctxt, Name
n forall a. Eq a => a -> a -> Bool
/= Name
n'
= Bool
True
findClash (App AppStatus Name
_ Type
f Type
a) (App AppStatus Name
_ Type
f' Type
a') = Type -> Type -> Bool
findClash Type
f Type
f' Bool -> Bool -> Bool
|| Type -> Type -> Bool
findClash Type
a Type
a'
findClash Type
l Type
r = Bool
False
isEmpty Context
ctxt Ctxt TypeInfo
tyinfo Type
ty = Bool
False
hasEmptyPat :: Context -> Ctxt TypeInfo -> Term -> Bool
hasEmptyPat :: Context -> Ctxt TypeInfo -> Type -> Bool
hasEmptyPat Context
ctxt Ctxt TypeInfo
tyctxt (Bind Name
n (PVar RigCount
_ Type
ty) Type
sc)
= Context -> Ctxt TypeInfo -> Type -> Bool
isEmpty Context
ctxt Ctxt TypeInfo
tyctxt Type
ty Bool -> Bool -> Bool
|| Context -> Ctxt TypeInfo -> Type -> Bool
hasEmptyPat Context
ctxt Ctxt TypeInfo
tyctxt Type
sc
hasEmptyPat Context
ctxt Ctxt TypeInfo
tyctxt Type
_ = Bool
False
findLinear :: RigCount -> IState -> [Name] -> Term -> [(Name, RigCount)]
findLinear :: RigCount -> IState -> [Name] -> Type -> [(Name, RigCount)]
findLinear RigCount
rig IState
ist [Name]
env Type
tm
| (P NameType
_ Name
f Type
_, [Type]
args) <- forall n. TT n -> (TT n, [TT n])
unApply Type
tm,
Name
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
env,
Just Type
ty_in <- Name -> Context -> Maybe Type
lookupTyExact Name
f (IState -> Context
tt_ctxt IState
ist)
= let ty :: Type
ty = Context -> Env -> Type -> Type
whnfArgs (IState -> Context
tt_ctxt IState
ist) [] Type
ty_in in
forall {b} {a}. (Ord b, Eq a) => [(a, b)] -> [(a, b)]
combineRig forall a b. (a -> b) -> a -> b
$ Type -> [Type] -> [(Name, RigCount)]
findLinArg Type
ty [Type]
args
where
findLinArg :: Type -> [Type] -> [(Name, RigCount)]
findLinArg (Bind Name
n (Pi RigCount
c Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc) (P NameType
_ Name
a Type
_ : [Type]
as)
= (Name
a, RigCount -> RigCount -> RigCount
rigMult RigCount
rig RigCount
c) forall a. a -> [a] -> [a]
: Type -> [Type] -> [(Name, RigCount)]
findLinArg Type
sc [Type]
as
findLinArg (Bind Name
n (Pi RigCount
c Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc) (Type
a : [Type]
as)
= RigCount -> IState -> [Name] -> Type -> [(Name, RigCount)]
findLinear (RigCount -> RigCount -> RigCount
rigMult RigCount
c RigCount
rig) IState
ist [Name]
env Type
a forall a. [a] -> [a] -> [a]
++
Type -> [Type] -> [(Name, RigCount)]
findLinArg (Context -> Env -> Type -> Type
whnf (IState -> Context
tt_ctxt IState
ist) [] (forall n. TT n -> TT n -> TT n
substV Type
a Type
sc)) [Type]
as
findLinArg Type
ty (Type
a : [Type]
as)
= RigCount -> IState -> [Name] -> Type -> [(Name, RigCount)]
findLinear RigCount
rig IState
ist [Name]
env Type
a forall a. [a] -> [a] -> [a]
++ Type -> [Type] -> [(Name, RigCount)]
findLinArg Type
ty [Type]
as
findLinArg Type
_ [] = []
combineRig :: [(a, b)] -> [(a, b)]
combineRig [] = []
combineRig ((a
n, b
r) : [(a, b)]
rs)
= let ([(a, b)]
rs', b
rig) = forall {b} {a}.
(Ord b, Eq a) =>
a -> b -> [(a, b)] -> [(a, b)] -> ([(a, b)], b)
findRestrictive a
n b
r [] [(a, b)]
rs in
(a
n, b
rig) forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)]
combineRig [(a, b)]
rs'
findRestrictive :: a -> b -> [(a, b)] -> [(a, b)] -> ([(a, b)], b)
findRestrictive a
n b
r [(a, b)]
acc [] = ([(a, b)]
acc, b
r)
findRestrictive a
n b
r [(a, b)]
acc ((a
n', b
r') : [(a, b)]
rs)
| a
n forall a. Eq a => a -> a -> Bool
== a
n' = a -> b -> [(a, b)] -> [(a, b)] -> ([(a, b)], b)
findRestrictive a
n (forall a. Ord a => a -> a -> a
max b
r b
r') [(a, b)]
acc [(a, b)]
rs
| Bool
otherwise = a -> b -> [(a, b)] -> [(a, b)] -> ([(a, b)], b)
findRestrictive a
n b
r ((a
n', b
r') forall a. a -> [a] -> [a]
: [(a, b)]
acc) [(a, b)]
rs
findLinear RigCount
rig IState
ist [Name]
env (App AppStatus Name
_ Type
f Type
a)
= forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ RigCount -> IState -> [Name] -> Type -> [(Name, RigCount)]
findLinear RigCount
rig IState
ist [Name]
env Type
f forall a. [a] -> [a] -> [a]
++ RigCount -> IState -> [Name] -> Type -> [(Name, RigCount)]
findLinear RigCount
rig IState
ist [Name]
env Type
a
findLinear RigCount
rig IState
ist [Name]
env (Bind Name
n Binder Type
b Type
sc) = RigCount -> IState -> [Name] -> Type -> [(Name, RigCount)]
findLinear RigCount
rig IState
ist (Name
n forall a. a -> [a] -> [a]
: [Name]
env) Type
sc
findLinear RigCount
rig IState
ist [Name]
_ Type
_ = []
setLinear :: [(Name, RigCount)] -> Term -> Term
setLinear :: [(Name, RigCount)] -> Type -> Type
setLinear [(Name, RigCount)]
ns (Bind Name
n b :: Binder Type
b@(PVar RigCount
r Type
t) Type
sc)
| Just RigCount
r <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, RigCount)]
ns = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (forall b. RigCount -> b -> Binder b
PVar RigCount
r Type
t) ([(Name, RigCount)] -> Type -> Type
setLinear [(Name, RigCount)]
ns Type
sc)
| Bool
otherwise = forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n Binder Type
b ([(Name, RigCount)] -> Type -> Type
setLinear [(Name, RigCount)]
ns Type
sc)
setLinear [(Name, RigCount)]
ns Type
tm = Type
tm
linearArg :: Type -> Bool
linearArg :: Type -> Bool
linearArg (Bind Name
n (Pi RigCount
Rig1 Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc) = Bool
True
linearArg (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
sc) = Type -> Bool
linearArg Type
sc
linearArg Type
_ = Bool
False
pruneByType :: Bool ->
Env -> Term ->
Type ->
IState -> [PTerm] -> [PTerm]
pruneByType :: Bool -> Env -> Type -> Type -> IState -> [PTerm] -> [PTerm]
pruneByType Bool
imp Env
env Type
t Type
goalty IState
c [PTerm]
as
| Just PTerm
a <- [PTerm] -> Maybe PTerm
locallyBound [PTerm]
as = [PTerm
a]
where
locallyBound :: [PTerm] -> Maybe PTerm
locallyBound [] = forall a. Maybe a
Nothing
locallyBound (PTerm
t:[PTerm]
ts)
| Just Name
n <- PTerm -> Maybe Name
getName PTerm
t,
Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env = forall a. a -> Maybe a
Just PTerm
t
| Bool
otherwise = [PTerm] -> Maybe PTerm
locallyBound [PTerm]
ts
getName :: PTerm -> Maybe Name
getName (PRef FC
_ [FC]
_ Name
n) = forall a. a -> Maybe a
Just Name
n
getName (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
l)) [PArg
_, PArg
_, PArg
arg])
| Text
l forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = PTerm -> Maybe Name
getName (forall t. PArg' t -> t
getTm PArg
arg)
getName (PApp FC
_ PTerm
f [PArg]
_) = PTerm -> Maybe Name
getName PTerm
f
getName (PHidden PTerm
t) = PTerm -> Maybe Name
getName PTerm
t
getName PTerm
_ = forall a. Maybe a
Nothing
pruneByType Bool
imp Env
env (P NameType
_ Name
n Type
_) Type
goalty IState
ist [PTerm]
as
| Maybe Type
Nothing <- Name -> Context -> Maybe Type
lookupTyExact Name
n Context
ctxt = [PTerm]
as
| Just (Maybe Name, Int, [Name], Bool, Bool)
_ <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) = [PTerm]
as
| Bool
otherwise
= let asV :: [PTerm]
asV = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Name -> PTerm -> Bool
headIs Bool
True Name
n) [PTerm]
as
as' :: [PTerm]
as' = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Name -> PTerm -> Bool
headIs Bool
False Name
n) [PTerm]
as in
case [PTerm]
as' of
[] -> [PTerm]
asV
[PTerm]
_ -> [PTerm]
as'
where
ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
ist
headIs :: Bool -> Name -> PTerm -> Bool
headIs Bool
var Name
f (PRef FC
_ [FC]
_ Name
f') = Bool -> Name -> Name -> Bool
typeHead Bool
var Name
f Name
f'
headIs Bool
var Name
f (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
l)) [PArg
_, PArg
_, PArg
arg])
| Text
l forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = Bool -> Name -> PTerm -> Bool
headIs Bool
var Name
f (forall t. PArg' t -> t
getTm PArg
arg)
headIs Bool
var Name
f (PApp FC
_ (PRef FC
_ [FC]
_ Name
f') [PArg]
_) = Bool -> Name -> Name -> Bool
typeHead Bool
var Name
f Name
f'
headIs Bool
var Name
f (PApp FC
_ PTerm
f' [PArg]
_) = Bool -> Name -> PTerm -> Bool
headIs Bool
var Name
f PTerm
f'
headIs Bool
var Name
f (PPi Plicity
_ Name
_ FC
_ PTerm
_ PTerm
sc) = Bool -> Name -> PTerm -> Bool
headIs Bool
var Name
f PTerm
sc
headIs Bool
var Name
f (PHidden PTerm
t) = Bool -> Name -> PTerm -> Bool
headIs Bool
var Name
f PTerm
t
headIs Bool
var Name
f PTerm
t = Bool
True
typeHead :: Bool -> Name -> Name -> Bool
typeHead Bool
var Name
f Name
f'
=
case Name -> Context -> Maybe Type
lookupTyExact Name
f' Context
ctxt of
Just Type
ty -> case forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
getRetTy Type
ty) of
(P NameType
_ Name
ctyn Type
_, [Type]
_) | Name -> Context -> Bool
isTConName Name
ctyn Context
ctxt Bool -> Bool -> Bool
&& Bool -> Bool
not (Name
ctyn forall a. Eq a => a -> a -> Bool
== Name
f)
-> Bool
False
(Type, [Type])
_ -> let ty' :: Type
ty' = Context -> Env -> Type -> Type
normalise Context
ctxt [] Type
ty in
case forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
getRetTy Type
ty') of
(V Int
_, [Type]
_) ->
IState -> Bool -> Env -> Name -> Type -> Bool
isPlausible IState
ist Bool
var Env
env Name
n Type
ty
(Type, [Type])
_ -> Bool -> Type -> Type -> Bool
matchingTypes Bool
imp (forall n. TT n -> TT n
getRetTy Type
ty') Type
goalty
Bool -> Bool -> Bool
|| Type -> Type -> Bool
isCoercion (forall n. TT n -> TT n
getRetTy Type
ty') Type
goalty
Maybe Type
_ -> Bool
False
matchingTypes :: Bool -> Type -> Type -> Bool
matchingTypes Bool
True = Type -> Type -> Bool
matchingHead
matchingTypes Bool
False = Type -> Type -> Bool
matching
matching :: Type -> Type -> Bool
matching (P NameType
_ Name
ctyn Type
_) (P NameType
_ Name
n' Type
_)
| Name -> Context -> Bool
isTConName Name
n' Context
ctxt Bool -> Bool -> Bool
&& Name -> Context -> Bool
isTConName Name
ctyn Context
ctxt = Name
ctyn forall a. Eq a => a -> a -> Bool
== Name
n'
| Bool
otherwise = Bool
True
matching (V Int
_) Type
_ = Bool
True
matching Type
_ (V Int
_) = Bool
True
matching Type
_ (P NameType
_ Name
n Type
_) = Bool -> Bool
not (Name -> Context -> Bool
isTConName Name
n Context
ctxt)
matching (P NameType
_ Name
n Type
_) Type
_ = Bool -> Bool
not (Name -> Context -> Bool
isTConName Name
n Context
ctxt)
matching (Bind Name
n Binder Type
_ Type
sc) Type
_ = Bool
True
matching Type
_ (Bind Name
n Binder Type
_ Type
sc) = Bool
True
matching apl :: Type
apl@(App AppStatus Name
_ Type
_ Type
_) apr :: Type
apr@(App AppStatus Name
_ Type
_ Type
_)
| (P NameType
_ Name
fl Type
_, [Type]
argsl) <- forall n. TT n -> (TT n, [TT n])
unApply Type
apl,
(P NameType
_ Name
fr Type
_, [Type]
argsr) <- forall n. TT n -> (TT n, [TT n])
unApply Type
apr
= Name
fl forall a. Eq a => a -> a -> Bool
== Name
fr Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Bool
matching [Type]
argsl [Type]
argsr)
Bool -> Bool -> Bool
|| (Bool -> Bool
not (Name -> Context -> Bool
isConName Name
fl Context
ctxt Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
fr Context
ctxt))
matching (App AppStatus Name
_ Type
f Type
a) (App AppStatus Name
_ Type
f' Type
a') = Bool
True
matching (TType UExp
_) (TType UExp
_) = Bool
True
matching (UType Universe
_) (UType Universe
_) = Bool
True
matching Type
l Type
r = Type
l forall a. Eq a => a -> a -> Bool
== Type
r
matchingHead :: Type -> Type -> Bool
matchingHead apl :: Type
apl@(App AppStatus Name
_ Type
_ Type
_) apr :: Type
apr@(App AppStatus Name
_ Type
_ Type
_)
| (P NameType
_ Name
fl Type
_, [Type]
argsl) <- forall n. TT n -> (TT n, [TT n])
unApply Type
apl,
(P NameType
_ Name
fr Type
_, [Type]
argsr) <- forall n. TT n -> (TT n, [TT n])
unApply Type
apr,
Name -> Context -> Bool
isConName Name
fl Context
ctxt Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
fr Context
ctxt
= Name
fl forall a. Eq a => a -> a -> Bool
== Name
fr
matchingHead Type
_ Type
_ = Bool
True
isCoercion :: Type -> Type -> Bool
isCoercion Type
rty Type
gty | (P NameType
_ Name
r Type
_, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
rty
= Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Name -> Type -> [Name]
getCoercionsBetween Name
r Type
gty))
isCoercion Type
_ Type
_ = Bool
False
getCoercionsBetween :: Name -> Type -> [Name]
getCoercionsBetween :: Name -> Type -> [Name]
getCoercionsBetween Name
r Type
goal
= let cs :: [Name]
cs = IState -> Type -> [Name]
getCoercionsTo IState
ist Type
goal in
forall {t}. t -> [Name] -> [Name]
findCoercions Name
r [Name]
cs
where findCoercions :: t -> [Name] -> [Name]
findCoercions t
t [] = []
findCoercions t
t (Name
n : [Name]
ns) =
let ps :: [Name]
ps = case Name -> Context -> [Type]
lookupTy Name
n (IState -> Context
tt_ctxt IState
ist) of
[Type
ty'] -> let as :: [Type]
as = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (forall n. TT n -> [(n, TT n)]
getArgTys (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] Type
ty')) in
[Name
n | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
useR [Type]
as]
[Type]
_ -> [] in
[Name]
ps forall a. [a] -> [a] -> [a]
++ t -> [Name] -> [Name]
findCoercions t
t [Name]
ns
useR :: Type -> Bool
useR Type
ty =
case forall n. TT n -> (TT n, [TT n])
unApply (forall n. TT n -> TT n
getRetTy Type
ty) of
(P NameType
_ Name
t Type
_, [Type]
_) -> Name
t forall a. Eq a => a -> a -> Bool
== Name
r
(Type, [Type])
_ -> Bool
False
pruneByType Bool
_ Env
_ Type
t Type
_ IState
_ [PTerm]
as = [PTerm]
as
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
isPlausible IState
ist Bool
var Env
env Name
n Type
ty
= let (Maybe Name
hvar, [(Type, [Name])]
_) = [Name]
-> [(Type, [Name])] -> Type -> (Maybe Name, [(Type, [Name])])
collectConstraints [] [] Type
ty in
case Maybe Name
hvar of
Maybe Name
Nothing -> Bool
True
Just Name
rth -> Bool
var
where
collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->
(Maybe Name, [(Term, [Name])])
collectConstraints :: [Name]
-> [(Type, [Name])] -> Type -> (Maybe Name, [(Type, [Name])])
collectConstraints [Name]
env [(Type, [Name])]
tcs (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ Type
ty Type
_) Type
sc)
= let tcs' :: [(Type, [Name])]
tcs' = case forall n. TT n -> (TT n, [TT n])
unApply Type
ty of
(P NameType
_ Name
c Type
_, [Type]
_) ->
case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
c (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
Just InterfaceInfo
tc -> ((Type
ty, forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
tc))
forall a. a -> [a] -> [a]
: [(Type, [Name])]
tcs)
Maybe InterfaceInfo
Nothing -> [(Type, [Name])]
tcs
(Type, [Type])
_ -> [(Type, [Name])]
tcs
in
[Name]
-> [(Type, [Name])] -> Type -> (Maybe Name, [(Type, [Name])])
collectConstraints (Name
n forall a. a -> [a] -> [a]
: [Name]
env) [(Type, [Name])]
tcs' Type
sc
collectConstraints [Name]
env [(Type, [Name])]
tcs Type
t
| (V Int
i, [Type]
_) <- forall n. TT n -> (TT n, [TT n])
unApply Type
t = (forall a. a -> Maybe a
Just ([Name]
env forall a. [a] -> Int -> a
!! Int
i), [(Type, [Name])]
tcs)
| Bool
otherwise = (forall a. Maybe a
Nothing, [(Type, [Name])]
tcs)