module Agda.TypeChecking.Level where
import Control.Applicative
import Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad ()
import Agda.TypeChecking.Monad.Builtin
import Agda.Utils.Except ( MonadError(catchError) )
#include "undefined.h"
import Agda.Utils.Impossible
data LevelKit = LevelKit
{ lvlType :: Term
, lvlSuc :: Term -> Term
, lvlMax :: Term -> Term -> Term
, lvlZero :: Term
, typeName :: QName
, sucName :: QName
, maxName :: QName
, zeroName :: QName
}
mlevel :: TCM (Maybe Term)
mlevel = liftTCM $ (Just <$> primLevel) `catchError` \_ -> return Nothing
levelType :: TCM Type
levelType = El (mkType 0) <$> primLevel
levelSucFunction :: TCM (Term -> Term)
levelSucFunction = do
suc <- primLevelSuc
return $ \a -> suc `apply` [defaultArg a]
builtinLevelKit :: TCM (Maybe LevelKit)
builtinLevelKit = liftTCM $ do
level@(Def l []) <- ignoreSharing <$> primLevel
zero@(Def z []) <- ignoreSharing <$> primLevelZero
suc@(Def s []) <- ignoreSharing <$> primLevelSuc
max@(Def m []) <- ignoreSharing <$> primLevelMax
let a @@ b = a `apply` [defaultArg b]
return $ Just $ LevelKit
{ lvlType = level
, lvlSuc = \a -> suc @@ a
, lvlMax = \a b -> max @@ a @@ b
, lvlZero = zero
, typeName = l
, sucName = s
, maxName = m
, zeroName = z
}
`catchError` \_ -> return Nothing
requireLevels :: TCM LevelKit
requireLevels = do
mKit <- builtinLevelKit
case mKit of
Nothing -> sequence_ [primLevel, primLevelZero, primLevelSuc, primLevelMax] >> __IMPOSSIBLE__
Just k -> return k
unLevel :: Term -> TCM Term
unLevel (Level l) = reallyUnLevelView l
unLevel (Shared p) = unLevel (derefPtr p)
unLevel v = return v
reallyUnLevelView :: MonadTCM tcm => Level -> tcm Term
reallyUnLevelView nv = liftTCM $ do
case nv of
Max [] -> primLevelZero
Max [Plus 0 a] -> return $ unLevelAtom a
Max [a] -> do
zer <- primLevelZero
suc <- primLevelSuc
return $ unPlusV zer (\n -> suc `apply` [defaultArg n]) a
_ -> (`unlevelWithKit` nv) <$> requireLevels
unlevelWithKit :: LevelKit -> Level -> Term
unlevelWithKit LevelKit{ lvlZero = zer, lvlSuc = suc, lvlMax = max } (Max as) =
case map (unPlusV zer suc) as of
[a] -> a
[] -> zer
as -> foldr1 max as
unPlusV :: Term -> (Term -> Term) -> PlusLevel -> Term
unPlusV zer suc (ClosedLevel n) = foldr (.) id (genericReplicate n suc) zer
unPlusV _ suc (Plus n a) = foldr (.) id (genericReplicate n suc) (unLevelAtom a)
maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
maybePrimCon prim = liftTCM $ do
Con c [] <- prim
return (Just c)
`catchError` \_ -> return Nothing
maybePrimDef :: TCM Term -> TCM (Maybe QName)
maybePrimDef prim = liftTCM $ do
Def f [] <- prim
return (Just f)
`catchError` \_ -> return Nothing
levelView :: Term -> TCM Level
levelView a = do
reportSLn "tc.level.view" 50 $ "{ levelView " ++ show a
v <- runReduceM $ levelView' a
reportSLn "tc.level.view" 50 $ " view: " ++ show v ++ "}"
return v
levelView' :: Term -> ReduceM Level
levelView' a = do
msuc <- (getCon =<<) <$> getBuiltin' builtinLevelSuc
mzer <- (getCon =<<) <$> getBuiltin' builtinLevelZero
mmax <- (getDef =<<) <$> getBuiltin' builtinLevelMax
let view a = do
a <- reduce' a
case ignoreSharing a of
Level l -> return l
Con s [arg]
| Just s == msuc -> inc <$> view (unArg arg)
Con z []
| Just z == mzer -> return $ closed 0
Def m [Apply arg1, Apply arg2]
| Just m == mmax -> levelLub <$> view (unArg arg1) <*> view (unArg arg2)
_ -> mkAtom a
v <- view a
return v
where
getCon (Con c []) = Just c
getCon _ = Nothing
getDef (Def f []) = Just f
getDef _ = Nothing
mkAtom a = do
b <- reduceB' a
return $ case ignoreSharing <$> b of
NotBlocked (MetaV m as) -> atom $ MetaLevel m as
NotBlocked _ -> atom $ NeutralLevel (ignoreBlocking b)
Blocked m _ -> atom $ BlockedLevel m (ignoreBlocking b)
atom a = Max [Plus 0 a]
closed n = Max [ClosedLevel n | n > 0]
inc (Max as) = Max $ map inc' as
where
inc' (ClosedLevel n) = ClosedLevel $ n + 1
inc' (Plus n a) = Plus (n + 1) a
levelLub :: Level -> Level -> Level
levelLub (Max as) (Max bs) = levelMax $ as ++ bs