    {-# LANGUAGE CPP #-}

    module Agda.TypeChecking.LevelConstraints ( simplifyLevelConstraint ) where

    import qualified Data.List as List
    import Data.Maybe
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Free
    import Agda.Utils.Impossible

    #include "undefined.h"

    -- | @simplifyLevelConstraint c cs@ turns an @c@ into an equality
    --   constraint if it is an inequality constraint and the reverse
    --   inequality is contained in @cs@.
    --
    --   The constraints doesn't necessarily have to live in the same context, but
    --   they do need to be universally quanitfied over the context. This function
    --   takes care of renaming variables when checking for matches.
    simplifyLevelConstraint :: Constraint -> [Constraint] -> [Constraint]
    simplifyLevelConstraint new old =
      case inequalities new of
        Just eqs -> map simpl eqs
        Nothing  -> [new]
      where
        simpl (a :=< b) | any (matchLeq (b :=< a)) leqs = LevelCmp CmpEq  (Max [a]) (Max [b])
                        | otherwise                     = LevelCmp CmpLeq (Max [a]) (Max [b])
        leqs = concat $ mapMaybe inequalities old

    data Leq = PlusLevel :=< PlusLevel
      deriving (Show, Eq)

    -- | Check if two inequality constraints are the same up to variable renaming.
    matchLeq :: Leq -> Leq -> Bool
    matchLeq (a :=< b) (c :=< d)
      | length xs == length ys = (a, b) == applySubst rho (c, d)
      | otherwise              = False
      where
        free :: Free a => a -> [Int]
        free = List.nub . runFree (:[]) IgnoreNot  -- Note: use a list to preserve order of variables
        xs  = free (a, b)
        ys  = free (c, d)
        rho = mkSub $ List.sort $ zip ys xs
        mkSub = go 0
          where
            go _ [] = IdS
            go y ren0@((y', x) : ren)
              | y == y'   = Var x [] :# go (y + 1) ren
              | otherwise = Strengthen __IMPOSSIBLE__ $ go (y + 1) ren0

    -- | Turn a level constraint into a list of level inequalities, if possible.

    inequalities :: Constraint -> Maybe [Leq]

    inequalities (LevelCmp CmpLeq (Max as) (Max [b])) = Just $ map (:=< b) as  -- Andreas, 2016-09-28
      -- Why was this most natural case missing?
      -- See test/Succeed/LevelLeqGeq.agda for where it is useful!

    -- These are very special cases only, in no way complete:
    inequalities (LevelCmp CmpEq (Max as) (Max [b])) =
      case break (== b) as of
        (as0, _ : as1) -> Just [ a :=< b | a <- as0 ++ as1 ]
        _              -> Nothing
    inequalities (LevelCmp CmpEq (Max [b]) (Max as)) =
      case break (== b) as of
        (as0, _ : as1) -> Just [ a :=< b | a <- as0 ++ as1 ]
        _              -> Nothing
    inequalities _ = Nothing