|
|
|
@ -234,22 +234,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
| x == x', length a == length a' = |
|
|
|
traverse_ (uncurry unify'Spine) (Seq.zip a a') |
|
|
|
|
|
|
|
go lhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs = |
|
|
|
case force i of |
|
|
|
VI0 -> unify' x rhs |
|
|
|
VI1 -> unify' y rhs |
|
|
|
_ -> case rhs of |
|
|
|
VSystem sys -> goSystem (flip unify') sys lhs |
|
|
|
_ -> fail |
|
|
|
|
|
|
|
go lhs rhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) = |
|
|
|
case force i of |
|
|
|
VI0 -> unify' lhs x |
|
|
|
VI1 -> unify' lhs y |
|
|
|
_ -> case lhs of |
|
|
|
VSystem sys -> goSystem unify' sys rhs |
|
|
|
_ -> fail |
|
|
|
|
|
|
|
go (VLam p (Closure _ k)) vl = do |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' (k t) (vApp p vl t) |
|
|
|
|
