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
irrelevantOrUnused :: Relevance -> Bool
irrelevantOrUnused Irrelevant = True
irrelevantOrUnused UnusedArg = True
irrelevantOrUnused NonStrict = False
irrelevantOrUnused Relevant = False
irrelevantOrUnused Forced = False
unusableRelevance :: Relevance -> Bool
unusableRelevance rel = NonStrict `moreRelevant` rel
composeRelevance :: Relevance -> Relevance -> Relevance
composeRelevance r r' =
case (r, r') of
(Irrelevant, _) -> Irrelevant
(_, Irrelevant) -> Irrelevant
(NonStrict, _) -> NonStrict
(_, NonStrict) -> NonStrict
(Forced, _) -> Forced
(_, Forced) -> Forced
(UnusedArg, _) -> UnusedArg
(_, UnusedArg) -> UnusedArg
(Relevant, Relevant) -> Relevant
inverseComposeRelevance :: Relevance -> Relevance -> Relevance
inverseComposeRelevance r x =
case (r, x) of
(Relevant, x) -> x
_ | r == x -> Relevant
(UnusedArg, x) -> x
(Forced, UnusedArg) -> Relevant
(Forced, x) -> x
(Irrelevant, x) -> Relevant
(_, Irrelevant) -> Irrelevant
(NonStrict, _) -> Relevant
ignoreForced :: Relevance -> Relevance
ignoreForced Forced = Relevant
ignoreForced UnusedArg = Relevant
ignoreForced Relevant = Relevant
ignoreForced NonStrict = NonStrict
ignoreForced Irrelevant = Irrelevant
irrToNonStrict :: Relevance -> Relevance
irrToNonStrict Irrelevant = NonStrict
irrToNonStrict rel = rel
nonStrictToIrr :: Relevance -> Relevance
nonStrictToIrr NonStrict = Irrelevant
nonStrictToIrr rel = rel
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
]