content: 
  module Unification (unify) where
  
  import Control.Exception
  import Data.IORef
  
  import qualified Data.IntMap as IM
  
  import Common
  import Errors
  import Evaluation
  import Metacontext
  import Syntax
  import Value
  
  -- Unification
  --------------------------------------------------------------------------------
  
  -- | partial renaming from Γ to Δ
  data PartialRenaming = PRen {
      dom :: Lvl             -- ^ size of Γ
    , cod :: Lvl             -- ^ size of Δ
    , ren :: IM.IntMap Lvl}  -- ^ mapping from Δ vars to Γ vars
  
  -- | Lifting a partial renaming over an extra bound variable.
  --   Given (σ : PRen Γ Δ), (lift σ : PRen (Γ, x : A[σ]) (Δ, x : A))
  lift :: PartialRenaming -> PartialRenaming
  lift (PRen dom cod ren) =
    PRen (dom + 1) (cod + 1) (IM.insert (unLvl cod) dom ren)
  
  -- | @invert : (Γ : Cxt) → (spine : Sub Δ Γ) → PRen Γ Δ@
  invert :: Lvl -> Spine -> IO PartialRenaming
  invert gamma sp = do
  
    let go :: Spine -> IO (Lvl, IM.IntMap Lvl)
        go []             = pure (0, mempty)
        go (sp :> (t, _)) = do
          (dom, ren) <- go sp
          case force t of
            VVar (Lvl x) | IM.notMember x ren -> pure (dom + 1, IM.insert x dom ren)
            _                                 -> throwIO UnifyError
  
    (dom, ren) <- go sp
    pure $ PRen dom gamma ren
  
  -- | Perform the partial renaming on rhs, while also checking for "m" occurrences.
  rename :: MetaVar -> PartialRenaming -> Val -> IO Tm
  rename m pren v = go pren v where
  
    goSp :: PartialRenaming -> Tm -> Spine -> IO Tm
    goSp pren t []             = pure t
    goSp pren t (sp :> (u, i)) = App <$> goSp pren t sp <*> go pren u <*> pure i
  
    go :: PartialRenaming -> Val -> IO Tm
    go pren t = case force t of
      VFlex m' sp | m == m'   -> throwIO UnifyError -- occurs check
                  | otherwise -> goSp pren (Meta m') sp
  
      VRigid (Lvl x) sp -> case IM.lookup x (ren pren) of
        Nothing -> throwIO UnifyError  -- scope error ("escaping variable" error)
        Just x' -> goSp pren (Var $ lvl2Ix (dom pren) x') sp
  
      VLam x i t  -> Lam x i <$> go (lift pren) (t $$ VVar (cod pren))
      VPi x i a b -> Pi x i <$> go pren a <*> go (lift pren) (b $$ VVar (cod pren))
      VU          -> pure U
  
  -- | Wrap a term in lambdas. We need an extra list of Icit-s to
  --   match the type of the to-be-solved meta.
  lams :: [Icit] -> Tm -> Tm
  lams = go (0 :: Int) where
    go x []     t = t
    go x (i:is) t = Lam ("x"++show (x+1)) i $ go (x + 1) is t
  
  --       Γ      ?α         sp       rhs
  solve :: Lvl -> MetaVar -> Spine -> Val -> IO ()
  solve gamma m sp rhs = do
    pren <- invert gamma sp
    rhs  <- rename m pren rhs
    let solution = eval [] $ lams (reverse $ map snd sp) rhs
    modifyIORef' mcxt $ IM.insert (unMetaVar m) (Solved solution)
  
  unifySp :: Lvl -> Spine -> Spine -> IO ()
  unifySp l sp sp' = case (sp, sp') of
    ([]          , []            ) -> pure ()
  
    -- Note: we don't have to compare Icit-s, since we know from the recursive
  -- call that sp and sp' have the same type.
    (sp :> (t, _), sp' :> (t', _)) -> unifySp l sp sp' >> unify l t t'
  
    _                              -> throwIO UnifyError -- rigid mismatch error
  
  unify :: Lvl -> Val -> Val -> IO ()
  unify l t u = case (force t, force u) of
    (VLam _ _ t , VLam _ _ t'    ) -> unify (l + 1) (t $$ VVar l) (t' $$ VVar l)
    (t          , VLam _ i t'    ) -> unify (l + 1) (vApp t (VVar l) i) (t' $$ VVar l)
    (VLam _ i t , t'             ) -> unify (l + 1) (t $$ VVar l) (vApp t' (VVar l) i)
    (VU         , VU             ) -> pure ()
    (VPi x i a b, VPi x' i' a' b') | i == i' -> unify l a a' >> unify (l + 1) (b $$ VVar l) (b' $$ VVar l)
    (VRigid x sp, VRigid x' sp'  ) | x == x' -> unifySp l sp sp'
    (VFlex m sp , VFlex m' sp'   ) | m == m' -> unifySp l sp sp'
  
    (VFlex m sp , t'           ) -> solve l m sp t'
    (t          , VFlex m' sp' ) -> solve l m' sp' t
    _                            -> throwIO UnifyError  -- rigid mismatch error
  