Agda.Syntax.Internal.Blockers

Blocked Terms

data NotBlocked' t

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

EmbPrj NotBlocked

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: NotBlocked -> S Int32

icod_ :: NotBlocked -> S Int32

value :: Int32 -> R NotBlocked

Eq NotBlocked

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: NotBlocked -> NotBlocked -> Bool

(/=) :: NotBlocked -> NotBlocked -> Bool

Pretty t => Pretty (NotBlocked' t)

Defined in Agda.Syntax.Internal.Blockers

Methods

pretty :: NotBlocked' t -> Doc

prettyPrec :: Int -> NotBlocked' t -> Doc

prettyList :: [NotBlocked' t] -> Doc

Monoid (NotBlocked' t)

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)

ReallyNotBlocked is the unit. MissingClauses is dominant. StuckOn{} should be propagated, if tied, we take the left.

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)

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)

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)

Defined in Agda.Syntax.Internal.Blockers

Methods

rnf :: NotBlocked' t -> ()

type Rep (NotBlocked' t)

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

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

EncodeTCM Blocker

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Blocker -> TCM Value

Pretty Blocker

Defined in Agda.Syntax.Internal.Blockers

Methods

pretty :: Blocker -> Doc

prettyPrec :: Int -> Blocker -> Doc

prettyList :: [Blocker] -> Doc

MentionsMeta Blocker

Defined in Agda.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Blocker -> Bool

PrettyTCM Blocker

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Blocker -> m Doc

ToTerm Blocker

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Blocker -> Term)

toTermR :: TCM (Blocker -> ReduceM Term)

Instantiate Blocker

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Blocker -> ReduceM Blocker

Unquote Blocker

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Blocker

Generic Blocker

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

Defined in Agda.Syntax.Internal.Blockers

Methods

showsPrec :: Int -> Blocker -> ShowS

show :: Blocker -> String

showList :: [Blocker] -> ShowS

NFData Blocker

Defined in Agda.Syntax.Internal.Blockers

Methods

rnf :: Blocker -> ()

Eq Blocker

Defined in Agda.Syntax.Internal.Blockers

Methods

(==) :: Blocker -> Blocker -> Bool

(/=) :: Blocker -> Blocker -> Bool

Ord Blocker

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

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

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

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

EmbPrj Blocked_

Defined in Agda.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Blocked_ -> S Int32

icod_ :: Blocked_ -> S Int32

value :: Int32 -> R Blocked_

MonadError Blocked_ NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a

catchError :: NLM a -> (Blocked_ -> NLM a) -> NLM a

Pretty a => Pretty (Blocked a)

Defined in Agda.Syntax.Internal

Methods

pretty :: Blocked a -> Doc

prettyPrec :: Int -> Blocked a -> Doc

prettyList :: [Blocked a] -> Doc

TermLike a => TermLike (Blocked a)

Defined in Agda.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Blocked a -> m (Blocked a)

foldTerm :: Monoid m => (Term -> m) -> Blocked a -> m

KillRange a => KillRange (Blocked a)

Defined in Agda.Syntax.Internal

Methods

killRange :: KillRangeT (Blocked a)

PrettyTCM a => PrettyTCM (Blocked a)

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Blocked a -> m Doc

Instantiate a => Instantiate (Blocked a)

Defined in Agda.TypeChecking.Reduce

Methods

instantiate' :: Blocked a -> ReduceM (Blocked a)

Apply t => Apply (Blocked t)

Defined in Agda.TypeChecking.Substitute

Methods

apply :: Blocked t -> Args -> Blocked t

applyE :: Blocked t -> Elims -> Blocked t

Subst a => Subst (Blocked a)

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg (Blocked a)

Methods

applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a

Decoration (Blocked' t)

Defined in Agda.Syntax.Internal.Blockers

Methods

traverseF :: Functor m => (a -> m b) -> Blocked' t a -> m (Blocked' t b)

distributeF :: Functor m => Blocked' t (m a) -> m (Blocked' t a)

Foldable (Blocked' t)

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)

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)

Blocking on _all_ blockers.

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)

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)

Defined in Agda.TypeChecking.Substitute

Methods

(==) :: Blocked t -> Blocked t -> Bool

(/=) :: Blocked t -> Blocked t -> Bool

(Semigroup a, Monoid a) => Monoid (Blocked' t a)

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)

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)

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)

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)

Defined in Agda.Syntax.Internal.Blockers

Methods

rnf :: Blocked' t a -> ()

type SubstArg (Blocked a)

Defined in Agda.TypeChecking.Substitute

type SubstArg (Blocked a) = SubstArg a

type Rep (Blocked' t a)

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

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

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

notBlocked :: a -> Blocked' t a

blocked_ :: MetaId -> Blocked' t ()

notBlocked_ :: Blocked' t ()

getBlocker :: Blocked' t a -> Blocker

Waking up logic

data WakeUp

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

Constructors

WakeUp

DontWakeUp (Maybe Blocker)

Instances

Show WakeUp

Defined in Agda.Syntax.Internal.Blockers

Methods

showsPrec :: Int -> WakeUp -> ShowS

show :: WakeUp -> String

showList :: [WakeUp] -> ShowS

Eq WakeUp

Defined in Agda.Syntax.Internal.Blockers

Methods

(==) :: WakeUp -> WakeUp -> Bool

(/=) :: WakeUp -> WakeUp -> Bool

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