Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Free.Base

Contents

Set of meta variables.
Flexible and rigid occurrences (semigroup)
Multi-dimensional feature vector for variable occurrence (semigroup)
Plain variable occurrence counting.

Synopsis

newtype MetaSet = MetaSet {
- theMetaSet :: HashSet MetaId
}
insertMetaSet :: MetaId -> MetaSet -> MetaSet
foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
metaSetToBlocker :: MetaSet -> Blocker
data FlexRig' a
- = Flexible !a
- | WeaklyRigid
- | Unguarded
- | StronglyRigid
type FlexRig = FlexRig' MetaSet
class LensFlexRig o a | o -> a where
- lensFlexRig :: Lens' o (FlexRig' a)
isFlexible :: LensFlexRig o a => o -> Bool
isUnguarded :: LensFlexRig o a => o -> Bool
isWeaklyRigid :: LensFlexRig o a => o -> Bool
isStronglyRigid :: LensFlexRig o a => o -> Bool
addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
zeroFlexRig :: Monoid a => FlexRig' a
omegaFlexRig :: FlexRig' a
composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a
oneFlexRig :: FlexRig' a
flexRigToBlocker :: FlexRig -> Blocker
data VarOcc' a = VarOcc {
- varFlexRig :: !(FlexRig' a)
- varModality :: !Modality
}
type VarOcc = VarOcc' MetaSet
topVarOcc :: VarOcc' a
composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a
oneVarOcc :: VarOcc' a
constructorFlexRig :: ConHead -> Elims -> FlexRig' a
type TheVarMap' a = IntMap (VarOcc' a)
newtype VarMap' a = VarMap {
- theVarMap :: TheVarMap' a
}
type TheVarMap = TheVarMap' MetaSet
type VarMap = VarMap' MetaSet
mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b
lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a)
newtype VarCounts = VarCounts {
- varCounts :: IntMap Int
}
data IgnoreSorts
- = IgnoreNot
- | IgnoreInAnnotations
- | IgnoreAll
type Variable = Int

Set of meta variables.

newtype MetaSet Source #

A set of meta variables. Forms a monoid under union.

Constructors

MetaSet
Fields theMetaSet :: HashSet MetaId

Instances

Instances details

Pretty MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods pretty :: MetaSet -> Doc Source # prettyPrec :: Int -> MetaSet -> Doc Source # prettyList :: [MetaSet] -> Doc Source #
PrettyTCM MetaSet Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => MetaSet -> m Doc Source #
Null MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods empty :: MetaSet Source # null :: MetaSet -> Bool Source #
Monoid MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods mempty :: MetaSet # mappend :: MetaSet -> MetaSet -> MetaSet # mconcat :: [MetaSet] -> MetaSet #
Semigroup MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (<>) :: MetaSet -> MetaSet -> MetaSet # sconcat :: NonEmpty MetaSet -> MetaSet # stimes :: Integral b => b -> MetaSet -> MetaSet #
Eq MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (==) :: MetaSet -> MetaSet -> Bool # (/=) :: MetaSet -> MetaSet -> Bool #
Show MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> MetaSet -> ShowS # show :: MetaSet -> String # showList :: [MetaSet] -> ShowS #
Singleton MetaId MetaSet Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods singleton :: MetaId -> MetaSet Source #

insertMetaSet :: MetaId -> MetaSet -> MetaSet Source #

foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a Source #

metaSetToBlocker :: MetaSet -> Blocker Source #

Flexible and rigid occurrences (semigroup)

data FlexRig' a Source #

Depending on the surrounding context of a variable, it's occurrence can be classified as flexible or rigid, with finer distinctions.

The constructors are listed in increasing order (wrt. information content).

Constructors

Flexible !a	In arguments of metas. The set of metas is used by '`NonLinMatch'` to generate the right blocking information. The semantics is that the status of a variable occurrence may change if one of the metas in the set gets solved. We may say the occurrence is tainted by the meta variables in the set.
WeaklyRigid	In arguments to variables and definitions.
Unguarded	In top position, or only under inductive record constructors (unit).
StronglyRigid	Under at least one and only inductive constructors.

Instances

Instances details

Functor FlexRig' Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods fmap :: (a -> b) -> FlexRig' a -> FlexRig' b # (<$) :: a -> FlexRig' b -> FlexRig' a #
Foldable FlexRig' Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods fold :: Monoid m => FlexRig' m -> m # foldMap :: Monoid m => (a -> m) -> FlexRig' a -> m # foldMap' :: Monoid m => (a -> m) -> FlexRig' a -> m # foldr :: (a -> b -> b) -> b -> FlexRig' a -> b # foldr' :: (a -> b -> b) -> b -> FlexRig' a -> b # foldl :: (b -> a -> b) -> b -> FlexRig' a -> b # foldl' :: (b -> a -> b) -> b -> FlexRig' a -> b # foldr1 :: (a -> a -> a) -> FlexRig' a -> a # foldl1 :: (a -> a -> a) -> FlexRig' a -> a # toList :: FlexRig' a -> [a] # null :: FlexRig' a -> Bool # length :: FlexRig' a -> Int # elem :: Eq a => a -> FlexRig' a -> Bool # maximum :: Ord a => FlexRig' a -> a # minimum :: Ord a => FlexRig' a -> a # sum :: Num a => FlexRig' a -> a # product :: Num a => FlexRig' a -> a #
Pretty a => Pretty (FlexRig' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods pretty :: FlexRig' a -> Doc Source # prettyPrec :: Int -> FlexRig' a -> Doc Source # prettyList :: [FlexRig' a] -> Doc Source #
PrettyTCM a => PrettyTCM (FlexRig' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => FlexRig' a -> m Doc Source #
Eq a => Eq (FlexRig' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (==) :: FlexRig' a -> FlexRig' a -> Bool # (/=) :: FlexRig' a -> FlexRig' a -> Bool #
Show a => Show (FlexRig' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> FlexRig' a -> ShowS # show :: FlexRig' a -> String # showList :: [FlexRig' a] -> ShowS #
LensFlexRig (FlexRig' a) a Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a) Source #

type FlexRig = FlexRig' MetaSet Source #

class LensFlexRig o a | o -> a where Source #

Methods

lensFlexRig :: Lens' o (FlexRig' a) Source #

Instances

Instances details

LensFlexRig (FlexRig' a) a Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a) Source #
LensFlexRig (VarOcc' a) a Source #	Access to `varFlexRig` in `VarOcc`.
Instance details Defined in Agda.TypeChecking.Free.Base Methods lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a) Source #

isFlexible :: LensFlexRig o a => o -> Bool Source #

isUnguarded :: LensFlexRig o a => o -> Bool Source #

isWeaklyRigid :: LensFlexRig o a => o -> Bool Source #

isStronglyRigid :: LensFlexRig o a => o -> Bool Source #

addFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a Source #

FlexRig aggregation (additive operation of the semiring). For combining occurrences of the same variable in subterms. This is a refinement of the max operation for FlexRig which would work if Flexible did not have the MetaSet as an argument. Now, to aggregate two Flexible occurrences, we union the involved MetaSets.

zeroFlexRig :: Monoid a => FlexRig' a Source #

Unit for addFlexRig.

omegaFlexRig :: FlexRig' a Source #

Absorptive for addFlexRig.

composeFlexRig :: Semigroup a => FlexRig' a -> FlexRig' a -> FlexRig' a Source #

FlexRig composition (multiplicative operation of the semiring). For accumulating the context of a variable.

Flexible is dominant. Once we are under a meta, we are flexible regardless what else comes. We taint all variable occurrences under a meta by this meta.

WeaklyRigid is next in strength. Destroys strong rigidity.

StronglyRigid is still dominant over Unguarded.

Unguarded is the unit. It is the top (identity) context.

oneFlexRig :: FlexRig' a Source #

Unit for composeFlexRig.

flexRigToBlocker :: FlexRig -> Blocker Source #

Extract a blocker from an occurrence

Multi-dimensional feature vector for variable occurrence (semigroup)

data VarOcc' a Source #

Occurrence of free variables is classified by several dimensions. Currently, we have FlexRig and Modality.

Constructors

VarOcc
Fields varFlexRig :: !(FlexRig' a) varModality :: !Modality

Instances

Instances details

LensModality (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods getModality :: VarOcc' a -> Modality Source # setModality :: Modality -> VarOcc' a -> VarOcc' a Source # mapModality :: (Modality -> Modality) -> VarOcc' a -> VarOcc' a Source #
LensQuantity (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods getQuantity :: VarOcc' a -> Quantity Source # setQuantity :: Quantity -> VarOcc' a -> VarOcc' a Source # mapQuantity :: (Quantity -> Quantity) -> VarOcc' a -> VarOcc' a Source #
LensRelevance (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods getRelevance :: VarOcc' a -> Relevance Source # setRelevance :: Relevance -> VarOcc' a -> VarOcc' a Source # mapRelevance :: (Relevance -> Relevance) -> VarOcc' a -> VarOcc' a Source #
Pretty a => Pretty (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods pretty :: VarOcc' a -> Doc Source # prettyPrec :: Int -> VarOcc' a -> Doc Source # prettyList :: [VarOcc' a] -> Doc Source #
PrettyTCM a => PrettyTCM (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => VarOcc' a -> m Doc Source #
Monoid a => Monoid (VarOcc' a) Source #	The neutral element for variable occurrence aggregation is least serious occurrence: flexible, irrelevant. This is also the absorptive element for `composeVarOcc`, if we ignore the `MetaSet` in `Flexible`.
Instance details Defined in Agda.TypeChecking.Free.Base Methods mempty :: VarOcc' a # mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a # mconcat :: [VarOcc' a] -> VarOcc' a #
Semigroup a => Semigroup (VarOcc' a) Source #	The default way of aggregating free variable info from subterms is by adding the variable occurrences. For instance, if we have a pair `(t₁,t₂)` then and `t₁` has `o₁` the occurrences of a variable `x` and `t₂` has `o₂` the occurrences of the same variable, then `(t₁,t₂)` has `mappend o₁ o₂` occurrences of that variable. From counting `Quantity`, we extrapolate this to `FlexRig` and `Relevance`: we care most about about `StronglyRigid` `Relevant` occurrences. E.g., if `t₁` has a `StronglyRigid` occurrence and `t₂` a `Flexible` occurrence, then `(t₁,t₂)` still has a `StronglyRigid` occurrence. Analogously, `Relevant` occurrences count most, as we wish e.g. to forbid relevant occurrences of variables that are declared to be irrelevant. `VarOcc` forms a semiring, and this monoid is the addition of the semiring.
Instance details Defined in Agda.TypeChecking.Free.Base Methods (<>) :: VarOcc' a -> VarOcc' a -> VarOcc' a # sconcat :: NonEmpty (VarOcc' a) -> VarOcc' a # stimes :: Integral b => b -> VarOcc' a -> VarOcc' a #
Eq a => Eq (VarOcc' a) Source #	Equality up to origin.
Instance details Defined in Agda.TypeChecking.Free.Base Methods (==) :: VarOcc' a -> VarOcc' a -> Bool # (/=) :: VarOcc' a -> VarOcc' a -> Bool #
Show a => Show (VarOcc' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> VarOcc' a -> ShowS # show :: VarOcc' a -> String # showList :: [VarOcc' a] -> ShowS #
LensFlexRig (VarOcc' a) a Source #	Access to `varFlexRig` in `VarOcc`.
Instance details Defined in Agda.TypeChecking.Free.Base Methods lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a) Source #

type VarOcc = VarOcc' MetaSet Source #

topVarOcc :: VarOcc' a Source #

The absorptive element of variable occurrence under aggregation: strongly rigid, relevant.

composeVarOcc :: Semigroup a => VarOcc' a -> VarOcc' a -> VarOcc' a Source #

First argument is the outer occurrence (context) and second is the inner. This multiplicative operation is to modify an occurrence under a context.

oneVarOcc :: VarOcc' a Source #

constructorFlexRig :: ConHead -> Elims -> FlexRig' a Source #

What's the rigidity of a constructor?

type TheVarMap' a = IntMap (VarOcc' a) Source #

Representation of a variable set as map from de Bruijn indices to VarOcc.

newtype VarMap' a Source #

Constructors

VarMap
Fields theVarMap :: TheVarMap' a

Instances

Instances details

Singleton Variable (VarMap' a) Source #	A "set"-style `Singleton` instance with default/initial variable occurrence.
Instance details Defined in Agda.TypeChecking.Free.Base Methods singleton :: Variable -> VarMap' a Source #
PrettyTCM a => PrettyTCM (VarMap' a) Source #
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => VarMap' a -> m Doc Source #
Semigroup a => Monoid (VarMap' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods mempty :: VarMap' a # mappend :: VarMap' a -> VarMap' a -> VarMap' a # mconcat :: [VarMap' a] -> VarMap' a #
Semigroup a => Semigroup (VarMap' a) Source #	Proper monoid instance for `VarMap` rather than inheriting the broken one from IntMap. We combine two occurrences of a variable using `mappend`.
Instance details Defined in Agda.TypeChecking.Free.Base Methods (<>) :: VarMap' a -> VarMap' a -> VarMap' a # sconcat :: NonEmpty (VarMap' a) -> VarMap' a # stimes :: Integral b => b -> VarMap' a -> VarMap' a #
Eq a => Eq (VarMap' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (==) :: VarMap' a -> VarMap' a -> Bool # (/=) :: VarMap' a -> VarMap' a -> Bool #
Show a => Show (VarMap' a) Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> VarMap' a -> ShowS # show :: VarMap' a -> String # showList :: [VarMap' a] -> ShowS #

type TheVarMap = TheVarMap' MetaSet Source #

type VarMap = VarMap' MetaSet Source #

mapVarMap :: (TheVarMap' a -> TheVarMap' b) -> VarMap' a -> VarMap' b Source #

lookupVarMap :: Variable -> VarMap' a -> Maybe (VarOcc' a) Source #

Plain variable occurrence counting.

newtype VarCounts Source #

Constructors

VarCounts
Fields varCounts :: IntMap Int

Instances

Instances details

Monoid VarCounts Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods mempty :: VarCounts # mappend :: VarCounts -> VarCounts -> VarCounts # mconcat :: [VarCounts] -> VarCounts #
Semigroup VarCounts Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (<>) :: VarCounts -> VarCounts -> VarCounts # sconcat :: NonEmpty VarCounts -> VarCounts # stimes :: Integral b => b -> VarCounts -> VarCounts #
Eq VarCounts Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (==) :: VarCounts -> VarCounts -> Bool # (/=) :: VarCounts -> VarCounts -> Bool #
Show VarCounts Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> VarCounts -> ShowS # show :: VarCounts -> String # showList :: [VarCounts] -> ShowS #

data IgnoreSorts Source #

Where should we skip sorts in free variable analysis?

Constructors

IgnoreNot	Do not skip.
IgnoreInAnnotations	Skip when annotation to a type.
IgnoreAll	Skip unconditionally.

Instances

Instances details

Eq IgnoreSorts Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods (==) :: IgnoreSorts -> IgnoreSorts -> Bool # (/=) :: IgnoreSorts -> IgnoreSorts -> Bool #
Show IgnoreSorts Source #
Instance details Defined in Agda.TypeChecking.Free.Base Methods showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS #

type Variable = Int Source #