{-# LANGUAGE ScopedTypeVariables #-}
module Agda.TypeChecking.Sort where
import Control.Monad
import Data.Functor
import Data.Maybe
import Agda.Interaction.Options (optCumulativity)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import {-# SOURCE #-} Agda.TypeChecking.Constraints ()
import {-# SOURCE #-} Agda.TypeChecking.Conversion
import {-# SOURCE #-} Agda.TypeChecking.MetaVars ()
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin (HasBuiltins)
import Agda.TypeChecking.Monad.Constraints (addConstraint, MonadConstraint)
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.MetaVars (metaType)
import Agda.TypeChecking.Monad.Signature (HasConstInfo(..), applyDef)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.ProjectionLike (elimView)
import Agda.TypeChecking.Records (getDefType)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Except
import Agda.Utils.Impossible
import Agda.Utils.Lens
import Agda.Utils.Monad
inferUnivSort
:: (MonadReduce m, MonadConstraint m, HasOptions m)
=> Sort -> m Sort
inferUnivSort s = do
s <- reduce s
ui <- univInf
case univSort' ui s of
Just s' -> return s'
Nothing -> do
addConstraint $ HasBiggerSort s
return $ UnivSort s
sortFitsIn :: MonadConversion m => Sort -> Sort -> m ()
sortFitsIn a b = do
b' <- inferUnivSort a
ifM (optCumulativity <$> pragmaOptions)
(leqSort b' b)
(equalSort b' b)
hasBiggerSort :: Sort -> TCM ()
hasBiggerSort = void . inferUnivSort
inferPiSort
:: (MonadReduce m, MonadAddContext m, MonadDebug m)
=> Dom Type -> Abs Sort -> m Sort
inferPiSort a s2 = do
s1' <- reduce $ getSort a
let a' = set lensSort s1' a
s2' <- mapAbstraction a' reduce s2
s2' <- instantiateFull s2'
return $ piSort a' s2'
inferFunSort :: Dom Type -> Sort -> TCM Sort
inferFunSort a s = inferPiSort a $ NoAbs underscore s
ptsRule :: Dom Type -> Abs Sort -> Sort -> TCM ()
ptsRule a b c = do
c' <- inferPiSort a b
ifM (optCumulativity <$> pragmaOptions)
(leqSort c' c)
(equalSort c' c)
ptsRule' :: Dom Type -> Sort -> Sort -> TCM ()
ptsRule' a b c = do
c' <- inferFunSort a b
ifM (optCumulativity <$> pragmaOptions)
(leqSort c' c)
(equalSort c' c)
hasPTSRule :: Dom Type -> Abs Sort -> TCM ()
hasPTSRule a b = void $ inferPiSort a b
checkTelePiSort :: Type -> TCM ()
checkTelePiSort _ = return ()
ifIsSort :: (MonadReduce m) => Type -> (Sort -> m a) -> m a -> m a
ifIsSort t yes no = do
t <- reduce t
case unEl t of
Sort s -> yes s
_ -> no
shouldBeSort
:: (MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m)
=> Type -> m Sort
shouldBeSort t = ifIsSort t return (typeError $ ShouldBeASort t)
sortOf
:: forall m. (MonadReduce m, MonadTCEnv m, MonadAddContext m, HasBuiltins m, HasConstInfo m)
=> Term -> m Sort
sortOf t = do
reportSDoc "tc.sort" 40 $ "sortOf" <+> prettyTCM t
sortOfT =<< elimView True t
where
sortOfT :: Term -> m Sort
sortOfT = \case
Pi adom b -> do
let a = unEl $ unDom adom
sa <- sortOf a
sb <- mapAbstraction adom (sortOf . unEl) b
return $ piSort (adom $> El sa a) sb
Sort s -> do
ui <- univInf
return $ univSort ui s
Var i es -> do
a <- typeOfBV i
sortOfE a (Var i) es
Def f es -> do
a <- defType <$> getConstInfo f
sortOfE a (Def f) es
MetaV x es -> do
a <- metaType x
sortOfE a (MetaV x) es
Lam{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s
sortOfE :: Type -> (Elims -> Term) -> Elims -> m Sort
sortOfE a hd [] = ifIsSort a return __IMPOSSIBLE__
sortOfE a hd (e:es) = case e of
Apply (Arg ai v) -> ifNotPiType a __IMPOSSIBLE__ $ \b c -> do
sortOfE (c `absApp` v) (hd . (e:)) es
Proj o f -> do
a <- reduce a
~(El _ (Pi b c)) <- fromMaybe __IMPOSSIBLE__ <$> getDefType f a
hd' <- applyE <$> applyDef o f (argFromDom b $> hd [])
sortOfE (c `absApp` (hd [])) hd' es
IApply x y r -> do
(b , c) <- fromMaybe __IMPOSSIBLE__ <$> isPath a
sortOfE (c `absApp` r) (hd . (e:)) es