    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.LevelConstraints ( simplifyLevelConstraint ) where

    import qualified Data.List as List

    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 Agda.Utils.List1 (List1)
    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.
      -> List1 Constraint    -- ^ Other constraints, enable simplification.
      -> Maybe [Constraint]  -- ^ @Just@: list of constraints equal to the original @c@.
                             --   @Nothing@: no simplification possible.
    simplifyLevelConstraint :: Constraint -> List1 Constraint -> Maybe [Constraint]
    simplifyLevelConstraint Constraint
    c List1 Constraint
    others = do
        cs <- Constraint -> Maybe [Leq]
    inequalities Constraint
    c
        case runChange $ mapM simpl 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 a. a -> ChangeT Identity a
    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]) -> List1 Constraint -> [[Leq]]
    forall a b. (a -> Maybe b) -> List1 a -> [b]
    List1.mapMaybe Constraint -> Maybe [Leq]
    inequalities List1 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
    $cshowsPrec :: Int -> Leq -> ShowS
    showsPrec :: Int -> Leq -> ShowS
    $cshow :: Leq -> String
    show :: Leq -> String
    $cshowList :: [Leq] -> ShowS
    showList :: [Leq] -> ShowS
    Show, Leq -> Leq -> Bool
    (Leq -> Leq -> Bool) -> (Leq -> Leq -> Bool) -> Eq Leq
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Leq -> Leq -> Bool
    == :: Leq -> Leq -> Bool
    $c/= :: Leq -> Leq -> Bool
    /= :: 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 a. [a] -> 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 a. [a] -> 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 {t}. (Eq t, Num t) => t -> [(t, Int)] -> Substitution' Term
    go Int
    0
          where
            go :: t -> [(t, Int)] -> Substitution' Term
    go t
    _ [] = Substitution' Term
    forall a. Substitution' a
    IdS
            go t
    y ren0 :: [(t, Int)]
    ren0@((t
    y', Int
    x) : [(t, Int)]
    ren)
              | t
    y t -> t -> Bool
    forall a. Eq a => a -> a -> Bool
    == t
    y'   = Int -> Elims -> Term
    Var Int
    x [] Term -> Substitution' Term -> Substitution' Term
    forall a. a -> Substitution' a -> Substitution' a
    :# t -> [(t, Int)] -> Substitution' Term
    go (t
    y t -> t -> t
    forall a. Num a => a -> a -> a
    + t
    1) [(t, Int)]
    ren
              | Bool
    otherwise = Impossible -> Int -> Substitution' Term -> Substitution' Term
    forall a. Impossible -> Int -> Substitution' a -> Substitution' a
    strengthenS' Impossible
    HasCallStack => Impossible
    impossible Int
    1 (Substitution' Term -> Substitution' Term)
    -> Substitution' Term -> Substitution' Term
    forall a b. (a -> b) -> a -> b
    $ t -> [(t, Int)] -> Substitution' Term
    go (t
    y t -> t -> t
    forall a. Num a => a -> a -> a
    + t
    1) [(t, 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
    $ List1 (SingleLevel' Term) -> [Item (List1 (SingleLevel' Term))]
    forall l. IsList l => l -> [Item l]
    List1.toList (List1 (SingleLevel' Term) -> [Item (List1 (SingleLevel' Term))])
    -> List1 (SingleLevel' Term) -> [Item (List1 (SingleLevel' Term))]
    forall a b. (a -> b) -> a -> b
    $ Level -> List1 (SingleLevel' Term)
    forall t. Level' t -> List1 (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)
    -> List1 (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 -> List1 (SingleLevel' Term)
    forall t. Level' t -> List1 (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)
    -> List1 (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 -> List1 (SingleLevel' Term)
    forall t. Level' t -> List1 (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