module Ditto.Funify where
import Ditto.Syntax
import Ditto.Whnf
import Ditto.Monad
import Ditto.Conv
import Ditto.Sub
import Ditto.Throw

----------------------------------------------------------------------

funifies :: [Name] -> Args -> Args -> TCM (Maybe Sub)
funifies xs [] [] = return . Just $ []
funifies xs (a1:as1) (a2:as2) = funify xs a1 a2 >>= \case
  Nothing -> return Nothing
  Just s -> do
    as1' <- subs as1 s
    as2' <- subs as2 s
    funifies xs as1' as2' >>= \case
      Nothing -> return Nothing
      -- TODO this may need to be substitution composition
      Just s' -> return . Just $ s ++ s'
funifies _ _ _ = throwGenErr "Unifiying equations of differing lengths"

funify :: [Name] -> Arg -> Arg -> TCM (Maybe Sub)
funify xs (i1, a1) (i2, a2) | i1 == i2 = do
  a1' <- whnf a1
  a2' <- whnf a2
  funify' xs a1' a2'
funify xs (i1, a1) (i2, a2) = return Nothing

funify' :: [Name] -> Exp -> Exp -> TCM (Maybe Sub)
funify' xs (EVar x) a | x `elem` fv a = return Nothing
funify' xs a (EVar x) | x `elem` fv a = return Nothing
funify' xs (EVar x) a | x `elem` xs = return . Just $ [(x, a)]
funify' xs a (EVar x) | x `elem` xs = return . Just $ [(x, a)]
funify' xs (ECon _ x1 as1) (ECon _ x2 as2) | x1 /= x2 = return Nothing
funify' xs (ECon _ x1 as1) (ECon _ x2 as2) = funifies xs as1 as2
funify' xs a1 a2 = convStatic (Just []) a1 a2

----------------------------------------------------------------------