Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Syntax.Internal.Blockers

Contents

Blocked Terms
Handling blocked terms.
Waking up logic

Synopsis

data NotBlocked' t
- = StuckOn (Elim' t)
- | Underapplied
- | AbsurdMatch
- | MissingClauses QName
- | ReallyNotBlocked
data Blocker
- = UnblockOnAll (Set Blocker)
- | UnblockOnAny (Set Blocker)
- | UnblockOnMeta MetaId
- | UnblockOnProblem ProblemId
- | UnblockOnDef QName
alwaysUnblock :: Blocker
neverUnblock :: Blocker
unblockOnAll :: Set Blocker -> Blocker
unblockOnAny :: Set Blocker -> Blocker
unblockOnEither :: Blocker -> Blocker -> Blocker
unblockOnBoth :: Blocker -> Blocker -> Blocker
unblockOnMeta :: MetaId -> Blocker
unblockOnProblem :: ProblemId -> Blocker
unblockOnDef :: QName -> Blocker
unblockOnAllMetas :: Set MetaId -> Blocker
unblockOnAnyMeta :: Set MetaId -> Blocker
onBlockingMetasM :: Monad m => (MetaId -> m Blocker) -> Blocker -> m Blocker
allBlockingMetas :: Blocker -> Set MetaId
allBlockingProblems :: Blocker -> Set ProblemId
allBlockingDefs :: Blocker -> Set QName
data Blocked' t a
- = Blocked {
  - theBlocker :: Blocker
  - ignoreBlocking :: a
  }
- | NotBlocked {
  - blockingStatus :: NotBlocked' t
  - ignoreBlocking :: a
  }
stuckOn :: Elim' t -> NotBlocked' t -> NotBlocked' t
blockedOn :: Blocker -> a -> Blocked' t a
blocked :: MetaId -> a -> Blocked' t a
notBlocked :: a -> Blocked' t a
blocked_ :: MetaId -> Blocked' t ()
notBlocked_ :: Blocked' t ()
getBlocker :: Blocked' t a -> Blocker
data WakeUp
- = WakeUp
- | DontWakeUp (Maybe Blocker)
wakeUpWhen :: (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp
wakeUpWhen_ :: (constr -> Bool) -> constr -> WakeUp
wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp
wakeIfBlockedOnMeta :: MetaId -> Blocker -> WakeUp
wakeIfBlockedOnDef :: QName -> Blocker -> WakeUp
unblockMeta :: MetaId -> Blocker -> Blocker
unblockProblem :: ProblemId -> Blocker -> Blocker
unblockDef :: QName -> Blocker -> Blocker

Blocked Terms

data NotBlocked' t Source #

Even if we are not stuck on a meta during reduction we can fail to reduce a definition by pattern matching for another reason.

Constructors

StuckOn (Elim' t)	The `Elim` is neutral and blocks a pattern match.
Underapplied	Not enough arguments were supplied to complete the matching.
AbsurdMatch	We matched an absurd clause, results in a neutral `Def`.
MissingClauses QName	We ran out of clauses for `QName`, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match.
ReallyNotBlocked	Reduction was not blocked, we reached a whnf which can be anything but a stuck `Def`.

Instances

Instances details

EmbPrj NotBlocked Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: NotBlocked -> S Int32 Source # icod_ :: NotBlocked -> S Int32 Source # value :: Int32 -> R NotBlocked Source #
Eq NotBlocked
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: NotBlocked -> NotBlocked -> Bool (/=) :: NotBlocked -> NotBlocked -> Bool
Pretty t => Pretty (NotBlocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods pretty :: NotBlocked' t -> Doc Source # prettyPrec :: Int -> NotBlocked' t -> Doc Source # prettyList :: [NotBlocked' t] -> Doc Source #
Monoid (NotBlocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods mempty :: NotBlocked' t mappend :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t mconcat :: [NotBlocked' t] -> NotBlocked' t
Semigroup (NotBlocked' t) Source #	`ReallyNotBlocked` is the unit. `MissingClauses` is dominant. `StuckOn{}` should be propagated, if tied, we take the left.
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (<>) :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t # sconcat :: NonEmpty (NotBlocked' t) -> NotBlocked' t stimes :: Integral b => b -> NotBlocked' t -> NotBlocked' t
Generic (NotBlocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Associated Types type Rep (NotBlocked' t) :: Type -> Type Methods from :: NotBlocked' t -> Rep (NotBlocked' t) x to :: Rep (NotBlocked' t) x -> NotBlocked' t
Show t => Show (NotBlocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> NotBlocked' t -> ShowS show :: NotBlocked' t -> String showList :: [NotBlocked' t] -> ShowS
NFData t => NFData (NotBlocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods rnf :: NotBlocked' t -> ()
type Rep (NotBlocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers type Rep (NotBlocked' t) = D1 ('MetaData "NotBlocked'" "Agda.Syntax.Internal.Blockers" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "StuckOn" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Elim' t))) :+: C1 ('MetaCons "Underapplied" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "AbsurdMatch" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MissingClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: C1 ('MetaCons "ReallyNotBlocked" 'PrefixI 'False) (U1 :: Type -> Type))))

data Blocker Source #

What is causing the blocking? Or in other words which metas or problems need to be solved to unblock the blocked computation/constraint.

Constructors

UnblockOnAll (Set Blocker)
UnblockOnAny (Set Blocker)
UnblockOnMeta MetaId	Unblock if meta is instantiated
UnblockOnProblem ProblemId
UnblockOnDef QName	Unblock when function is defined

Instances

Instances details

EncodeTCM Blocker Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Blocker -> TCM Value Source #
Pretty Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods pretty :: Blocker -> Doc Source # prettyPrec :: Int -> Blocker -> Doc Source # prettyList :: [Blocker] -> Doc Source #
MentionsMeta Blocker Source #
Instance details Defined in Agda.TypeChecking.MetaVars.Mention Methods mentionsMetas :: HashSet MetaId -> Blocker -> Bool Source #
PrettyTCM Blocker Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocker -> m Doc Source #
ToTerm Blocker Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Blocker -> Term) Source # toTermR :: TCM (Blocker -> ReduceM Term) Source #
Instantiate Blocker Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocker -> ReduceM Blocker Source #
Unquote Blocker Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Blocker Source #
Generic Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Associated Types type Rep Blocker :: Type -> Type Methods from :: Blocker -> Rep Blocker x to :: Rep Blocker x -> Blocker
Show Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> Blocker -> ShowS show :: Blocker -> String showList :: [Blocker] -> ShowS
NFData Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods rnf :: Blocker -> ()
Eq Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (==) :: Blocker -> Blocker -> Bool (/=) :: Blocker -> Blocker -> Bool
Ord Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods compare :: Blocker -> Blocker -> Ordering (<) :: Blocker -> Blocker -> Bool (<=) :: Blocker -> Blocker -> Bool (>) :: Blocker -> Blocker -> Bool (>=) :: Blocker -> Blocker -> Bool max :: Blocker -> Blocker -> Blocker min :: Blocker -> Blocker -> Blocker
type Rep Blocker Source #
Instance details Defined in Agda.Syntax.Internal.Blockers type Rep Blocker = D1 ('MetaData "Blocker" "Agda.Syntax.Internal.Blockers" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "UnblockOnAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Blocker))) :+: C1 ('MetaCons "UnblockOnAny" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Blocker)))) :+: (C1 ('MetaCons "UnblockOnMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MetaId)) :+: (C1 ('MetaCons "UnblockOnProblem" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ProblemId)) :+: C1 ('MetaCons "UnblockOnDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))))

alwaysUnblock :: Blocker Source #

neverUnblock :: Blocker Source #

unblockOnAll :: Set Blocker -> Blocker Source #

unblockOnAny :: Set Blocker -> Blocker Source #

unblockOnEither :: Blocker -> Blocker -> Blocker Source #

unblockOnBoth :: Blocker -> Blocker -> Blocker Source #

unblockOnMeta :: MetaId -> Blocker Source #

unblockOnProblem :: ProblemId -> Blocker Source #

unblockOnDef :: QName -> Blocker Source #

unblockOnAllMetas :: Set MetaId -> Blocker Source #

unblockOnAnyMeta :: Set MetaId -> Blocker Source #

onBlockingMetasM :: Monad m => (MetaId -> m Blocker) -> Blocker -> m Blocker Source #

allBlockingMetas :: Blocker -> Set MetaId Source #

allBlockingProblems :: Blocker -> Set ProblemId Source #

allBlockingDefs :: Blocker -> Set QName Source #

data Blocked' t a Source #

Something where a meta variable may block reduction. Notably a top-level meta is considered blocking. This did not use to be the case (pre Aug 2020).

Constructors

Blocked
Fields theBlocker :: Blocker ignoreBlocking :: a
NotBlocked
Fields blockingStatus :: NotBlocked' t ignoreBlocking :: a

Instances

Instances details

EmbPrj Blocked_ Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Blocked_ -> S Int32 Source # icod_ :: Blocked_ -> S Int32 Source # value :: Int32 -> R Blocked_ Source #
MonadError Blocked_ NLM
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods throwError :: Blocked_ -> NLM a catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a
Pretty a => Pretty (Blocked a) Source #
Instance details Defined in Agda.Syntax.Internal Methods pretty :: Blocked a -> Doc Source # prettyPrec :: Int -> Blocked a -> Doc Source # prettyList :: [Blocked a] -> Doc Source #
TermLike a => TermLike (Blocked a) Source #
Instance details Defined in Agda.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a) Source # foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m Source #
KillRange a => KillRange (Blocked a) Source #
Instance details Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source #
PrettyTCM a => PrettyTCM (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Blocked a -> m Doc Source #
Instantiate a => Instantiate (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiate' :: Blocked a -> ReduceM (Blocked a) Source #
Apply t => Apply (Blocked t) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Blocked t -> Args -> Blocked t Source # applyE :: Blocked t -> Elims -> Blocked t Source #
Subst a => Subst (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg (Blocked a) Source # Methods applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source #
Decoration (Blocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods traverseF :: Functor m => (a -> m b) -> Blocked' t a -> m (Blocked' t b) Source # distributeF :: Functor m => Blocked' t (m a) -> m (Blocked' t a) Source #
Foldable (Blocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods fold :: Monoid m => Blocked' t m -> m foldMap :: Monoid m => (a -> m) -> Blocked' t a -> m foldMap' :: Monoid m => (a -> m) -> Blocked' t a -> m foldr :: (a -> b -> b) -> b -> Blocked' t a -> b foldr' :: (a -> b -> b) -> b -> Blocked' t a -> b foldl :: (b -> a -> b) -> b -> Blocked' t a -> b foldl' :: (b -> a -> b) -> b -> Blocked' t a -> b foldr1 :: (a -> a -> a) -> Blocked' t a -> a foldl1 :: (a -> a -> a) -> Blocked' t a -> a toList :: Blocked' t a -> [a] null :: Blocked' t a -> Bool length :: Blocked' t a -> Int elem :: Eq a => a -> Blocked' t a -> Bool maximum :: Ord a => Blocked' t a -> a minimum :: Ord a => Blocked' t a -> a sum :: Num a => Blocked' t a -> a product :: Num a => Blocked' t a -> a
Traversable (Blocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods traverse :: Applicative f => (a -> f b) -> Blocked' t a -> f (Blocked' t b) sequenceA :: Applicative f => Blocked' t (f a) -> f (Blocked' t a) mapM :: Monad m => (a -> m b) -> Blocked' t a -> m (Blocked' t b) sequence :: Monad m => Blocked' t (m a) -> m (Blocked' t a)
Applicative (Blocked' t) Source #	Blocking on _all_ blockers.
Instance details Defined in Agda.Syntax.Internal.Blockers Methods pure :: a -> Blocked' t a (<>) :: Blocked' t (a -> b) -> Blocked' t a -> Blocked' t b # liftA2 :: (a -> b -> c) -> Blocked' t a -> Blocked' t b -> Blocked' t c (>) :: Blocked' t a -> Blocked' t b -> Blocked' t b (<*) :: Blocked' t a -> Blocked' t b -> Blocked' t a
Functor (Blocked' t) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods fmap :: (a -> b) -> Blocked' t a -> Blocked' t b (<$) :: a -> Blocked' t b -> Blocked' t a #
Eq t => Eq (Blocked t)
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Blocked t -> Blocked t -> Bool (/=) :: Blocked t -> Blocked t -> Bool
(Semigroup a, Monoid a) => Monoid (Blocked' t a) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods mempty :: Blocked' t a mappend :: Blocked' t a -> Blocked' t a -> Blocked' t a mconcat :: [Blocked' t a] -> Blocked' t a
Semigroup a => Semigroup (Blocked' t a) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (<>) :: Blocked' t a -> Blocked' t a -> Blocked' t a # sconcat :: NonEmpty (Blocked' t a) -> Blocked' t a stimes :: Integral b => b -> Blocked' t a -> Blocked' t a
Generic (Blocked' t a) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Associated Types type Rep (Blocked' t a) :: Type -> Type Methods from :: Blocked' t a -> Rep (Blocked' t a) x to :: Rep (Blocked' t a) x -> Blocked' t a
(Show t, Show a) => Show (Blocked' t a) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> Blocked' t a -> ShowS show :: Blocked' t a -> String showList :: [Blocked' t a] -> ShowS
(NFData t, NFData a) => NFData (Blocked' t a) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods rnf :: Blocked' t a -> ()
type SubstArg (Blocked a) Source #
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a
type Rep (Blocked' t a) Source #
Instance details Defined in Agda.Syntax.Internal.Blockers type Rep (Blocked' t a) = D1 ('MetaData "Blocked'" "Agda.Syntax.Internal.Blockers" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "Blocked" 'PrefixI 'True) (S1 ('MetaSel ('Just "theBlocker") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Blocker) :: S1 ('MetaSel ('Just "ignoreBlocking") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NotBlocked" 'PrefixI 'True) (S1 ('MetaSel ('Just "blockingStatus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NotBlocked' t)) :: S1 ('MetaSel ('Just "ignoreBlocking") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

stuckOn :: Elim' t -> NotBlocked' t -> NotBlocked' t Source #

When trying to reduce f es, on match failed on one elimination e ∈ es that came with info r :: NotBlocked. stuckOn e r produces the new NotBlocked info.

MissingClauses must be propagated, as this is blockage that can be lifted in the future (as more clauses are added).

StuckOn e0 is also propagated, since it provides more precise information as StuckOn e (as e0 is the original reason why reduction got stuck and usually a subterm of e). An information like StuckOn (Apply (Arg info (Var i []))) (stuck on a variable) could be used by the lhs/coverage checker to trigger a split on that (pattern) variable.

In the remaining cases for r, we are terminally stuck due to StuckOn e. Propagating AbsurdMatch does not seem useful.

Underapplied must not be propagated, as this would mean that f es is underapplied, which is not the case (it is stuck). Note that Underapplied can only arise when projection patterns were missing to complete the original match (in e). (Missing ordinary pattern would mean the e is of function type, but we cannot match against something of function type.)

Handling blocked terms.

blockedOn :: Blocker -> a -> Blocked' t a Source #

blocked :: MetaId -> a -> Blocked' t a Source #

notBlocked :: a -> Blocked' t a Source #

blocked_ :: MetaId -> Blocked' t () Source #

notBlocked_ :: Blocked' t () Source #

getBlocker :: Blocked' t a -> Blocker Source #

Waking up logic

data WakeUp Source #

Should a constraint wake up or not? If not, we might refine the unblocker.

Constructors

WakeUp
DontWakeUp (Maybe Blocker)

Instances

Instances details

Show WakeUp Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> WakeUp -> ShowS show :: WakeUp -> String showList :: [WakeUp] -> ShowS
Eq WakeUp Source #
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (==) :: WakeUp -> WakeUp -> Bool (/=) :: WakeUp -> WakeUp -> Bool

wakeUpWhen :: (constr -> Bool) -> (constr -> WakeUp) -> constr -> WakeUp Source #

wakeUpWhen_ :: (constr -> Bool) -> constr -> WakeUp Source #

wakeIfBlockedOnProblem :: ProblemId -> Blocker -> WakeUp Source #

wakeIfBlockedOnMeta :: MetaId -> Blocker -> WakeUp Source #

wakeIfBlockedOnDef :: QName -> Blocker -> WakeUp Source #

unblockMeta :: MetaId -> Blocker -> Blocker Source #

unblockProblem :: ProblemId -> Blocker -> Blocker Source #

unblockDef :: QName -> Blocker -> Blocker Source #