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 {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 -> 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
$ 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
$ 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