{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Forcing
( computeForcingAnnotations,
isForced,
nextIsForced ) where
import Control.Arrow (first)
import Control.Monad
import Control.Monad.Trans.Maybe
import Control.Monad.Writer (WriterT(..), tell, lift)
import Data.Foldable as Fold hiding (any)
import Data.Maybe
import Data.List ((\\))
import Data.Function (on)
import Data.Monoid
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Pretty hiding ((<>))
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Impossible
computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations :: QName -> Type -> TCM [IsForced]
computeForcingAnnotations c :: QName
c t :: Type
t =
TCMT IO Bool -> TCM [IsForced] -> TCM [IsForced] -> TCM [IsForced]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (PragmaOptions -> Bool
optForcing (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions) ([IsForced] -> TCM [IsForced]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (TCM [IsForced] -> TCM [IsForced])
-> TCM [IsForced] -> TCM [IsForced]
forall a b. (a -> b) -> a -> b
$ do
Type
t <- Type -> TCMT IO Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
TelV tel :: Tele (Dom Type)
tel (El _ a :: Term
a) <- Type -> TCM (TelV Type)
telViewPath Type
t
let vs :: Elims
vs = case Term
a of
Def _ us :: Elims
us -> Elims
us
_ -> Elims
forall a. HasCallStack => a
__IMPOSSIBLE__
n :: Int
n = Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
tel
xs :: [(Modality, Nat)]
xs :: [(Modality, Int)]
xs = Elims -> [(Modality, Int)]
forall a. ForcedVariables a => a -> [(Modality, Int)]
forcedVariables Elims
vs
isForced :: Modality -> Nat -> Bool
isForced :: Modality -> Int -> Bool
isForced m :: Modality
m i :: Int
i = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and
[ Modality -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 Modality
m Bool -> Bool -> Bool
|| Modality -> Bool
forall a. LensQuantity a => a -> Bool
noUserQuantity Modality
m
, Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
Irrelevant
, ((Modality, Int) -> Bool) -> [(Modality, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\ (m' :: Modality
m', j :: Int
j) -> Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& Modality
m' Modality -> Modality -> Bool
`moreUsableModality` Modality
m) [(Modality, Int)]
xs
]
forcedArgs :: [IsForced]
forcedArgs =
[ if Modality -> Int -> Bool
isForced Modality
m Int
i then IsForced
Forced else IsForced
NotForced
| (i :: Int
i, m :: Modality
m) <- [Int] -> [Modality] -> [(Int, Modality)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
n) ([Modality] -> [(Int, Modality)])
-> [Modality] -> [(Int, Modality)]
forall a b. (a -> b) -> a -> b
$ (Dom (ArgName, Type) -> Modality)
-> [Dom (ArgName, Type)] -> [Modality]
forall a b. (a -> b) -> [a] -> [b]
map Dom (ArgName, Type) -> Modality
forall a. LensModality a => a -> Modality
getModality (Tele (Dom Type) -> [Dom (ArgName, Type)]
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel)
]
ArgName -> Int -> [ArgName] -> TCMT IO ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
ArgName -> Int -> a -> m ()
reportS "tc.force" 60
[ "Forcing analysis for " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Show a => a -> ArgName
show QName
c
, " xs = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [Int] -> ArgName
forall a. Show a => a -> ArgName
show (((Modality, Int) -> Int) -> [(Modality, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Modality, Int) -> Int
forall a b. (a, b) -> b
snd [(Modality, Int)]
xs)
, " forcedArgs = " ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ [IsForced] -> ArgName
forall a. Show a => a -> ArgName
show [IsForced]
forcedArgs
]
[IsForced] -> TCM [IsForced]
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 = (b -> [(Modality, Int)]) -> t b -> [(Modality, Int)]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> [(Modality, Int)]
forall a. ForcedVariables a => a -> [(Modality, Int)]
forcedVariables
instance ForcedVariables a => ForcedVariables [a] where
instance ForcedVariables a => ForcedVariables (Elim' a) where
forcedVariables :: Elim' a -> [(Modality, Int)]
forcedVariables (Apply x :: Arg a
x) = Arg a -> [(Modality, Int)]
forall a. ForcedVariables a => a -> [(Modality, Int)]
forcedVariables Arg a
x
forcedVariables IApply{} = []
forcedVariables Proj{} = []
instance ForcedVariables a => ForcedVariables (Arg a) where
forcedVariables :: Arg a -> [(Modality, Int)]
forcedVariables x :: Arg a
x = [ (Modality
m Modality -> Modality -> Modality
forall a. Semigroup a => a -> a -> a
<> Modality
m', Int
i) | (m' :: Modality
m', i :: Int
i) <- a -> [(Modality, Int)]
forall a. ForcedVariables a => a -> [(Modality, Int)]
forcedVariables (Arg a -> a
forall e. Arg e -> e
unArg Arg a
x) ]
where m :: Modality
m = Arg a -> Modality
forall a. LensModality a => a -> Modality
getModality Arg a
x
instance ForcedVariables Term where
forcedVariables :: Term -> [(Modality, Int)]
forcedVariables t :: Term
t = case Term
t of
Var i :: Int
i [] -> [(Modality
forall a. Monoid a => a
mempty, Int
i)]
Con _ _ vs :: Elims
vs -> Elims -> [(Modality, Int)]
forall a. ForcedVariables a => a -> [(Modality, Int)]
forcedVariables Elims
vs
_ -> []
isForced :: IsForced -> Bool
isForced :: IsForced -> Bool
isForced Forced = Bool
True
isForced NotForced = Bool
False
nextIsForced :: [IsForced] -> (IsForced, [IsForced])
nextIsForced :: [IsForced] -> (IsForced, [IsForced])
nextIsForced [] = (IsForced
NotForced, [])
nextIsForced (f :: IsForced
f:fs :: [IsForced]
fs) = (IsForced
f, [IsForced]
fs)