{-# LANGUAGE FlexibleContexts, PatternGuards #-}
module Idris.Core.Unify(
match_unify, unify
, Fails, FailContext(..), FailAt(..)
, unrecoverable
) where
import Idris.Core.Evaluate
import Idris.Core.TT
import Control.Monad.State.Strict
import Data.List
import Data.Maybe
data FailAt = Match | Unify
deriving (Int -> FailAt -> ShowS
[FailAt] -> ShowS
FailAt -> String
(Int -> FailAt -> ShowS)
-> (FailAt -> String) -> ([FailAt] -> ShowS) -> Show FailAt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FailAt] -> ShowS
$cshowList :: [FailAt] -> ShowS
show :: FailAt -> String
$cshow :: FailAt -> String
showsPrec :: Int -> FailAt -> ShowS
$cshowsPrec :: Int -> FailAt -> ShowS
Show, FailAt -> FailAt -> Bool
(FailAt -> FailAt -> Bool)
-> (FailAt -> FailAt -> Bool) -> Eq FailAt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FailAt -> FailAt -> Bool
$c/= :: FailAt -> FailAt -> Bool
== :: FailAt -> FailAt -> Bool
$c== :: FailAt -> FailAt -> Bool
Eq)
data FailContext = FailContext { FailContext -> FC
fail_sourceloc :: FC,
FailContext -> Name
fail_fn :: Name,
FailContext -> Name
fail_param :: Name
}
deriving (FailContext -> FailContext -> Bool
(FailContext -> FailContext -> Bool)
-> (FailContext -> FailContext -> Bool) -> Eq FailContext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FailContext -> FailContext -> Bool
$c/= :: FailContext -> FailContext -> Bool
== :: FailContext -> FailContext -> Bool
$c== :: FailContext -> FailContext -> Bool
Eq, Int -> FailContext -> ShowS
[FailContext] -> ShowS
FailContext -> String
(Int -> FailContext -> ShowS)
-> (FailContext -> String)
-> ([FailContext] -> ShowS)
-> Show FailContext
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FailContext] -> ShowS
$cshowList :: [FailContext] -> ShowS
show :: FailContext -> String
$cshow :: FailContext -> String
showsPrec :: Int -> FailContext -> ShowS
$cshowsPrec :: Int -> FailContext -> ShowS
Show)
type Fails = [(TT Name, TT Name,
Bool,
Env, Err, [FailContext], FailAt)]
unrecoverable :: Fails -> Bool
unrecoverable :: Fails -> Bool
unrecoverable = ((TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Bool)
-> Fails -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Bool
forall a b c d t f g. (a, b, c, d, Err' t, f, g) -> Bool
bad
where bad :: (a, b, c, d, Err' t, f, g) -> Bool
bad (_,_,_,_, err :: Err' t
err, _, _) = Err' t -> Bool
forall t. Err' t -> Bool
unrec Err' t
err
unrec :: Err' t -> Bool
unrec (CantUnify r :: Bool
r _ _ _ _ _) = Bool -> Bool
not Bool
r
unrec (At _ e :: Err' t
e) = Err' t -> Bool
unrec Err' t
e
unrec (Elaborating _ _ _ e :: Err' t
e) = Err' t -> Bool
unrec Err' t
e
unrec (ElaboratingArg _ _ _ e :: Err' t
e) = Err' t -> Bool
unrec Err' t
e
unrec _ = Bool
False
data UInfo = UI Int Fails
deriving Int -> UInfo -> ShowS
[UInfo] -> ShowS
UInfo -> String
(Int -> UInfo -> ShowS)
-> (UInfo -> String) -> ([UInfo] -> ShowS) -> Show UInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UInfo] -> ShowS
$cshowList :: [UInfo] -> ShowS
show :: UInfo -> String
$cshow :: UInfo -> String
showsPrec :: Int -> UInfo -> ShowS
$cshowsPrec :: Int -> UInfo -> ShowS
Show
cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
cantUnify :: [FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [] r :: Bool
r t1 :: (t, Maybe Provenance)
t1 t2 :: (t, Maybe Provenance)
t2 e :: Err' t
e ctxt :: [(Name, t)]
ctxt i :: Int
i = Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt Int
i
cantUnify (FailContext fc :: FC
fc f :: Name
f x :: Name
x : prev :: [FailContext]
prev) r :: Bool
r t1 :: (t, Maybe Provenance)
t1 t2 :: (t, Maybe Provenance)
t2 e :: Err' t
e ctxt :: [(Name, t)]
ctxt i :: Int
i =
FC -> Err' t -> Err' t
forall t. FC -> Err' t -> Err' t
At FC
fc (Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
forall t. Name -> Name -> [(Name, Name)] -> Err' t -> Err' t
ElaboratingArg Name
f Name
x
((FailContext -> (Name, Name)) -> [FailContext] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(FailContext _ f' :: Name
f' x' :: Name
x') -> (Name
f', Name
x')) [FailContext]
prev)
(Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt Int
i))
match_unify :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] ->
TC [(Name, TT Name)]
match_unify :: Context
-> Env
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [Name]
-> [Name]
-> [FailContext]
-> TC [(Name, TT Name)]
match_unify ctxt :: Context
ctxt env :: Env
env (topx :: TT Name
topx, xfrom :: Maybe Provenance
xfrom) (topy :: TT Name
topy, yfrom :: Maybe Provenance
yfrom) inj :: [Name]
inj holes :: [Name]
holes from :: [FailContext]
from =
case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [] (Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topx)
(Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topy)) (Int -> Fails -> UInfo
UI 0 []) of
OK (v :: [(Name, TT Name)]
v, UI _ []) ->
do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall a r.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
[(Name, TT Name)] -> TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall a. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v')
res :: TC ([(Name, TT Name)], UInfo)
res ->
let topxn :: TT Name
topxn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topx)
topyn :: TT Name
topyn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topy) in
case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [] TT Name
topxn TT Name
topyn)
(Int -> Fails -> UInfo
UI 0 []) of
OK (v :: [(Name, TT Name)]
v, UI _ fails :: Fails
fails) ->
do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall a r.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
[(Name, TT Name)] -> TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall a. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v')
Error e :: Err' (TT Name)
e ->
case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ([((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [] TT Name
topxn TT Name
topy)
(Int -> Fails -> UInfo
UI 0 []) of
OK (v :: [(Name, TT Name)]
v, UI _ fails :: Fails
fails) ->
do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall a r.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
[(Name, TT Name)] -> TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall a. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v')
_ -> Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
e
where
un :: [((Name, Name), TT Name)] -> TT Name -> TT Name ->
StateT UInfo
TC [(Name, TT Name)]
un :: [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un names :: [((Name, Name), TT Name)]
names tx :: TT Name
tx@(P _ x :: Name
x _) tm :: TT Name
tm
| TT Name
tx TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
/= TT Name
tm Bool -> Bool -> Bool
&& Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
= do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *).
(MonadTrans t, MonadState UInfo (t TC)) =>
[((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> t TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
names TT Name
tx (Name
x, TT Name
tm)
un names :: [((Name, Name), TT Name)]
names tm :: TT Name
tm ty :: TT Name
ty@(P _ y :: Name
y _)
| TT Name
ty TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
/= TT Name
tm Bool -> Bool -> Bool
&& Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
= do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *).
(MonadTrans t, MonadState UInfo (t TC)) =>
[((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> t TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
names TT Name
ty (Name
y, TT Name
tm)
un bnames :: [((Name, Name), TT Name)]
bnames (V i :: Int
i) (P _ x :: Name
x _)
| [((Name, Name), TT Name)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
(Name, Name) -> Name
forall a b. (a, b) -> a
fst (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
(Name, Name) -> Name
forall a b. (a, b) -> b
snd (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
un bnames :: [((Name, Name), TT Name)]
bnames (P _ x :: Name
x _) (V i :: Int
i)
| [((Name, Name), TT Name)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
(Name, Name) -> Name
forall a b. (a, b) -> a
fst (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
(Name, Name) -> Name
forall a b. (a, b) -> b
snd (((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst ([((Name, Name), TT Name)]
bnames[((Name, Name), TT Name)] -> Int -> ((Name, Name), TT Name)
forall a. [a] -> Int -> a
!!Int
i)) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
un bnames :: [((Name, Name), TT Name)]
bnames (Bind x :: Name
x bx :: Binder (TT Name)
bx sx :: TT Name
sx) (Bind y :: Name
y by :: Binder (TT Name)
by sy :: TT Name
sy) | Binder (TT Name) -> Bool
forall b. Binder b -> Bool
notHole Binder (TT Name)
bx Bool -> Bool -> Bool
&& Binder (TT Name) -> Bool
forall b. Binder b -> Bool
notHole Binder (TT Name)
by
= do [(Name, TT Name)]
h1 <- [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB [((Name, Name), TT Name)]
bnames Binder (TT Name)
bx Binder (TT Name)
by
[(Name, TT Name)]
h2 <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un (((Name
x, Name
y), Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
bx) ((Name, Name), TT Name)
-> [((Name, Name), TT Name)] -> [((Name, Name), TT Name)]
forall a. a -> [a] -> [a]
: [((Name, Name), TT Name)]
bnames) TT Name
sx TT Name
sy
[((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
un names :: [((Name, Name), TT Name)]
names (App _ fx :: TT Name
fx ax :: TT Name
ax) (App _ fy :: TT Name
fy ay :: TT Name
ay)
= do [(Name, TT Name)]
hf <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
names TT Name
fx TT Name
fy
[(Name, TT Name)]
ha <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
names TT Name
ax TT Name
ay
[((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
names [(Name, TT Name)]
hf [(Name, TT Name)]
ha
un names :: [((Name, Name), TT Name)]
names x :: TT Name
x y :: TT Name
y
| OK True <- Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' Context
ctxt [Name]
holes TT Name
x TT Name
y = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x)
(Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
(TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
if (Bool -> Bool
not Bool
r) then TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err
else do UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
x, TT Name
y, Bool
True, Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err
uB :: [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB bnames :: [((Name, Name), TT Name)]
bnames (Let _ tx :: TT Name
tx vx :: TT Name
vx) (Let _ ty :: TT Name
ty vy :: TT Name
vy)
= do [(Name, TT Name)]
h1 <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
[(Name, TT Name)]
h2 <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
vx TT Name
vy
[((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
uB bnames :: [((Name, Name), TT Name)]
bnames (Lam _ tx :: TT Name
tx) (Lam _ ty :: TT Name
ty) = [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
uB bnames :: [((Name, Name), TT Name)]
bnames (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i tx :: TT Name
tx _) (Pi r' :: RigCount
r' i' :: Maybe ImplicitInfo
i' ty :: TT Name
ty _) = [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
uB bnames :: [((Name, Name), TT Name)]
bnames x :: Binder (TT Name)
x y :: Binder (TT Name)
y = do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x))
(Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y))
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
(Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Maybe Provenance
forall a. Maybe a
Nothing)
(Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s)
(Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y,
Bool
False,
Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
notHole :: Binder b -> Bool
notHole (Hole _) = Bool
False
notHole _ = Bool
True
sc :: Int -> m ()
sc i :: Int
i = do UI s :: Int
s f :: Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
UInfo -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI (Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) Fails
f)
unifyFail :: TT Name -> TT Name -> t TC b
unifyFail x :: TT Name
x y :: TT Name
y = do UI s :: Int
s f :: Fails
f <- t TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x)
(Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
(TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
(Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
UInfo -> t TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
x, TT Name
y, Bool
True, Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
TC b -> t TC b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC b -> t TC b) -> TC b -> t TC b
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC b
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err
combine :: [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
combine bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as ((n :: Name
n, t :: TT Name
t) : bs :: [(Name, TT Name)]
bs)
= case Name -> [(Name, TT Name)] -> Maybe (TT Name)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, TT Name)]
as of
Nothing -> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames ([(Name, TT Name)]
as [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name
n,TT Name
t)]) [(Name, TT Name)]
bs
Just t' :: TT Name
t' -> do [(Name, TT Name)]
ns <- [((Name, Name), TT Name)]
-> TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
un [((Name, Name), TT Name)]
bnames TT Name
t TT Name
t'
let ns' :: [(Name, TT Name)]
ns' = ((Name, TT Name) -> Bool) -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (x :: Name
x, _) -> Name
xName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n) [(Name, TT Name)]
ns
Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
[((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ([(Name, TT Name)]
ns' [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, TT Name)]
bs)
checkCycle :: [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> t TC [(Name, TT Name)]
checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm p :: (Name, TT Name)
p@(x :: Name
x, P _ x' :: Name
x' _) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm p :: (Name, TT Name)
p@(x :: Name
x, P _ _ _) = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm (x :: Name
x, tm :: TT Name
tm)
| Context -> Name -> TT Name -> Bool
conGuarded Context
ctxt Name
x TT Name
tm = TC [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> t TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err' (TT Name)
forall t. Name -> t -> [(Name, t)] -> Err' t
InfiniteUnify Name
x TT Name
tm (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env))
| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TT Name -> [Name]
forall n. Eq n => TT n -> [n]
freeNames TT Name
tm = TT Name -> TT Name -> t TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
xtm TT Name
tm
| Bool
otherwise = [((Name, Name), TT Name)]
-> (Name, TT Name) -> t TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t TC)) =>
[((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope [((Name, Name), TT Name)]
ns (Name
x, TT Name
tm)
checkScope :: [((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope ns :: [((Name, Name), TT Name)]
ns (x :: a
x, tm :: TT Name
tm) =
let v :: Int
v = Int -> TT Name -> Int
highV (-1) TT Name
tm in
if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
ns
then TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(a, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "SCOPE ERROR")
else [(a, TT Name)] -> t TC [(a, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a
x, Int -> [((Name, Name), TT Name)] -> TT Name -> TT Name
forall n. Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
v [((Name, Name), TT Name)]
ns TT Name
tm)]
bind :: Int -> [((n, n), TT n)] -> TT n -> TT n
bind i :: Int
i ns :: [((n, n), TT n)]
ns tm :: TT n
tm
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = TT n
tm
| Bool
otherwise = let ((x :: n
x,y :: n
y),ty :: TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. [a] -> Int -> a
!!Int
i in
AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
forall n. AppStatus n
MaybeHoles (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
y (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT n
ty) (Int -> [((n, n), TT n)] -> TT n -> TT n
bind (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [((n, n), TT n)]
ns TT n
tm))
(NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
x TT n
ty)
renameBinders :: Env -> (a, TT Name) -> (a, TT Name)
renameBinders env :: Env
env (x :: a
x, t :: TT Name
t) = (a
x, Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
t)
renameBindersTm :: Env -> TT Name -> TT Name
renameBindersTm :: Env -> TT Name -> TT Name
renameBindersTm env :: Env
env tm :: TT Name
tm = [Name] -> TT Name -> TT Name
uniqueBinders (((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall a b c. (a, b, c) -> a
fstEnv Env
env) TT Name
tm
where
uniqueBinders :: [Name] -> TT Name -> TT Name
uniqueBinders env :: [Name]
env (Bind n :: Name
n b :: Binder (TT Name)
b sc :: TT Name
sc)
| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
env
= let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n [Name]
env in
TT Name -> TT Name
forall n. TT n -> TT n
explicitHole (TT Name -> TT Name) -> TT Name -> TT Name
forall a b. (a -> b) -> a -> b
$ Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name] -> TT Name -> TT Name
uniqueBinders [Name]
env) Binder (TT Name)
b)
([Name] -> TT Name -> TT Name
uniqueBinders (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) (Name -> Name -> TT Name -> TT Name
forall n. Eq n => n -> n -> TT n -> TT n
rename Name
n Name
n' TT Name
sc))
| Bool
otherwise = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name] -> TT Name -> TT Name
uniqueBinders (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env)) Binder (TT Name)
b)
([Name] -> TT Name -> TT Name
uniqueBinders (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) TT Name
sc)
uniqueBinders env :: [Name]
env (App s :: AppStatus Name
s f :: TT Name
f a :: TT Name
a) = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([Name] -> TT Name -> TT Name
uniqueBinders [Name]
env TT Name
f) ([Name] -> TT Name -> TT Name
uniqueBinders [Name]
env TT Name
a)
uniqueBinders env :: [Name]
env t :: TT Name
t = TT Name
t
rename :: n -> n -> TT n -> TT n
rename n :: n
n n' :: n
n' (P nt :: NameType
nt x :: n
x ty :: TT n
ty) | n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
x = NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
nt n
n' TT n
ty
rename n :: n
n n' :: n
n' (Bind x :: n
x b :: Binder (TT n)
b sc :: TT n
sc) = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
x ((TT n -> TT n) -> Binder (TT n) -> Binder (TT n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (n -> n -> TT n -> TT n
rename n
n n
n') Binder (TT n)
b) (n -> n -> TT n -> TT n
rename n
n n
n' TT n
sc)
rename n :: n
n n' :: n
n' (App s :: AppStatus n
s f :: TT n
f a :: TT n
a) = AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
s (n -> n -> TT n -> TT n
rename n
n n
n' TT n
f) (n -> n -> TT n -> TT n
rename n
n n
n' TT n
a)
rename n :: n
n n' :: n
n' t :: TT n
t = TT n
t
explicitHole :: TT n -> TT n
explicitHole (Bind n :: n
n (Hole ty :: TT n
ty) sc :: TT n
sc)
= n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (TT n -> Binder (TT n)
forall b. b -> Binder b
Hole TT n
ty) (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
instantiate (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n TT n
ty) TT n
sc)
explicitHole t :: TT n
t = TT n
t
trimSolutions :: (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (topx :: TT Name
topx, xfrom :: Maybe Provenance
xfrom) (topy :: TT Name
topy, yfrom :: Maybe Provenance
yfrom) from :: [FailContext]
from env :: [(Name, r, Binder (TT Name))]
env topns :: [(a, TT a)]
topns = [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
forall a. Eq a => [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [] ([(a, TT a)] -> [(a, TT a)]
forall a. Eq a => [(a, TT a)] -> [(a, TT a)]
dropPairs [(a, TT a)]
topns)
where dropPairs :: [(a, TT a)] -> [(a, TT a)]
dropPairs [] = []
dropPairs (n :: (a, TT a)
n@(x :: a
x, P _ x' :: a
x' _) : ns :: [(a, TT a)]
ns)
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' = [(a, TT a)] -> [(a, TT a)]
dropPairs [(a, TT a)]
ns
| Bool
otherwise
= (a, TT a)
n (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)] -> [(a, TT a)]
dropPairs
(((a, TT a) -> Bool) -> [(a, TT a)] -> [(a, TT a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\t :: (a, TT a)
t -> case (a, TT a)
t of
(n :: a
n, P _ n' :: a
n' _) -> Bool -> Bool
not (a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x' Bool -> Bool -> Bool
&& a
n' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x)
_ -> Bool
True) [(a, TT a)]
ns)
dropPairs (n :: (a, TT a)
n : ns :: [(a, TT a)]
ns) = (a, TT a)
n (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)] -> [(a, TT a)]
dropPairs [(a, TT a)]
ns
followSols :: [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols vs :: [(a, a)]
vs [] = [(a, TT a)] -> TC [(a, TT a)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
followSols vs :: [(a, a)]
vs ((n :: a
n, P _ t :: a
t _) : ns :: [(a, TT a)]
ns)
| Just t' :: TT a
t' <- a -> [(a, TT a)] -> Maybe (TT a)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup a
t [(a, TT a)]
ns
= do [(a, a)]
vs' <- case TT a
t' of
P _ tn :: a
tn _ ->
if (a
n, a
tn) (a, a) -> [(a, a)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(a, a)]
vs then
Err' (TT Name) -> TC [(a, a)]
forall a. Err' (TT Name) -> TC a
tfail ([FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
False (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
(String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") ([(Name, r, Binder (TT Name))] -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv [(Name, r, Binder (TT Name))]
env) 0)
else [(a, a)] -> TC [(a, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
n, a
tn) (a, a) -> [(a, a)] -> [(a, a)]
forall a. a -> [a] -> [a]
: [(a, a)]
vs)
_ -> [(a, a)] -> TC [(a, a)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a, a)]
vs
[(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [(a, a)]
vs' ((a
n, TT a
t') (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)]
ns)
followSols vs :: [(a, a)]
vs (n :: (a, TT a)
n : ns :: [(a, TT a)]
ns) = do [(a, TT a)]
ns' <- [(a, a)] -> [(a, TT a)] -> TC [(a, TT a)]
followSols [(a, a)]
vs [(a, TT a)]
ns
[(a, TT a)] -> TC [(a, TT a)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, TT a)] -> TC [(a, TT a)]) -> [(a, TT a)] -> TC [(a, TT a)]
forall a b. (a -> b) -> a -> b
$ (a, TT a)
n (a, TT a) -> [(a, TT a)] -> [(a, TT a)]
forall a. a -> [a] -> [a]
: [(a, TT a)]
ns'
unify :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) ->
[Name] -> [Name] -> [Name] -> [FailContext] ->
TC ([(Name, TT Name)], Fails)
unify :: Context
-> Env
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [Name]
-> [Name]
-> [Name]
-> [FailContext]
-> TC ([(Name, TT Name)], Fails)
unify ctxt :: Context
ctxt env :: Env
env (topx :: TT Name
topx, xfrom :: Maybe Provenance
xfrom) (topy :: TT Name
topy, yfrom :: Maybe Provenance
yfrom) inj :: [Name]
inj holes :: [Name]
holes usersupp :: [Name]
usersupp from :: [FailContext]
from =
case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un Bool
False [] (Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topx)
(Env -> TT Name -> TT Name
renameBindersTm Env
env TT Name
topy)) (Int -> Fails -> UInfo
UI 0 []) of
OK (v :: [(Name, TT Name)]
v, UI _ []) -> do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall a r.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
([(Name, TT Name)], Fails) -> TC ([(Name, TT Name)], Fails)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall a. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v', [])
res :: TC ([(Name, TT Name)], UInfo)
res ->
let topxn :: TT Name
topxn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topx)
topyn :: TT Name
topyn = Env -> TT Name -> TT Name
renameBindersTm Env
env (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
topy) in
case StateT UInfo TC [(Name, TT Name)]
-> UInfo -> TC ([(Name, TT Name)], UInfo)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un Bool
False [] TT Name
topxn TT Name
topyn)
(Int -> Fails -> UInfo
UI 0 []) of
OK (v :: [(Name, TT Name)]
v, UI _ fails :: Fails
fails) ->
do [(Name, TT Name)]
v' <- (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> Env
-> [(Name, TT Name)]
-> TC [(Name, TT Name)]
forall a r.
Eq a =>
(TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> [FailContext]
-> [(Name, r, Binder (TT Name))]
-> [(a, TT a)]
-> TC [(a, TT a)]
trimSolutions (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from Env
env [(Name, TT Name)]
v
([(Name, TT Name)], Fails) -> TC ([(Name, TT Name)], Fails)
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, TT Name) -> (Name, TT Name))
-> [(Name, TT Name)] -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (Name, TT Name) -> (Name, TT Name)
forall a. Env -> (a, TT Name) -> (a, TT Name)
renameBinders Env
env) [(Name, TT Name)]
v', Fails -> Fails
forall a. [a] -> [a]
reverse Fails
fails)
Error e :: Err' (TT Name)
e -> Err' (TT Name) -> TC ([(Name, TT Name)], Fails)
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
e
where
injective :: TT n -> Bool
injective (P (DCon _ _ _) _ _) = Bool
True
injective (P (TCon _ _) _ _) = Bool
True
injective (App _ f :: TT n
f a :: TT n
a) = TT n -> Bool
injective TT n
f
injective _ = Bool
False
injectiveVar :: TT Name -> Bool
injectiveVar (P _ n :: Name
n _) = Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj
injectiveVar (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> Bool
injectiveVar TT Name
f
injectiveVar _ = Bool
False
injectiveApp :: TT Name -> Bool
injectiveApp x :: TT Name
x = TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
x Bool -> Bool -> Bool
|| TT Name -> Bool
injectiveVar TT Name
x
notP :: TT n -> Bool
notP (P _ _ _) = Bool
False
notP _ = Bool
True
sc :: Int -> m ()
sc i :: Int
i = do UI s :: Int
s f :: Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
UInfo -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI (Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
i) Fails
f)
uplus :: m b -> m b -> m b
uplus u1 :: m b
u1 u2 :: m b
u2 = do UI s :: Int
s f :: Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
b
r <- m b
u1
UI s :: Int
s f' :: Fails
f' <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
if (Fails -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Fails -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
f')
then b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return b
r
else do UInfo -> m ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s Fails
f); m b
u2
un :: Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
StateT UInfo
TC [(Name, TT Name)]
un :: Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env
un' :: Env -> Bool -> [((Name, Name), TT Name)] -> TT Name -> TT Name ->
StateT UInfo
TC [(Name, TT Name)]
un' :: Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names x :: TT Name
x y :: TT Name
y | TT Name
x TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
y = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon _ _ _) x :: Name
x _) topy :: TT Name
topy@(P (DCon _ _ _) y :: Name
y _)
| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon _ _) x :: Name
x _) topy :: TT Name
topy@(P (TCon _ _) y :: Name
y _)
| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon _ _ _) x :: Name
x _) topy :: TT Name
topy@(P (TCon _ _) y :: Name
y _)
= TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon _ _) x :: Name
x _) topy :: TT Name
topy@(P (DCon _ _ _) y :: Name
y _)
= TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Constant _) topy :: TT Name
topy@(P (TCon _ _) y :: Name
y _)
= TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon _ _) x :: Name
x _) topy :: TT Name
topy@(Constant _)
= TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
topx TT Name
topy
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames tx :: TT Name
tx@(P _ x :: Name
x _) ty :: TT Name
ty@(P _ y :: Name
y _)
| (Name
x,Name
y) (Name, Name) -> [(Name, Name)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames Bool -> Bool -> Bool
|| Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
tx Bool -> Bool -> Bool
&& Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
= TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tx TT Name
ty
| TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
ty Bool -> Bool -> Bool
&& Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
= TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tx TT Name
ty
| TT Name
tx TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
/= TT Name
ty Bool -> Bool -> Bool
&& (Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
Bool -> Bool -> Bool
&& (Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
= case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Name -> Env -> Integer
forall t t b c. (Eq t, Num t) => t -> t -> [(t, b, c)] -> t
envPos 0 Name
x Env
env) (Integer -> Name -> Env -> Integer
forall t t b c. (Eq t, Num t) => t -> t -> [(t, b, c)] -> t
envPos 0 Name
y Env
env) of
LT -> do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
tx (Name
x, TT Name
ty)
_ -> do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
ty (Name
y, TT Name
tx)
where envPos :: t -> t -> [(t, b, c)] -> t
envPos i :: t
i n :: t
n ((n' :: t
n',_,_):env :: [(t, b, c)]
env) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
n' = t
i
envPos i :: t
i n :: t
n (_:env :: [(t, b, c)]
env) = t -> t -> [(t, b, c)] -> t
envPos (t
it -> t -> t
forall a. Num a => a -> a -> a
+1) t
n [(t, b, c)]
env
envPos _ _ _ = 100000
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames xtm :: TT Name
xtm@(P _ x :: Name
x _) tm :: TT Name
tm
| TT Name -> Bool
pureTerm TT Name
tm, Env -> Name -> Bool
holeIn Env
env Name
x Bool -> Bool -> Bool
|| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
= do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
[(Name, TT Name)]
x <- [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
xtm (Name
x, TT Name
tm)
if (TT Name -> Bool
forall n. TT n -> Bool
notP TT Name
tm Bool -> Bool -> Bool
&& Bool
fn)
then TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
xtm TT Name
tm
else do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
x
| TT Name -> Bool
pureTerm TT Name
tm, Bool -> Bool
not (TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
xtm) Bool -> Bool -> Bool
&& TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
tm
= do [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
xtm (Name
x, TT Name
tm)
TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
xtm TT Name
tm
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames tm :: TT Name
tm ytm :: TT Name
ytm@(P _ y :: Name
y _)
| TT Name -> Bool
pureTerm TT Name
tm, Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
= do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
[(Name, TT Name)]
x <- [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
ytm (Name
y, TT Name
tm)
if (TT Name -> Bool
forall n. TT n -> Bool
notP TT Name
tm Bool -> Bool -> Bool
&& Bool
fn)
then TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tm TT Name
ytm
else do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
x
| TT Name -> Bool
pureTerm TT Name
tm, Bool -> Bool
not (TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
ytm) Bool -> Bool -> Bool
&& TT Name -> Bool
forall n. TT n -> Bool
injective TT Name
tm
= do [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
ytm (Name
y, TT Name
tm)
TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
tm TT Name
ytm
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (V i :: Int
i) (P _ x :: Name
x _)
| [((Name, Name), TT Name)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
(Name, Name) -> Name
forall a b. (a, b) -> a
fst (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
(Name, Name) -> Name
forall a b. (a, b) -> b
snd (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (P _ x :: Name
x _) (V i :: Int
i)
| [((Name, Name), TT Name)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
bnames Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i,
(Name, Name) -> Name
forall a b. (a, b) -> a
fst (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x Bool -> Bool -> Bool
||
(Name, Name) -> Name
forall a b. (a, b) -> b
snd (((((Name, Name), TT Name) -> (Name, Name))
-> [((Name, Name), TT Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Name), TT Name) -> (Name, Name)
forall a b. (a, b) -> a
fst [((Name, Name), TT Name)]
bnames)[(Name, Name)] -> Int -> (Name, Name)
forall a. [a] -> Int -> a
!!Int
i) Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Bind n :: Name
n (Hole t :: TT Name
t) sc :: TT Name
sc) y :: TT Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
topx TT Name
y
un' env :: Env
env fn :: Bool
fn names :: [((Name, Name), TT Name)]
names x :: TT Name
x topy :: TT Name
topy@(Bind n :: Name
n (Hole t :: TT Name
t) sc :: TT Name
sc) = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
x TT Name
topy
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames tm :: TT Name
tm app :: TT Name
app@(App _ _ _)
| (mvtm :: TT Name
mvtm@(P _ mv :: Name
mv _), args :: [TT Name]
args) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
app,
Env -> Name -> Bool
holeIn Env
env Name
mv Bool -> Bool -> Bool
|| Name
mv Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes,
(TT Name -> Bool) -> [TT Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TT Name -> Bool
rigid [TT Name]
args,
[Name] -> [Int] -> TT Name -> Bool
forall (t :: * -> *).
Foldable t =>
t Name -> [Int] -> TT Name -> Bool
containsOnly ((TT Name -> Maybe Name) -> [TT Name] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TT Name -> Maybe Name
forall a. TT a -> Maybe a
getname [TT Name]
args) ((TT Name -> Maybe Int) -> [TT Name] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe TT Name -> Maybe Int
forall n. TT n -> Maybe Int
getV [TT Name]
args) TT Name
tm
=
[((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle [((Name, Name), TT Name)]
bnames TT Name
mvtm (Name
mv, [(Name, RigCount, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, RigCount, TT n)] -> TT n -> TT n
eta [] (TT Name -> TT Name) -> TT Name -> TT Name
forall a b. (a -> b) -> a -> b
$ [TT Name] -> TT Name -> TT Name
bindLams [TT Name]
args (Env -> TT Name -> TT Name
forall n b. [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv Env
env TT Name
tm))
where rigid :: TT Name -> Bool
rigid (V i :: Int
i) = Bool
True
rigid (P _ t :: Name
t _) = Name
t Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall a b c. (a, b, c) -> a
fstEnv Env
env Bool -> Bool -> Bool
&&
Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
t Bool -> Bool -> Bool
|| Name
t Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
rigid _ = Bool
False
getV :: TT n -> Maybe Int
getV (V i :: Int
i) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
getV _ = Maybe Int
forall a. Maybe a
Nothing
getname :: TT a -> Maybe a
getname (P _ n :: a
n _) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
getname _ = Maybe a
forall a. Maybe a
Nothing
containsOnly :: t Name -> [Int] -> TT Name -> Bool
containsOnly args :: t Name
args vs :: [Int]
vs (V i :: Int
i) = Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
vs
containsOnly args :: t Name
args vs :: [Int]
vs (P Bound n :: Name
n ty :: TT Name
ty)
= Name
n Name -> t Name -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
args Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
ty
containsOnly args :: t Name
args vs :: [Int]
vs (P _ n :: Name
n ty :: TT Name
ty)
= Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
n Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
ty
containsOnly args :: t Name
args vs :: [Int]
vs (App _ f :: TT Name
f a :: TT Name
a)
= t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
f Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
a
containsOnly args :: t Name
args vs :: [Int]
vs (Bind _ b :: Binder (TT Name)
b sc :: TT Name
sc)
= t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b) Bool -> Bool -> Bool
&&
t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args (0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> Int
forall a. Num a => a -> a -> a
+1) [Int]
vs) TT Name
sc
containsOnly args :: t Name
args vs :: [Int]
vs _ = Bool
True
bindLams :: [TT Name] -> TT Name -> TT Name
bindLams [] tm :: TT Name
tm = TT Name
tm
bindLams (a :: TT Name
a : as :: [TT Name]
as) tm :: TT Name
tm = TT Name -> TT Name -> TT Name
bindLam TT Name
a ([TT Name] -> TT Name -> TT Name
bindLams [TT Name]
as TT Name
tm)
bindLam :: TT Name -> TT Name -> TT Name
bindLam (V i :: Int
i) tm :: TT Name
tm = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind ((Name, RigCount, Binder (TT Name)) -> Name
forall a b c. (a, b, c) -> a
fstEnv (Env
env Env -> Int -> (Name, RigCount, Binder (TT Name))
forall a. [a] -> Int -> a
!! Int
i))
(RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy ((Name, RigCount, Binder (TT Name)) -> Binder (TT Name)
forall a b c. (a, b, c) -> c
sndEnv (Env
env Env -> Int -> (Name, RigCount, Binder (TT Name))
forall a. [a] -> Int -> a
!! Int
i))))
TT Name
tm
bindLam (P _ n :: Name
n ty :: TT Name
ty) tm :: TT Name
tm = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT Name
ty) TT Name
tm
bindLam _ tm :: TT Name
tm = String -> TT Name
forall a. HasCallStack => String -> a
error "Can't happen [non rigid bindLam]"
substEnv :: [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv [] tm :: TT n
tm = TT n
tm
substEnv ((n :: n
n, _, t :: Binder (TT n)
t) : env :: [(n, b, Binder (TT n))]
env) tm :: TT n
tm
= [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv [(n, b, Binder (TT n))]
env (TT n -> TT n -> TT n
forall n. TT n -> TT n -> TT n
substV (NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
n (Binder (TT n) -> TT n
forall b. Binder b -> b
binderTy Binder (TT n)
t)) TT n
tm)
eta :: [(n, RigCount, TT n)] -> TT n -> TT n
eta ks :: [(n, RigCount, TT n)]
ks (Bind n :: n
n (Lam r :: RigCount
r ty :: TT n
ty) sc :: TT n
sc) = [(n, RigCount, TT n)] -> TT n -> TT n
eta ((n
n, RigCount
r, TT n
ty) (n, RigCount, TT n)
-> [(n, RigCount, TT n)] -> [(n, RigCount, TT n)]
forall a. a -> [a] -> [a]
: [(n, RigCount, TT n)]
ks) TT n
sc
eta ks :: [(n, RigCount, TT n)]
ks t :: TT n
t = [(n, RigCount, TT n)] -> TT n -> TT n
rebind [(n, RigCount, TT n)]
ks TT n
t
rebind :: [(n, RigCount, TT n)] -> TT n -> TT n
rebind ((n :: n
n, r :: RigCount
r, ty :: TT n
ty) : ks :: [(n, RigCount, TT n)]
ks) (App _ f :: TT n
f (P _ n' :: n
n' _))
| n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
== n
n' = [(n, RigCount, TT n)] -> TT n -> TT n
eta [(n, RigCount, TT n)]
ks TT n
f
rebind ((n :: n
n, r :: RigCount
r, ty :: TT n
ty) : ks :: [(n, RigCount, TT n)]
ks) t :: TT n
t = [(n, RigCount, TT n)] -> TT n -> TT n
rebind [(n, RigCount, TT n)]
ks (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
r TT n
ty) TT n
t)
rebind _ t :: TT n
t = TT n
t
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App _ _ _) appy :: TT Name
appy@(App _ _ _)
= Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
forall p.
Env
-> p
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
unApp Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
appx TT Name
appy
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames x :: TT Name
x (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ y :: TT Name
y (P Bound n' :: Name
n' _)))
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ x :: TT Name
x (P Bound n' :: Name
n' _))) y :: TT Name
y
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames x :: TT Name
x (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ y :: TT Name
y (V 0)))
= Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind n :: Name
n (Lam _ t :: TT Name
t) (App _ x :: TT Name
x (V 0))) y :: TT Name
y
= Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (App _ f :: TT Name
f x :: TT Name
x) (Bind n :: Name
n (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i t :: TT Name
t k :: TT Name
k) y :: TT Name
y)
| Name -> TT Name -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence Name
n TT Name
y Bool -> Bool -> Bool
&& TT Name -> Bool
injectiveApp TT Name
f
= do [(Name, TT Name)]
ux <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
[(Name, TT Name)]
uf <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
f (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (Int -> String -> Name
sMN 0 "uv") (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW (UExp -> TT Name
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] 0)))
(Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount
-> Maybe ImplicitInfo -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) (Int -> TT Name
forall n. Int -> TT n
V 1)))
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
ux [(Name, TT Name)]
uf
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind n :: Name
n (Pi r :: RigCount
r i :: Maybe ImplicitInfo
i t :: TT Name
t k :: TT Name
k) y :: TT Name
y) (App _ f :: TT Name
f x :: TT Name
x)
| Name -> TT Name -> Bool
forall n. Eq n => n -> TT n -> Bool
noOccurrence Name
n TT Name
y Bool -> Bool -> Bool
&& TT Name -> Bool
injectiveApp TT Name
f
= do [(Name, TT Name)]
ux <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
y TT Name
x
[(Name, TT Name)]
uf <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames (Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (Int -> String -> Name
sMN 0 "uv") (RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW (UExp -> TT Name
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] 0)))
(Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n (RigCount
-> Maybe ImplicitInfo -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) (Int -> TT Name
forall n. Int -> TT n
V 1))) TT Name
f
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
ux [(Name, TT Name)]
uf
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames (Bind x :: Name
x bx :: Binder (TT Name)
bx sx :: TT Name
sx) (Bind y :: Name
y by :: Binder (TT Name)
by sy :: TT Name
sy)
| Binder (TT Name) -> Binder (TT Name) -> Bool
forall b b. Binder b -> Binder b -> Bool
sameBinder Binder (TT Name)
bx Binder (TT Name)
by
= do [(Name, TT Name)]
h1 <- Env
-> [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB Env
env [((Name, Name), TT Name)]
bnames Binder (TT Name)
bx Binder (TT Name)
by
[(Name, TT Name)]
h2 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' ((Name
x, RigCount
RigW, Binder (TT Name)
bx) (Name, RigCount, Binder (TT Name)) -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env) Bool
False (((Name
x,Name
y),Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
bx)((Name, Name), TT Name)
-> [((Name, Name), TT Name)] -> [((Name, Name), TT Name)]
forall a. a -> [a] -> [a]
:[((Name, Name), TT Name)]
bnames) TT Name
sx TT Name
sy
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
where sameBinder :: Binder b -> Binder b -> Bool
sameBinder (Lam _ _) (Lam _ _) = Bool
True
sameBinder (Pi _ i :: Maybe ImplicitInfo
i _ _) (Pi _ i' :: Maybe ImplicitInfo
i' _ _) = Bool
True
sameBinder _ _ = Bool
False
un' env :: Env
env fn :: Bool
fn bnames :: [((Name, Name), TT Name)]
bnames x :: TT Name
x y :: TT Name
y
| OK True <- Context -> [Name] -> TT Name -> TT Name -> TC Bool
convEq' Context
ctxt [Name]
holes TT Name
x TT Name
y = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| TT Name -> Bool
isUniverse TT Name
x Bool -> Bool -> Bool
&& TT Name -> Bool
isUniverse TT Name
y = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x)
(Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
(TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) (Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
if (Bool -> Bool
not Bool
r) then TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err
else do UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
x, TT Name
y, Bool
True, Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
unApp :: Env
-> p
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
unApp env :: Env
env fn :: p
fn bnames :: [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App _ fx :: TT Name
fx ax :: TT Name
ax) appy :: TT Name
appy@(App _ fy :: TT Name
fy ay :: TT Name
ay)
| (TT Name -> Bool
injectiveApp TT Name
fx Bool -> Bool -> Bool
&& TT Name
fx TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
fy)
= Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
ax TT Name
ay
| (TT Name -> Bool
injectiveApp TT Name
fx Bool -> Bool -> Bool
&& TT Name -> Bool
injectiveApp TT Name
fy)
Bool -> Bool -> Bool
|| (TT Name -> Bool
injectiveApp TT Name
fx Bool -> Bool -> Bool
&& TT Name -> Bool
metavarApp TT Name
fy Bool -> Bool -> Bool
&& TT Name
ax TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
ay)
Bool -> Bool -> Bool
|| (TT Name -> Bool
injectiveApp TT Name
fy Bool -> Bool -> Bool
&& TT Name -> Bool
metavarApp TT Name
fx Bool -> Bool -> Bool
&& TT Name
ax TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
ay)
Bool -> Bool -> Bool
|| (TT Name -> TT Name -> Bool
injectiveTC TT Name
fx TT Name
fy)
= do let (headx :: TT Name
headx, _) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fx
let (heady :: TT Name
heady, _) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fy
TT Name -> TT Name -> StateT UInfo TC [Any]
forall a (t :: (* -> *) -> * -> *) a.
(Eq a, MonadState UInfo (t TC), MonadTrans t) =>
TT a -> TT a -> t TC [a]
checkHeads TT Name
headx TT Name
heady
StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) b. MonadState UInfo m => m b -> m b -> m b
uplus
(do [(Name, TT Name)]
hf <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
True [((Name, Name), TT Name)]
bnames TT Name
fx TT Name
fy
let ax' :: TT Name
ax' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall a. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
hf Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ax)
let ay' :: TT Name
ay' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall a. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
hf Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ay)
[(Name, TT Name)]
ha <- StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) b. MonadState UInfo m => m b -> m b -> m b
uplus (Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ax)
([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
hf TT Name
ay))
(Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
ax' TT Name
ay')
Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
hf [(Name, TT Name)]
ha)
(do [(Name, TT Name)]
ha <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
ax TT Name
ay
let fx' :: TT Name
fx' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall a. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
ha Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fx)
let fy' :: TT Name
fy' = [(Name, TT Name)] -> Context -> Env -> TT Name -> TT Name
forall a. [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [(Name, TT Name)]
ha Context
ctxt Env
env ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fy)
[(Name, TT Name)]
hf <- StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) b. MonadState UInfo m => m b -> m b -> m b
uplus (Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames ([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fx)
([(Name, TT Name)] -> TT Name -> TT Name
forall n. Eq n => [(n, TT n)] -> TT n -> TT n
substNames [(Name, TT Name)]
ha TT Name
fy))
(Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
fx' TT Name
fy')
Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
hf [(Name, TT Name)]
ha)
| Bool
otherwise = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
appx TT Name
appy
where hnormalise :: [a] -> Context -> Env -> TT Name -> TT Name
hnormalise [] _ _ t :: TT Name
t = TT Name
t
hnormalise ns :: [a]
ns ctxt :: Context
ctxt env :: Env
env t :: TT Name
t = Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
t
checkHeads :: TT a -> TT a -> t TC [a]
checkHeads (P (DCon _ _ _) x :: a
x _) (P (DCon _ _ _) y :: a
y _)
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y = TT Name -> TT Name -> t TC [a]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
checkHeads (P (TCon _ _) x :: a
x _) (P (TCon _ _) y :: a
y _)
| a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
y = TT Name -> TT Name -> t TC [a]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
checkHeads (P (DCon _ _ _) x :: a
x _) (P (TCon _ _) y :: a
y _)
= TT Name -> TT Name -> t TC [a]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
checkHeads (P (TCon _ _) x :: a
x _) (P (DCon _ _ _) y :: a
y _)
= TT Name -> TT Name -> t TC [a]
forall (t :: (* -> *) -> * -> *) b.
(MonadState UInfo (t TC), MonadTrans t) =>
TT Name -> TT Name -> t TC b
unifyFail TT Name
appx TT Name
appy
checkHeads _ _ = [a] -> t TC [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
metavarApp :: TT Name -> Bool
metavarApp tm :: TT Name
tm = let (f :: TT Name
f, args :: [TT Name]
args) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm in
(TT Name -> Bool
metavar TT Name
f Bool -> Bool -> Bool
&&
(TT Name -> Bool) -> [TT Name] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\x :: TT Name
x -> TT Name -> Bool
metavarApp TT Name
x) [TT Name]
args
Bool -> Bool -> Bool
&& [TT Name] -> [TT Name]
forall a. Eq a => [a] -> [a]
nub [TT Name]
args [TT Name] -> [TT Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [TT Name]
args) Bool -> Bool -> Bool
||
TT Name -> Bool
globmetavar TT Name
tm
globmetavar :: TT Name -> Bool
globmetavar t :: TT Name
t = case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t of
(P _ x :: Name
x _, _) ->
case Name -> Context -> [Def]
lookupDef Name
x Context
ctxt of
[TyDecl _ _] -> Bool
True
_ -> Bool
False
_ -> Bool
False
metavar :: TT Name -> Bool
metavar t :: TT Name
t = case TT Name
t of
P _ x :: Name
x _ -> (Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Name]
usersupp Bool -> Bool -> Bool
&&
(Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes Bool -> Bool -> Bool
|| Env -> Name -> Bool
holeIn Env
env Name
x))
Bool -> Bool -> Bool
|| TT Name -> Bool
globmetavar TT Name
t
_ -> Bool
False
injectiveTC :: TT Name -> TT Name -> Bool
injectiveTC t :: TT Name
t@(P Ref n :: Name
n _) t' :: TT Name
t'@(P Ref n' :: Name
n' _)
| Just ni :: Bool
ni <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n Context
ctxt,
Just ni' :: Bool
ni' <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n' Context
ctxt
= (Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' Bool -> Bool -> Bool
&& Bool
ni) Bool -> Bool -> Bool
||
(Bool
ni Bool -> Bool -> Bool
&& TT Name -> Bool
metavar TT Name
t') Bool -> Bool -> Bool
||
(TT Name -> Bool
metavar TT Name
t Bool -> Bool -> Bool
&& Bool
ni')
injectiveTC (App _ f :: TT Name
f a :: TT Name
a) (App _ f' :: TT Name
f' a' :: TT Name
a') = TT Name -> TT Name -> Bool
injectiveTC TT Name
f TT Name
f'
injectiveTC _ _ = Bool
False
unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail :: TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail x :: TT Name
x y :: TT Name
y
= do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x) (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
(TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
(Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
topx, TT Name
topy, Bool
True, Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
unifyFail :: TT Name -> TT Name -> t TC b
unifyFail x :: TT Name
x y :: TT Name
y = do UI s :: Int
s f :: Fails
f <- t TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
x) (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
y)
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r
(TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
(Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (TT Name
x, Maybe Provenance
forall a. Maybe a
Nothing) (TT Name
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s) (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
UInfo -> t TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((TT Name
topx, TT Name
topy, Bool
True, Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
TC b -> t TC b
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC b -> t TC b) -> TC b -> t TC b
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC b
forall a. Err' (TT Name) -> TC a
tfail Err' (TT Name)
err
uB :: Env
-> [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (Let _ tx :: TT Name
tx vx :: TT Name
vx) (Let _ ty :: TT Name
ty vy :: TT Name
vy)
= do [(Name, TT Name)]
h1 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
[(Name, TT Name)]
h2 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
vx TT Name
vy
Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (Guess tx :: TT Name
tx vx :: TT Name
vx) (Guess ty :: TT Name
ty vy :: TT Name
vy)
= do [(Name, TT Name)]
h1 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
[(Name, TT Name)]
h2 <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
vx TT Name
vy
Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
h1 [(Name, TT Name)]
h2
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (Lam _ tx :: TT Name
tx) (Lam _ ty :: TT Name
ty) = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (Pi _ _ tx :: TT Name
tx _) (Pi _ _ ty :: TT Name
ty _) = do Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1; Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (Hole tx :: TT Name
tx) (Hole ty :: TT Name
ty) = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames (PVar _ tx :: TT Name
tx) (PVar _ ty :: TT Name
ty) = Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
tx TT Name
ty
uB env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames x :: Binder (TT Name)
x y :: Binder (TT Name)
y
= do UI s :: Int
s f :: Fails
f <- StateT UInfo TC UInfo
forall s (m :: * -> *). MonadState s m => m s
get
let r :: Bool
r = TT Name -> TT Name -> Bool
recoverable (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x))
(Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y))
let err :: Err' (TT Name)
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
[FailContext]
-> Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
cantUnify [FailContext]
from Bool
r (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom)
(Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err' (TT Name)
-> [(Name, TT Name)]
-> Int
-> Err' (TT Name)
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
r (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Maybe Provenance
forall a. Maybe a
Nothing) (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y, Maybe Provenance
forall a. Maybe a
Nothing) (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "") (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s)
(Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env) Int
s
UInfo -> StateT UInfo TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Int -> Fails -> UInfo
UI Int
s ((Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
x, Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
y,
Bool
False,
Env
env, Err' (TT Name)
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err' (TT Name), [FailContext],
FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
checkCycle :: [((Name, Name), TT Name)]
-> TT Name -> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm p :: (Name, TT Name)
p@(x :: Name
x, P _ _ _) = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
checkCycle ns :: [((Name, Name), TT Name)]
ns xtm :: TT Name
xtm (x :: Name
x, tm :: TT Name
tm)
| Context -> Name -> TT Name -> Bool
conGuarded Context
ctxt Name
x TT Name
tm = TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)])
-> TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(Name, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err' (TT Name)
forall t. Name -> t -> [(Name, t)] -> Err' t
InfiniteUnify Name
x TT Name
tm (Env -> [(Name, TT Name)]
forall a r b. [(a, r, Binder b)] -> [(a, b)]
errEnv Env
env))
| Name
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` TT Name -> [Name]
forall n. Eq n => TT n -> [n]
freeNames TT Name
tm = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
xtm TT Name
tm
| Bool
otherwise = [((Name, Name), TT Name)]
-> (Name, TT Name) -> StateT UInfo TC [(Name, TT Name)]
forall (t :: (* -> *) -> * -> *) a.
(MonadTrans t, Monad (t TC)) =>
[((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope [((Name, Name), TT Name)]
ns (Name
x, TT Name
tm)
checkScope :: [((Name, Name), TT Name)] -> (a, TT Name) -> t TC [(a, TT Name)]
checkScope ns :: [((Name, Name), TT Name)]
ns (x :: a
x, tm :: TT Name
tm) | TT Name -> Bool
pureTerm TT Name
tm =
let v :: Int
v = Int -> TT Name -> Int
highV (-1) TT Name
tm in
if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Name, Name), TT Name)]
ns
then TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(a, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "SCOPE ERROR")
else [(a, TT Name)] -> t TC [(a, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a
x, Int -> [((Name, Name), TT Name)] -> TT Name -> TT Name
forall n. Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
v [((Name, Name), TT Name)]
ns TT Name
tm)]
checkScope ns :: [((Name, Name), TT Name)]
ns (x :: a
x, tm :: TT Name
tm) = TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err' (TT Name) -> TC [(a, TT Name)]
forall a. Err' (TT Name) -> TC a
tfail (String -> Err' (TT Name)
forall t. String -> Err' t
Msg "HOLE ERROR")
bind :: Int -> [((n, n), TT n)] -> TT n -> TT n
bind i :: Int
i ns :: [((n, n), TT n)]
ns tm :: TT n
tm
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = TT n
tm
| Bool
otherwise = let ((x :: n
x,y :: n
y),ty :: TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. [a] -> Int -> a
!!Int
i in
AppStatus n -> TT n -> TT n -> TT n
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus n
forall n. AppStatus n
MaybeHoles (n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
y (RigCount -> TT n -> Binder (TT n)
forall b. RigCount -> b -> Binder b
Lam RigCount
RigW TT n
ty) (Int -> [((n, n), TT n)] -> TT n -> TT n
bind (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [((n, n), TT n)]
ns TT n
tm))
(NameType -> n -> TT n -> TT n
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound n
x TT n
ty)
combine :: Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
combine env :: Env
env bnames :: [((Name, Name), TT Name)]
bnames as :: [(Name, TT Name)]
as ((n :: Name
n, t :: TT Name
t) : bs :: [(Name, TT Name)]
bs)
= case Name -> [(Name, TT Name)] -> Maybe (TT Name)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, TT Name)]
as of
Nothing -> Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames ([(Name, TT Name)]
as [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name
n,TT Name
t)]) [(Name, TT Name)]
bs
Just t' :: TT Name
t' -> do [(Name, TT Name)]
ns <- Env
-> Bool
-> [((Name, Name), TT Name)]
-> TT Name
-> TT Name
-> StateT UInfo TC [(Name, TT Name)]
un' Env
env Bool
False [((Name, Name), TT Name)]
bnames TT Name
t TT Name
t'
let ns' :: [(Name, TT Name)]
ns' = ((Name, TT Name) -> Bool) -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (x :: Name
x, _) -> Name
xName -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/=Name
n) [(Name, TT Name)]
ns
Int -> StateT UInfo TC ()
forall (m :: * -> *). MonadState UInfo m => Int -> m ()
sc 1
Env
-> [((Name, Name), TT Name)]
-> [(Name, TT Name)]
-> [(Name, TT Name)]
-> StateT UInfo TC [(Name, TT Name)]
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ([(Name, TT Name)]
ns' [(Name, TT Name)] -> [(Name, TT Name)] -> [(Name, TT Name)]
forall a. [a] -> [a] -> [a]
++ [(Name, TT Name)]
bs)
highV :: Int -> Term -> Int
highV :: Int -> TT Name -> Int
highV i :: Int
i (V j :: Int
j) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i = Int
j
| Bool
otherwise = Int
i
highV i :: Int
i (Bind n :: Name
n b :: Binder (TT Name)
b sc :: TT Name
sc) = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int
i, Int -> TT Name -> Int
highV Int
i (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b), (Int -> TT Name -> Int
highV Int
i TT Name
sc Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)]
highV i :: Int
i (App _ f :: TT Name
f x :: TT Name
x) = Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Int -> TT Name -> Int
highV Int
i TT Name
f) (Int -> TT Name -> Int
highV Int
i TT Name
x)
highV i :: Int
i _ = Int
i
recoverable :: TT Name -> TT Name -> Bool
recoverable t :: TT Name
t@(App _ _ _) _
| (P _ (UN l :: Text
l) _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t, Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Delayed" = Bool
False
recoverable _ t :: TT Name
t@(App _ _ _)
| (P _ (UN l :: Text
l) _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t, Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt "Delayed" = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (P (DCon _ _ _) y :: Name
y _) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (P (TCon _ _) x :: Name
x _) (P (TCon _ _) y :: Name
y _) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (TType _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable (UType _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable (Constant _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable (Constant x :: Const
x) (Constant y :: Const
y) = Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y
recoverable (P (DCon _ _ _) x :: Name
x _) (TType _) = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (UType _) = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (Constant _) = Bool
False
recoverable (TType _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (UType _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (Constant _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (TType _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (UType _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (Constant _) = Bool
False
recoverable (P (DCon _ _ _) x :: Name
x _) (P (TCon _ _) y :: Name
y _) = Bool
False
recoverable (P (TCon _ _) x :: Name
x _) (P (DCon _ _ _) y :: Name
y _) = Bool
False
recoverable p :: TT Name
p@(TType _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(UType _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(Constant _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(TType _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(UType _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(Constant _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable p :: TT Name
p@(P _ n :: Name
n _) (App _ f :: TT Name
f a :: TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App _ f :: TT Name
f a :: TT Name
a) p :: TT Name
p@(P _ _ _) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App _ f :: TT Name
f a :: TT Name
a) (App _ f' :: TT Name
f' a' :: TT Name
a')
| TT Name
f TT Name -> TT Name -> Bool
forall a. Eq a => a -> a -> Bool
== TT Name
f' = TT Name -> TT Name -> Bool
recoverable TT Name
a TT Name
a'
recoverable (App _ f :: TT Name
f a :: TT Name
a) (App _ f' :: TT Name
f' a' :: TT Name
a')
= TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
f'
recoverable f :: TT Name
f (Bind _ (Pi _ _ _ _) sc :: TT Name
sc)
| (P (DCon _ _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (P (TCon _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (Constant _) <- TT Name
f = Bool
False
| TType _ <- TT Name
f = Bool
False
| UType _ <- TT Name
f = Bool
False
recoverable (Bind _ (Pi _ _ _ _) sc :: TT Name
sc) f :: TT Name
f
| (P (DCon _ _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (P (TCon _ _) _ _, _) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (Constant _) <- TT Name
f = Bool
False
| TType _ <- TT Name
f = Bool
False
| UType _ <- TT Name
f = Bool
False
recoverable (Bind _ (Lam _ _) sc :: TT Name
sc) f :: TT Name
f = TT Name -> TT Name -> Bool
recoverable TT Name
sc TT Name
f
recoverable f :: TT Name
f (Bind _ (Lam _ _) sc :: TT Name
sc) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
sc
recoverable x :: TT Name
x y :: TT Name
y = Bool
True
errEnv :: [(a, r, Binder b)] -> [(a, b)]
errEnv :: [(a, r, Binder b)] -> [(a, b)]
errEnv = ((a, r, Binder b) -> (a, b)) -> [(a, r, Binder b)] -> [(a, b)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: a
x, _, b :: Binder b
b) -> (a
x, Binder b -> b
forall b. Binder b -> b
binderTy Binder b
b))
holeIn :: Env -> Name -> Bool
holeIn :: Env -> Name -> Bool
holeIn env :: Env
env n :: Name
n = case Name -> Env -> Maybe (Binder (TT Name))
forall n. Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
lookupBinder Name
n Env
env of
Just (Hole _) -> Bool
True
Just (Guess _ _) -> Bool
True
_ -> Bool
False