{-# OPTIONS_GHC -Wunused-imports #-}
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
:: Constraint
-> [Constraint]
-> Maybe [Constraint]
simplifyLevelConstraint :: Constraint -> [Constraint] -> Maybe [Constraint]
simplifyLevelConstraint Constraint
c [Constraint]
others = do
cs <- Constraint -> Maybe [Leq]
inequalities Constraint
c
case runChange $ mapM simpl cs of
([Constraint]
cs', Bool
True) -> [Constraint] -> Maybe [Constraint]
forall a. a -> Maybe a
Just [Constraint]
cs'
([Constraint]
_, Bool
False) -> Maybe [Constraint]
forall a. Maybe a
Nothing
where
simpl :: Leq -> Change (Constraint)
simpl :: Leq -> ChangeT Identity Constraint
simpl (SingleLevel' Term
a :=< SingleLevel' Term
b)
| (Leq -> Bool) -> [Leq] -> Bool
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 = UpdaterT Identity Constraint
forall (m :: * -> *) a. Monad m => UpdaterT m a
dirty UpdaterT Identity Constraint -> UpdaterT Identity Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
CmpEq (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
a) (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
b)
| Bool
otherwise = UpdaterT Identity Constraint
forall a. a -> ChangeT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return UpdaterT Identity Constraint -> UpdaterT Identity Constraint
forall a b. (a -> b) -> a -> b
$ Comparison -> Level -> Level -> Constraint
LevelCmp Comparison
CmpLeq (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
a) (SingleLevel' Term -> Level
forall t. SingleLevel' t -> Level' t
unSingleLevel SingleLevel' Term
b)
leqs :: [Leq]
leqs = [[Leq]] -> [Leq]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Leq]] -> [Leq]) -> [[Leq]] -> [Leq]
forall a b. (a -> b) -> a -> b
$ (Constraint -> Maybe [Leq]) -> [Constraint] -> [[Leq]]
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
(Int -> Leq -> ShowS)
-> (Leq -> String) -> ([Leq] -> ShowS) -> Show Leq
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Leq -> ShowS
showsPrec :: Int -> Leq -> ShowS
$cshow :: Leq -> String
show :: Leq -> String
$cshowList :: [Leq] -> ShowS
showList :: [Leq] -> ShowS
Show, Leq -> Leq -> Bool
(Leq -> Leq -> Bool) -> (Leq -> Leq -> Bool) -> Eq Leq
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Leq -> Leq -> Bool
== :: Leq -> Leq -> Bool
$c/= :: Leq -> Leq -> Bool
/= :: Leq -> Leq -> Bool
Eq)
matchLeq :: Leq -> Leq -> Bool
matchLeq :: Leq -> Leq -> Bool
matchLeq (SingleLevel' Term
a :=< SingleLevel' Term
b) (SingleLevel' Term
c :=< SingleLevel' Term
d)
| [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
ys = (SingleLevel' Term
a, SingleLevel' Term
b) (SingleLevel' Term, SingleLevel' Term)
-> (SingleLevel' Term, SingleLevel' Term) -> Bool
forall a. Eq a => a -> a -> Bool
== Substitution' (SubstArg (SingleLevel' Term, SingleLevel' Term))
-> (SingleLevel' Term, SingleLevel' Term)
-> (SingleLevel' Term, SingleLevel' Term)
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' Term
Substitution' (SubstArg (SingleLevel' Term, SingleLevel' 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 = (Int -> Int) -> [Int] -> [Int]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn Int -> Int
forall a. a -> a
id ([Int] -> [Int]) -> (a -> [Int]) -> a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SingleVar [Int] -> IgnoreSorts -> a -> [Int]
forall a c t.
(IsVarSet a c, Free t) =>
SingleVar c -> IgnoreSorts -> t -> c
runFree (Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[]) IgnoreSorts
IgnoreNot
xs :: [Int]
xs = (SingleLevel' Term, SingleLevel' Term) -> [Int]
forall a. Free a => a -> [Int]
free (SingleLevel' Term
a, SingleLevel' Term
b)
ys :: [Int]
ys = (SingleLevel' Term, SingleLevel' Term) -> [Int]
forall a. Free a => a -> [Int]
free (SingleLevel' Term
c, SingleLevel' Term
d)
rho :: Substitution' Term
rho = [(Int, Int)] -> Substitution' Term
mkSub ([(Int, Int)] -> Substitution' Term)
-> [(Int, Int)] -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ [(Int, Int)] -> [(Int, Int)]
forall a. Ord a => [a] -> [a]
List.sort ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
ys [Int]
xs
mkSub :: [(Int, Int)] -> Substitution' Term
mkSub = Int -> [(Int, Int)] -> Substitution' Term
forall {t}. (Eq t, Num t) => t -> [(t, Int)] -> Substitution' Term
go Int
0
where
go :: t -> [(t, Int)] -> Substitution' Term
go t
_ [] = Substitution' Term
forall a. Substitution' a
IdS
go t
y ren0 :: [(t, Int)]
ren0@((t
y', Int
x) : [(t, Int)]
ren)
| t
y t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
y' = Int -> Elims -> Term
Var Int
x [] Term -> Substitution' Term -> Substitution' Term
forall a. a -> Substitution' a -> Substitution' a
:# t -> [(t, Int)] -> Substitution' Term
go (t
y t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [(t, Int)]
ren
| Bool
otherwise = Impossible -> Int -> Substitution' Term -> Substitution' Term
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
strengthenS' Impossible
HasCallStack => Impossible
impossible Int
1 (Substitution' Term -> Substitution' Term)
-> Substitution' Term -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ t -> [(t, Int)] -> Substitution' Term
go (t
y t -> t -> t
forall a. Num a => a -> a -> a
+ t
1) [(t, Int)]
ren0
inequalities :: Constraint -> Maybe [Leq]
inequalities :: Constraint -> Maybe [Leq]
inequalities (LevelCmp Comparison
CmpLeq Level
a Level
b)
| Just SingleLevel' Term
b' <- Level -> Maybe (SingleLevel' Term)
forall t. Level' t -> Maybe (SingleLevel' t)
singleLevelView Level
b = [Leq] -> Maybe [Leq]
forall a. a -> Maybe a
Just ([Leq] -> Maybe [Leq]) -> [Leq] -> Maybe [Leq]
forall a b. (a -> b) -> a -> b
$ (SingleLevel' Term -> Leq) -> [SingleLevel' Term] -> [Leq]
forall a b. (a -> b) -> [a] -> [b]
map (SingleLevel' Term -> SingleLevel' Term -> Leq
:=< SingleLevel' Term
b') ([SingleLevel' Term] -> [Leq]) -> [SingleLevel' Term] -> [Leq]
forall a b. (a -> b) -> a -> b
$ List1 (SingleLevel' Term) -> [Item (List1 (SingleLevel' Term))]
forall l. IsList l => l -> [Item l]
List1.toList (List1 (SingleLevel' Term) -> [Item (List1 (SingleLevel' Term))])
-> List1 (SingleLevel' Term) -> [Item (List1 (SingleLevel' Term))]
forall a b. (a -> b) -> a -> b
$ Level -> List1 (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
a
inequalities (LevelCmp Comparison
CmpEq Level
a Level
b)
| Just SingleLevel' Term
a' <- Level -> Maybe (SingleLevel' Term)
forall t. Level' t -> Maybe (SingleLevel' t)
singleLevelView Level
a =
case (SingleLevel' Term -> Bool)
-> List1 (SingleLevel' Term)
-> ([SingleLevel' Term], [SingleLevel' Term])
forall a. (a -> Bool) -> NonEmpty a -> ([a], [a])
List1.break (SingleLevel' Term -> SingleLevel' Term -> Bool
forall a. Eq a => a -> a -> Bool
== SingleLevel' Term
a') (Level -> List1 (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
b) of
([SingleLevel' Term]
bs0, SingleLevel' Term
_ : [SingleLevel' Term]
bs1) -> [Leq] -> Maybe [Leq]
forall a. a -> Maybe a
Just [ SingleLevel' Term
b' SingleLevel' Term -> SingleLevel' Term -> Leq
:=< SingleLevel' Term
a' | SingleLevel' Term
b' <- [SingleLevel' Term]
bs0 [SingleLevel' Term] -> [SingleLevel' Term] -> [SingleLevel' Term]
forall a. [a] -> [a] -> [a]
++ [SingleLevel' Term]
bs1 ]
([SingleLevel' Term], [SingleLevel' Term])
_ -> Maybe [Leq]
forall a. Maybe a
Nothing
inequalities (LevelCmp Comparison
CmpEq Level
a Level
b)
| Just SingleLevel' Term
b' <- Level -> Maybe (SingleLevel' Term)
forall t. Level' t -> Maybe (SingleLevel' t)
singleLevelView Level
b =
case (SingleLevel' Term -> Bool)
-> List1 (SingleLevel' Term)
-> ([SingleLevel' Term], [SingleLevel' Term])
forall a. (a -> Bool) -> NonEmpty a -> ([a], [a])
List1.break (SingleLevel' Term -> SingleLevel' Term -> Bool
forall a. Eq a => a -> a -> Bool
== SingleLevel' Term
b') (Level -> List1 (SingleLevel' Term)
forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level
a) of
([SingleLevel' Term]
as0, SingleLevel' Term
_ : [SingleLevel' Term]
as1) -> [Leq] -> Maybe [Leq]
forall a. a -> Maybe a
Just [ SingleLevel' Term
a' SingleLevel' Term -> SingleLevel' Term -> Leq
:=< SingleLevel' Term
b' | SingleLevel' Term
a' <- [SingleLevel' Term]
as0 [SingleLevel' Term] -> [SingleLevel' Term] -> [SingleLevel' Term]
forall a. [a] -> [a] -> [a]
++ [SingleLevel' Term]
as1 ]
([SingleLevel' Term], [SingleLevel' Term])
_ -> Maybe [Leq]
forall a. Maybe a
Nothing
inequalities Constraint
_ = Maybe [Leq]
forall a. Maybe a
Nothing