module Agda.TypeChecking.LevelConstraints ( simplifyLevelConstraint ) where
import Data.List as List
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Free
import Agda.Utils.Impossible
#include "undefined.h"
simplifyLevelConstraint :: Constraint -> [Constraint] -> Constraint
simplifyLevelConstraint new old =
case inequalities new of
[a :=< b] | any (matchLeq (b :=< a)) leqs -> LevelCmp CmpEq (Max [a]) (Max [b])
_ -> new
where
leqs = concatMap inequalities old
data Leq = PlusLevel :=< PlusLevel
deriving (Show, Eq)
matchLeq :: Leq -> Leq -> Bool
matchLeq (a :=< b) (c :=< d)
| length xs == length ys = (a, b) == applySubst rho (c, d)
| otherwise = False
where
free :: Free' a [Int] => a -> [Int]
free = nub . runFree ((:[]) . fst) IgnoreNot
xs = free (a, b)
ys = free (c, d)
rho = mkSub $ List.sort $ zip ys xs
mkSub = go 0
where
go _ [] = IdS
go y ren0@((y', x) : ren)
| y == y' = Var x [] :# go (y + 1) ren
| otherwise = Strengthen __IMPOSSIBLE__ $ go (y + 1) ren0
inequalities :: Constraint -> [Leq]
inequalities (LevelCmp CmpLeq (Max as) (Max [b])) = map (:=< b) as
inequalities (LevelCmp CmpEq (Max [a, b]) (Max [c]))
| a == c = [b :=< a]
| b == c = [a :=< b]
inequalities (LevelCmp CmpEq (Max [a]) (Max [b, c]))
| a == b = [c :=< b]
| a == c = [b :=< c]
inequalities _ = []