module Agda.TypeChecking.Forcing
( computeForcingAnnotations,
isForced,
nextIsForced ) where
import Data.Monoid
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size
import Agda.Utils.Impossible
computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations QName
c Type
t =
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optForcing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions ) (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a b. (a -> b) -> a -> b
$ do
Type
t <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
TelV Tele (Dom Type)
tel (El Sort' Term
_ Term
a) <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
let vs :: Elims
vs = case Term
a of
Def QName
_ Elims
us -> Elims
us
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
n :: Nat
n = forall a. Sized a => a -> Nat
size Tele (Dom Type)
tel
xs :: [(Modality, Nat)]
xs :: [(Modality, Nat)]
xs = forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables Elims
vs
isForced :: Modality -> Nat -> Bool
isForced :: Modality -> Nat -> Bool
isForced Modality
m Nat
i =
(forall a. LensQuantity a => a -> Bool
hasQuantity0 Modality
m Bool -> Bool -> Bool
|| forall a. LensQuantity a => a -> Bool
noUserQuantity Modality
m)
Bool -> Bool -> Bool
&& (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant)
Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Modality
m', Nat
j) -> Nat
i forall a. Eq a => a -> a -> Bool
== Nat
j
Bool -> Bool -> Bool
&& Modality
m' Modality -> Modality -> Bool
`moreUsableModality` Modality
m) [(Modality, Nat)]
xs
forcedArgs :: [IsForced]
forcedArgs =
[ if Modality -> Nat -> Bool
isForced Modality
m Nat
i then IsForced
Forced else IsForced
NotForced
| (Nat
i, Modality
m) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Integral a => a -> [a]
downFrom Nat
n) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. LensModality a => a -> Modality
getModality (forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel)
]
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
ArgName -> Nat -> a -> m ()
reportS ArgName
"tc.force" Nat
60
[ ArgName
"Forcing analysis for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
c
, ArgName
" xs = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Modality, Nat)]
xs)
, ArgName
" forcedArgs = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show [IsForced]
forcedArgs
]
forall (m :: * -> *) a. Monad m => a -> m a
return [IsForced]
forcedArgs
class ForcedVariables a where
forcedVariables :: a -> [(Modality, Nat)]
default forcedVariables :: (ForcedVariables b, Foldable t, a ~ t b) => a -> [(Modality, Nat)]
forcedVariables = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables
instance ForcedVariables a => ForcedVariables [a] where
instance ForcedVariables a => ForcedVariables (Elim' a) where
forcedVariables :: Elim' a -> [(Modality, Nat)]
forcedVariables (Apply Arg a
x) = forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables Arg a
x
forcedVariables IApply{} = []
forcedVariables Proj{} = []
instance ForcedVariables a => ForcedVariables (Arg a) where
forcedVariables :: Arg a -> [(Modality, Nat)]
forcedVariables Arg a
x = [ (Modality -> Modality -> Modality
composeModality Modality
m Modality
m', Nat
i) | (Modality
m', Nat
i) <- forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables (forall e. Arg e -> e
unArg Arg a
x) ]
where m :: Modality
m = forall a. LensModality a => a -> Modality
getModality Arg a
x
instance ForcedVariables Term where
forcedVariables :: Term -> [(Modality, Nat)]
forcedVariables = \case
Var Nat
i [] -> [(Modality
unitModality, Nat
i)]
Con ConHead
_ ConInfo
_ Elims
vs -> forall a. ForcedVariables a => a -> [(Modality, Nat)]
forcedVariables Elims
vs
Term
_ -> []
isForced :: IsForced -> Bool
isForced :: IsForced -> Bool
isForced IsForced
Forced = Bool
True
isForced IsForced
NotForced = Bool
False
nextIsForced :: [IsForced] -> (IsForced, [IsForced])
nextIsForced :: [IsForced] -> (IsForced, [IsForced])
nextIsForced [] = (IsForced
NotForced, [])
nextIsForced (IsForced
f:[IsForced]
fs) = (IsForced
f, [IsForced]
fs)