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

        holesOK :: t Name -> Type -> Bool
holesOK t Name
hs ap :: Type
ap@(App AppStatus Name
_ Type
_ Type
_)
           | (P NameType
_ Name
n Type
_, [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 Int
0 [Type]
args
        holesOK t Name
hs (App AppStatus Name
_ Type
f 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 t Name
hs (P NameType
_ Name
n Type
_) = 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
hs)
        holesOK t Name
hs (Bind Name
n Binder Type
b 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 t Name
hs Type
_ = Bool
True

        holeArgsOK :: t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n Int
p [] = Bool
True
        holeArgsOK t Name
hs Name
n Int
p (Type
a : [Type]
as)
           | (Name
n, Int
p) (Name, Int) -> [(Name, Int)] -> Bool
forall a. Eq a => a -> [a] -> 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
+ Int
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
+ Int
1) [Type]
as

trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialTCs :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialTCs [(Name, Int)]
ok PTerm -> ElabD ()
elab 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 String
"prf") (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC String
"prf") [] Name
eqCon) [Name -> PTerm -> Bool -> PArg
forall {t}. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN String
"A") PTerm
Placeholder Bool
False, Name -> PTerm -> Bool -> PArg
forall {t}. Name -> t -> Bool -> PArg' t
pimp (String -> Name
sUN String
"x") PTerm
Placeholder Bool
False])
                () -> ElabD ()
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
            (do env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
                g <- goal
                tryAll env
                return ()) Bool
True
      where
        tryAll :: [(Name, b, Binder Type)] -> ElabD ()
tryAll []     = String -> ElabD ()
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No trivial solution"
        tryAll ((Name
x, b
_, Binder Type
b):[(Name, b, Binder Type)]
xs)
           = do -- if type of x has any holes in it, move on
                hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                g <- goal
                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))
                   (holesOK hs (binderTy b) && tcArg env (binderTy b))
                   then try' (elab (PRef (fileFC "prf") [] x))
                             (tryAll xs) True
                   else tryAll xs

        tcArg :: Env -> Type -> Bool
tcArg Env
env Type
ty
           | (P NameType
_ Name
n Type
_, [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 InterfaceInfo
_ -> Bool
True
                        Maybe InterfaceInfo
_ -> Bool
False
           | Bool
otherwise = Bool
False

        holesOK :: t Name -> Type -> Bool
holesOK t Name
hs ap :: Type
ap@(App AppStatus Name
_ Type
_ Type
_)
           | (P NameType
_ Name
n Type
_, [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 Int
0 [Type]
args
        holesOK t Name
hs (App AppStatus Name
_ Type
f 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 t Name
hs (P NameType
_ Name
n Type
_) = 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
hs)
        holesOK t Name
hs (Bind Name
n Binder Type
b 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 t Name
hs Type
_ = Bool
True

        holeArgsOK :: t Name -> Name -> Int -> [Type] -> Bool
holeArgsOK t Name
hs Name
n Int
p [] = Bool
True
        holeArgsOK t Name
hs Name
n Int
p (Type
a : [Type]
as)
           | (Name
n, Int
p) (Name, Int) -> [(Name, Int)] -> Bool
forall a. Eq a => a -> [a] -> 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
+ Int
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
+ Int
1) [Type]
as

cantSolveGoal :: ElabD a
cantSolveGoal :: forall a. ElabD a
cantSolveGoal = do g <- Elab' EState Type
forall aux. Elab' aux Type
goal
                   env <- get_env
                   lift $ tfail $
                      CantSolveGoal g (map (\(Name
n,RigCount
_,Binder Type
b) -> (Name
n, Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)) 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 Bool
False Bool
fromProver Bool
ambigok Bool
deferonfail Int
depth PTerm -> ElabD ()
elab Maybe Name
_ Name
nroot [Name]
psnames [Name
fn] 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 ((Name, [PArg' t])
f : [(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 (Name
f, [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
                         ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                         hs <- get_holes
                         args <- map snd <$> try' (apply (Var f) imps)
                                                  (match_apply (Var f) imps) True
                         ps' <- get_probs
--                          when (length ps < length ps') $ fail "Can't apply constructor"
                         -- Make metavariables for new holes
                         hs' <- get_holes
                         ptm <- get_term
                         if fromProver then cantSolveGoal
                           else do
                             mapM_ (\ 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)
                                 (hs' \\ hs)
--                                  (filter (\ (x, y) -> not x) (zip (map fst imps) args))
                             solve

    isImp :: PArg' t -> (Bool, Int)
isImp (PImp Int
p Bool
_ [ArgOpt]
_ Name
_ t
_) = (Bool
True, Int
p)
    isImp 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 Bool
rec Bool
fromProver Bool
ambigok Bool
deferonfail Int
maxDepth PTerm -> ElabD ()
elab Maybe Name
fn Name
nroot [Name]
psnames [Name]
hints IState
ist
       = do ElabD ()
forall aux. Elab' aux ()
compute
            ty <- Elab' EState Type
forall aux. Elab' aux Type
goal
            hs <- get_holes
            env <- get_env
            tm <- get_term
            argsok <- conArgsOK ty
            if ambigok || argsok then
               case lookupCtxt nroot (idris_tyinfodata ist) of
                    [TISolution [Type]
ts] -> [Type] -> ElabD ()
findInferredTy [Type]
ts
                    [TIData]
_ -> 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 String
"auto"))
               else autoArg (sUN "auto") -- not enough info in the type yet
  where
    findInferredTy :: [Type] -> ElabD ()
findInferredTy (Type
t : [Type]
_) = PTerm -> ElabD ()
elab (IState -> Type -> PTerm
delab IState
ist (Type -> Type
toUN Type
t))

    cantsolve :: Err' t -> Bool
cantsolve (InternalMsg String
_) = Bool
True
    cantsolve (CantSolveGoal t
_ [(Name, t)]
_) = Bool
True
    cantsolve (IncompleteTerm t
_) = Bool
True
    cantsolve (At FC
_ Err' t
e) = Err' t -> Bool
cantsolve Err' t
e
    cantsolve (Elaborating String
_ Name
_ Maybe t
_ Err' t
e) = Err' t -> Bool
cantsolve Err' t
e
    cantsolve (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err' t
e) = Err' t -> Bool
cantsolve Err' t
e
    cantsolve Err' t
err = Bool
False

    conArgsOK :: Type -> StateT (ElabState EState) TC Bool
conArgsOK Type
ty
       = let (Type
f, [Type]
as) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
ty in
           case Type
f of
              P NameType
_ Name
n Type
_ ->
                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
                                     Maybe [Name]
Nothing -> []
                                     Just [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 TypeInfo
t -> do 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)
                                           return (and rs)
                              Maybe TypeInfo
Nothing -> -- local variable, go for it
                                    Bool -> StateT (ElabState EState) TC Bool
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
              TType UExp
_ -> Bool -> StateT (ElabState EState) TC Bool
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
              Type
_ -> 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 [Type]
as Name
n
       = case Name -> Context -> Maybe Type
lookupTyExact Name
n (IState -> Context
tt_ctxt IState
ist) of
              Just Type
ty -> do let (Type
_, [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
                            hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
                            return $ and (map (notHole hs) (zip as cs))
              Maybe Type
Nothing -> String -> StateT (ElabState EState) TC Bool
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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 t a
hs (P NameType
_ a
n TT a
_, Type
c)
       | (P NameType
_ Name
cn Type
_, [Type]
_) <- Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
c,
         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
hs Bool -> Bool -> Bool
&& Name -> Context -> Bool
isConName Name
cn (IState -> Context
tt_ctxt IState
ist) = Bool
False
       | Constant Const
_ <- Type
c = Bool -> Bool
not (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
hs)
    -- if fa is a metavariable applied to anything, we're not ready to run yet.
    notHole t a
hs (TT a
fa, Type
c)
       | (P NameType
_ a
fn TT a
_, args :: [TT a]
args@(TT a
_:[TT a]
_)) <- 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 t a
_ (TT a, Type)
_ = Bool
True

    toUN :: Type -> Type
toUN t :: Type
t@(P NameType
nt (MN Int
i Text
n) Type
ty)
       | (Char
'_':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 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 -> Type
toUN Type
f) (Type -> Type
toUN Type
a)
    toUN 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 Bool
_ Int
0 [Name]
locs Set Type
tys | Bool
fromProver = ElabD ()
forall a. ElabD a
cantSolveGoal
    psRec Bool
rec Int
0 [Name]
locs 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 Bool
False Int
d [Name]
locs Set Type
tys = Int -> [Name] -> Set Type -> [Name] -> ElabD ()
tryCons Int
d [Name]
locs Set Type
tys [Name]
hints
    psRec Bool
True Int
d [Name]
locs Set Type
tys
                 = do ElabD ()
forall aux. Elab' aux ()
compute
                      ty <- Elab' EState Type
forall aux. Elab' aux Type
goal
                      when (S.member ty tys) $ fail "Been here before"
                      let tys' = Type -> Set Type -> Set Type
forall a. Ord a => a -> Set a -> Set a
S.insert Type
ty Set Type
tys
                      try' (try' (trivialHoles psnames [] elab ist)
                                 (resolveTC False False 20 ty nroot elab ist)
                                 True)
                           (try' (try' (resolveByCon (d - 1) locs tys')
                                       (resolveByLocals (d - 1) locs tys')
                                 True)
             -- if all else fails, make a new metavariable
                         (if fromProver
                             then fail "cantSolveGoal"
                             else do attack; defer [] [] nroot; solve) True) True

    -- get recursive function name. Only user given names make sense.
    getFn :: Int -> Maybe Name -> [Name]
getFn Int
d (Just 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
-Int
1 Bool -> Bool -> Bool
&& Name -> Bool
usersname Name
f = [Name
f]
                     | Bool
otherwise = []
    getFn Int
d Maybe Name
_ = []

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

    resolveByCon :: Int -> [Name] -> Set Type -> ElabD ()
resolveByCon Int
d [Name]
locs Set Type
tys
        = do t <- Elab' EState Type
forall aux. Elab' aux Type
goal
             let (f, _) = unApply t
             case f of
                P NameType
_ Name
n Type
_ ->
                   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
                                           Maybe [Name]
Nothing -> []
                                           Just [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 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)
                          Maybe TypeInfo
Nothing -> Type -> ElabD ()
forall {t :: (* -> *) -> * -> *} {a}.
MonadTrans t =>
Type -> t TC a
typeNotSearchable Type
t
                Type
_ -> 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 Int
d [Name]
locs Set Type
tys
        = do env <- Elab' EState Env
forall aux. Elab' aux Env
get_env
             tryLocals d locs tys env

    tryLocals :: Int -> [Name] -> Set Type -> [(Name, b, Binder Type)] -> ElabD ()
tryLocals Int
d [Name]
locs Set Type
tys [] = String -> ElabD ()
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Locals failed"
    tryLocals Int
d [Name]
locs Set Type
tys ((Name
x, b
_, Binder Type
t) : [(Name, b, Binder Type)]
xs)
       | 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]
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 Int
d [Name]
locs Set Type
tys [] = String -> ElabD ()
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Constructors failed"
    tryCons Int
d [Name]
locs Set Type
tys (Name
c : [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 Int
d [Name]
locs Set Type
tys Name
n 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 Int
d [Name]
locs Set Type
tys Name
n t
0 = PTerm -> ElabD ()
elab (FC -> [FC] -> Name -> PTerm
PRef (String -> FC
fileFC String
"prf") [] Name
n)
    tryLocalArg Int
d [Name]
locs Set Type
tys Name
n 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
- t
1))
                (Bool -> Int -> [Name] -> Set Type -> ElabD ()
psRec Bool
True Int
d [Name]
locs Set Type
tys) String
"proof search local apply"

    -- Like interface resolution, but searching with constructors
    tryCon :: Int -> [Name] -> Set Type -> Name -> ElabD ()
tryCon Int
d [Name]
locs Set Type
tys Name
n =
         do ty <- Elab' EState Type
forall aux. Elab' aux Type
goal
            let 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
                            Maybe [PArg]
Nothing -> []
                            Just [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
            ps <- get_probs
            hs <- get_holes
            args <- map snd <$> try' (apply (Var n) imps)
                                     (match_apply (Var n) imps) True
            ps' <- get_probs
            hs' <- get_holes
            when (length ps < length ps') $ fail "Can't apply constructor"
            let newhs = ((Bool, Name) -> Bool) -> [(Bool, Name)] -> [(Bool, Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Bool
x, 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)
            mapM_ (\ (Bool
_, Name
h) -> do Name -> ElabD ()
forall aux. Name -> Elab' aux ()
focus Name
h
                                  aty <- Elab' EState Type
forall aux. Elab' aux Type
goal
                                  psRec True d locs tys) newhs
            solve

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

    typeNotSearchable :: Type -> t TC a
typeNotSearchable Type
ty =
       TC a -> t TC a
forall (m :: * -> *) a. Monad m => m a -> t m 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 String
"Attempted to find an element of type",
        Type -> ErrorReportPart
TermPart Type
ty,
        String -> ErrorReportPart
TextPart String
"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 Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) Type
_) -> [String -> ErrorReportPart
TextPart String
"In particular, function types are not supported."]
         Type
_ -> []

-- | 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 Bool
def Bool
openOK Int
depth Type
top Name
fn PTerm -> ElabD ()
elab IState
ist
  = do hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
       resTC' [] def openOK hs depth top fn elab ist

resTC' :: [Type]
-> Bool
-> Bool
-> [Name]
-> t
-> Type
-> Name
-> (PTerm -> ElabD ())
-> IState
-> ElabD ()
resTC' [Type]
tcs Bool
def Bool
openOK [Name]
topholes t
0 Type
topg Name
fn PTerm -> ElabD ()
elab IState
ist = String -> ElabD ()
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't resolve interface"
resTC' [Type]
tcs Bool
def Bool
openOK [Name]
topholes t
1 Type
topg Name
fn PTerm -> ElabD ()
elab 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 Int
0 Type
topg Name
fn PTerm -> ElabD ()
elab IState
ist) Bool
True
resTC' [Type]
tcs Bool
defaultOn Bool
openOK [Name]
topholes t
depth Type
topg Name
fn PTerm -> ElabD ()
elab 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 [Name]
open = do t <- Elab' EState Type
forall aux. Elab' aux Type
goal
                          blunderbuss t depth [] 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.
       g <- Elab' EState Type
forall aux. Elab' aux Type
goal
       let (argsok, okholePos) = case tcArgsOK g topholes of
                                    Maybe [Int]
Nothing -> (Bool
False, [])
                                    Just [Int]
hs -> (Bool
True, [Int]
hs)
       env <- get_env
       probs <- get_probs
       if not argsok -- && not mvok)
         then lift $ tfail $ CantResolve True topg (probErr probs)
         else do
           ptm <- get_term
           ulog <- getUnifyLog
           hs <- get_holes
           env <- get_env
           t <- goal
           let (tc, ttypes) = unApply (getRetTy t)
           let okholes = case Type
tc of
                              P NameType
_ Name
n Type
_ -> [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Name -> [Name]
forall a. a -> [a]
repeat Name
n) [Int]
okholePos
                              Type
_ -> []

           traceWhen ulog ("Resolving interface " ++ show g ++ "\nin" ++ show env ++ "\n" ++ show okholes) $
            try' (trivialTCs okholes elab ist)
                (do addDefault t tc ttypes
                    let 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 = IState -> [Name]
idris_openimpls IState
ist [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ IState -> Type -> [Name]
findImplementations IState
ist Type
t
                    blunderbuss t depth stk (stk ++ impls)) 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 Type
ty [Name]
hs | (P NameType
_ Name
nc Type
_, [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 Type
ty [Name]
hs -- if any determining arguments are metavariables, postpone
       = let (Type
f, [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 NameType
_ Name
cn Type
_ -> 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 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 Int
0 (InterfaceInfo -> [Int]
interface_determiners InterfaceInfo
ci) [Name]
hs [Type]
as
                                   Maybe InterfaceInfo
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 []
                  Type
_ -> 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 a
i t a
ds [Name]
hs (Type
x : [Type]
xs)
        | a
i 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
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
+ a
1) t a
ds [Name]
hs [Type]
xs
        | Bool
otherwise = do rs <- a -> t a -> [Name] -> [Type] -> Maybe [a]
tcDetArgsOK (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) t a
ds [Name]
hs [Type]
xs
                         case x of
                              P NameType
_ Name
n Type
_ -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just (a
i a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)
                              Type
_ -> [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a]
rs
    tcDetArgsOK a
_ t a
_ [Name]
_ [] = [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 String
""
    probErr ((a
_,b
_,c
_,d
_,Err' t
err,f
_,g
_) : [(a, b, c, d, Err' t, f, g)]
_) = Err' t
err

    isMeta :: [Name] -> Term -> Bool
    isMeta :: [Name] -> Type -> Bool
isMeta [Name]
ns (P NameType
_ Name
n Type
_) = 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
    isMeta [Name]
_ Type
_ = Bool
False

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

    addDefault :: p -> Type -> [Type] -> StateT (ElabState aux) TC ()
addDefault p
t num :: Type
num@(P NameType
_ Name
nc Type
_) [P NameType
Bound Name
a Type
_] | 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 p
t Type
f [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 a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- True -- fail $ "Can't resolve " ++ show t
    addDefault p
t Type
f [Type]
a = () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- trace (show t) $ return ()

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

    blunderbuss :: t -> t -> t -> [Name] -> ElabD ()
blunderbuss t
t t
d t
stk [] = do ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
                                lift $ tfail $ CantResolve False topg (probErr ps)
    blunderbuss t
t t
d t
stk (Name
n:[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)
                    (\Err
e -> case Err
e of
                             CantResolve Bool
True Type
_ Err
_ -> TC () -> ElabD ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState EState) m a
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
                             Err
_ -> 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 g <- Elab' aux Type
forall aux. Elab' aux Type
goal
                   case g of
                        (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ Type
_ Type
_) 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
                                                       num <- StateT (ElabState aux) TC Int
introImps
                                                       return (num + 1)
                        Type
_ -> Int -> StateT (ElabState aux) TC Int
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0

    solven :: Int -> StateT (ElabState aux) TC ()
solven 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 Name
n t
depth
       | t
depth t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
0 = String -> ElabD ()
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't resolve interface"
       | Bool
otherwise
           = do lams <- StateT (ElabState EState) TC Int
forall {aux}. StateT (ElabState aux) TC Int
introImps
                t <- 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 = case Name -> Ctxt [PArg] -> [(Name, [PArg])]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n (IState -> Ctxt [PArg]
idris_implicits IState
ist) of
                                [] -> []
                                [(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!
                                [(Name, [PArg])]
xs -> String -> [(Bool, Int)]
forall a. HasCallStack => String -> a
error String
"The impossible happened - overloading is not expected here!"
                ps <- get_probs
                tm <- get_term
                args <- map snd <$> apply (Var n) imps
                solven lams -- close any implicit lambdas we introduced
                ps' <- get_probs
                when (length ps < length ps' || unrecoverable ps') $
                     fail "Can't apply interface"
--                 traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
                mapM_ (\ (Bool
_,Name
n) -> do Name -> ElabD ()
forall aux. Name -> Elab' aux ()
focus Name
n
                                     t' <- Elab' EState Type
forall aux. Elab' aux Type
goal
                                     let (tc', _) = unApply (getRetTy t')
                                     let 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' = if Type
tc' Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> 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
- t
1 else t
depth
                                     resTC' (got : tcs) defaultOn openOK topholes depth' topg fn elab ist)
                      (filter (\ (Bool
x, Name
y) -> Bool -> Bool
not Bool
x) (zip (map fst imps) args))
                -- if there's any arguments left, we've failed to resolve
                hs <- get_holes
                ulog <- getUnifyLog
                solve
                traceWhen ulog ("Got " ++ show n) $ return ()
       where isImp :: PArg' t -> (Bool, Int)
isImp (PImp Int
p Bool
_ [ArgOpt]
_ Name
_ t
_) = (Bool
True, Int
p)
             isImp 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 IState
ist Type
t
    | (P NameType
_ Name
n Type
_, [Type]
_) <- 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
            [InterfaceInfo
ci] -> let ins :: [(Name, Bool)]
ins = InterfaceInfo -> [(Name, Bool)]
interface_implementations InterfaceInfo
ci in
                        [Name
n | (Name
n, Bool
True) <- [(Name, Bool)]
ins, Name -> Bool
accessible Name
n]
            [InterfaceInfo]
_ -> []
    | Bool
otherwise = []
  where accessible :: Name -> Bool
accessible Name
n = case Name -> Bool -> Context -> Maybe (Def, Accessibility)
lookupDefAccExact Name
n Bool
False (IState -> Context
tt_ctxt IState
ist) of
                            Just (Def
_, Accessibility
Hidden) -> Bool
False
                            Just (Def
_, Accessibility
Private) -> Bool
False
                            Maybe (Def, Accessibility)
_ -> Bool
True