module Agda.TypeChecking.Irrelevance where
import Control.Applicative
import Control.Monad.Reader
import qualified Data.Map as Map
import Agda.Interaction.Options hiding (tests)
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
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
doWorkOnTypes :: TCM a -> TCM a
doWorkOnTypes = verboseBracket "tc.irr" 20 "workOnTypes" . workOnTypes' True
workOnTypes' :: Bool -> TCM a -> TCM a
workOnTypes' allowed cont =
if allowed then
liftTCM $ modifyContext (modifyContextEntries $ mapRelevance $ irrToNonStrict) cont
else cont
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
prop_galois :: Relevance -> Relevance -> Relevance -> Bool
prop_galois r x y =
x `moreRelevant` (r `composeRelevance` y) ==
(r `inverseComposeRelevance` x) `moreRelevant` y
tests :: IO Bool
tests = runTests "Agda.TypeChecking.Irrelevance"
[ quickCheck' prop_galois
]