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.TypeChecking.Monad
#include "../undefined.h"
import Agda.Utils.Impossible
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 a = a
{ domRelevance = nonStrictToIrr (domRelevance a)
, domHiding = Hidden
}
inverseApplyRelevance :: Relevance -> Dom a -> Dom a
inverseApplyRelevance rel = mapDomRelevance (rel `inverseComposeRelevance`)
applyRelevance :: Relevance -> Dom a -> Dom a
applyRelevance rel = mapDomRelevance (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 $ mapDomRelevance $ 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
]