Agda-2.6.2.2.20221106: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Internal.Blockers

Synopsis

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

Eq NotBlocked Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Monoid (NotBlocked' t) Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

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

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

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.2.2.20221106-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

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 #

Instantiate Blocker Source # 
Instance details

Defined in Agda.TypeChecking.Reduce

Pretty Blocker Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

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

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

type Rep Blocker Source # 
Instance details

Defined in Agda.Syntax.Internal.Blockers

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).

Instances

Instances details
EmbPrj Blocked_ Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Internal

MonadError Blocked_ NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

Methods

throwError :: Blocked_ -> NLM a #

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

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

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

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 #

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 #

Pretty a => Pretty (Blocked a) Source # 
Instance details

Defined in Agda.Syntax.Internal

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) Source # 
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 a, Show t) => 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 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.2.2.20221106-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.

blocked :: MetaId -> a -> Blocked' t a 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

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 #