{-|
Module      : Idris.Elab.Utils
Description : Elaborator utilities.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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 -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

         Context
ctxt <- Idris Context
getContext
         Raw
t' <- case Type -> Maybe Raw
safeForget Type
t of
                    Just Raw
ft -> Raw -> StateT IState (ExceptT Err IO) Raw
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Raw
ft
                    Maybe Raw
Nothing -> TC Raw -> StateT IState (ExceptT Err IO) Raw
forall a. TC a -> Idris a
tclift (TC Raw -> StateT IState (ExceptT Err IO) Raw)
-> TC Raw -> StateT IState (ExceptT Err IO) Raw
forall a b. (a -> b) -> a -> b
$ Err -> TC Raw
forall a. Err -> TC a
tfail (Err -> TC Raw) -> Err -> TC Raw
forall a b. (a -> b) -> a -> b
$ Err -> Err
mkerr (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Type -> Err
forall t. t -> Err' t
IncompleteTerm Type
t))
         (Type
tm, Type
ty, UCs
cs) <- TC (Type, Type, UCs) -> Idris (Type, Type, UCs)
forall a. TC a -> Idris a
tclift (TC (Type, Type, UCs) -> Idris (Type, Type, UCs))
-> TC (Type, Type, UCs) -> Idris (Type, Type, UCs)
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 -> Err -> TC (Type, Type, UCs)
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err
mkerr Err
e))
                                   OK (Type, Type, UCs)
x -> (Type, Type, UCs) -> TC (Type, Type, UCs)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type, Type, UCs)
x
         Int -> String -> Idris ()
logElab Int
6 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"CONSTRAINTS ADDED: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Type, Type, UCs) -> String
forall a. Show a => a -> String
show (Type
tm, Type
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_ (\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) (Type -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Type
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) (Type -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Type
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) (Type -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Type
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) (Type -> [Name]
forall n. Eq n => TT n -> [n]
allTTNames Type
ty)

         (Type, Type) -> StateT IState (ExceptT Err IO) (Type, Type)
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just 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 String
"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
                                         String
"" -> OutputDoc
forall a. Doc a
Util.Pretty.empty
                                         String
_ -> 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 Name
n = do
  Maybe String
r <- Name -> Idris (Maybe String)
getFragile Name
n
  case Maybe String
r of
    Maybe String
Nothing -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just 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 String
"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
                          String
"" -> OutputDoc
forall a. Doc a
Util.Pretty.empty
                          String
_  -> 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 -> 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 [] = [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
forall a. a -> StateT IState (ExceptT Err IO) a
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Rechecking deferred name " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, Type, Bool) -> String
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
                    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, 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
                    [(Name, (Int, Maybe Name, Type, [Name]))]
-> Idris [(Name, (Int, Maybe Name, Type, [Name]))]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name
n, (Int
i, Maybe Name
top, Type
t', [Name]
psns)) (Name, (Int, Maybe Name, Type, [Name]))
-> [(Name, (Int, Maybe Name, Type, [Name]))]
-> [(Name, (Int, Maybe Name, Type, [Name]))]
forall a. a -> [a] -> [a]
: [(Name, (Int, Maybe Name, Type, [Name]))]
ns')

-- | Get the list of (index, name) of inaccessible arguments from an elaborated
-- type
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) (Int, Name) -> [(Int, Name)] -> [(Int, Name)]
forall a. a -> [a] -> [a]
: Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
sc [Bool]
ins
    | Bool
otherwise = Int -> Type -> [Bool] -> [(Int, Name)]
inaccessibleImps (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
sc [Bool]
ins
inaccessibleImps Int
_ Type
_ [Bool]
_ = []

-- | Get the list of (index, name) of inaccessible arguments from the type.
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 ArgOpt -> [ArgOpt] -> Bool
forall a. Eq a => a -> [a] -> 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
+Int
1) PTerm
t  -- an .{erased : Implicit}
    | Bool
otherwise
        = Int -> PTerm -> [(Int, Name)]
inaccessibleArgs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) PTerm
t      -- a {regular : Implicit}
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"CASE BLOCK: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, PDecl) -> String
forall a. Show a => a -> String
show (Name
n, PDecl
d)
             -- propagate totality assertion to the new definitions
             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 FnOpt
AssertTotal = Bool
True
    propagatable FnOpt
Inlinable = Bool
True
    propagatable FnOpt
_ = Bool
False

-- | Check that the result of type checking matches what the programmer wrote
-- (i.e. - if we inferred any arguments that the user provided, make sure
-- they are the same!)
checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred FC
fc PTerm
inf PTerm
user =
     do Int -> String -> Idris ()
logElab Int
6 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Checked to\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
inf String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n\nFROM\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                     PTerm -> String
showTmImpls PTerm
user
        Int -> String -> Idris ()
logElab Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"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
            Either (PTerm, PTerm) [(Name, PTerm)]
_ -> () -> TC ()
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--             Left (x, y) -> tfail $ At fc
--                                     (Msg $ "The type-checked term and given term do not match: "
--                                            ++ show x ++ " and " ++ show y)
        Int -> String -> Idris ()
logElab Int
10 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Checked match"
--                           ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

-- | Return whether inferred term is different from given term
-- (as above, but return a Bool)
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Checked to\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PTerm -> String
showTmImpls PTerm
inf String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\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 [(Name, PTerm)]
vs -> Bool -> TC Bool
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
            Left (PTerm
x, PTerm
y) -> Bool -> TC Bool
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

-- | Check a PTerm against documentation and ensure that every documented
-- argument actually exists.  This must be run _after_ implicits have been
-- found, or it will give spurious errors.
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 = 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 Map Name a
as (PPi Plicity
_ Name
n FC
_ PTerm
_ 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 Map Name a
as PTerm
_ | Map Name a -> Bool
forall k a. Map k a -> Bool
Map.null Map Name a
as = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                | Bool
otherwise   = Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (String -> Err) -> String -> Idris ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err) -> (String -> Err) -> String -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$
                                String
"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] -> [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]
++ 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) = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
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)
   = 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 Name
n PTerm
t [PTerm]
as PTerm
w [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 Name
n PTerm
t [PTerm]
as PTerm
w Maybe (Name, FC)
pn [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 (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


-- if 't' is an interface application, assume its arguments are injective
pbinds :: IState -> Term -> ElabD ()
pbinds :: IState -> Type -> ElabD ()
pbinds IState
i (Bind Name
n (PVar RigCount
rig Type
t) Type
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 Type -> (Type, [Type])
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 Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
c (IState -> Ctxt InterfaceInfo
idris_interfaces IState
i) of
                                   [] -> () -> ElabD ()
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                   [InterfaceInfo]
_ -> -- interface, set as injective
                                        (Type -> ElabD ()) -> [Type] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> ElabD ()
forall {aux}. Type -> Elab' aux ()
setinjArg [Type]
args
              (Type, [Type])
_ -> () -> ElabD ()
forall a. a -> StateT (ElabState EState) TC a
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
_) = Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
setinj Name
n
        setinjArg Type
_ = () -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
pbinds IState
i Type
tm = () -> ElabD ()
forall a. a -> StateT (ElabState EState) TC a
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 = 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 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) (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 a
n (PVTy TT a
t) 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 TT a
_ = []

psolve :: TT n -> StateT (ElabState aux) TC ()
psolve (Bind n
n (PVar RigCount
_ TT n
t) TT n
sc) = do StateT (ElabState aux) TC ()
forall aux. Elab' aux ()
solve; TT n -> StateT (ElabState aux) TC ()
psolve TT n
sc
psolve TT n
tm = () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
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) (Name, PTerm) -> [(Name, PTerm)] -> [(Name, PTerm)]
forall a. a -> [a] -> [a]
: [(Name, Type)] -> Type -> [(Name, PTerm)]
pv' ((Name
n, Type
t) (Name, Type) -> [(Name, Type)] -> [(Name, Type)]
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)
    = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [] Type
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
            IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) [PArg' t]
is (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
            [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t of
                    (P NameType
_ Name
n Type
_, [Type]
_) -> if Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) [PArg' t]
is (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
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) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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 TypeInfo
t -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Type] -> [Name] -> [Int] -> [Name]
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
[TT a] -> t a -> [Int] -> [a]
paramNames [Type]
args [Name]
env (TypeInfo -> [Int]
param_pos TypeInfo
t) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
                            IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
                            IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
a
            Maybe TypeInfo
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] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
                             IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
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] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg' t]
is Type
f [Name] -> [Name] -> [Name]
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)
    = [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 a. Eq a => a -> t a -> Bool
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 []) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
            IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) t Name
ps (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
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) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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 TypeInfo
t -> [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Type] -> [Name] -> [Int] -> [Name]
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
[TT a] -> t a -> [Int] -> [a]
paramNames [Type]
args [Name]
env [Int
x | Int
x <- [Int
0..[Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args],
                                                     Bool -> Bool
not (Int
x Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> 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 -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
f [Name] -> [Name] -> [Name]
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 Name -> Ctxt FnInfo -> Maybe FnInfo
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 [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ [Type] -> [Name] -> [Int] -> [Name]
forall {t :: * -> *} {a}.
(Foldable t, Eq a) =>
[TT a] -> t a -> [Int] -> [a]
paramNames [Type]
args [Name]
env [Int
x | Int
x <- [Int
0..[Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
args],
                                                         Bool -> Bool
not (Int
x Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> 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 -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
f [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
                              IState -> [Name] -> t Name -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
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 -> Type -> [Name]
getFlexInType IState
i [Name]
env t Name
ps Type
f [Name] -> [Name] -> [Name]
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
_ = []

-- | Treat a name as a parameter if it appears in parameter positions in
-- types, and never in a non-parameter position in a (non-param) argument 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 = IState -> [Name] -> [PArg] -> Type -> [Name]
forall {t}. IState -> [Name] -> [PArg' t] -> Type -> [Name]
getFixedInType IState
i [Name]
env [PArg]
ps Type
t
                                 flex :: [Name]
flex = IState -> [Name] -> [Name] -> Type -> [Name]
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
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 [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ IState -> Type -> [Name]
getTCinj IState
i (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
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) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap,
      Name -> Bool
isTCName Name
n = (Type -> Maybe Name) -> [Type] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Type -> Maybe Name
forall {a}. TT a -> Maybe a
getInjName [Type]
args
    | Bool
otherwise = []
  where
    isTCName :: Name -> Bool
isTCName 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 InterfaceInfo
_ -> Bool
True
                      Maybe InterfaceInfo
_ -> Bool
False
    getInjName :: TT a -> Maybe a
getInjName TT a
t | (P NameType
_ a
x TT a
_, [TT a]
_) <- 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 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 = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ IState -> Type -> [Name]
getTCinj IState
i Type
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 a. Eq a => a -> [a] -> 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 [TT a]
args t a
env [] = []
paramNames [TT a]
args t a
env (Int
p : [Int]
ps)
   | [TT a] -> Int
forall a. [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. HasCallStack => [a] -> Int -> a
!!Int
p of
                          P NameType
_ a
n TT a
_ -> if a
n a -> t a -> Bool
forall a. Eq a => 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
_ -> [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

-- Get all the names with multiplicity '1' used in a partial proof term
getLinearUsed :: Context -> Term -> [Name]
getLinearUsed :: Context -> Type -> [Name]
getLinearUsed Context
ctxt Type
tm = State [Name] () -> [Name] -> [Name]
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) (Name, RigCount, Binder Type) -> 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) 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Bool)] -> Int
forall a. [a] -> 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. HasCallStack => [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. HasCallStack => [a] -> Int -> a
!!Int
1)) else () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    getLin Env
env [(Name, Bool)]
us (P NameType
_ Name
n Type
_)
       | Just 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 a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    getLin Env
env [(Name, Bool)]
us Type
_ = () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
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) = () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
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 = () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    use :: a -> m ()
use 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 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 = State [Name] () -> [Name] -> [Name]
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 (((Name, RigCount, Binder Type) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) (Binder Type -> Type
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)(Name, RigCount, Binder Type) -> 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) 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Name, Bool)] -> Int
forall a. [a] -> 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. HasCallStack => [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. HasCallStack => [a] -> Int -> a
!!Int
i)) else () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    getUniq Env
env [(Name, Bool)]
us (P NameType
_ Name
n Type
_)
       | Just 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 a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    getUniq Env
env [(Name, Bool)]
us Type
_ = () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    use :: a -> m ()
use 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 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 us (Pi _ _ t v) = do getUniq env us t; getUniq env us 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 = () -> State [Name] ()
forall a. a -> StateT [Name] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- getUniq env us (binderTy b)

-- In a functional application, return the names which are used
-- directly in a static position
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 (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
forall n. TT n
Erased) Type
sc)
getStaticNames IState
ist Type
tm
    | (P NameType
_ Name
fn Type
_, [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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 [Bool]
stpos -> [Type] -> [Bool] -> [Name]
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 a -> [a] -> [a]
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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] -> Type -> [Bool]
getStatics [Name]
ns Type
t
    | Bool
otherwise = Bool
False Bool -> [Bool] -> [Bool]
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)
    = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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 }) 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

-- Check that a name has the minimum required accessibility
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 -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just 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 -> TC ()
forall a. Err -> TC a
tfail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc
                                      (String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> String -> Err
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 -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                             String
" 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 -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
ref))
                              else () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()


-- | Find the type constructor arguments that are parameters, given a
-- list of constructor types.
--
-- Parameters are names which are unchanged across the structure.
-- They appear at least once in every constructor type, always appear
-- in the same argument position(s), and nothing else ever appears in those
-- argument positions.
findParams :: Name   -- ^ the name of the family that we are finding parameters for
           -> Type   -- ^ the type of the type constructor (normalised already)
           -> [Type] -- ^ the declared constructor types
           -> [Int]
findParams :: Name -> Type -> [Type] -> [Int]
findParams Name
tyn Type
famty [Type]
ts =
    let allapps :: [[[Maybe Name]]]
allapps = (Type -> [[Maybe Name]]) -> [Type] -> [[[Maybe Name]]]
forall a b. (a -> b) -> [a] -> [b]
map Type -> [[Maybe Name]]
getDataApp [Type]
ts
        -- do each constructor separately, then merge the results (names
        -- may change between constructors)
        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 ([Int]
x : [[Int]]
xs) = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Int
p -> ([Int] -> Bool) -> [[Int]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\[Int]
ps -> Int
p Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> 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 ([Maybe Name]
args : [[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 [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 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 [(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 ([(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 [] [Maybe a]
_ = []
        update [(a, Maybe a)]
_ [] = []
        update ((a
n, Just a
x) : [(a, Maybe a)]
as) (Just a
x' : [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 ((a
n, Maybe a
_) : [(a, Maybe a)]
as) (Maybe a
_ : [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 :: Type -> [[Maybe Name]]
getDataApp f :: Type
f@(App AppStatus Name
_ Type
_ Type
_)
        | (P NameType
_ Name
d Type
_, [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
f
               = if (Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tyn) then [[Type] -> [Type] -> [Maybe Name]
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 [[Maybe Name]] -> [[Maybe Name]] -> [[Maybe Name]]
forall a. [a] -> [a] -> [a]
++ Type -> [[Maybe Name]]
getDataApp (Type -> Type -> Type
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n Type
t) Type
sc)
    getDataApp Type
_ = []

    -- keep the arguments which are single names, which appear
    -- in the return type, counting only the first time they appear in
    -- the return type as the parameter position
    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)
           | Bool -> a -> [TT a] -> Bool
forall {a}. Eq a => Bool -> a -> [TT a] -> 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 -> 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 a -> a -> Bool
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 a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TT a -> [a]
forall n. Eq n => TT n -> [n]
freeNames TT a
t = Bool
False -- not a single name
                   | Bool
otherwise = Bool -> a -> [TT a] -> Bool
paramIn Bool
ok a
n [TT a]
ts

              -- If the name appears again later, don't count that appearance
              -- as a parameter position
              noN :: a -> TT a -> Bool
noN a
n (P NameType
_ a
t TT a
_) = a
n a -> a -> Bool
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) = 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

-- | Mark a name as detaggable in the global state (should be called
-- for type and constructor names of single-constructor datatypes)
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 Name -> Ctxt OptInfo -> [OptInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n Ctxt OptInfo
opt of
        [OptInfo
oi] -> IState -> Idris ()
putIState IState
ist { idris_optimisation = addDef n oi { detaggable = True } opt }
        [OptInfo]
_    -> IState -> Idris ()
putIState IState
ist { idris_optimisation = addDef n (Optimise [] True []) opt }

displayWarnings :: EState -> Idris ()
displayWarnings :: EState -> Idris ()
displayWarnings 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, 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]
++ String
" is bound as an implicit\n"
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\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]
++ String
"?"
        FC -> OutputDoc -> Idris ()
iWarn FC
fc (IState -> Err -> OutputDoc
pprintErr IState
ist (String -> Err
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 <- PArg -> PTerm
forall t. PArg' t -> t
getTm PArg
t,
                Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ps,
                Bool -> Bool
not (Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
bound)
                    = PArg
t { getTm = PPatvar NoFC n } PArg -> [PArg] -> [PArg]
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 PArg -> [PArg] -> [PArg]
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 Name -> Ctxt [PArg] -> [[PArg]]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt [PArg]
idris_implicits IState
i) of
            [[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 (\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')
            [[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 Name -> Name -> Bool
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

-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
-- them in a canonical order
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) = AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f ([(Name, Binder Type)] -> Type -> Type
op [] Type
a) -- for Infer terms

    op [(Name, Binder Type)]
ps (Bind Name
n (PVar RigCount
r Type
t) Type
sc) = [(Name, Binder Type)] -> Type -> Type
op ((Name
n, RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
PVar RigCount
r Type
t) (Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
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, Type -> Binder Type
forall b. b -> Binder b
Hole Type
t) (Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
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, RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i Type
t Type
k) (Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
forall a. a -> [a] -> [a]
: [(Name, Binder Type)]
ps) Type
sc
    op [(Name, Binder Type)]
ps Type
sc = [(Name, Binder Type)] -> Type -> Type
forall n. [(n, Binder (TT n))] -> TT n -> TT n
bindAll ([(Name, Binder Type)] -> [(Name, Binder Type)]
sortP [(Name, Binder Type)]
ps) Type
sc

    -- Keep explicit Pi in the same order, insert others as necessary,
    -- Pi as early as possible, Hole as late as possible
    sortP :: [(Name, Binder Type)] -> [(Name, Binder Type)]
sortP [(Name, Binder Type)]
ps = let ([(Name, Binder Type)]
exps, [(Name, Binder Type)]
imps) = ((Name, Binder Type) -> Bool)
-> [(Name, Binder Type)]
-> ([(Name, Binder Type)], [(Name, Binder Type)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Name, Binder Type) -> Bool
forall {a} {b}. (a, Binder b) -> Bool
isExp [(Name, Binder Type)]
ps in
               [(Name, Binder Type)]
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
pick ([(Name, Binder Type)] -> [(Name, Binder Type)]
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)]
    -- if 't' uses any of the names which appear later, insert it later
    insert Name
n Binder Type
t rest :: [(Name, Binder Type)]
rest@((Name
n', Binder Type
t') : [(Name, Binder Type)]
ps)
        | (Name -> Bool) -> [Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Name
x -> Name
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Type -> [Name]
refsIn (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
t)) (Name
n' Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ((Name, Binder Type) -> Name) -> [(Name, Binder Type)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Binder Type) -> Name
forall a b. (a, b) -> a
fst [(Name, Binder Type)]
ps)
              = (Name
n', Binder Type
t') (Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
forall a. a -> [a] -> [a]
: Name
-> Binder Type -> [(Name, Binder Type)] -> [(Name, Binder Type)]
insert Name
n Binder Type
t [(Name, Binder Type)]
ps
        -- otherwise it's fine where it is (preserve ordering)
        | Bool
otherwise = (Name
n, Binder Type
t) (Name, Binder Type)
-> [(Name, Binder Type)] -> [(Name, Binder Type)]
forall a. a -> [a] -> [a]
: [(Name, Binder Type)]
rest

-- Make sure all the pattern bindings are as far out as possible
liftPats :: Term -> Term
liftPats :: Type -> Type
liftPats Type
tm = let (Type
tm', [(Name, Type)]
ps) = State [(Name, Type)] Type
-> [(Name, Type)] -> (Type, [(Name, Type)])
forall s a. State s a -> s -> (a, s)
runState (Type -> State [(Name, Type)] Type
getPats Type
tm) [] in
                  Type -> Type
orderPats (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [(Name, Type)] -> Type -> Type
forall {n}. Eq n => [(n, TT n)] -> TT n -> TT n
bindPats ([(Name, Type)] -> [(Name, Type)]
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 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 :: Type -> State [(Name, Type)] Type
getPats (Bind Name
n (PVar RigCount
_ Type
t) Type
sc) = do [(Name, Type)]
ps <- StateT [(Name, Type)] Identity [(Name, Type)]
forall s (m :: * -> *). MonadState s m => m s
get
                                        [(Name, Type)] -> StateT [(Name, Type)] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((Name
n, Type
t) (Name, Type) -> [(Name, Type)] -> [(Name, Type)]
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
                                         Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Type -> Type -> Binder Type
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
                                           Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Type -> Binder Type
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
                                            Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Maybe ImplicitInfo -> Type -> Type -> Binder Type
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
                                       Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
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
                                      Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (Type -> Binder Type
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
                             Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s Type
f' Type
a')
    getPats Type
t = Type -> State [(Name, Type)] Type
forall a. a -> StateT [(Name, Type)] Identity a
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) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty,
      Just TypeInfo
tyinfo <- Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tyname Ctxt TypeInfo
tyctxt
      -- Compare all the constructor types against the type we need
      -- If they *all* have an argument position where some constructor
      -- clashes with the needed type, then the type we're looking for must
      -- be empty
         = let neededty :: Type
neededty = Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty
               contys :: [Type]
contys = (Name -> Maybe Type) -> [Name] -> [Type]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Name -> Maybe Type
getConType (TypeInfo -> [Name]
con_names TypeInfo
tyinfo) in
                 (Type -> Bool) -> [Type] -> Bool
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
                      Type -> Maybe Type
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type
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]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
l,
         (P NameType
_ Name
n' Type
_, [Type]
_) <- Type -> (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 Name -> Name -> Bool
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

-- Find names which are applied to a function in a Rig1/Rig0 position
-- 'rig' is the multiplicity of the outer argument. When we go under a
-- function application, multiply them (it only needs to be Rig1 if it's
-- a linear argument to a linear argument; it needs to be a Rig0 if it's
-- Rig0 at any level)
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) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
tm,
        Name
f Name -> [Name] -> Bool
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
           [(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
$ 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) (Name, RigCount) -> [(Name, RigCount)] -> [(Name, RigCount)]
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 [(Name, RigCount)] -> [(Name, RigCount)] -> [(Name, RigCount)]
forall a. [a] -> [a] -> [a]
++
               Type -> [Type] -> [(Name, RigCount)]
findLinArg (Context -> Env -> Type -> Type
whnf (IState -> Context
tt_ctxt IState
ist) [] (Type -> Type -> Type
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 [(Name, RigCount)] -> [(Name, RigCount)] -> [(Name, RigCount)]
forall a. [a] -> [a] -> [a]
++ Type -> [Type] -> [(Name, RigCount)]
findLinArg Type
ty [Type]
as
    findLinArg Type
_ [] = []

    -- If a name is used multiple times in a pattern, take the least restrictive
    -- use of it
    combineRig :: [(a, b)] -> [(a, b)]
combineRig [] = []
    combineRig ((a
n, b
r) : [(a, b)]
rs)
        = let ([(a, b)]
rs', 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 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 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 RigCount
rig IState
ist [Name]
env (App AppStatus Name
_ Type
f Type
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] -> Type -> [(Name, RigCount)]
findLinear RigCount
rig IState
ist [Name]
env Type
f [(Name, RigCount)] -> [(Name, RigCount)] -> [(Name, RigCount)]
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 Name -> [Name] -> [Name]
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 <- Name -> [(Name, RigCount)] -> Maybe RigCount
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, RigCount)]
ns = Name -> Binder Type -> Type -> Type
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> Type -> Binder Type
forall b. RigCount -> b -> Binder b
PVar RigCount
r Type
t) ([(Name, RigCount)] -> Type -> Type
setLinear [(Name, RigCount)]
ns Type
sc)
   | Bool
otherwise = Name -> Binder Type -> Type -> Type
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

-- Rule out alternatives that don't return the same type as the head of the goal
-- (If there are none left as a result, do nothing)
pruneByType :: Bool -> -- In an impossible clause
               Env -> Term -> -- head of the goal
               Type -> -- goal
               IState -> [PTerm] -> [PTerm]
-- if an alternative has a locally bound name at the head, take it
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 [] = Maybe PTerm
forall a. Maybe a
Nothing
    locallyBound (PTerm
t:[PTerm]
ts)
       | Just Name
n <- PTerm -> Maybe Name
getName PTerm
t,
         Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, RigCount, Binder Type) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder Type) -> 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 FC
_ [FC]
_ Name
n) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
    getName (PApp FC
_ (PRef FC
_ [FC]
_ (UN Text
l)) [PArg
_, PArg
_, PArg
arg]) -- ignore Delays
       | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = PTerm -> Maybe Name
getName (PArg -> PTerm
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
_ = Maybe Name
forall a. Maybe a
Nothing

-- 'n' is the name at the head of the goal type
pruneByType Bool
imp Env
env (P NameType
_ Name
n Type
_) Type
goalty IState
ist [PTerm]
as
-- if the goal type is polymorphic, keep everything
   | Maybe Type
Nothing <- Name -> Context -> Maybe Type
lookupTyExact Name
n Context
ctxt = [PTerm]
as
-- if the goal type is a ?metavariable, keep everything
   | Just (Maybe Name, Int, [Name], Bool, Bool)
_ <- 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]
_ -> [PTerm]
as'
  where
    ctxt :: Context
ctxt = IState -> Context
tt_ctxt IState
ist

    -- Get the function at the head of the alternative and see if it's
    -- a plausible match against the goal type. Keep if so. Also keep if
    -- there is a possible coercion to the goal type.
    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 Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay" = Bool -> Name -> PTerm -> Bool
headIs Bool
var Name
f (PArg -> PTerm
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 -- keep if it's not an application

    typeHead :: Bool -> Name -> Name -> Bool
typeHead Bool
var Name
f Name
f'
        = -- trace ("Trying " ++ show f' ++ " for " ++ show n) $
          case Name -> Context -> Maybe Type
lookupTyExact Name
f' Context
ctxt of
               Just Type
ty -> case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
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 Name -> Name -> Bool
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
--                                    trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty
--                                       ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $
                                     case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
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 (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty') Type
goalty
                                                 Bool -> Bool -> Bool
|| Type -> Type -> Bool
isCoercion (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty') Type
goalty
-- May be useful to keep for debugging purposes for a bit:
--                                                let res = matching (getRetTy ty') goalty in
--                                                   traceWhen (not res)
--                                                     ("Rejecting " ++ show (getRetTy ty', goalty)) res
               Maybe Type
_ -> Bool
False

    matchingTypes :: Bool -> Type -> Type -> Bool
matchingTypes Bool
True = Type -> Type -> Bool
matchingHead
    matchingTypes Bool
False = Type -> Type -> Bool
matching

    -- If the goal is a constructor, it must match the suggested function type
    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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n'
         | Bool
otherwise = Bool
True
    -- Variables match anything
    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)
    -- Binders are a plausible match, so keep them
    matching (Bind Name
n Binder Type
_ Type
sc) Type
_ = Bool
True
    matching Type
_ (Bind Name
n Binder Type
_ Type
sc) = Bool
True
    -- If we hit a function name, it's a plausible match
    matching apl :: Type
apl@(App AppStatus Name
_ Type
_ Type
_) apr :: Type
apr@(App AppStatus Name
_ Type
_ Type
_)
         | (P NameType
_ Name
fl Type
_, [Type]
argsl) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
apl,
           (P NameType
_ Name
fr Type
_, [Type]
argsr) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
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 ((Type -> Type -> Bool) -> [Type] -> [Type] -> [Bool]
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))
    -- If the application structures aren't easily comparable, it's a
    -- plausible match
    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 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
r

    -- In impossible-case mode, only look at the heads (this is to account for
    -- the non type-directed case with 'impossible' - we'd be ruling out
    -- too much and wouldn't find the mismatch we're looking for)
    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) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
apl,
           (P NameType
_ Name
fr Type
_, [Type]
argsr) <- Type -> (Type, [Type])
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
fr
    matchingHead Type
_ Type
_ = Bool
True

    -- Return whether there is a possible coercion between the return type
    -- of an alternative and the goal type
    isCoercion :: Type -> Type -> Bool
isCoercion Type
rty Type
gty | (P NameType
_ Name
r Type
_, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
rty
            = Bool -> Bool
not ([Name] -> Bool
forall a. [a] -> Bool
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
             Name -> [Name] -> [Name]
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 = ((Name, Type) -> Type) -> [(Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Type) -> Type
forall a b. (a, b) -> b
snd (Type -> [(Name, Type)]
forall n. TT n -> [(n, TT n)]
getArgTys (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) [] Type
ty')) in
                                            [Name
n | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
useR [Type]
as]
                               [Type]
_ -> [] in
                     [Name]
ps [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ t -> [Name] -> [Name]
findCoercions t
t [Name]
ns

              useR :: Type -> Bool
useR Type
ty =
                  case Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty) of
                       (P NameType
_ Name
t Type
_, [Type]
_) -> Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
r
                       (Type, [Type])
_ -> Bool
False


pruneByType Bool
_ Env
_ Type
t Type
_ IState
_ [PTerm]
as = [PTerm]
as

-- Could the name feasibly be the return type?
-- If there is an interface constraint on the return type, and no implementation
-- in the environment or globally for that name, then no
-- Otherwise, yes
-- (FIXME: This isn't complete, but I'm leaving it here and coming back
-- to it later - just returns 'var' for now. EB)
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 -- trace (show (rth, interfaces)) 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 Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty of
                           (P NameType
_ Name
c Type
_, [Type]
_) ->
                               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 InterfaceInfo
tc -> ((Type
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))
                                                     (Type, [Name]) -> [(Type, [Name])] -> [(Type, [Name])]
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 Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) [(Type, [Name])]
tcs' Type
sc
     collectConstraints [Name]
env [(Type, [Name])]
tcs Type
t
         | (V Int
i, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t = (Name -> Maybe Name
forall a. a -> Maybe a
Just ([Name]
env [Name] -> Int -> Name
forall a. HasCallStack => [a] -> Int -> a
!! Int
i), [(Type, [Name])]
tcs)
         | Bool
otherwise = (Maybe Name
forall a. Maybe a
Nothing, [(Type, [Name])]
tcs)