{-|
Module      : Idris.ProofSearch
Description : Searches current context for proofs'

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE PatternGuards #-}

module Idris.ProofSearch(
    trivial
  , trivialHoles
  , proofSearch
  , resolveTC
  ) where

import Idris.AbsSyntax
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Unify
import Idris.Delaborate

import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import qualified Data.Set as S

-- Pass in a term elaborator to avoid a cyclic dependency with ElabTerm

trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
trivial = [Name]
-> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles [] []

trivialHoles :: [Name] -> -- user visible names, when working
                          -- in interactive mode
                [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles :: [Name]
-> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles psnames :: [Name]
psnames ok :: [(Name, Int)]
ok elab :: PTerm -> ElabD ()
elab ist :: IState
ist
     = ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (do PTerm -> ElabD ()
elab (FC -> PTerm -> [PArg] -> PTerm
PApp (String -> FC
fileFC "prf") (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC "prf") [] Name
eqCon) [Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "A") PTerm
Placeholder Bool
False, Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "x") PTerm
Placeholder Bool
False])
                () -> ElabD ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
            (do Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
                Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
                Env -> ElabD ()
forall b. [(Name, b, Binder Type)] -> ElabD ()
tryAll Env
env
                () -> ElabD ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) Bool
True
      where
        tryAll :: [(Name, b, Binder Type)] -> ElabD ()
tryAll []     = String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "No trivial solution"
        tryAll ((x :: Name
x, _, b :: Binder Type
b):xs :: [(Name, b, Binder Type)]
xs)
           = do -- if type of x has any holes in it, move on
                [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
                -- anywhere but the top is okay for a hole, if holesOK set
                if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
                   ([Name] -> Type -> Bool
forall (t :: * -> *). Foldable t => t Name -> Type -> Bool
holesOK [Name]
hs (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b) Bool -> Bool -> Bool
&& ([Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
psnames Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
psnames))
                   then ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (PTerm -> ElabD ()
elab (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC "prf") [] Name
x))
                             ([(Name, b, Binder Type)] -> ElabD ()
tryAll [(Name, b, Binder Type)]
xs) Bool
True
                   else [(Name, b, Binder Type)] -> ElabD ()
tryAll [(Name, b, Binder Type)]
xs

        holesOK :: t Name -> Type -> Bool
holesOK hs :: t Name
hs ap :: Type
ap@(App _ _ _)
           | (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap
                = t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n 0 [Type]
args
        holesOK hs :: t Name
hs (App _ f :: Type
f a :: Type
a) = t Name -> Type -> Bool
holesOK t Name
hs Type
f Bool -> Bool -> Bool
&& t Name -> Type -> Bool
holesOK t Name
hs Type
a
        holesOK hs :: t Name
hs (P _ n :: Name
n _) = Bool -> Bool
not (Name
n Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
hs)
        holesOK hs :: t Name
hs (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = t Name -> Type -> Bool
holesOK t Name
hs (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b) Bool -> Bool -> Bool
&&
                                   t Name -> Type -> Bool
holesOK t Name
hs Type
sc
        holesOK hs :: t Name
hs _ = Bool
True

        holeArgsOK :: t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK hs :: t Name
hs n :: Name
n p :: Int
p [] = Bool
True
        holeArgsOK hs :: t Name
hs n :: Name
n p :: Int
p (a :: Type
a : as :: [Type]
as)
           | (Name
n, Int
p) (Name, Int) -> [(Name, Int)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Int)]
ok = t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [Type]
as
           | Bool
otherwise = t Name -> Type -> Bool
holesOK t Name
hs Type
a Bool -> Bool -> Bool
&& t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [Type]
as

trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialTCs ok :: [(Name, Int)]
ok elab :: PTerm -> ElabD ()
elab ist :: IState
ist
     = ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (do PTerm -> ElabD ()
elab (FC -> PTerm -> [PArg] -> PTerm
PApp (String -> FC
fileFC "prf") (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC "prf") [] Name
eqCon) [Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "A") PTerm
Placeholder Bool
False, Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN "x") PTerm
Placeholder Bool
False])
                () -> ElabD ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
            (do Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
                Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
                Env -> ElabD ()
forall b. [(Name, b, Binder Type)] -> ElabD ()
tryAll Env
env
                () -> ElabD ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) Bool
True
      where
        tryAll :: [(Name, b, Binder Type)] -> ElabD ()
tryAll []     = String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "No trivial solution"
        tryAll ((x :: Name
x, _, b :: Binder Type
b):xs :: [(Name, b, Binder Type)]
xs)
           = do -- if type of x has any holes in it, move on
                [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
                Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
                -- anywhere but the top is okay for a hole, if holesOK set
                if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))
                   ([Name] -> Type -> Bool
forall (t :: * -> *). Foldable t => t Name -> Type -> Bool
holesOK [Name]
hs (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b) Bool -> Bool -> Bool
&& Env -> Type -> Bool
tcArg Env
env (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b))
                   then ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (PTerm -> ElabD ()
elab (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC "prf") [] Name
x))
                             ([(Name, b, Binder Type)] -> ElabD ()
tryAll [(Name, b, Binder Type)]
xs) Bool
True
                   else [(Name, b, Binder Type)] -> ElabD ()
tryAll [(Name, b, Binder Type)]
xs

        tcArg :: Env -> Type -> Bool
tcArg env :: Env
env ty :: Type
ty
           | (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy (Context -> Env -> Type -> Type
normalise (IState -> Context
tt_ctxt IState
ist) Env
env Type
ty))
                 = case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                        Just _ -> Bool
True
                        _ -> Bool
False
           | Bool
otherwise = Bool
False

        holesOK :: t Name -> Type -> Bool
holesOK hs :: t Name
hs ap :: Type
ap@(App _ _ _)
           | (P _ n :: Name
n _, args :: [Type]
args) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ap
                = t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n 0 [Type]
args
        holesOK hs :: t Name
hs (App _ f :: Type
f a :: Type
a) = t Name -> Type -> Bool
holesOK t Name
hs Type
f Bool -> Bool -> Bool
&& t Name -> Type -> Bool
holesOK t Name
hs Type
a
        holesOK hs :: t Name
hs (P _ n :: Name
n _) = Bool -> Bool
not (Name
n Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
hs)
        holesOK hs :: t Name
hs (Bind n :: Name
n b :: Binder Type
b sc :: Type
sc) = t Name -> Type -> Bool
holesOK t Name
hs (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b) Bool -> Bool -> Bool
&&
                                   t Name -> Type -> Bool
holesOK t Name
hs Type
sc
        holesOK hs :: t Name
hs _ = Bool
True

        holeArgsOK :: t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK hs :: t Name
hs n :: Name
n p :: Int
p [] = Bool
True
        holeArgsOK hs :: t Name
hs n :: Name
n p :: Int
p (a :: Type
a : as :: [Type]
as)
           | (Name
n, Int
p) (Name, Int) -> [(Name, Int)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Name, Int)]
ok = t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [Type]
as
           | Bool
otherwise = t Name -> Type -> Bool
holesOK t Name
hs Type
a Bool -> Bool -> Bool
&& t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) [Type]
as

cantSolveGoal :: ElabD a
cantSolveGoal :: ElabD a
cantSolveGoal = do Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
                   Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
                   TC a -> ElabD a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> ElabD a) -> TC a -> ElabD a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (Err -> TC a) -> Err -> TC a
forall a b. (a -> b) -> a -> b
$
                      Type -> [(Name, Type)] -> Err
forall t. t -> [(Name, t)] -> Err' t
CantSolveGoal Type
g (((Name, RigCount, Binder Type) -> (Name, Type))
-> Env -> [(Name, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n,_,b :: Binder Type
b) -> (Name
n, Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)) Env
env)

proofSearch :: Bool -- ^ recursive search (False for 'refine')
            -> Bool -- ^ invoked from a tactic proof. If so, making new metavariables is meaningless, and there should be an error reported instead.
            -> Bool -- ^ ambiguity ok
            -> Bool -- ^ defer on failure
            -> Int  -- ^ maximum depth
            -> (PTerm -> ElabD ())
            -> Maybe Name
            -> Name
            -> [Name]
            -> [Name]
            -> IState
            -> ElabD ()
proofSearch :: Bool
-> Bool
-> Bool
-> Bool
-> Int
-> (PTerm -> ElabD ())
-> Maybe Name
-> Name
-> [Name]
-> [Name]
-> IState
-> ElabD ()
proofSearch False fromProver :: Bool
fromProver ambigok :: Bool
ambigok deferonfail :: Bool
deferonfail depth :: Int
depth elab :: PTerm -> ElabD ()
elab _ nroot :: Name
nroot psnames :: [Name]
psnames [fn :: Name
fn] ist :: IState
ist
       = do -- get all possible versions of the name, take the first one that
            -- works
            let all_imps :: [(Name, [PArg])]
all_imps = Name -> Ctxt [PArg] -> [(Name, [PArg])]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
fn (IState -> Ctxt [PArg]
idris_implicits IState
ist)
            [(Name, [PArg])] -> ElabD ()
forall t. [(Name, [PArg' t])] -> ElabD ()
tryAllFns [(Name, [PArg])]
all_imps
  where
    -- if nothing worked, make a new metavariable
    tryAllFns :: [(Name, [PArg' t])] -> ElabD ()
tryAllFns [] | Bool
fromProver = ElabD ()
forall a. ElabD a
cantSolveGoal
    tryAllFns [] = do ElabD ()
forall aux. Elab' aux ()
attack; [Name] -> [Name] -> Name -> Elab' EState Name
forall aux. [Name] -> [Name] -> Name -> Elab' aux Name
defer [] [] Name
nroot; ElabD ()
forall aux. Elab' aux ()
solve
    tryAllFns (f :: (Name, [PArg' t])
f : fs :: [(Name, [PArg' t])]
fs) = ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' ((Name, [PArg' t]) -> ElabD ()
forall t. (Name, [PArg' t]) -> ElabD ()
tryFn (Name, [PArg' t])
f) ([(Name, [PArg' t])] -> ElabD ()
tryAllFns [(Name, [PArg' t])]
fs) Bool
True

    tryFn :: (Name, [PArg' t]) -> ElabD ()
tryFn (f :: Name
f, args :: [PArg' t]
args) = do let imps :: [(Bool, Int)]
imps = (PArg' t -> (Bool, Int)) -> [PArg' t] -> [(Bool, Int)]
forall a b. (a -> b) -> [a] -> [b]
map PArg' t -> (Bool, Int)
forall t. PArg' t -> (Bool, Int)
isImp [PArg' t]
args
                         Fails
ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                         [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                         [Name]
args <- ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)] -> [Name])
-> StateT (ElabState EState) TC [(Name, Name)]
-> Elab' EState [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (ElabState EState) TC [(Name, Name)]
-> StateT (ElabState EState) TC [(Name, Name)]
-> Bool
-> StateT (ElabState EState) TC [(Name, Name)]
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (Raw -> [(Bool, Int)] -> StateT (ElabState EState) TC [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
f) [(Bool, Int)]
imps)
                                                  (Raw -> [(Bool, Int)] -> StateT (ElabState EState) TC [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
match_apply (Name -> Raw
Var Name
f) [(Bool, Int)]
imps) Bool
True
                         Fails
ps' <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
--                          when (length ps < length ps') $ fail "Can't apply constructor"
                         -- Make metavariables for new holes
                         [Name]
hs' <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                         Type
ptm <- Elab' EState Type
forall aux. Elab' aux Type
get_term
                         if Bool
fromProver then ElabD ()
forall a. ElabD a
cantSolveGoal
                           else do
                             (Name -> ElabD ()) -> [Name] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ h :: Name
h -> do Name -> ElabD ()
forall aux. Name -> Elab' aux ()
focus Name
h
                                              ElabD ()
forall aux. Elab' aux ()
attack; [Name] -> [Name] -> Name -> Elab' EState Name
forall aux. [Name] -> [Name] -> Name -> Elab' aux Name
defer [] [] Name
nroot; ElabD ()
forall aux. Elab' aux ()
solve)
                                 ([Name]
hs' [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
hs)
--                                  (filter (\ (x, y) -> not x) (zip (map fst imps) args))
                             ElabD ()
forall aux. Elab' aux ()
solve

    isImp :: PArg' t -> (Bool, Int)
isImp (PImp p :: Int
p _ _ _ _) = (Bool
True, Int
p)
    isImp arg :: PArg' t
arg = (Bool
True, PArg' t -> Int
forall t. PArg' t -> Int
priority PArg' t
arg) -- try to get all of them by unification
proofSearch rec :: Bool
rec fromProver :: Bool
fromProver ambigok :: Bool
ambigok deferonfail :: Bool
deferonfail maxDepth :: Int
maxDepth elab :: PTerm -> ElabD ()
elab fn :: Maybe Name
fn nroot :: Name
nroot psnames :: [Name]
psnames hints :: [Name]
hints ist :: IState
ist
       = do ElabD ()
forall aux. Elab' aux ()
compute
            Type
ty <- Elab' EState Type
forall aux. Elab' aux Type
goal
            [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
            Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
            Type
tm <- Elab' EState Type
forall aux. Elab' aux Type
get_term
            Bool
argsok <- Type -> StateT (ElabState EState) TC Bool
conArgsOK Type
ty
            if Bool
ambigok Bool -> Bool -> Bool
|| Bool
argsok then
               case Name -> Ctxt TIData -> [TIData]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
nroot (IState -> Ctxt TIData
idris_tyinfodata IState
ist) of
                    [TISolution ts :: [Type]
ts] -> [Type] -> ElabD ()
findInferredTy [Type]
ts
                    _ -> if Bool
ambigok then Bool -> Int -> [Name] -> Set Type -> ElabD ()
psRec Bool
rec Int
maxDepth [] Set Type
forall a. Set a
S.empty
                            -- postpone if it fails early in elaboration
                            else (Err -> Bool) -> ElabD () -> ElabD () -> ElabD ()
forall aux a.
(Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
handleError Err -> Bool
forall t. Err' t -> Bool
cantsolve
                                      (Bool -> Int -> [Name] -> Set Type -> ElabD ()
psRec Bool
rec Int
maxDepth [] Set Type
forall a. Set a
S.empty)
                                      (Name -> ElabD ()
forall aux. Name -> Elab' aux ()
autoArg (String -> Name
sUN "auto"))
               else Name -> ElabD ()
forall aux. Name -> Elab' aux ()
autoArg (String -> Name
sUN "auto") -- not enough info in the type yet
  where
    findInferredTy :: [Type] -> ElabD ()
findInferredTy (t :: Type
t : _) = PTerm -> ElabD ()
elab (IState -> Type -> PTerm
delab IState
ist (Type -> Type
toUN Type
t))

    cantsolve :: Err' t -> Bool
cantsolve (InternalMsg _) = Bool
True
    cantsolve (CantSolveGoal _ _) = Bool
True
    cantsolve (IncompleteTerm _) = Bool
True
    cantsolve (At _ e :: Err' t
e) = Err' t -> Bool
cantsolve Err' t
e
    cantsolve (Elaborating _ _ _ e :: Err' t
e) = Err' t -> Bool
cantsolve Err' t
e
    cantsolve (ElaboratingArg _ _ _ e :: Err' t
e) = Err' t -> Bool
cantsolve Err' t
e
    cantsolve err :: Err' t
err = Bool
False

    conArgsOK :: Type -> StateT (ElabState EState) TC Bool
conArgsOK ty :: Type
ty
       = let (f :: Type
f, as :: [Type]
as) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty in
           case Type
f of
              P _ n :: Name
n _ ->
                let autohints :: [Name]
autohints = case Name -> Ctxt [Name] -> Maybe [Name]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Name]
idris_autohints IState
ist) of
                                     Nothing -> []
                                     Just hs :: [Name]
hs -> [Name]
hs in
                    case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
                              Just t :: TypeInfo
t -> do [Bool]
rs <- (Name -> StateT (ElabState EState) TC Bool)
-> [Name] -> StateT (ElabState EState) TC [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Type] -> Name -> StateT (ElabState EState) TC Bool
conReady [Type]
as)
                                                      ([Name]
autohints [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ TypeInfo -> [Name]
con_names TypeInfo
t)
                                           Bool -> StateT (ElabState EState) TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
rs)
                              Nothing -> -- local variable, go for it
                                    Bool -> StateT (ElabState EState) TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
              TType _ -> Bool -> StateT (ElabState EState) TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
              _ -> Type -> StateT (ElabState EState) TC Bool
forall (t :: (* -> *) -> * -> *) a. MonadTrans t => Type -> t TC a
typeNotSearchable Type
ty

    conReady :: [Term] -> Name -> ElabD Bool
    conReady :: [Type] -> Name -> StateT (ElabState EState) TC Bool
conReady as :: [Type]
as n :: Name
n
       = case Name -> Context -> Maybe Type
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
              Just ty :: Type
ty -> do let (_, cs :: [Type]
cs) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty)
                            -- if any metavariables in 'as' correspond to
                            -- a constructor form in 'cs', then we're not
                            -- ready to run auto yet. Otherwise, go for it
                            [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                            Bool -> StateT (ElabState EState) TC Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> StateT (ElabState EState) TC Bool)
-> Bool -> StateT (ElabState EState) TC Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (((Type, Type) -> Bool) -> [(Type, Type)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map ([Name] -> (Type, Type) -> Bool
forall (t :: * -> *) a.
(Foldable t, Eq a) =>
t a -> (TT a, Type) -> Bool
notHole [Name]
hs) ([Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
as [Type]
cs))
              Nothing -> String -> StateT (ElabState EState) TC Bool
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't happen"

    -- if n is a metavariable, and c is a constructor form, we're not ready
    -- to run yet
    notHole :: t a -> (TT a, Type) -> Bool
notHole hs :: t a
hs (P _ n :: a
n _, c :: Type
c)
       | (P _ cn :: Name
cn _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
c,
         a
n a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
cn (IState -> Context
tt_ctxt IState
ist) = Bool
False
       | Constant _ <- Type
c = Bool -> Bool
not (a
n a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
hs)
    -- if fa is a metavariable applied to anything, we're not ready to run yet.
    notHole hs :: t a
hs (fa :: TT a
fa, c :: Type
c)
       | (P _ fn :: a
fn _, args :: [TT a]
args@(_:_)) <- TT a -> (TT a, [TT a])
forall n. TT n -> (TT n, [TT n])
unApply TT a
fa = a
fn a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` t a
hs
    notHole _ _ = Bool
True

    toUN :: Type -> Type
toUN t :: Type
t@(P nt :: NameType
nt (MN i :: Int
i n :: Text
n) ty :: Type
ty)
       | ('_':xs :: String
xs) <- Text -> String
str Text
n = Type
t
       | Bool
otherwise = NameType -> Name -> Type -> Type
forall n. NameType -> n -> TT n -> TT n
P NameType
nt (Text -> Name
UN Text
n) Type
ty
    toUN (App s :: AppStatus Name
s f :: Type
f a :: Type
a) = AppStatus Name -> Type -> Type -> Type
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s (Type -> Type
toUN Type
f) (Type -> Type
toUN Type
a)
    toUN t :: Type
t = Type
t

    -- psRec counts depth and the local variable applications we're under
    -- (so we don't try a pointless application of something to itself,
    -- which obviously won't work anyway but might lead us on a wild
    -- goose chase...)
    -- Also keep track of the types we've proved so far in this branch
    -- (if we get back to one we've been to before, we're just in a cycle and
    -- that's no use)
    psRec :: Bool -> Int -> [Name] -> S.Set Type -> ElabD ()
    psRec :: Bool -> Int -> [Name] -> Set Type -> ElabD ()
psRec _ 0 locs :: [Name]
locs tys :: Set Type
tys | Bool
fromProver = ElabD ()
forall a. ElabD a
cantSolveGoal
    psRec rec :: Bool
rec 0 locs :: [Name]
locs tys :: Set Type
tys = do ElabD ()
forall aux. Elab' aux ()
attack; [Name] -> [Name] -> Name -> Elab' EState Name
forall aux. [Name] -> [Name] -> Name -> Elab' aux Name
defer [] [] Name
nroot; ElabD ()
forall aux. Elab' aux ()
solve --fail "Maximum depth reached"
    psRec False d :: Int
d locs :: [Name]
locs tys :: Set Type
tys = Int -> [Name] -> Set Type -> [Name] -> ElabD ()
tryCons Int
d [Name]
locs Set Type
tys [Name]
hints
    psRec True d :: Int
d locs :: [Name]
locs tys :: Set Type
tys
                 = do ElabD ()
forall aux. Elab' aux ()
compute
                      Type
ty <- Elab' EState Type
forall aux. Elab' aux Type
goal
                      Bool -> ElabD () -> ElabD ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Type -> Set Type -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Type
ty Set Type
tys) (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Been here before"
                      let tys' :: Set Type
tys' = Type -> Set Type -> Set Type
forall a. Ord a => a -> Set a -> Set a
S.insert Type
ty Set Type
tys
                      ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' ([Name]
-> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles [Name]
psnames [] PTerm -> ElabD ()
elab IState
ist)
                                 (Bool
-> Bool
-> Int
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resolveTC Bool
False Bool
False 20 Type
ty Name
nroot PTerm -> ElabD ()
elab IState
ist)
                                 Bool
True)
                           (ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (Int -> [Name] -> Set Type -> ElabD ()
resolveByCon (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [Name]
locs Set Type
tys')
                                       (Int -> [Name] -> Set Type -> ElabD ()
resolveByLocals (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) [Name]
locs Set Type
tys')
                                 Bool
True)
             -- if all else fails, make a new metavariable
                         (if Bool
fromProver
                             then String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "cantSolveGoal"
                             else do ElabD ()
forall aux. Elab' aux ()
attack; [Name] -> [Name] -> Name -> Elab' EState Name
forall aux. [Name] -> [Name] -> Name -> Elab' aux Name
defer [] [] Name
nroot; ElabD ()
forall aux. Elab' aux ()
solve) Bool
True) Bool
True

    -- get recursive function name. Only user given names make sense.
    getFn :: Int -> Maybe Name -> [Name]
getFn d :: Int
d (Just f :: Name
f) | Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxDepthInt -> Int -> Int
forall a. Num a => a -> a -> a
-1 Bool -> Bool -> Bool
&& Name -> Bool
usersname Name
f = [Name
f]
                     | Bool
otherwise = []
    getFn d :: Int
d _ = []

    usersname :: Name -> Bool
usersname (UN _) = Bool
True
    usersname (NS n :: Name
n _) = Name -> Bool
usersname Name
n
    usersname _ = Bool
False

    resolveByCon :: Int -> [Name] -> Set Type -> ElabD ()
resolveByCon d :: Int
d locs :: [Name]
locs tys :: Set Type
tys
        = do Type
t <- Elab' EState Type
forall aux. Elab' aux Type
goal
             let (f :: Type
f, _) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t
             case Type
f of
                P _ n :: Name
n _ ->
                   do let autohints :: [Name]
autohints = case Name -> Ctxt [Name] -> Maybe [Name]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [Name]
idris_autohints IState
ist) of
                                           Nothing -> []
                                           Just hs :: [Name]
hs -> [Name]
hs
                      case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
ist) of
                          Just t :: TypeInfo
t -> do
                             let others :: [Name]
others = [Name]
hints [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ TypeInfo -> [Name]
con_names TypeInfo
t [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
autohints
                             Int -> [Name] -> Set Type -> [Name] -> ElabD ()
tryCons Int
d [Name]
locs Set Type
tys ([Name]
others [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Int -> Maybe Name -> [Name]
getFn Int
d Maybe Name
fn)
                          Nothing -> Type -> ElabD ()
forall (t :: (* -> *) -> * -> *) a. MonadTrans t => Type -> t TC a
typeNotSearchable Type
t
                _ -> Type -> ElabD ()
forall (t :: (* -> *) -> * -> *) a. MonadTrans t => Type -> t TC a
typeNotSearchable Type
t

    -- if there are local variables which have a function type, try
    -- applying them too
    resolveByLocals :: Int -> [Name] -> Set Type -> ElabD ()
resolveByLocals d :: Int
d locs :: [Name]
locs tys :: Set Type
tys
        = do Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
             Int -> [Name] -> Set Type -> Env -> ElabD ()
forall b.
Int -> [Name] -> Set Type -> [(Name, b, Binder Type)] -> ElabD ()
tryLocals Int
d [Name]
locs Set Type
tys Env
env

    tryLocals :: Int -> [Name] -> Set Type -> [(Name, b, Binder Type)] -> ElabD ()
tryLocals d :: Int
d locs :: [Name]
locs tys :: Set Type
tys [] = String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Locals failed"
    tryLocals d :: Int
d locs :: [Name]
locs tys :: Set Type
tys ((x :: Name
x, _, t :: Binder Type
t) : xs :: [(Name, b, Binder Type)]
xs)
       | Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
locs Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
psnames = Int -> [Name] -> Set Type -> [(Name, b, Binder Type)] -> ElabD ()
tryLocals Int
d [Name]
locs Set Type
tys [(Name, b, Binder Type)]
xs
       | Bool
otherwise = ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (Int -> [Name] -> Set Type -> Name -> Binder Type -> ElabD ()
tryLocal Int
d (Name
x Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
locs) Set Type
tys Name
x Binder Type
t)
                          (Int -> [Name] -> Set Type -> [(Name, b, Binder Type)] -> ElabD ()
tryLocals Int
d [Name]
locs Set Type
tys [(Name, b, Binder Type)]
xs) Bool
True

    tryCons :: Int -> [Name] -> Set Type -> [Name] -> ElabD ()
tryCons d :: Int
d locs :: [Name]
locs tys :: Set Type
tys [] = String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Constructors failed"
    tryCons d :: Int
d locs :: [Name]
locs tys :: Set Type
tys (c :: Name
c : cs :: [Name]
cs)
        = ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (Int -> [Name] -> Set Type -> Name -> ElabD ()
tryCon Int
d [Name]
locs Set Type
tys Name
c) (Int -> [Name] -> Set Type -> [Name] -> ElabD ()
tryCons Int
d [Name]
locs Set Type
tys [Name]
cs) Bool
True

    tryLocal :: Int -> [Name] -> Set Type -> Name -> Binder Type -> ElabD ()
tryLocal d :: Int
d locs :: [Name]
locs tys :: Set Type
tys n :: Name
n t :: Binder Type
t
          = do let a :: Int
a = PTerm -> Int
getPArity (IState -> Type -> PTerm
delab IState
ist (Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
t))
               Int -> [Name] -> Set Type -> Name -> Int -> ElabD ()
forall t.
(Eq t, Num t) =>
Int -> [Name] -> Set Type -> Name -> t -> ElabD ()
tryLocalArg Int
d [Name]
locs Set Type
tys Name
n Int
a

    tryLocalArg :: Int -> [Name] -> Set Type -> Name -> t -> ElabD ()
tryLocalArg d :: Int
d locs :: [Name]
locs tys :: Set Type
tys n :: Name
n 0 = PTerm -> ElabD ()
elab (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC "prf") [] Name
n)
    tryLocalArg d :: Int
d locs :: [Name]
locs tys :: Set Type
tys n :: Name
n i :: t
i
        = Bool -> ElabD () -> ElabD () -> String -> ElabD ()
forall aux.
Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
simple_app Bool
False (Int -> [Name] -> Set Type -> Name -> t -> ElabD ()
tryLocalArg Int
d [Name]
locs Set Type
tys Name
n (t
i t -> t -> t
forall a. Num a => a -> a -> a
- 1))
                (Bool -> Int -> [Name] -> Set Type -> ElabD ()
psRec Bool
True Int
d [Name]
locs Set Type
tys) "proof search local apply"

    -- Like interface resolution, but searching with constructors
    tryCon :: Int -> [Name] -> Set Type -> Name -> ElabD ()
tryCon d :: Int
d locs :: [Name]
locs tys :: Set Type
tys n :: Name
n =
         do Type
ty <- Elab' EState Type
forall aux. Elab' aux Type
goal
            let imps :: [(Bool, Int)]
imps = case Name -> Ctxt [PArg] -> Maybe [PArg]
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
                            Nothing -> []
                            Just args :: [PArg]
args -> (PArg -> (Bool, Int)) -> [PArg] -> [(Bool, Int)]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> (Bool, Int)
forall t. PArg' t -> (Bool, Int)
isImp [PArg]
args
            Fails
ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
            [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
            [Name]
args <- ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)] -> [Name])
-> StateT (ElabState EState) TC [(Name, Name)]
-> Elab' EState [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (ElabState EState) TC [(Name, Name)]
-> StateT (ElabState EState) TC [(Name, Name)]
-> Bool
-> StateT (ElabState EState) TC [(Name, Name)]
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' (Raw -> [(Bool, Int)] -> StateT (ElabState EState) TC [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
n) [(Bool, Int)]
imps)
                                     (Raw -> [(Bool, Int)] -> StateT (ElabState EState) TC [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
match_apply (Name -> Raw
Var Name
n) [(Bool, Int)]
imps) Bool
True
            Fails
ps' <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
            [Name]
hs' <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
            Bool -> ElabD () -> ElabD ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Fails -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Fails -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
ps') (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't apply constructor"
            let newhs :: [(Bool, Name)]
newhs = ((Bool, Name) -> Bool) -> [(Bool, Name)] -> [(Bool, Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (x :: Bool
x, y :: Name
y) -> Bool -> Bool
not Bool
x) ([Bool] -> [Name] -> [(Bool, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Bool, Int) -> Bool) -> [(Bool, Int)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, Int) -> Bool
forall a b. (a, b) -> a
fst [(Bool, Int)]
imps) [Name]
args)
            ((Bool, Name) -> ElabD ()) -> [(Bool, Name)] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (_, h :: Name
h) -> do Name -> ElabD ()
forall aux. Name -> Elab' aux ()
focus Name
h
                                  Type
aty <- Elab' EState Type
forall aux. Elab' aux Type
goal
                                  Bool -> Int -> [Name] -> Set Type -> ElabD ()
psRec Bool
True Int
d [Name]
locs Set Type
tys) [(Bool, Name)]
newhs
            ElabD ()
forall aux. Elab' aux ()
solve

    isImp :: PArg' t -> (Bool, Int)
isImp (PImp p :: Int
p _ _ _ _) = (Bool
True, Int
p)
    isImp arg :: PArg' t
arg = (Bool
False, PArg' t -> Int
forall t. PArg' t -> Int
priority PArg' t
arg)

    typeNotSearchable :: Type -> t TC a
typeNotSearchable ty :: Type
ty =
       TC a -> t TC a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> t TC a) -> TC a -> t TC a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (Err -> TC a) -> Err -> TC a
forall a b. (a -> b) -> a -> b
$ [ErrorReportPart] -> Err
forall t. [ErrorReportPart] -> Err' t
FancyMsg ([ErrorReportPart] -> Err) -> [ErrorReportPart] -> Err
forall a b. (a -> b) -> a -> b
$
       [String -> ErrorReportPart
TextPart "Attempted to find an element of type",
        Type -> ErrorReportPart
TermPart Type
ty,
        String -> ErrorReportPart
TextPart "using proof search, but proof search only works on datatypes with constructors."] [ErrorReportPart] -> [ErrorReportPart] -> [ErrorReportPart]
forall a. [a] -> [a] -> [a]
++
       case Type
ty of
         (Bind _ (Pi _ _ _ _) _) -> [String -> ErrorReportPart
TextPart "In particular, function types are not supported."]
         _ -> []

-- | Resolve interfaces. This will only pick up 'normal'
-- implementations, never named implementations (which is enforced by
-- 'findImplementations').
resolveTC :: Bool                -- ^ using default Int
          -> Bool                -- ^ allow open implementations
          -> Int                 -- ^ depth
          -> Term                -- ^ top level goal, for error messages
          -> Name                -- ^ top level function name, to prevent loops
          -> (PTerm -> ElabD ()) -- ^ top level elaborator
          -> IState -> ElabD ()
resolveTC :: Bool
-> Bool
-> Int
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resolveTC def :: Bool
def openOK :: Bool
openOK depth :: Int
depth top :: Type
top fn :: Name
fn elab :: PTerm -> ElabD ()
elab ist :: IState
ist
  = do [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
       [Type]
-> Bool
-> Bool
-> [Name]
-> Int
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
forall t.
(Eq t, Num t) =>
[Type]
-> Bool
-> Bool
-> [Name]
-> t
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resTC' [] Bool
def Bool
openOK [Name]
hs Int
depth Type
top Name
fn PTerm -> ElabD ()
elab IState
ist

resTC' :: [Type]
-> Bool
-> Bool
-> [Name]
-> t
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resTC' tcs :: [Type]
tcs def :: Bool
def openOK :: Bool
openOK topholes :: [Name]
topholes 0 topg :: Type
topg fn :: Name
fn elab :: PTerm -> ElabD ()
elab ist :: IState
ist = String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't resolve interface"
resTC' tcs :: [Type]
tcs def :: Bool
def openOK :: Bool
openOK topholes :: [Name]
topholes 1 topg :: Type
topg fn :: Name
fn elab :: PTerm -> ElabD ()
elab ist :: IState
ist = ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' ((PTerm -> ElabD ()) -> IState -> ElabD ()
trivial PTerm -> ElabD ()
elab IState
ist) (Bool
-> Bool
-> Int
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resolveTC Bool
def Bool
False 0 Type
topg Name
fn PTerm -> ElabD ()
elab IState
ist) Bool
True
resTC' tcs :: [Type]
tcs defaultOn :: Bool
defaultOn openOK :: Bool
openOK topholes :: [Name]
topholes depth :: t
depth topg :: Type
topg fn :: Name
fn elab :: PTerm -> ElabD ()
elab ist :: IState
ist
  = do ElabD ()
forall aux. Elab' aux ()
compute
       if Bool
openOK
          then ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' ([Name] -> ElabD ()
resolveOpen (IState -> [Name]
idris_openimpls IState
ist))
                    ElabD ()
resolveNormal
                    Bool
True
          else ElabD ()
resolveNormal

  where
    -- try all the Open implementations first
    resolveOpen :: [Name] -> ElabD ()
resolveOpen open :: [Name]
open = do Type
t <- Elab' EState Type
forall aux. Elab' aux Type
goal
                          Type -> t -> [Any] -> [Name] -> ElabD ()
forall t t. t -> t -> t -> [Name] -> ElabD ()
blunderbuss Type
t t
depth [] [Name]
open

    resolveNormal :: ElabD ()
resolveNormal = do
       -- Resolution can proceed only if there is something concrete in the
       -- determining argument positions. Keep track of the holes in the
       -- non-determining position, because it's okay for 'trivial' to solve
       -- those holes and no others.
       Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
       let (argsok :: Bool
argsok, okholePos :: [Int]
okholePos) = case Type -> [Name] -> Maybe [Int]
tcArgsOK Type
g [Name]
topholes of
                                    Nothing -> (Bool
False, [])
                                    Just hs :: [Int]
hs -> (Bool
True, [Int]
hs)
       Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
       Fails
probs <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
       if Bool -> Bool
not Bool
argsok -- && not mvok)
         then TC () -> ElabD ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> ElabD ()) -> TC () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ Bool -> Type -> Err -> Err
forall t. Bool -> t -> Err' t -> Err' t
CantResolve Bool
True Type
topg (Fails -> Err
forall a b c d t f g. [(a, b, c, d, Err' t, f, g)] -> Err' t
probErr Fails
probs)
         else do
           Type
ptm <- Elab' EState Type
forall aux. Elab' aux Type
get_term
           Bool
ulog <- StateT (ElabState EState) TC Bool
forall aux. Elab' aux Bool
getUnifyLog
           [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
           Env
env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
           Type
t <- Elab' EState Type
forall aux. Elab' aux Type
goal
           let (tc :: Type
tc, ttypes :: [Type]
ttypes) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
t)
           let okholes :: [(Name, Int)]
okholes = case Type
tc of
                              P _ n :: Name
n _ -> [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Name -> [Name]
forall a. a -> [a]
repeat Name
n) [Int]
okholePos
                              _ -> []

           Bool -> String -> ElabD () -> ElabD ()
forall p. Bool -> String -> p -> p
traceWhen Bool
ulog ("Resolving interface " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
g String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\nin" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Env -> String
forall a. Show a => a -> String
show Env
env String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, Int)] -> String
forall a. Show a => a -> String
show [(Name, Int)]
okholes) (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$
            ElabD () -> ElabD () -> Bool -> ElabD ()
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' ([(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialTCs [(Name, Int)]
okholes PTerm -> ElabD ()
elab IState
ist)
                (do Type -> Type -> [Type] -> ElabD ()
forall p aux. p -> Type -> [Type] -> StateT (ElabState aux) TC ()
addDefault Type
t Type
tc [Type]
ttypes
                    let stk :: [Name]
stk = ((Name, Bool) -> Name) -> [(Name, Bool)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Bool) -> Name
forall a b. (a, b) -> a
fst (((Name, Bool) -> Bool) -> [(Name, Bool)] -> [(Name, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name, Bool) -> Bool
forall a b. (a, b) -> b
snd ([(Name, Bool)] -> [(Name, Bool)])
-> [(Name, Bool)] -> [(Name, Bool)]
forall a b. (a -> b) -> a -> b
$ IState -> [(Name, Bool)]
elab_stack IState
ist)
                    let impls :: [Name]
impls = IState -> [Name]
idris_openimpls IState
ist [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ IState -> Type -> [Name]
findImplementations IState
ist Type
t
                    Type -> t -> [Name] -> [Name] -> ElabD ()
forall t t. t -> t -> t -> [Name] -> ElabD ()
blunderbuss Type
t t
depth [Name]
stk ([Name]
stk [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
impls)) Bool
True

    -- returns Just hs if okay, where hs are holes which are okay in the
    -- goal, or Nothing if not okay to proceed
    tcArgsOK :: Type -> [Name] -> Maybe [Int]
tcArgsOK ty :: Type
ty hs :: [Name]
hs | (P _ nc :: Name
nc _, as :: [Type]
as) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty), Name
nc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
numinterface Bool -> Bool -> Bool
&& Bool
defaultOn
       = [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just []
    tcArgsOK ty :: Type
ty hs :: [Name]
hs -- if any determining arguments are metavariables, postpone
       = let (f :: Type
f, as :: [Type]
as) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
ty) in
             case Type
f of
                  P _ cn :: Name
cn _ -> case Name -> Ctxt InterfaceInfo -> Maybe InterfaceInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                                   Just ci :: InterfaceInfo
ci -> Int -> [Int] -> [Name] -> [Type] -> Maybe [Int]
forall (t :: * -> *) a.
(Foldable t, Eq a, Num a) =>
a -> t a -> [Name] -> [Type] -> Maybe [a]
tcDetArgsOK 0 (InterfaceInfo -> [Int]
interface_determiners InterfaceInfo
ci) [Name]
hs [Type]
as
                                   Nothing -> if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Name] -> Type -> Bool
isMeta [Name]
hs) [Type]
as
                                                 then Maybe [Int]
forall a. Maybe a
Nothing
                                                 else [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just []
                  _ -> if (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ([Name] -> Type -> Bool
isMeta [Name]
hs) [Type]
as
                          then Maybe [Int]
forall a. Maybe a
Nothing
                          else [Int] -> Maybe [Int]
forall a. a -> Maybe a
Just []

    -- return the list of argument positions which can safely be a hole
    -- or Nothing if one of the determining arguments is a hole
    tcDetArgsOK :: a -> t a -> [Name] -> [Type] -> Maybe [a]
tcDetArgsOK i :: a
i ds :: t a
ds hs :: [Name]
hs (x :: Type
x : xs :: [Type]
xs)
        | a
i a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
ds = if [Name] -> Type -> Bool
isMeta [Name]
hs Type
x
                           then Maybe [a]
forall a. Maybe a
Nothing
                           else a -> t a -> [Name] -> [Type] -> Maybe [a]
tcDetArgsOK (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) t a
ds [Name]
hs [Type]
xs
        | Bool
otherwise = do [a]
rs <- a -> t a -> [Name] -> [Type] -> Maybe [a]
tcDetArgsOK (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ 1) t a
ds [Name]
hs [Type]
xs
                         case Type
x of
                              P _ n :: Name
n _ -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
i a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)
                              _ -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a]
rs
    tcDetArgsOK _ _ _ [] = [a] -> Maybe [a]
forall a. a -> Maybe a
Just []

    probErr :: [(a, b, c, d, Err' t, f, g)] -> Err' t
probErr [] = String -> Err' t
forall t. String -> Err' t
Msg ""
    probErr ((_,_,_,_,err :: Err' t
err,_,_) : _) = Err' t
err

    isMeta :: [Name] -> Term -> Bool
    isMeta :: [Name] -> Type -> Bool
isMeta ns :: [Name]
ns (P _ n :: Name
n _) = Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns
    isMeta _ _ = Bool
False

    numinterface :: Name
numinterface = Name -> [String] -> Name
sNS (String -> Name
sUN "Num") ["Interfaces","Prelude"]

    addDefault :: p -> Type -> [Type] -> StateT (ElabState aux) TC ()
addDefault t :: p
t num :: Type
num@(P _ nc :: Name
nc _) [P Bound a :: Name
a _] | Name
nc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
numinterface Bool -> Bool -> Bool
&& Bool
defaultOn
        = do Name -> StateT (ElabState aux) TC ()
forall aux. Name -> Elab' aux ()
focus Name
a
             Raw -> StateT (ElabState aux) TC ()
forall aux. Raw -> Elab' aux ()
fill (Const -> Raw
RConstant (ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))) -- default Integer
             StateT (ElabState aux) TC ()
forall aux. Elab' aux ()
solve
    addDefault t :: p
t f :: Type
f as :: [Type]
as
          | (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
forall n. TT n -> Bool
boundVar [Type]
as = () -> StateT (ElabState aux) TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- True -- fail $ "Can't resolve " ++ show t
    addDefault t :: p
t f :: Type
f a :: [Type]
a = () -> StateT (ElabState aux) TC ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- trace (show t) $ return ()

    boundVar :: TT n -> Bool
boundVar (P Bound _ _) = Bool
True
    boundVar _ = Bool
False

    blunderbuss :: t -> t -> t -> [Name] -> ElabD ()
blunderbuss t :: t
t d :: t
d stk :: t
stk [] = do Fails
ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                                TC () -> ElabD ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> ElabD ()) -> TC () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$ Bool -> Type -> Err -> Err
forall t. Bool -> t -> Err' t -> Err' t
CantResolve Bool
False Type
topg (Fails -> Err
forall a b c d t f g. [(a, b, c, d, Err' t, f, g)] -> Err' t
probErr Fails
ps)
    blunderbuss t :: t
t d :: t
d stk :: t
stk (n :: Name
n:ns :: [Name]
ns)
        | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
fn -- && (n `elem` stk)
              = ElabD () -> (Err -> ElabD ()) -> ElabD ()
forall aux a. Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
tryCatch (Name -> t -> ElabD ()
resolve Name
n t
d)
                    (\e :: Err
e -> case Err
e of
                             CantResolve True _ _ -> TC () -> ElabD ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> ElabD ()) -> TC () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail Err
e
                             _ -> t -> t -> t -> [Name] -> ElabD ()
blunderbuss t
t t
d t
stk [Name]
ns)
        | Bool
otherwise = t -> t -> t -> [Name] -> ElabD ()
blunderbuss t
t t
d t
stk [Name]
ns

    introImps :: StateT (ElabState aux) TC Int
introImps = do Type
g <- Elab' aux Type
forall aux. Elab' aux Type
goal
                   case Type
g of
                        (Bind _ (Pi _ _ _ _) sc :: Type
sc) -> do Elab' aux ()
forall aux. Elab' aux ()
attack; Maybe Name -> Elab' aux ()
forall aux. Maybe Name -> Elab' aux ()
intro Maybe Name
forall a. Maybe a
Nothing
                                                       Int
num <- StateT (ElabState aux) TC Int
introImps
                                                       Int -> StateT (ElabState aux) TC Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
num Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
                        _ -> Int -> StateT (ElabState aux) TC Int
forall (m :: * -> *) a. Monad m => a -> m a
return 0

    solven :: Int -> StateT (ElabState aux) TC ()
solven n :: Int
n = Int -> StateT (ElabState aux) TC () -> StateT (ElabState aux) TC ()
forall (m :: * -> *) a. Applicative m => Int -> m a -> m ()
replicateM_ Int
n StateT (ElabState aux) TC ()
forall aux. Elab' aux ()
solve

    resolve :: Name -> t -> ElabD ()
resolve n :: Name
n depth :: t
depth
       | t
depth t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't resolve interface"
       | Bool
otherwise
           = do Int
lams <- StateT (ElabState EState) TC Int
forall aux. StateT (ElabState aux) TC Int
introImps
                Type
t <- Elab' EState Type
forall aux. Elab' aux Type
goal
--                 if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist
--                   else do
                   -- if there's a hole in the goal, don't even try
                let imps :: [(Bool, Int)]
imps = case Name -> Ctxt [PArg] -> [(Name, [PArg])]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
                                [] -> []
                                [args :: (Name, [PArg])
args] -> (PArg -> (Bool, Int)) -> [PArg] -> [(Bool, Int)]
forall a b. (a -> b) -> [a] -> [b]
map PArg -> (Bool, Int)
forall t. PArg' t -> (Bool, Int)
isImp ((Name, [PArg]) -> [PArg]
forall a b. (a, b) -> b
snd (Name, [PArg])
args) -- won't be overloaded!
                                xs :: [(Name, [PArg])]
xs -> String -> [(Bool, Int)]
forall a. HasCallStack => String -> a
error "The impossible happened - overloading is not expected here!"
                Fails
ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                Type
tm <- Elab' EState Type
forall aux. Elab' aux Type
get_term
                [Name]
args <- ((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd ([(Name, Name)] -> [Name])
-> StateT (ElabState EState) TC [(Name, Name)]
-> Elab' EState [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Raw -> [(Bool, Int)] -> StateT (ElabState EState) TC [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
n) [(Bool, Int)]
imps
                Int -> ElabD ()
forall aux. Int -> StateT (ElabState aux) TC ()
solven Int
lams -- close any implicit lambdas we introduced
                Fails
ps' <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                Bool -> ElabD () -> ElabD ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Fails -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Fails -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
ps' Bool -> Bool -> Bool
|| Fails -> Bool
unrecoverable Fails
ps') (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$
                     String -> ElabD ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Can't apply interface"
--                 traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
                ((Bool, Name) -> ElabD ()) -> [(Bool, Name)] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (_,n :: Name
n) -> do Name -> ElabD ()
forall aux. Name -> Elab' aux ()
focus Name
n
                                     Type
t' <- Elab' EState Type
forall aux. Elab' aux Type
goal
                                     let (tc' :: Type
tc', _) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
t')
                                     let got :: Type
got = (Type, [Type]) -> Type
forall a b. (a, b) -> a
fst (Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
t))
                                     let depth' :: t
depth' = if Type
tc' Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type]
tcs
                                                     then t
depth t -> t -> t
forall a. Num a => a -> a -> a
- 1 else t
depth
                                     [Type]
-> Bool
-> Bool
-> [Name]
-> t
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resTC' (Type
got Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
tcs) Bool
defaultOn Bool
openOK [Name]
topholes t
depth' Type
topg Name
fn PTerm -> ElabD ()
elab IState
ist)
                      (((Bool, Name) -> Bool) -> [(Bool, Name)] -> [(Bool, Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (x :: Bool
x, y :: Name
y) -> Bool -> Bool
not Bool
x) ([Bool] -> [Name] -> [(Bool, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip (((Bool, Int) -> Bool) -> [(Bool, Int)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, Int) -> Bool
forall a b. (a, b) -> a
fst [(Bool, Int)]
imps) [Name]
args))
                -- if there's any arguments left, we've failed to resolve
                [Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                Bool
ulog <- StateT (ElabState EState) TC Bool
forall aux. Elab' aux Bool
getUnifyLog
                ElabD ()
forall aux. Elab' aux ()
solve
                Bool -> String -> ElabD () -> ElabD ()
forall p. Bool -> String -> p -> p
traceWhen Bool
ulog ("Got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n) (ElabD () -> ElabD ()) -> ElabD () -> ElabD ()
forall a b. (a -> b) -> a -> b
$ () -> ElabD ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       where isImp :: PArg' t -> (Bool, Int)
isImp (PImp p :: Int
p _ _ _ _) = (Bool
True, Int
p)
             isImp arg :: PArg' t
arg = (Bool
False, PArg' t -> Int
forall t. PArg' t -> Int
priority PArg' t
arg)

-- | Find the names of implementations that have been designeated for
-- searching (i.e. non-named implementations or implementations from Elab scripts)
findImplementations :: IState -> Term -> [Name]
findImplementations :: IState -> Type -> [Name]
findImplementations ist :: IState
ist t :: Type
t
    | (P _ n :: Name
n _, _) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply (Type -> Type
forall n. TT n -> TT n
getRetTy Type
t)
        = case Name -> Ctxt InterfaceInfo -> [InterfaceInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
            [ci :: InterfaceInfo
ci] -> let ins :: [(Name, Bool)]
ins = InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci in
                        [Name
n | (n :: Name
n, True) <- [(Name, Bool)]
ins, Name -> Bool
accessible Name
n]
            _ -> []
    | Bool
otherwise = []
  where accessible :: Name -> Bool
accessible n :: Name
n = case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False (IState -> Context
tt_ctxt IState
ist) of
                            Just (_, Hidden) -> Bool
False
                            Just (_, Private) -> Bool
False
                            _ -> Bool
True