    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.TypeChecking.Level

    import Agda.Utils.Impossible
    import Agda.Utils.List (nubOn)
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Update

    -- | @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 don'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 @c@ to simplify.
      -> [Constraint]        -- ^ Other constraints, enable simplification.
      -> Maybe [Constraint]  -- ^ @Just@: list of constraints equal to the original @c@.
                             --   @Nothing@: no simplification possible.
    simplifyLevelConstraint :: Constraint -> [Constraint] -> Maybe [Constraint]
    simplifyLevelConstraint Constraint
    c [Constraint]
    others = do
        [Leq]
    cs <- Constraint -> Maybe [Leq]
    inequalities Constraint
    c
        case Change [Constraint] -> ([Constraint], Bool)
    forall a. Change a -> (a, Bool)
    runChange (Change [Constraint] -> ([Constraint], Bool))
    -> Change [Constraint] -> ([Constraint], Bool)
    forall a b. (a -> b) -> a -> b
    $ (Leq -> ChangeT Identity Constraint)
    -> [Leq] -> Change [Constraint]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Leq -> ChangeT Identity Constraint
    simpl [Leq]
    cs of
          ([Constraint]
    cs', Bool
    True) -> [Constraint] -> Maybe [Constraint]
    forall a. a -> Maybe a
    Just [Constraint]
    cs'
          ([Constraint]
    _,  Bool
    False) -> Maybe [Constraint]
    forall a. Maybe a
    Nothing

      where
        simpl :: Leq -> Change (Constraint)
        simpl :: Leq -> ChangeT Identity Constraint
    simpl (SingleLevel' Term
    a :=< SingleLevel' Term
    b)
          | (Leq -> Bool) -> [Leq] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Leq -> Leq -> Bool
    matchLeq (SingleLevel' Term
    b SingleLevel' Term -> SingleLevel' Term -> Leq
    :=< SingleLevel' Term
    a)) [Leq]
    leqs = UpdaterT Identity Constraint
    forall (m :: * -> *) a. Monad m => UpdaterT m a
    dirty  UpdaterT Identity Constraint -> UpdaterT Identity Constraint
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Level -> Level -> Constraint
    LevelCmp Comparison
    CmpEq  (SingleLevel' Term -> Level
    forall t. SingleLevel' t -> Level' t
    unSingleLevel SingleLevel' Term
    a) (SingleLevel' Term -> Level
    forall t. SingleLevel' t -> Level' t
    unSingleLevel SingleLevel' Term
    b)
          | Bool
    otherwise                     = UpdaterT Identity Constraint
    forall (m :: * -> *) a. Monad m => a -> m a
    return UpdaterT Identity Constraint -> UpdaterT Identity Constraint
    forall a b. (a -> b) -> a -> b
    $ Comparison -> Level -> Level -> Constraint
    LevelCmp Comparison
    CmpLeq (SingleLevel' Term -> Level
    forall t. SingleLevel' t -> Level' t
    unSingleLevel SingleLevel' Term
    a) (SingleLevel' Term -> Level
    forall t. SingleLevel' t -> Level' t
    unSingleLevel SingleLevel' Term
    b)
        leqs :: [Leq]
    leqs = [[Leq]] -> [Leq]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Leq]] -> [Leq]) -> [[Leq]] -> [Leq]
    forall a b. (a -> b) -> a -> b
    $ (Constraint -> Maybe [Leq]) -> [Constraint] -> [[Leq]]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Constraint -> Maybe [Leq]
    inequalities [Constraint]
    others

    data Leq = SingleLevel :=< SingleLevel
      deriving (Int -> Leq -> ShowS
    [Leq] -> ShowS
    Leq -> String
    (Int -> Leq -> ShowS)
    -> (Leq -> String) -> ([Leq] -> ShowS) -> Show Leq
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Leq] -> ShowS
    $cshowList :: [Leq] -> ShowS
    show :: Leq -> String
    $cshow :: Leq -> String
    showsPrec :: Int -> Leq -> ShowS
    $cshowsPrec :: Int -> Leq -> ShowS
    Show, Leq -> Leq -> Bool
    (Leq -> Leq -> Bool) -> (Leq -> Leq -> Bool) -> Eq Leq
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Leq -> Leq -> Bool
    $c/= :: Leq -> Leq -> Bool
    == :: Leq -> Leq -> Bool
    $c== :: Leq -> Leq -> Bool
    Eq)

    -- | Check if two inequality constraints are the same up to variable renaming.
    matchLeq :: Leq -> Leq -> Bool
    matchLeq :: Leq -> Leq -> Bool
    matchLeq (SingleLevel' Term
    a :=< SingleLevel' Term
    b) (SingleLevel' Term
    c :=< SingleLevel' Term
    d)
      | [Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Int]
    xs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Int] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Int]
    ys = (SingleLevel' Term
    a, SingleLevel' Term
    b) (SingleLevel' Term, SingleLevel' Term)
    -> (SingleLevel' Term, SingleLevel' Term) -> Bool
    forall a. Eq a => a -> a -> Bool
    == Substitution' (SubstArg (SingleLevel' Term, SingleLevel' Term))
    -> (SingleLevel' Term, SingleLevel' Term)
    -> (SingleLevel' Term, SingleLevel' Term)
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst Substitution' Term
    Substitution' (SubstArg (SingleLevel' Term, SingleLevel' Term))
    rho (SingleLevel' Term
    c, SingleLevel' Term
    d)
      | Bool
    otherwise              = Bool
    False
      where
        free :: Free a => a -> [Int]
        free :: forall a. Free a => a -> [Int]
    free = (Int -> Int) -> [Int] -> [Int]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn Int -> Int
    forall a. a -> a
    id ([Int] -> [Int]) -> (a -> [Int]) -> a -> [Int]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SingleVar [Int] -> IgnoreSorts -> a -> [Int]
    forall a c t.
    (IsVarSet a c, Free t) =>
    SingleVar c -> IgnoreSorts -> t -> c
    runFree (Int -> [Int] -> [Int]
    forall a. a -> [a] -> [a]
    :[]) IgnoreSorts
    IgnoreNot  -- Note: use a list to preserve order of variables
        xs :: [Int]
    xs  = (SingleLevel' Term, SingleLevel' Term) -> [Int]
    forall a. Free a => a -> [Int]
    free (SingleLevel' Term
    a, SingleLevel' Term
    b)
        ys :: [Int]
    ys  = (SingleLevel' Term, SingleLevel' Term) -> [Int]
    forall a. Free a => a -> [Int]
    free (SingleLevel' Term
    c, SingleLevel' Term
    d)
        rho :: Substitution' Term
    rho = [(Int, Int)] -> Substitution' Term
    mkSub ([(Int, Int)] -> Substitution' Term)
    -> [(Int, Int)] -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ [(Int, Int)] -> [(Int, Int)]
    forall a. Ord a => [a] -> [a]
    List.sort ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
    forall a b. (a -> b) -> a -> b
    $ [Int] -> [Int] -> [(Int, Int)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int]
    ys [Int]
    xs
        mkSub :: [(Int, Int)] -> Substitution' Term
    mkSub = Int -> [(Int, Int)] -> Substitution' Term
    forall {a}. (Eq a, Num a) => a -> [(a, Int)] -> Substitution' Term
    go Int
    0
          where
            go :: a -> [(a, Int)] -> Substitution' Term
    go a
    _ [] = Substitution' Term
    forall a. Substitution' a
    IdS
            go a
    y ren0 :: [(a, Int)]
    ren0@((a
    y', Int
    x) : [(a, Int)]
    ren)
              | a
    y a -> a -> Bool
    forall a. Eq a => a -> a -> Bool
    == a
    y'   = Int -> Elims -> Term
    Var Int
    x [] Term -> Substitution' Term -> Substitution' Term
    forall a. a -> Substitution' a -> Substitution' a
    :# a -> [(a, Int)] -> Substitution' Term
    go (a
    y a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1) [(a, Int)]
    ren
              | Bool
    otherwise = Impossible -> Substitution' Term -> Substitution' Term
    forall a. Impossible -> Substitution' a -> Substitution' a
    Strengthen Impossible
    HasCallStack => Impossible
    impossible (Substitution' Term -> Substitution' Term)
    -> Substitution' Term -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ a -> [(a, Int)] -> Substitution' Term
    go (a
    y a -> a -> a
    forall a. Num a => a -> a -> a
    + a
    1) [(a, Int)]
    ren0

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

    inequalities :: Constraint -> Maybe [Leq]

    inequalities :: Constraint -> Maybe [Leq]
    inequalities (LevelCmp Comparison
    CmpLeq Level
    a Level
    b)
      | Just SingleLevel' Term
    b' <- Level -> Maybe (SingleLevel' Term)
    forall t. Level' t -> Maybe (SingleLevel' t)
    singleLevelView Level
    b = [Leq] -> Maybe [Leq]
    forall a. a -> Maybe a
    Just ([Leq] -> Maybe [Leq]) -> [Leq] -> Maybe [Leq]
    forall a b. (a -> b) -> a -> b
    $ (SingleLevel' Term -> Leq) -> [SingleLevel' Term] -> [Leq]
    forall a b. (a -> b) -> [a] -> [b]
    map (SingleLevel' Term -> SingleLevel' Term -> Leq
    :=< SingleLevel' Term
    b') ([SingleLevel' Term] -> [Leq]) -> [SingleLevel' Term] -> [Leq]
    forall a b. (a -> b) -> a -> b
    $ NonEmpty (SingleLevel' Term) -> [SingleLevel' Term]
    forall a. NonEmpty a -> [a]
    List1.toList (NonEmpty (SingleLevel' Term) -> [SingleLevel' Term])
    -> NonEmpty (SingleLevel' Term) -> [SingleLevel' Term]
    forall a b. (a -> b) -> a -> b
    $ Level -> NonEmpty (SingleLevel' Term)
    forall t. Level' t -> NonEmpty (SingleLevel' t)
    levelMaxView Level
    a
      -- 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:
    -- E.g.: a = a ⊔ b ⊔ c --> b ≤ a & c ≤ a

    inequalities (LevelCmp Comparison
    CmpEq Level
    a Level
    b)
      | Just SingleLevel' Term
    a' <- Level -> Maybe (SingleLevel' Term)
    forall t. Level' t -> Maybe (SingleLevel' t)
    singleLevelView Level
    a =
      case (SingleLevel' Term -> Bool)
    -> NonEmpty (SingleLevel' Term)
    -> ([SingleLevel' Term], [SingleLevel' Term])
    forall a. (a -> Bool) -> NonEmpty a -> ([a], [a])
    List1.break (SingleLevel' Term -> SingleLevel' Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == SingleLevel' Term
    a') (Level -> NonEmpty (SingleLevel' Term)
    forall t. Level' t -> NonEmpty (SingleLevel' t)
    levelMaxView Level
    b) of
        ([SingleLevel' Term]
    bs0, SingleLevel' Term
    _ : [SingleLevel' Term]
    bs1) -> [Leq] -> Maybe [Leq]
    forall a. a -> Maybe a
    Just [ SingleLevel' Term
    b' SingleLevel' Term -> SingleLevel' Term -> Leq
    :=< SingleLevel' Term
    a' | SingleLevel' Term
    b' <- [SingleLevel' Term]
    bs0 [SingleLevel' Term] -> [SingleLevel' Term] -> [SingleLevel' Term]
    forall a. [a] -> [a] -> [a]
    ++ [SingleLevel' Term]
    bs1 ]
        ([SingleLevel' Term], [SingleLevel' Term])
    _              -> Maybe [Leq]
    forall a. Maybe a
    Nothing

    inequalities (LevelCmp Comparison
    CmpEq Level
    a Level
    b)
      | Just SingleLevel' Term
    b' <- Level -> Maybe (SingleLevel' Term)
    forall t. Level' t -> Maybe (SingleLevel' t)
    singleLevelView Level
    b =
      case (SingleLevel' Term -> Bool)
    -> NonEmpty (SingleLevel' Term)
    -> ([SingleLevel' Term], [SingleLevel' Term])
    forall a. (a -> Bool) -> NonEmpty a -> ([a], [a])
    List1.break (SingleLevel' Term -> SingleLevel' Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == SingleLevel' Term
    b') (Level -> NonEmpty (SingleLevel' Term)
    forall t. Level' t -> NonEmpty (SingleLevel' t)
    levelMaxView Level
    a) of
        ([SingleLevel' Term]
    as0, SingleLevel' Term
    _ : [SingleLevel' Term]
    as1) -> [Leq] -> Maybe [Leq]
    forall a. a -> Maybe a
    Just [ SingleLevel' Term
    a' SingleLevel' Term -> SingleLevel' Term -> Leq
    :=< SingleLevel' Term
    b' | SingleLevel' Term
    a' <- [SingleLevel' Term]
    as0 [SingleLevel' Term] -> [SingleLevel' Term] -> [SingleLevel' Term]
    forall a. [a] -> [a] -> [a]
    ++ [SingleLevel' Term]
    as1 ]
        ([SingleLevel' Term], [SingleLevel' Term])
    _              -> Maybe [Leq]
    forall a. Maybe a
    Nothing
    inequalities Constraint
    _ = Maybe [Leq]
    forall a. Maybe a
    Nothing