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 forall a. Change a -> (a, Bool)
runChange forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Leq -> Change Constraint
simpl [Leq]
cs of
      ([Constraint]
cs', Bool
True) -> forall a. a -> Maybe a
Just [Constraint]
cs'
      ([Constraint]
_,  Bool
False) -> forall a. Maybe a
Nothing

  where
    simpl :: Leq -> Change (Constraint)
    simpl :: Leq -> Change Constraint
simpl (SingleLevel' Term
a :=< SingleLevel' Term
b)
      | 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 = forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty  forall a b. (a -> b) -> a -> b
$ Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
CmpEq  (forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
a) (forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
b)
      | Bool
otherwise                     = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
CmpLeq (forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
a) (forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
b)
    leqs :: [Leq]
leqs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ 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
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
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)
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys = (SingleLevel' Term
a, SingleLevel' Term
b) forall a. Eq a => a -> a -> Bool
== forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' 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 = forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (forall a. a -> [a] -> [a]
:[]) IgnoreSorts
IgnoreNot  -- Note: use a list to preserve order of variables
    xs :: [Int]
xs  = forall a. Free a => a -> [Int]
free (SingleLevel' Term
a, SingleLevel' Term
b)
    ys :: [Int]
ys  = forall a. Free a => a -> [Int]
free (SingleLevel' Term
c, SingleLevel' Term
d)
    rho :: Substitution' Term
rho = [(Int, Int)] -> Substitution' Term
mkSub forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
List.sort forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ys [Int]
xs
    mkSub :: [(Int, Int)] -> Substitution' Term
mkSub = forall {t}. (Eq t, Num t) => t -> [(t, Int)] -> Substitution' Term
go Int
0
      where
        go :: t -> [(t, Int)] -> Substitution' Term
go t
_ [] = forall a. Substitution' a
IdS
        go t
y ren0 :: [(t, Int)]
ren0@((t
y', Int
x) : [(t, Int)]
ren)
          | t
y forall a. Eq a => a -> a -> Bool
== t
y'   = Int -> Elims -> Term
Var Int
x [] forall a. a -> Substitution' a -> Substitution' a
:# t -> [(t, Int)] -> Substitution' Term
go (t
y forall a. Num a => a -> a -> a
+ t
1) [(t, Int)]
ren
          | Bool
otherwise = forall a. Impossible -> Int -> Substitution' a -> Substitution' a
strengthenS' HasCallStack => Impossible
impossible Int
1 forall a b. (a -> b) -> a -> b
$ t -> [(t, Int)] -> Substitution' Term
go (t
y 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' <- forall t. Level' t -> Maybe (SingleLevel' t)
singleLevelView Level
b = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (SingleLevel' Term -> SingleLevel' Term -> Leq
:=< SingleLevel' Term
b') forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ 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' <- forall t. Level' t -> Maybe (SingleLevel' t)
singleLevelView Level
a =
  case forall a. (a -> Bool) -> NonEmpty a -> ([a], [a])
List1.break (forall a. Eq a => a -> a -> Bool
== SingleLevel' Term
a') (forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
b) of
    ([SingleLevel' Term]
bs0, SingleLevel' Term
_ : [SingleLevel' Term]
bs1) -> forall a. a -> Maybe a
Just [ SingleLevel' Term
b' SingleLevel' Term -> SingleLevel' Term -> Leq
:=< SingleLevel' Term
a' | SingleLevel' Term
b' <- [SingleLevel' Term]
bs0 forall a. [a] -> [a] -> [a]
++ [SingleLevel' Term]
bs1 ]
    ([SingleLevel' Term], [SingleLevel' Term])
_              -> forall a. Maybe a
Nothing

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