Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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 Word32 Source # icod_ :: NotBlocked -> S Word32 Source # value :: Word32 -> R NotBlocked Source #
Eq NotBlocked Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: NotBlocked -> NotBlocked -> Bool Source # (/=) :: NotBlocked -> NotBlocked -> Bool Source #
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 #
NFData t => NFData (NotBlocked' t) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods rnf :: NotBlocked' t -> () Source #
Monoid (NotBlocked' t) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods mempty :: NotBlocked' t Source # mappend :: NotBlocked' t -> NotBlocked' t -> NotBlocked' t Source # mconcat :: [NotBlocked' t] -> NotBlocked' t Source #
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 Source # sconcat :: NonEmpty (NotBlocked' t) -> NotBlocked' t Source # stimes :: Integral b => b -> NotBlocked' t -> NotBlocked' t Source #
Generic (NotBlocked' t) Source # |

Instance details

Defined in Agda.Syntax.Internal.Blockers

Associated Types

type Rep (NotBlocked' t) |

Instance details

Defined in Agda.Syntax.Internal.Blockers

type Rep (NotBlocked' t) = D1 ('MetaData "NotBlocked'" "Agda.Syntax.Internal.Blockers" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: NotBlocked' t -> Rep (NotBlocked' t) x Source #

to :: Rep (NotBlocked' t) x -> NotBlocked' t Source #

Show t => Show (NotBlocked' t) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> NotBlocked' t -> ShowS Source # show :: NotBlocked' t -> String Source # showList :: [NotBlocked' t] -> ShowS Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> 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 #
NFData Blocker Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods rnf :: Blocker -> () Source #
Generic Blocker Source # |

Instance details

Defined in Agda.Syntax.Internal.Blockers

Associated Types

type Rep Blocker |

Instance details

Defined in Agda.Syntax.Internal.Blockers

type Rep Blocker = D1 ('MetaData "Blocker" "Agda.Syntax.Internal.Blockers" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))))

Methods

from :: Blocker -> Rep Blocker x Source #

to :: Rep Blocker x -> Blocker Source #

Show Blocker Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> Blocker -> ShowS Source # show :: Blocker -> String Source # showList :: [Blocker] -> ShowS Source #
Eq Blocker Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (==) :: Blocker -> Blocker -> Bool Source # (/=) :: Blocker -> Blocker -> Bool Source #
Ord Blocker Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods compare :: Blocker -> Blocker -> Ordering Source # (<) :: Blocker -> Blocker -> Bool Source # (<=) :: Blocker -> Blocker -> Bool Source # (>) :: Blocker -> Blocker -> Bool Source # (>=) :: Blocker -> Blocker -> Bool Source # max :: Blocker -> Blocker -> Blocker Source # min :: Blocker -> Blocker -> Blocker Source #
type Rep Blocker Source # |

Instance details

Defined in Agda.Syntax.Internal.Blockers

type Rep Blocker = D1 ('MetaData "Blocker" "Agda.Syntax.Internal.Blockers" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Word32 Source # icod_ :: Blocked_ -> S Word32 Source # value :: Word32 -> R Blocked_ Source #
MonadError Blocked_ NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch Methods throwError :: Blocked_ -> NLM a Source # catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a Source #
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) |
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg (Blocked a) = SubstArg a

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 #
Applicative (Blocked' t) Source # | Blocking on _all_ blockers.
Instance details Defined in Agda.Syntax.Internal.Blockers Methods pure :: a -> Blocked' t a Source # (<*>) :: Blocked' t (a -> b) -> Blocked' t a -> Blocked' t b Source # liftA2 :: (a -> b -> c) -> Blocked' t a -> Blocked' t b -> Blocked' t c Source # (*>) :: Blocked' t a -> Blocked' t b -> Blocked' t b Source # (<*) :: Blocked' t a -> Blocked' t b -> Blocked' t a Source #
Functor (Blocked' t) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods fmap :: (a -> b) -> Blocked' t a -> Blocked' t b Source # (<$) :: a -> Blocked' t b -> Blocked' t a Source #
Foldable (Blocked' t) Source # |

Instance details

Defined in Agda.Syntax.Internal.Blockers

Methods

fold :: Monoid m => Blocked' t m -> m Source #

foldMap :: Monoid m => (a -> m) -> Blocked' t a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Blocked' t a -> m Source #

foldr :: (a -> b -> b) -> b -> Blocked' t a -> b Source #

foldr' :: (a -> b -> b) -> b -> Blocked' t a -> b Source #

foldl :: (b -> a -> b) -> b -> Blocked' t a -> b Source #

foldl' :: (b -> a -> b) -> b -> Blocked' t a -> b Source #

foldr1 :: (a -> a -> a) -> Blocked' t a -> a Source #

foldl1 :: (a -> a -> a) -> Blocked' t a -> a Source #

toList :: Blocked' t a -> [a] Source #

null :: Blocked' t a -> Bool Source #

length :: Blocked' t a -> Int Source #

elem :: Eq a => a -> Blocked' t a -> Bool Source #

maximum :: Ord a => Blocked' t a -> a Source #

minimum :: Ord a => Blocked' t a -> a Source #

sum :: Num a => Blocked' t a -> a Source #

product :: Num a => Blocked' t a -> a Source #

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) Source # sequenceA :: Applicative f => Blocked' t (f a) -> f (Blocked' t a) Source # mapM :: Monad m => (a -> m b) -> Blocked' t a -> m (Blocked' t b) Source # sequence :: Monad m => Blocked' t (m a) -> m (Blocked' t a) Source #
Eq t => Eq (Blocked t) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods (==) :: Blocked t -> Blocked t -> Bool Source # (/=) :: Blocked t -> Blocked t -> Bool Source #
(NFData t, NFData a) => NFData (Blocked' t a) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods rnf :: Blocked' t a -> () Source #
(Semigroup a, Monoid a) => Monoid (Blocked' t a) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods mempty :: Blocked' t a Source # mappend :: Blocked' t a -> Blocked' t a -> Blocked' t a Source # mconcat :: [Blocked' t a] -> Blocked' t a Source #
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 Source # sconcat :: NonEmpty (Blocked' t a) -> Blocked' t a Source # stimes :: Integral b => b -> Blocked' t a -> Blocked' t a Source #
Generic (Blocked' t a) Source # |

Instance details

Defined in Agda.Syntax.Internal.Blockers

Associated Types

type Rep (Blocked' t a) |

Instance details

Defined in Agda.Syntax.Internal.Blockers

type Rep (Blocked' t a) = D1 ('MetaData "Blocked'" "Agda.Syntax.Internal.Blockers" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: Blocked' t a -> Rep (Blocked' t a) x Source #

to :: Rep (Blocked' t a) x -> Blocked' t a Source #

(Show t, Show a) => Show (Blocked' t a) Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods showsPrec :: Int -> Blocked' t a -> ShowS Source # show :: Blocked' t a -> String Source # showList :: [Blocked' t a] -> ShowS Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source # show :: WakeUp -> String Source # showList :: [WakeUp] -> ShowS Source #
Eq WakeUp Source # |
Instance details Defined in Agda.Syntax.Internal.Blockers Methods (==) :: WakeUp -> WakeUp -> Bool Source # (/=) :: WakeUp -> WakeUp -> Bool Source #

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 #