module Agda.TypeChecking.LevelConstraints ( simplifyLevelConstraint ) where
import Data.List
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Substitute
import Agda.Utils.Size
simplifyLevelConstraint :: Integer -> Constraint -> Constraints -> Constraint
simplifyLevelConstraint n new old =
case inequalities new of
[a :=< b] | elem (b' :=< a') leqs -> LevelCmp CmpEq (Max [a]) (Max [b])
where (a', b') = raise (n) (a, b)
_ -> new
where
leqs = concatMap (inequalities . unClosure) old
unClosure c = raise (size (envContext $ clEnv cl)) $ clValue cl
where cl = theConstraint c
data Leq = PlusLevel :=< PlusLevel
deriving (Show, Eq)
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 _ = []