module Agda.TypeChecking.Irrelevance where
import Control.Applicative
import Control.Monad.Reader
import qualified Data.Map as Map
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
hideAndRelParams :: Dom a -> Dom a
hideAndRelParams = hideOrKeepInstance . mapRelevance nonStrictToIrr
inverseApplyRelevance :: Relevance -> Dom a -> Dom a
inverseApplyRelevance rel = mapRelevance (rel `inverseComposeRelevance`)
applyRelevance :: Relevance -> Dom a -> Dom a
applyRelevance rel = mapRelevance (rel `composeRelevance`)
workOnTypes :: TCM a -> TCM a
workOnTypes cont = do
allowed <- optExperimentalIrrelevance <$> pragmaOptions
verboseBracket "tc.irr" 20 "workOnTypes" $ workOnTypes' allowed cont
workOnTypes' :: Bool -> TCM a -> TCM a
workOnTypes' experimental cont = modifyContext (modifyContextEntries $ mapRelevance f) cont
where
f | experimental = irrToNonStrict
| otherwise = nonStrictToRel
applyRelevanceToContext :: Relevance -> TCM a -> TCM a
applyRelevanceToContext rel =
case rel of
Relevant -> id
Forced{} -> id
_ -> local $ \ e -> e
{ envContext = modifyContextEntries (inverseApplyRelevance rel) (envContext e)
, envLetBindings = Map.map
(fmap $ \ (t, a) -> (t, inverseApplyRelevance rel a))
(envLetBindings e)
, envRelevance = composeRelevance rel (envRelevance e)
}
wakeIrrelevantVars :: TCM a -> TCM a
wakeIrrelevantVars = applyRelevanceToContext Irrelevant