{-# 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
$cshowsPrec :: Int -> FailAt -> ShowS
showsPrec :: Int -> FailAt -> ShowS
$cshow :: FailAt -> String
show :: FailAt -> String
$cshowList :: [FailAt] -> ShowS
showList :: [FailAt] -> ShowS
Show, FailAt -> FailAt -> Bool
(FailAt -> FailAt -> Bool)
-> (FailAt -> FailAt -> Bool) -> Eq FailAt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FailAt -> FailAt -> Bool
== :: FailAt -> FailAt -> Bool
$c/= :: FailAt -> FailAt -> Bool
/= :: 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
$c== :: FailContext -> FailContext -> Bool
== :: FailContext -> FailContext -> Bool
$c/= :: FailContext -> FailContext -> Bool
/= :: 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
$cshowsPrec :: Int -> FailContext -> ShowS
showsPrec :: Int -> FailContext -> ShowS
$cshow :: FailContext -> String
show :: FailContext -> String
$cshowList :: [FailContext] -> ShowS
showList :: [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, [FailContext], FailAt) -> Bool)
-> Fails -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TT Name, TT Name, Bool, Env, Err, [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 (a
_,b
_,c
_,d
_, Err' t
err, f
_, g
_) = Err' t -> Bool
forall {t}. Err' t -> Bool
unrec Err' t
err
unrec :: Err' t -> Bool
unrec (CantUnify Bool
r (t, Maybe Provenance)
_ (t, Maybe Provenance)
_ Err' t
_ [(Name, t)]
_ Int
_) = Bool -> Bool
not Bool
r
unrec (At FC
_ Err' t
e) = Err' t -> Bool
unrec Err' t
e
unrec (Elaborating String
_ Name
_ Maybe t
_ Err' t
e) = Err' t -> Bool
unrec Err' t
e
unrec (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err' t
e) = Err' t -> Bool
unrec Err' t
e
unrec Err' t
_ = 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
$cshowsPrec :: Int -> UInfo -> ShowS
showsPrec :: Int -> UInfo -> ShowS
$cshow :: UInfo -> String
show :: UInfo -> String
$cshowList :: [UInfo] -> ShowS
showList :: [UInfo] -> ShowS
Show
cantUnify :: [FailContext] -> Bool -> (t, Maybe Provenance) -> (t, Maybe Provenance) -> (Err' t) -> [(Name, t)] -> Int -> Err' t
cantUnify :: forall t.
[FailContext]
-> 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 = 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 Name
f Name
x : [FailContext]
prev) Bool
r (t, Maybe Provenance)
t1 (t, Maybe Provenance)
t2 Err' t
e [(Name, t)]
ctxt 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 FC
_ Name
f' 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 Context
ctxt Env
env (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [Name]
inj [Name]
holes [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 Int
0 []) of
OK ([(Name, TT Name)]
v, UI Int
_ []) ->
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 a. a -> TC a
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')
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 Int
0 []) of
OK ([(Name, TT Name)]
v, UI Int
_ 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 a. a -> TC a
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 Err
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 Int
0 []) of
OK ([(Name, TT Name)]
v, UI Int
_ 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 a. a -> TC a
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')
TC ([(Name, TT Name)], UInfo)
_ -> Err -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
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 [((Name, Name), TT Name)]
names tx :: TT Name
tx@(P NameType
_ Name
x TT Name
_) 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 a. Eq a => a -> [a] -> 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 Int
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 [((Name, Name), TT Name)]
names TT Name
tm ty :: TT Name
ty@(P NameType
_ Name
y TT Name
_)
| 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 a. Eq a => a -> [a] -> 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 Int
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 [((Name, Name), TT Name)]
bnames (V Int
i) (P NameType
_ Name
x TT Name
_)
| [((Name, Name), TT Name)] -> Int
forall a. [a] -> 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. HasCallStack => [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. HasCallStack => [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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
un [((Name, Name), TT Name)]
bnames (P NameType
_ Name
x TT Name
_) (V Int
i)
| [((Name, Name), TT Name)] -> Int
forall a. [a] -> 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. HasCallStack => [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. HasCallStack => [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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
un [((Name, Name), TT Name)]
bnames (Bind Name
x Binder (TT Name)
bx TT Name
sx) (Bind Name
y Binder (TT Name)
by 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 [((Name, Name), TT Name)]
names (App AppStatus Name
_ TT Name
fx TT Name
ax) (App AppStatus Name
_ TT Name
fy 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 [((Name, Name), TT Name)]
names TT Name
x TT Name
y
| OK Bool
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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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 (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
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 -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
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
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
TC [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
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 -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
err
uB :: [((Name, Name), TT Name)]
-> Binder (TT Name)
-> Binder (TT Name)
-> StateT UInfo TC [(Name, TT Name)]
uB [((Name, Name), TT Name)]
bnames (Let RigCount
_ TT Name
tx TT Name
vx) (Let RigCount
_ TT Name
ty 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 [((Name, Name), TT Name)]
bnames (Lam RigCount
_ TT Name
tx) (Lam RigCount
_ 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 [((Name, Name), TT Name)]
bnames (Pi RigCount
r Maybe ImplicitInfo
i TT Name
tx TT Name
_) (Pi RigCount
r' Maybe ImplicitInfo
i' TT Name
ty TT Name
_) = [((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 [((Name, Name), TT Name)]
bnames Binder (TT Name)
x Binder (TT Name)
y = do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
notHole :: Binder b -> Bool
notHole (Hole b
_) = Bool
False
notHole Binder b
_ = Bool
True
sc :: Int -> m ()
sc Int
i = do UI Int
s 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 TT Name
x TT Name
y = do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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
err, [FailContext]
from, FailAt
Match) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
TC b -> t TC b
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC b -> t TC b) -> TC b -> t TC b
forall a b. (a -> b) -> a -> b
$ Err -> TC b
forall a. Err -> TC a
tfail Err
err
combine :: [((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)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
combine [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ((Name
n, TT Name
t) : [(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
Maybe (TT Name)
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 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 (\ (Name
x, TT Name
_) -> 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 Int
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 [((Name, Name), TT Name)]
ns TT Name
xtm p :: (Name, TT Name)
p@(Name
x, P NameType
_ Name
x' TT Name
_) | Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x' = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm p :: (Name, TT Name)
p@(Name
x, P NameType
_ Name
_ TT Name
_) = [(Name, TT Name)] -> t TC [(Name, TT Name)]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm (Name
x, 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 (m :: * -> *) a. Monad m => m a -> t m a
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 -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err
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 a. Eq a => a -> [a] -> 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 [((Name, Name), TT Name)]
ns (a
x, TT Name
tm) =
let v :: Int
v = Int -> TT Name -> Int
highV (-Int
1) TT Name
tm in
if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> Int
forall a. [a] -> 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 (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(a, TT Name)]
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
Msg String
"SCOPE ERROR")
else [(a, TT Name)] -> t TC [(a, TT Name)]
forall a. a -> t TC a
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 Int
i [((n, n), TT n)]
ns TT n
tm
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = TT n
tm
| Bool
otherwise = let ((n
x,n
y),TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. HasCallStack => [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
-Int
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 (a
x, 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 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 [Name]
env (Bind Name
n Binder (TT Name)
b TT Name
sc)
| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
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 a b. (a -> b) -> Binder a -> Binder b
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 {t}. Eq t => t -> t -> TT t -> TT t
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 a b. (a -> b) -> Binder a -> Binder b
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 [Name]
env (App AppStatus Name
s TT Name
f 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 [Name]
env TT Name
t = TT Name
t
rename :: t -> t -> TT t -> TT t
rename t
n t
n' (P NameType
nt t
x TT t
ty) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
x = NameType -> t -> TT t -> TT t
forall n. NameType -> n -> TT n -> TT n
P NameType
nt t
n' TT t
ty
rename t
n t
n' (Bind t
x Binder (TT t)
b TT t
sc) = t -> Binder (TT t) -> TT t -> TT t
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind t
x ((TT t -> TT t) -> Binder (TT t) -> Binder (TT t)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> t -> TT t -> TT t
rename t
n t
n') Binder (TT t)
b) (t -> t -> TT t -> TT t
rename t
n t
n' TT t
sc)
rename t
n t
n' (App AppStatus t
s TT t
f TT t
a) = AppStatus t -> TT t -> TT t -> TT t
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus t
s (t -> t -> TT t -> TT t
rename t
n t
n' TT t
f) (t -> t -> TT t -> TT t
rename t
n t
n' TT t
a)
rename t
n t
n' TT t
t = TT t
t
explicitHole :: TT n -> TT n
explicitHole (Bind n
n (Hole TT n
ty) 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 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 (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [FailContext]
from [(Name, r, Binder (TT Name))]
env [(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@(a
x, P NameType
_ a
x' TT a
_) : [(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 (\(a, TT a)
t -> case (a, TT a)
t of
(a
n, P NameType
_ a
n' TT a
_) -> 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)
(a, TT a)
_ -> Bool
True) [(a, TT a)]
ns)
dropPairs ((a, TT a)
n : [(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 [(a, a)]
vs [] = [(a, TT a)] -> TC [(a, TT a)]
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
followSols [(a, a)]
vs ((a
n, P NameType
_ a
t TT a
_) : [(a, TT a)]
ns)
| Just 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 NameType
_ a
tn TT a
_ ->
if (a
n, a
tn) (a, a) -> [(a, a)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(a, a)]
vs then
Err -> TC [(a, a)]
forall a. Err -> TC a
tfail ([FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") ([(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) Int
0)
else [(a, a)] -> TC [(a, a)]
forall a. a -> TC 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)
TT a
_ -> [(a, a)] -> TC [(a, a)]
forall a. a -> TC 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 [(a, a)]
vs ((a, TT a)
n : [(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 a. a -> TC 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 Context
ctxt Env
env (TT Name
topx, Maybe Provenance
xfrom) (TT Name
topy, Maybe Provenance
yfrom) [Name]
inj [Name]
holes [Name]
usersupp [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 Int
0 []) of
OK ([(Name, TT Name)]
v, UI Int
_ []) -> 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 a. a -> TC a
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', [])
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 Int
0 []) of
OK ([(Name, TT Name)]
v, UI Int
_ 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 a. a -> TC a
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 Err
e -> Err -> TC ([(Name, TT Name)], Fails)
forall a. Err -> TC a
tfail Err
e
where
injective :: TT n -> Bool
injective (P (DCon Int
_ Int
_ Bool
_) n
_ TT n
_) = Bool
True
injective (P (TCon Int
_ Int
_) n
_ TT n
_) = Bool
True
injective (App AppStatus n
_ TT n
f TT n
a) = TT n -> Bool
injective TT n
f
injective TT n
_ = Bool
False
injectiveVar :: TT Name -> Bool
injectiveVar (P NameType
_ Name
n TT Name
_) = Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
inj
injectiveVar (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> Bool
injectiveVar TT Name
f
injectiveVar TT Name
_ = Bool
False
injectiveApp :: TT Name -> Bool
injectiveApp 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 NameType
_ n
_ TT n
_) = Bool
False
notP TT n
_ = Bool
True
sc :: Int -> m ()
sc Int
i = do UI Int
s 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 m b
u1 m b
u2 = do UI Int
s Fails
f <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
b
r <- m b
u1
UI Int
s Fails
f' <- m UInfo
forall s (m :: * -> *). MonadState s m => m s
get
if (Fails -> Int
forall a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
f')
then b -> m b
forall a. a -> m a
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 Bool
fn [((Name, Name), TT Name)]
names TT Name
x 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 a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) topy :: TT Name
topy@(P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_)
| 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 Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon Int
_ Int
_) Name
x TT Name
_) topy :: TT Name
topy@(P (TCon Int
_ Int
_) Name
y TT Name
_)
| 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 Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) topy :: TT Name
topy@(P (TCon Int
_ Int
_) Name
y TT Name
_)
= 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 Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon Int
_ Int
_) Name
x TT Name
_) topy :: TT Name
topy@(P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_)
= 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 Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Constant Const
_) topy :: TT Name
topy@(P (TCon Int
_ Int
_) Name
y TT Name
_)
= 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 Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(P (TCon Int
_ Int
_) Name
x TT Name
_) topy :: TT Name
topy@(Constant Const
_)
= 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 Bool
fn [((Name, Name), TT Name)]
bnames tx :: TT Name
tx@(P NameType
_ Name
x TT Name
_) ty :: TT Name
ty@(P NameType
_ Name
y TT Name
_)
| (Name
x,Name
y) (Name, Name) -> [(Name, Name)] -> Bool
forall a. Eq a => a -> [a] -> 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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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 Integer
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 Integer
0 Name
y Env
env) of
Ordering
LT -> do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
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)
Ordering
_ -> do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
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 t
i t
n ((t
n',b
_,c
_):[(t, b, c)]
env) | t
n t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
n' = t
i
envPos t
i t
n ((t, b, c)
_:[(t, b, c)]
env) = t -> t -> [(t, b, c)] -> t
envPos (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) t
n [(t, b, c)]
env
envPos t
_ t
_ [(t, b, c)]
_ = t
100000
un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames xtm :: TT Name
xtm@(P NameType
_ Name
x TT Name
_) 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 a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
= do UI Int
s 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 Int
1
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
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 Bool
fn [((Name, Name), TT Name)]
bnames TT Name
tm ytm :: TT Name
ytm@(P NameType
_ Name
y TT Name
_)
| TT Name -> Bool
pureTerm TT Name
tm, Env -> Name -> Bool
holeIn Env
env Name
y Bool -> Bool -> Bool
|| Name
y Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes
= do UI Int
s 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 Int
1
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
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 Bool
fn [((Name, Name), TT Name)]
bnames (V Int
i) (P NameType
_ Name
x TT Name
_)
| [((Name, Name), TT Name)] -> Int
forall a. [a] -> 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. HasCallStack => [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. HasCallStack => [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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames (P NameType
_ Name
x TT Name
_) (V Int
i)
| [((Name, Name), TT Name)] -> Int
forall a. [a] -> 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. HasCallStack => [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. HasCallStack => [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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
un' Env
env Bool
fn [((Name, Name), TT Name)]
names topx :: TT Name
topx@(Bind Name
n (Hole TT Name
t) TT Name
sc) TT Name
y = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
topx TT Name
y
un' Env
env Bool
fn [((Name, Name), TT Name)]
names TT Name
x topy :: TT Name
topy@(Bind Name
n (Hole TT Name
t) TT Name
sc) = TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
x TT Name
topy
un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
tm app :: TT Name
app@(App AppStatus Name
_ TT Name
_ TT Name
_)
| (mvtm :: TT Name
mvtm@(P NameType
_ Name
mv TT Name
_), [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 a. Eq a => a -> [a] -> 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 {a}. Eq a => [(a, RigCount, TT a)] -> TT a -> TT a
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 Int
i) = Bool
True
rigid (P NameType
_ Name
t TT Name
_) = Name
t Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, RigCount, Binder (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 a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
rigid TT Name
_ = Bool
False
getV :: TT n -> Maybe Int
getV (V Int
i) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
getV TT n
_ = Maybe Int
forall a. Maybe a
Nothing
getname :: TT a -> Maybe a
getname (P NameType
_ a
n TT a
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
n
getname TT a
_ = Maybe a
forall a. Maybe a
Nothing
containsOnly :: t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs (V Int
i) = Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
vs
containsOnly t Name
args [Int]
vs (P NameType
Bound Name
n TT Name
ty)
= Name
n Name -> t Name -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t Name
args Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
ty
containsOnly t Name
args [Int]
vs (P NameType
_ Name
n TT Name
ty)
= Bool -> Bool
not (Env -> Name -> Bool
holeIn Env
env Name
n Bool -> Bool -> Bool
|| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
holes)
Bool -> Bool -> Bool
&& t Name -> [Int] -> TT Name -> Bool
containsOnly t Name
args [Int]
vs TT Name
ty
containsOnly t Name
args [Int]
vs (App AppStatus Name
_ TT Name
f 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 t Name
args [Int]
vs (Bind Name
_ Binder (TT Name)
b 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 (Int
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
+Int
1) [Int]
vs) TT Name
sc
containsOnly t Name
args [Int]
vs TT Name
_ = Bool
True
bindLams :: [TT Name] -> TT Name -> TT Name
bindLams [] TT Name
tm = TT Name
tm
bindLams (TT Name
a : [TT Name]
as) 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 Int
i) 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. HasCallStack => [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. HasCallStack => [a] -> Int -> a
!! Int
i))))
TT Name
tm
bindLam (P NameType
_ Name
n TT Name
ty) 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 TT Name
_ TT Name
tm = String -> TT Name
forall a. HasCallStack => String -> a
error String
"Can't happen [non rigid bindLam]"
substEnv :: [(n, b, Binder (TT n))] -> TT n -> TT n
substEnv [] TT n
tm = TT n
tm
substEnv ((n
n, b
_, Binder (TT n)
t) : [(n, b, Binder (TT n))]
env) 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 :: [(a, RigCount, TT a)] -> TT a -> TT a
eta [(a, RigCount, TT a)]
ks (Bind a
n (Lam RigCount
r TT a
ty) TT a
sc) = [(a, RigCount, TT a)] -> TT a -> TT a
eta ((a
n, RigCount
r, TT a
ty) (a, RigCount, TT a)
-> [(a, RigCount, TT a)] -> [(a, RigCount, TT a)]
forall a. a -> [a] -> [a]
: [(a, RigCount, TT a)]
ks) TT a
sc
eta [(a, RigCount, TT a)]
ks TT a
t = [(a, RigCount, TT a)] -> TT a -> TT a
rebind [(a, RigCount, TT a)]
ks TT a
t
rebind :: [(a, RigCount, TT a)] -> TT a -> TT a
rebind ((a
n, RigCount
r, TT a
ty) : [(a, RigCount, TT a)]
ks) (App AppStatus a
_ TT a
f (P NameType
_ a
n' TT a
_))
| a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n' = [(a, RigCount, TT a)] -> TT a -> TT a
eta [(a, RigCount, TT a)]
ks TT a
f
rebind ((a
n, RigCount
r, TT a
ty) : [(a, RigCount, TT a)]
ks) TT a
t = [(a, RigCount, TT a)] -> TT a -> TT a
rebind [(a, RigCount, TT a)]
ks (a -> Binder (TT a) -> TT a -> TT a
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind a
n (RigCount -> TT a -> Binder (TT a)
forall b. RigCount -> b -> Binder b
Lam RigCount
r TT a
ty) TT a
t)
rebind [(a, RigCount, TT a)]
_ TT a
t = TT a
t
un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App AppStatus Name
_ TT Name
_ TT Name
_) appy :: TT Name
appy@(App AppStatus Name
_ TT Name
_ TT Name
_)
= 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 Bool
fn [((Name, Name), TT Name)]
bnames TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (P NameType
Bound Name
n' TT Name
_)))
| 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 Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (P NameType
Bound Name
n' TT Name
_))) 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 Bool
fn [((Name, Name), TT Name)]
bnames TT Name
x (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
y (V Int
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 Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
n (Lam RigCount
_ TT Name
t) (App AppStatus Name
_ TT Name
x (V Int
0))) 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 Bool
fn [((Name, Name), TT Name)]
bnames (App AppStatus Name
_ TT Name
f TT Name
x) (Bind Name
n (Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) 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 Int
0 String
"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 [] Int
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 Int
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 Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
n (Pi RigCount
r Maybe ImplicitInfo
i TT Name
t TT Name
k) TT Name
y) (App AppStatus Name
_ TT Name
f 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 Int
0 String
"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 [] Int
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 Int
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 Bool
fn [((Name, Name), TT Name)]
bnames (Bind Name
x Binder (TT Name)
bx TT Name
sx) (Bind Name
y Binder (TT Name)
by 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 RigCount
_ b
_) (Lam RigCount
_ b
_) = Bool
True
sameBinder (Pi RigCount
_ Maybe ImplicitInfo
i b
_ b
_) (Pi RigCount
_ Maybe ImplicitInfo
i' b
_ b
_) = Bool
True
sameBinder Binder b
_ Binder b
_ = Bool
False
un' Env
env Bool
fn [((Name, Name), TT Name)]
bnames TT Name
x TT Name
y
| OK Bool
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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
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 Int
1; [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
| Bool
otherwise = do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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 (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
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 -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail Err
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
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
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 p
fn [((Name, Name), TT Name)]
bnames appx :: TT Name
appx@(App AppStatus Name
_ TT Name
fx TT Name
ax) appy :: TT Name
appy@(App AppStatus Name
_ TT Name
fy 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 (TT Name
headx, [TT Name]
_) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
fx
let (TT Name
heady, [TT Name]
_) = 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 Int
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 Int
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 [] Context
_ Env
_ TT Name
t = TT Name
t
hnormalise [a]
ns Context
ctxt Env
env 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 Int
_ Int
_ Bool
_) a
x TT a
_) (P (DCon Int
_ Int
_ Bool
_) a
y TT a
_)
| 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 Int
_ Int
_) a
x TT a
_) (P (TCon Int
_ Int
_) a
y TT a
_)
| 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 Int
_ Int
_ Bool
_) a
x TT a
_) (P (TCon Int
_ Int
_) a
y TT a
_)
= 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 Int
_ Int
_) a
x TT a
_) (P (DCon Int
_ Int
_ Bool
_) a
y TT a
_)
= 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 TT a
_ TT a
_ = [a] -> t TC [a]
forall a. a -> t TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
metavarApp :: TT Name -> Bool
metavarApp TT Name
tm = let (TT Name
f, [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 (\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 TT Name
t = case TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
t of
(P NameType
_ Name
x TT Name
_, [TT Name]
_) ->
case Name -> Context -> [Def]
lookupDef Name
x Context
ctxt of
[TyDecl NameType
_ TT Name
_] -> Bool
True
[Def]
_ -> Bool
False
(TT Name, [TT Name])
_ -> Bool
False
metavar :: TT Name -> Bool
metavar TT Name
t = case TT Name
t of
P NameType
_ Name
x TT Name
_ -> (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 a. Eq a => a -> [a] -> 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
TT Name
_ -> Bool
False
injectiveTC :: TT Name -> TT Name -> Bool
injectiveTC t :: TT Name
t@(P NameType
Ref Name
n TT Name
_) t' :: TT Name
t'@(P NameType
Ref Name
n' TT Name
_)
| Just Bool
ni <- Name -> Context -> Maybe Bool
lookupInjectiveExact Name
n Context
ctxt,
Just 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 AppStatus Name
_ TT Name
f TT Name
a) (App AppStatus Name
_ TT Name
f' TT Name
a') = TT Name -> TT Name -> Bool
injectiveTC TT Name
f TT Name
f'
injectiveTC TT Name
_ TT Name
_ = Bool
False
unifyTmpFail :: Term -> Term -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail :: TT Name -> TT Name -> StateT UInfo TC [(Name, TT Name)]
unifyTmpFail TT Name
x TT Name
y
= do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return []
unifyFail :: TT Name -> TT Name -> t TC b
unifyFail TT Name
x TT Name
y = do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
TC b -> t TC b
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC b -> t TC b) -> TC b -> t TC b
forall a b. (a -> b) -> a -> b
$ Err -> TC b
forall a. Err -> TC a
tfail Err
err
uB :: 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 (Let RigCount
_ TT Name
tx TT Name
vx) (Let RigCount
_ TT Name
ty 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 Int
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 [((Name, Name), TT Name)]
bnames (Guess TT Name
tx TT Name
vx) (Guess TT Name
ty 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 Int
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 [((Name, Name), TT Name)]
bnames (Lam RigCount
_ TT Name
tx) (Lam RigCount
_ TT Name
ty) = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
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 [((Name, Name), TT Name)]
bnames (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
tx TT Name
_) (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
ty TT Name
_) = do Int -> StateT UInfo TC ()
forall {m :: * -> *}. MonadState UInfo m => Int -> m ()
sc Int
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 [((Name, Name), TT Name)]
bnames (Hole TT Name
tx) (Hole 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 [((Name, Name), TT Name)]
bnames (PVar RigCount
_ TT Name
tx) (PVar RigCount
_ 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 [((Name, Name), TT Name)]
bnames Binder (TT Name)
x Binder (TT Name)
y
= do UI Int
s 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
err = [FailContext]
-> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
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
-> [(Name, TT Name)]
-> Int
-> Err
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
forall t. String -> Err' t
Msg String
"") (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
err, [FailContext]
from, FailAt
Unify) (TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> Fails -> Fails
forall a. a -> [a] -> [a]
: Fails
f))
[(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
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 [((Name, Name), TT Name)]
ns TT Name
xtm p :: (Name, TT Name)
p@(Name
x, P NameType
_ Name
_ TT Name
_) = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)
p]
checkCycle [((Name, Name), TT Name)]
ns TT Name
xtm (Name
x, 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 (m :: * -> *) a. Monad m => m a -> StateT UInfo m a
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 -> TC [(Name, TT Name)]
forall a. Err -> TC a
tfail (Name -> TT Name -> [(Name, TT Name)] -> Err
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 a. Eq a => a -> [a] -> 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 [((Name, Name), TT Name)]
ns (a
x, TT Name
tm) | TT Name -> Bool
pureTerm TT Name
tm =
let v :: Int
v = Int -> TT Name -> Int
highV (-Int
1) TT Name
tm in
if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [((Name, Name), TT Name)] -> Int
forall a. [a] -> 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 (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(a, TT Name)]
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
Msg String
"SCOPE ERROR")
else [(a, TT Name)] -> t TC [(a, TT Name)]
forall a. a -> t TC a
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 [((Name, Name), TT Name)]
ns (a
x, TT Name
tm) = TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(a, TT Name)] -> t TC [(a, TT Name)])
-> TC [(a, TT Name)] -> t TC [(a, TT Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(a, TT Name)]
forall a. Err -> TC a
tfail (String -> Err
forall t. String -> Err' t
Msg String
"HOLE ERROR")
bind :: Int -> [((n, n), TT n)] -> TT n -> TT n
bind Int
i [((n, n), TT n)]
ns TT n
tm
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 = TT n
tm
| Bool
otherwise = let ((n
x,n
y),TT n
ty) = [((n, n), TT n)]
ns[((n, n), TT n)] -> Int -> ((n, n), TT n)
forall a. HasCallStack => [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
-Int
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 [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as [] = [(Name, TT Name)] -> StateT UInfo TC [(Name, TT Name)]
forall a. a -> StateT UInfo TC a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TT Name)]
as
combine Env
env [((Name, Name), TT Name)]
bnames [(Name, TT Name)]
as ((Name
n, TT Name
t) : [(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
Maybe (TT Name)
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 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 (\ (Name
x, TT Name
_) -> 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 Int
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 Int
i (V Int
j) | Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i = Int
j
| Bool
otherwise = Int
i
highV Int
i (Bind Name
n Binder (TT Name)
b TT Name
sc) = [Int] -> Int
forall a. Ord a => [a] -> a
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
- Int
1)]
highV Int
i (App AppStatus Name
_ TT Name
f 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 Int
i TT Name
_ = Int
i
recoverable :: TT Name -> TT Name -> Bool
recoverable t :: TT Name
t@(App AppStatus Name
_ TT Name
_ TT Name
_) TT Name
_
| (P NameType
_ (UN Text
l) TT Name
_, [TT Name]
_) <- 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 String
"Delayed" = Bool
False
recoverable TT Name
_ t :: TT Name
t@(App AppStatus Name
_ TT Name
_ TT Name
_)
| (P NameType
_ (UN Text
l) TT Name
_, [TT Name]
_) <- 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 String
"Delayed" = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Name
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
y
recoverable (TType UExp
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable (UType Universe
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable (Constant Const
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable (Constant Const
x) (Constant Const
y) = Const
x Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
y
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (TType UExp
_) = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (UType Universe
_) = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (Constant Const
_) = Bool
False
recoverable (TType UExp
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (UType Universe
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (Constant Const
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (TType UExp
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (UType Universe
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (Constant Const
_) = Bool
False
recoverable (P (DCon Int
_ Int
_ Bool
_) Name
x TT Name
_) (P (TCon Int
_ Int
_) Name
y TT Name
_) = Bool
False
recoverable (P (TCon Int
_ Int
_) Name
x TT Name
_) (P (DCon Int
_ Int
_ Bool
_) Name
y TT Name
_) = Bool
False
recoverable p :: TT Name
p@(TType UExp
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(UType Universe
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable p :: TT Name
p@(Constant Const
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(TType UExp
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(UType Universe
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(Constant Const
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable p :: TT Name
p@(P NameType
_ Name
n TT Name
_) (App AppStatus Name
_ TT Name
f TT Name
a) = TT Name -> TT Name -> Bool
recoverable TT Name
p TT Name
f
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) p :: TT Name
p@(P NameType
_ Name
_ TT Name
_) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
p
recoverable (App AppStatus Name
_ TT Name
f TT Name
a) (App AppStatus Name
_ TT Name
f' 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 AppStatus Name
_ TT Name
f TT Name
a) (App AppStatus Name
_ TT Name
f' TT Name
a')
= TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
f'
recoverable TT Name
f (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc)
| (P (DCon Int
_ Int
_ Bool
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (P (TCon Int
_ Int
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (Constant Const
_) <- TT Name
f = Bool
False
| TType UExp
_ <- TT Name
f = Bool
False
| UType Universe
_ <- TT Name
f = Bool
False
recoverable (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc) TT Name
f
| (P (DCon Int
_ Int
_ Bool
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (P (TCon Int
_ Int
_) Name
_ TT Name
_, [TT Name]
_) <- TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
f = Bool
False
| (Constant Const
_) <- TT Name
f = Bool
False
| TType UExp
_ <- TT Name
f = Bool
False
| UType Universe
_ <- TT Name
f = Bool
False
recoverable (Bind Name
_ (Lam RigCount
_ TT Name
_) TT Name
sc) TT Name
f = TT Name -> TT Name -> Bool
recoverable TT Name
sc TT Name
f
recoverable TT Name
f (Bind Name
_ (Lam RigCount
_ TT Name
_) TT Name
sc) = TT Name -> TT Name -> Bool
recoverable TT Name
f TT Name
sc
recoverable TT Name
x TT Name
y = Bool
True
errEnv :: [(a, r, Binder b)] -> [(a, b)]
errEnv :: forall a r b. [(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 (\(a
x, r
_, 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 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 TT Name
_) -> Bool
True
Just (Guess TT Name
_ TT Name
_) -> Bool
True
Maybe (Binder (TT Name))
_ -> Bool
False