{-# LANGUAGE CPP #-}
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.Utils.Impossible
#include "undefined.h"
simplifyLevelConstraint :: Constraint -> [Constraint] -> [Constraint]
simplifyLevelConstraint new old =
case inequalities new of
Just eqs -> map simpl eqs
Nothing -> [new]
where
simpl (a :=< b) | any (matchLeq (b :=< a)) leqs = LevelCmp CmpEq (Max [a]) (Max [b])
| otherwise = LevelCmp CmpLeq (Max [a]) (Max [b])
leqs = concat $ catMaybes $ map 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 => a -> [Int]
free = List.nub . runFree (:[]) 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 -> Maybe [Leq]
inequalities (LevelCmp CmpLeq (Max as) (Max [b])) = Just $ map (:=< b) as
inequalities (LevelCmp CmpEq (Max as) (Max [b])) =
case break (== b) as of
(as0, _ : as1) -> Just [ a :=< b | a <- as0 ++ as1 ]
_ -> Nothing
inequalities (LevelCmp CmpEq (Max [b]) (Max as)) =
case break (== b) as of
(as0, _ : as1) -> Just [ a :=< b | a <- as0 ++ as1 ]
_ -> Nothing
inequalities _ = Nothing