module Agda.TypeChecking.LevelConstraints ( simplifyLevelConstraint ) where

import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
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 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
a :=< SingleLevel
b)
      | (Leq -> Bool) -> [Leq] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Leq -> Leq -> Bool
matchLeq (SingleLevel
b SingleLevel -> SingleLevel -> Leq
:=< SingleLevel
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 -> Level
unSingleLevel SingleLevel
a) (SingleLevel -> Level
unSingleLevel SingleLevel
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 -> Level
unSingleLevel SingleLevel
a) (SingleLevel -> Level
unSingleLevel SingleLevel
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
a :=< SingleLevel
b) (SingleLevel
c :=< SingleLevel
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
a, SingleLevel
b) (SingleLevel, SingleLevel) -> (SingleLevel, SingleLevel) -> Bool
forall a. Eq a => a -> a -> Bool
== Substitution' Term
-> (SingleLevel, SingleLevel) -> (SingleLevel, SingleLevel)
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
rho (SingleLevel
c, SingleLevel
d)
  | Bool
otherwise              = Bool
False
  where
    free :: Free a => a -> [Int]
    free :: 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, SingleLevel) -> [Int]
forall a. Free a => a -> [Int]
free (SingleLevel
a, SingleLevel
b)
    ys :: [Int]
ys  = (SingleLevel, SingleLevel) -> [Int]
forall a. Free a => a -> [Int]
free (SingleLevel
c, SingleLevel
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 = Empty -> Substitution' Term -> Substitution' Term
forall a. Empty -> Substitution' a -> Substitution' a
Strengthen Empty
forall a. HasCallStack => a
__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
b' <- Level -> Maybe SingleLevel
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 -> Leq) -> [SingleLevel] -> [Leq]
forall a b. (a -> b) -> [a] -> [b]
map (SingleLevel -> SingleLevel -> Leq
:=< SingleLevel
b') ([SingleLevel] -> [Leq]) -> [SingleLevel] -> [Leq]
forall a b. (a -> b) -> a -> b
$ NonEmpty SingleLevel -> [SingleLevel]
forall a. NonEmpty a -> [a]
NonEmpty.toList (NonEmpty SingleLevel -> [SingleLevel])
-> NonEmpty SingleLevel -> [SingleLevel]
forall a b. (a -> b) -> a -> b
$ Level -> NonEmpty SingleLevel
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
a' <- Level -> Maybe SingleLevel
singleLevelView Level
a =
  case (SingleLevel -> Bool)
-> [SingleLevel] -> ([SingleLevel], [SingleLevel])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (SingleLevel -> SingleLevel -> Bool
forall a. Eq a => a -> a -> Bool
== SingleLevel
a') (NonEmpty SingleLevel -> [SingleLevel]
forall a. NonEmpty a -> [a]
NonEmpty.toList (NonEmpty SingleLevel -> [SingleLevel])
-> NonEmpty SingleLevel -> [SingleLevel]
forall a b. (a -> b) -> a -> b
$ Level -> NonEmpty SingleLevel
levelMaxView Level
b) of
    ([SingleLevel]
bs0, SingleLevel
_ : [SingleLevel]
bs1) -> [Leq] -> Maybe [Leq]
forall a. a -> Maybe a
Just [ SingleLevel
b' SingleLevel -> SingleLevel -> Leq
:=< SingleLevel
a' | SingleLevel
b' <- [SingleLevel]
bs0 [SingleLevel] -> [SingleLevel] -> [SingleLevel]
forall a. [a] -> [a] -> [a]
++ [SingleLevel]
bs1 ]
    ([SingleLevel], [SingleLevel])
_              -> Maybe [Leq]
forall a. Maybe a
Nothing

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