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