{-# 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 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 doesn'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] -> [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 $ mapMaybe inequalities old
data Leq = PlusLevel :=< PlusLevel
deriving (Show, Eq)
-- | Check if two inequality constraints are the same up to variable renaming.
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 -- Note: use a list to preserve order of variables
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
-- | Turn a level constraint into a list of level inequalities, if possible.
inequalities :: Constraint -> Maybe [Leq]
inequalities (LevelCmp CmpLeq (Max as) (Max [b])) = Just $ map (:=< b) as -- 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:
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