module Agda.TypeChecking.UniversePolymorphism where
import Control.Applicative
import Control.Monad.Error
import Data.List
import Agda.Syntax.Internal
import Agda.Syntax.Common
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Level
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad.Builtin
import qualified Agda.Utils.Warshall as W
import Agda.Utils.Impossible
#include "../undefined.h"
mlevel :: MonadTCM tcm => tcm (Maybe Term)
mlevel = liftTCM $ (Just <$> primLevel) `catchError` \_ -> return Nothing
compareLevel :: MonadTCM tcm => Comparison -> Term -> Term -> tcm Constraints
compareLevel cmp u v = do
reportSDoc "tc.conv.level" 10 $ vcat
[ text "Comparing levels"
, nest 2 $ sep [ prettyTCM u <+> prettyTCM cmp
, prettyTCM v
]
]
u <- reduce u
v <- reduce v
reportSDoc "tc.conv.level" 15 $
nest 2 $ sep [ text (show u) <+> prettyTCM cmp
, text (show v)
]
let unMax (Max [a]) = a
unMax _ = __IMPOSSIBLE__
l1' <- unMax <$> levelView u
l2' <- unMax <$> levelView v
let bad = typeError $ UnequalLevel cmp u v
let c = min (constant l1') (constant l2')
l1 = minus l1 c
l2 = minus l2 c
case (cmp, l1, l2) of
(cmp, ClosedLevel n, ClosedLevel m) ->
case cmp of
CmpEq | n == m -> return []
CmpLeq | n <= m -> return []
_ -> bad
(CmpLeq, ClosedLevel 0, _) -> return []
_ -> buildConstraint $ LevelCmp cmp u v
where
constant (ClosedLevel n) = n
constant (Plus n _) = n
minus (ClosedLevel n) m = ClosedLevel (n m)
minus (Plus n l) m = Plus (n m) l
isLevelConstraint LevelCmp{} = True
isLevelConstraint _ = False
warshallConstraint :: Constraint -> TCM [W.Constraint]
warshallConstraint (LevelCmp cmp a b) = do
return []
warshallConstraint _ = __IMPOSSIBLE__
solveLevelConstraints :: TCM ()
solveLevelConstraints = do
cs <- takeConstraints
let (lcs, rest) = partition (isLevelConstraint . clValue) cs
lcs <- concat <$> mapM warshallConstraint (map clValue lcs)
let msol = W.solve lcs
case msol of
Nothing -> typeError $ GenericError "Bad universe levels! No further information provided. You suck!"
Just sol -> do
addConstraints rest
return ()