| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Internal.Blockers
Synopsis
- data NotBlocked' t
- data Blocker
- 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
- = Blocked {
- 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 |
| Underapplied | Not enough arguments were supplied to complete the matching. |
| AbsurdMatch | We matched an absurd clause, results in a neutral |
| MissingClauses QName | We ran out of clauses for |
| ReallyNotBlocked | Reduction was not blocked, we reached a whnf
which can be anything but a stuck |
Instances
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 Source # | |||||
| Pretty Blocker Source # | |||||
| MentionsMeta Blocker Source # | |||||
Defined in Agda.TypeChecking.MetaVars.Mention | |||||
| PrettyTCM Blocker Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| ToTerm Blocker Source # | |||||
| Instantiate Blocker Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| Unquote Blocker Source # | |||||
| Generic Blocker Source # | |||||
Defined in Agda.Syntax.Internal.Blockers Associated Types
| |||||
| Show Blocker Source # | |||||
| NFData Blocker Source # | |||||
Defined in Agda.Syntax.Internal.Blockers | |||||
| Eq Blocker Source # | |||||
| Ord Blocker Source # | |||||
Defined in Agda.Syntax.Internal.Blockers | |||||
| type Rep Blocker Source # | |||||
Defined in Agda.Syntax.Internal.Blockers type Rep Blocker = D1 ('MetaData "Blocker" "Agda.Syntax.Internal.Blockers" "Agda-2.6.4.3-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))))) | |||||
unblockOnMeta :: MetaId -> Blocker Source #
unblockOnProblem :: ProblemId -> Blocker Source #
unblockOnDef :: QName -> Blocker 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
| |
| NotBlocked | |
Fields
| |
Instances
| EmbPrj Blocked_ Source # | |||||
| MonadError Blocked_ NLM Source # | |||||
Defined in Agda.TypeChecking.Rewriting.NonLinMatch | |||||
| Pretty a => Pretty (Blocked a) Source # | |||||
| TermLike a => TermLike (Blocked a) Source # | |||||
| KillRange a => KillRange (Blocked a) Source # | |||||
Defined in Agda.Syntax.Internal Methods killRange :: KillRangeT (Blocked a) Source # | |||||
| PrettyTCM a => PrettyTCM (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Pretty | |||||
| Instantiate a => Instantiate (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Reduce | |||||
| Apply t => Apply (Blocked t) Source # | |||||
| Subst a => Subst (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Blocked a)) -> Blocked a -> Blocked a Source # | |||||
| Decoration (Blocked' t) Source # | |||||
| Foldable (Blocked' t) Source # | |||||
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 # | |||||
| Traversable (Blocked' t) Source # | |||||
Defined in Agda.Syntax.Internal.Blockers | |||||
| Applicative (Blocked' t) Source # | Blocking on _all_ blockers. | ||||
Defined in Agda.Syntax.Internal.Blockers | |||||
| Functor (Blocked' t) Source # | |||||
| Eq t => Eq (Blocked t) Source # | |||||
| (Semigroup a, Monoid a) => Monoid (Blocked' t a) Source # | |||||
| Semigroup a => Semigroup (Blocked' t a) Source # | |||||
| Generic (Blocked' t a) Source # | |||||
Defined in Agda.Syntax.Internal.Blockers Associated Types
| |||||
| (Show t, Show a) => Show (Blocked' t a) Source # | |||||
| (NFData t, NFData a) => NFData (Blocked' t a) Source # | |||||
Defined in Agda.Syntax.Internal.Blockers | |||||
| type SubstArg (Blocked a) Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
| type Rep (Blocked' t a) Source # | |||||
Defined in Agda.Syntax.Internal.Blockers type Rep (Blocked' t a) = D1 ('MetaData "Blocked'" "Agda.Syntax.Internal.Blockers" "Agda-2.6.4.3-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 e0StuckOn 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
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.
notBlocked :: a -> Blocked' t a Source #
notBlocked_ :: Blocked' t () Source #
getBlocker :: Blocked' t a -> Blocker Source #
Waking up logic
Should a constraint wake up or not? If not, we might refine the unblocker.
Constructors
| WakeUp | |
| DontWakeUp (Maybe Blocker) |
Instances
wakeUpWhen_ :: (constr -> Bool) -> constr -> WakeUp Source #