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 hiding (Arg, Dom, NamedArg, ArgInfo)
import Agda.Syntax.Internal (Dom)
import Agda.TypeChecking.Monad
import Agda.Utils.QuickCheck
import Agda.Utils.TestHelpers
hideAndRelParams :: Dom a -> Dom a
hideAndRelParams = setHiding Hidden . 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
]