{-# 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
trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()
trivial = [Name]
-> [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()
trivialHoles [] []
trivialHoles :: [Name] ->
[(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
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 a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
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
[Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
if
([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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
psnames Bool -> Bool -> Bool
|| 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]
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 String
"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 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
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 a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
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
[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
if
([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 String
"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 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 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 (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 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 (\(Name
n,RigCount
_,Binder Type
b) -> (Name
n, Binder Type -> Type
forall b. Binder b -> b
binderTy Binder Type
b)) Env
env)
proofSearch :: Bool
-> Bool
-> Bool
-> Bool
-> Int
-> (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
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
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
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
[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_ (\ 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)
ElabD ()
forall aux. Elab' aux ()
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)
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
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 [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
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 Name -> ElabD ()
forall aux. Name -> Elab' aux ()
autoArg (String -> Name
sUN String
"auto")
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 [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)
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)
Bool -> StateT (ElabState EState) TC Bool
forall a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
rs)
Maybe TypeInfo
Nothing ->
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)
[Name]
hs <- Elab' EState [Name]
forall aux. Elab' aux [Name]
get_holes
Bool -> StateT (ElabState EState) TC Bool
forall a. a -> StateT (ElabState EState) TC a
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))
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"
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)
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 :: 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
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
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 a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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 Int
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
- Int
1) [Name]
locs Set Type
tys')
(Int -> [Name] -> Set Type -> ElabD ()
resolveByLocals (Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Name]
locs Set Type
tys')
Bool
True)
(if Bool
fromProver
then String -> ElabD ()
forall a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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
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 Type
t <- Elab' EState Type
forall aux. Elab' aux Type
goal
let (Type
f, [Type]
_) = Type -> (Type, [Type])
forall n. TT n -> (TT n, [TT n])
unApply Type
t
case Type
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
resolveByLocals :: Int -> [Name] -> Set Type -> ElabD ()
resolveByLocals Int
d [Name]
locs 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 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"
tryCon :: Int -> [Name] -> Set Type -> Name -> ElabD ()
tryCon Int
d [Name]
locs Set Type
tys 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
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
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 a. [a] -> 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 a. [a] -> 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 a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't apply constructor"
let newhs :: [(Bool, Name)]
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)
((Bool, Name) -> ElabD ()) -> [(Bool, Name)] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Bool
_, 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 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
_ -> []
resolveTC :: Bool
-> Bool
-> Int
-> Term
-> Name
-> (PTerm -> ElabD ())
-> 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 [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' [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
resolveOpen :: [Name] -> ElabD ()
resolveOpen [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
Type
g <- Elab' EState Type
forall aux. Elab' aux Type
goal
let (Bool
argsok, [Int]
okholePos) = case Type -> [Name] -> Maybe [Int]
tcArgsOK Type
g [Name]
topholes of
Maybe [Int]
Nothing -> (Bool
False, [])
Just [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
then 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 -> 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 (Type
tc, [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 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
_ -> []
Bool -> String -> ElabD () -> ElabD ()
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"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]
++ String
"\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]
++ String
"\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
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
= 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 []
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 [a]
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 Type
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)))
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 ()
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 ()
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 Fails
ps <- Elab' EState Fails
forall aux. Elab' aux Fails
get_probs
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 -> 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
stk (Name
n:[Name]
ns)
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
fn
= 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 Type
g <- Elab' aux Type
forall aux. Elab' aux Type
goal
case Type
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
Int
num <- StateT (ElabState aux) TC Int
introImps
Int -> StateT (ElabState aux) TC Int
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
num Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 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
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
[] -> []
[(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)
[(Name, [PArg])]
xs -> String -> [(Bool, Int)]
forall a. HasCallStack => String -> a
error String
"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
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 a. [a] -> 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 a. [a] -> 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 a. String -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't apply interface"
((Bool, Name) -> ElabD ()) -> [(Bool, Name)] -> ElabD ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Bool
_,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 (Type
tc', [Type]
_) = 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 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
[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 (\ (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))
[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 {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"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 a. a -> StateT (ElabState EState) TC a
forall (m :: * -> *) a. Monad m => a -> m a
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)
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