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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Free.Lazy

Contents

- Set of meta variables.
- Flexible and rigid occurrences (semigroup)
- Multi-dimensional feature vector for variable occurrence (semigroup)
- Storing variable occurrences (semimodule).
- Simple flexible/rigid variable collection.
- Environment for collecting free variables.
- Recursively collecting free variables.
- Orphan instances

Description

Computing the free variables of a term lazily.

We implement a reduce (traversal into monoid) over internal syntax for a generic collection (monoid with singletons). This should allow a more efficient test for the presence of a particular variable.

Worst-case complexity does not change (i.e. the case when a variable does not occur), but best case-complexity does matter. For instance, see `mkAbs`: each time we construct a dependent function type, we check whether it is actually dependent.

The distinction between rigid and strongly rigid occurrences comes from: Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)

The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly in t. It might have a solution if the occurrence is not strongly rigid, e.g.

x = f -> suc (f (x ( y -> k))) has x = f -> suc (f (suc k))

Jason C. Reed, PhD thesis, page 106

Under coinductive constructors, occurrences are never strongly rigid. Also, function types and lambdas do not establish strong rigidity. Only inductive constructors do so. (See issue 1271).

For further reading on semirings and semimodules for variable occurrence, see e.g. Conor McBrides "I got plenty of nuttin'" (Wadlerfest 2016). There, he treats the "quantity" dimension of variable occurrences.

The semiring has an additive operation for combining occurrences of subterms, and a multiplicative operation of representing function composition. E.g. if variable `x` appears `o` in term `u`, but `u` appears in context `q` in term `t` then occurrence of variable `x` coming from `u` is accounted for as `q o` in `t`.

Consider example `(λ{ x → (x,x)}) y`:

- Variable `x` occurs once unguarded in `x`.
- It occurs twice unguarded in the aggregation `x` `x`
- Inductive constructor `,` turns this into two strictly rigid occurrences.

If `,` is a record constructor, then we stay unguarded.

- The function `({λ x → (x,x)})` provides a context for variable `y`. This context can be described as weakly rigid with quantity two.
- The final occurrence of `y` is obtained as composing the context with the occurrence of `y` in itself (which is the unit for composition). Thus, `y` occurs weakly rigid with quantity two.

It is not a given that the context can be described in the same way as the variable occurrence. However, for quantity it is the case and we obtain a semiring of occurrences with 0, 1, and even ω, which is an absorptive element for addition.

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
- 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
- class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where
  - withVarOcc :: VarOcc' a -> c -> c
- 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)
- type TheFlexRigMap = IntMap (FlexRig' ())
- newtype FlexRigMap = FlexRigMap {
  - theFlexRigMap :: TheFlexRigMap
  }
- mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap
- data IgnoreSorts
  - = IgnoreNot
  - | IgnoreInAnnotations
  - | IgnoreAll
- data FreeEnv' a b c = FreeEnv {
  - feExtra :: !b
  - feFlexRig :: !(FlexRig' a)
  - feModality :: !Modality
  - feSingleton :: Maybe Variable -> c
  }
- type Variable = Int
- type SingleVar c = Variable -> c
- type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c
- feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts
- initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c
- type FreeT a b (m :: Type -> Type) c = ReaderT (FreeEnv' a b c) m c
- type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c
- runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c
- variable :: forall (m :: Type -> Type) a c b. (Monad m, IsVarSet a c) => Int -> FreeT a b m c
- subVar :: Int -> Maybe Variable -> Maybe Variable
- underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z
- underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z
- underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z
- underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z
- underQuantity :: (MonadReader r m, LensQuantity r, LensQuantity o) => o -> m a -> m a
- underFlexRig :: (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) => o -> m z -> m z
- underConstructor :: (MonadReader r m, LensFlexRig r a, Semigroup a) => ConHead -> Elims -> m z -> m z
- class Free t where
  - freeVars' :: IsVarSet a c => t -> FreeM a c

# 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

Null MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods empty :: MetaSet Source # null :: MetaSet -> Bool Source #
Monoid MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods mempty :: MetaSet Source # mappend :: MetaSet -> MetaSet -> MetaSet Source # mconcat :: [MetaSet] -> MetaSet Source #
Semigroup MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: MetaSet -> MetaSet -> MetaSet Source # sconcat :: NonEmpty MetaSet -> MetaSet Source # stimes :: Integral b => b -> MetaSet -> MetaSet Source #
Show MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> MetaSet -> ShowS Source # show :: MetaSet -> String Source # showList :: [MetaSet] -> ShowS Source #
Eq MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: MetaSet -> MetaSet -> Bool Source # (/=) :: MetaSet -> MetaSet -> Bool Source #
Singleton MetaId MetaSet Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy 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.Lazy Methods fmap :: (a -> b) -> FlexRig' a -> FlexRig' b Source # (<$) :: a -> FlexRig' b -> FlexRig' a Source #
Foldable FlexRig' Source # |

Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

fold :: Monoid m => FlexRig' m -> m Source #

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

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

foldr :: (a -> b -> b) -> b -> FlexRig' a -> b Source #

foldr' :: (a -> b -> b) -> b -> FlexRig' a -> b Source #

foldl :: (b -> a -> b) -> b -> FlexRig' a -> b Source #

foldl' :: (b -> a -> b) -> b -> FlexRig' a -> b Source #

foldr1 :: (a -> a -> a) -> FlexRig' a -> a Source #

foldl1 :: (a -> a -> a) -> FlexRig' a -> a Source #

toList :: FlexRig' a -> [a] Source #

null :: FlexRig' a -> Bool Source #

length :: FlexRig' a -> Int Source #

elem :: Eq a => a -> FlexRig' a -> Bool Source #

maximum :: Ord a => FlexRig' a -> a Source #

minimum :: Ord a => FlexRig' a -> a Source #

sum :: Num a => FlexRig' a -> a Source #

product :: Num a => FlexRig' a -> a Source #

Show a => Show (FlexRig' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> FlexRig' a -> ShowS Source # show :: FlexRig' a -> String Source # showList :: [FlexRig' a] -> ShowS Source #
Eq a => Eq (FlexRig' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: FlexRig' a -> FlexRig' a -> Bool Source # (/=) :: FlexRig' a -> FlexRig' a -> Bool Source #
LensFlexRig (FlexRig' a) a Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods lensFlexRig :: Lens' (FlexRig' a) (FlexRig' a) Source #
Singleton (Variable, FlexRig' ()) FlexRigMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: (Variable, FlexRig' ()) -> FlexRigMap 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.Lazy 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.Lazy Methods lensFlexRig :: Lens' (VarOcc' a) (FlexRig' a) Source #
LensFlexRig (FreeEnv' a b c) a Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods lensFlexRig :: Lens' (FreeEnv' a b c) (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 `MetaSet`s.

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

# 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.Lazy 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.Lazy 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.Lazy Methods getRelevance :: VarOcc' a -> Relevance Source # setRelevance :: Relevance -> VarOcc' a -> VarOcc' a Source # mapRelevance :: (Relevance -> Relevance) -> VarOcc' a -> VarOcc' a Source #
(Semigroup a, 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.Lazy Methods mempty :: VarOcc' a Source # mappend :: VarOcc' a -> VarOcc' a -> VarOcc' a Source # mconcat :: [VarOcc' a] -> VarOcc' a Source #

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.Lazy Methods (<>) :: VarOcc' a -> VarOcc' a -> VarOcc' a Source # sconcat :: NonEmpty (VarOcc' a) -> VarOcc' a Source # stimes :: Integral b => b -> VarOcc' a -> VarOcc' a Source #
Show a => Show (VarOcc' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> VarOcc' a -> ShowS Source # show :: VarOcc' a -> String Source # showList :: [VarOcc' a] -> ShowS Source #
Eq a => Eq (VarOcc' a) Source # | Equality up to origin.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: VarOcc' a -> VarOcc' a -> Bool Source # (/=) :: VarOcc' a -> VarOcc' a -> Bool Source #
LensFlexRig (VarOcc' a) a Source # | Access to `varFlexRig` in `VarOcc`.
Instance details Defined in Agda.TypeChecking.Free.Lazy 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 #

# Storing variable occurrences (semimodule).

class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where Source #

Any representation `c` of a set of variables need to be able to be modified by a variable occurrence. This is to ensure that free variable analysis is compositional. For instance, it should be possible to compute `fv (v [u/x])` from `fv v` and `fv u`.

In algebraic terminology, a variable set `a` needs to be (almost) a left semimodule to the semiring `VarOcc`.

Methods

withVarOcc :: VarOcc' a -> c -> c Source #

Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition: ``` withVarOcc oneVarOcc = id withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ``` * Respects VarOcc aggregation: ``` withVarOcc (o1 <> o2) x = withVarOcc o1 x <> withVarOcc o2 x ``` Since the corresponding unit law may fail, ``` withVarOcc mempty x = mempty ``` it is not quite a semimodule.

#### Instances

Instances details

IsVarSet () VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> VarCounts -> VarCounts Source #
IsVarSet () FlexRigMap Source # | Compose everything with the `varFlexRig` part of the `VarOcc`.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap Source #
IsVarSet () AllowedVar Source # |
Instance details Defined in Agda.TypeChecking.MetaVars.Occurs Methods withVarOcc :: VarOcc' () -> AllowedVar -> AllowedVar Source #
IsVarSet () All Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> All -> All Source #
IsVarSet () Any Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> Any -> Any Source #
IsVarSet () [Int] Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> [Int] -> [Int] Source #
(Singleton MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a Source #

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 MetaId a, Semigroup a, Monoid a) => IsVarSet a (VarMap' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc' a -> VarMap' a -> VarMap' a Source #
Singleton Variable (VarMap' a) Source # | A "set"-style `Singleton` instance with default/initial variable occurrence.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: Variable -> VarMap' a Source #
Semigroup a => Monoid (VarMap' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods mempty :: VarMap' a Source # mappend :: VarMap' a -> VarMap' a -> VarMap' a Source # mconcat :: [VarMap' a] -> VarMap' a Source #
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.Lazy Methods (<>) :: VarMap' a -> VarMap' a -> VarMap' a Source # sconcat :: NonEmpty (VarMap' a) -> VarMap' a Source # stimes :: Integral b => b -> VarMap' a -> VarMap' a Source #
Show a => Show (VarMap' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> VarMap' a -> ShowS Source # show :: VarMap' a -> String Source # showList :: [VarMap' a] -> ShowS Source #
Eq a => Eq (VarMap' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: VarMap' a -> VarMap' a -> Bool Source # (/=) :: VarMap' a -> VarMap' a -> Bool Source #

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 #

# Simple flexible/rigid variable collection.

type TheFlexRigMap = IntMap (FlexRig' ()) Source #

Keep track of `FlexRig` for every variable, but forget the involved meta vars.

newtype FlexRigMap Source #

Constructors

FlexRigMap |

Fields

- theFlexRigMap :: TheFlexRigMap

#### Instances

Instances details

Monoid FlexRigMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods mempty :: FlexRigMap Source # mappend :: FlexRigMap -> FlexRigMap -> FlexRigMap Source # mconcat :: [FlexRigMap] -> FlexRigMap Source #
Semigroup FlexRigMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: FlexRigMap -> FlexRigMap -> FlexRigMap Source # sconcat :: NonEmpty FlexRigMap -> FlexRigMap Source # stimes :: Integral b => b -> FlexRigMap -> FlexRigMap Source #
Show FlexRigMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> FlexRigMap -> ShowS Source # show :: FlexRigMap -> String Source # showList :: [FlexRigMap] -> ShowS Source #
IsVarSet () FlexRigMap Source # | Compose everything with the `varFlexRig` part of the `VarOcc`.
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc' () -> FlexRigMap -> FlexRigMap Source #
Singleton (Variable, FlexRig' ()) FlexRigMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: (Variable, FlexRig' ()) -> FlexRigMap Source #

mapFlexRigMap :: (TheFlexRigMap -> TheFlexRigMap) -> FlexRigMap -> FlexRigMap Source #

# Environment for collecting free variables.

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

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

data FreeEnv' a b c Source #

The current context.

Constructors

FreeEnv |

Fields

- feExtra :: !b

  Additional context, e.g., whether to ignore free variables in sorts.

- feFlexRig :: !(FlexRig' a)

  Are we flexible or rigid?

- feModality :: !Modality

  What is the current relevance and quantity?

- feSingleton :: Maybe Variable -> c

  Method to return a single variable.

#### Instances

Instances details

LensModality (FreeEnv' a b c) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getModality :: FreeEnv' a b c -> Modality Source # setModality :: Modality -> FreeEnv' a b c -> FreeEnv' a b c Source # mapModality :: (Modality -> Modality) -> FreeEnv' a b c -> FreeEnv' a b c Source #
LensQuantity (FreeEnv' a b c) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getQuantity :: FreeEnv' a b c -> Quantity Source # setQuantity :: Quantity -> FreeEnv' a b c -> FreeEnv' a b c Source # mapQuantity :: (Quantity -> Quantity) -> FreeEnv' a b c -> FreeEnv' a b c Source #
LensRelevance (FreeEnv' a b c) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getRelevance :: FreeEnv' a b c -> Relevance Source # setRelevance :: Relevance -> FreeEnv' a b c -> FreeEnv' a b c Source # mapRelevance :: (Relevance -> Relevance) -> FreeEnv' a b c -> FreeEnv' a b c Source #
LensFlexRig (FreeEnv' a b c) a Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods lensFlexRig :: Lens' (FreeEnv' a b c) (FlexRig' a) Source #
(Functor m, Applicative m, Monad m, Semigroup c, Monoid c) => Monoid (FreeT a b m c) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods mempty :: FreeT a b m c Source # mappend :: FreeT a b m c -> FreeT a b m c -> FreeT a b m c Source # mconcat :: [FreeT a b m c] -> FreeT a b m c Source #

type Variable = Int Source #

type SingleVar c = Variable -> c Source #

type FreeEnv c = FreeEnv' MetaSet IgnoreSorts c Source #

feIgnoreSorts :: FreeEnv' a IgnoreSorts c -> IgnoreSorts Source #

Ignore free variables in sorts.

initFreeEnv :: Monoid c => b -> SingleVar c -> FreeEnv' a b c Source #

The initial context.

type FreeT a b (m :: Type -> Type) c = ReaderT (FreeEnv' a b c) m c Source #

type FreeM a c = Reader (FreeEnv' a IgnoreSorts c) c Source #

runFreeM :: IsVarSet a c => SingleVar c -> IgnoreSorts -> FreeM a c -> c Source #

Run function for FreeM.

variable :: forall (m :: Type -> Type) a c b. (Monad m, IsVarSet a c) => Int -> FreeT a b m c Source #

Base case: a variable.

subVar :: Int -> Maybe Variable -> Maybe Variable Source #

Subtract, but return Nothing if result is negative.

underBinder :: MonadReader (FreeEnv' a b c) m => m z -> m z Source #

Going under a binder.

underBinder' :: MonadReader (FreeEnv' a b c) m => Nat -> m z -> m z Source #

Going under `n` binders.

underModality :: (MonadReader r m, LensModality r, LensModality o) => o -> m z -> m z Source #

Changing the `Modality`.

underRelevance :: (MonadReader r m, LensRelevance r, LensRelevance o) => o -> m z -> m z Source #

Changing the `Relevance`.

underQuantity :: (MonadReader r m, LensQuantity r, LensQuantity o) => o -> m a -> m a Source #

In the given computation the `Quantity` is locally scaled using the `Quantity` of the first argument.

underFlexRig :: (MonadReader r m, LensFlexRig r a, Semigroup a, LensFlexRig o a) => o -> m z -> m z Source #

Changing the `FlexRig` context.

underConstructor :: (MonadReader r m, LensFlexRig r a, Semigroup a) => ConHead -> Elims -> m z -> m z Source #

What happens to the variables occurring under a constructor?

# Recursively collecting free variables.

class Free t where Source #

Gather free variables in a collection.

Minimal complete definition

Nothing

Methods

freeVars' :: IsVarSet a c => t -> FreeM a c Source #

default freeVars' :: forall (f :: Type -> Type) b a c. (t ~ f b, Foldable f, Free b, IsVarSet a c) => t -> FreeM a c Source #

#### Instances

Instances details

Free Clause Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Clause -> FreeM a c Source #
Free EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => EqualityView -> FreeM a c Source #
Free Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Level -> FreeM a c Source #
Free Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Sort -> FreeM a c Source #
Free Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Term -> FreeM a c Source #
Free Candidate Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet a c => Candidate -> FreeM a c Source #
Free CompareAs Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet a c => CompareAs -> FreeM a c Source #
Free Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet a c => Constraint -> FreeM a c Source #
Free DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet a c => DisplayForm -> FreeM a c Source #
Free DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet a c => DisplayTerm -> FreeM a c Source #
Free NLPSort Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods freeVars' :: IsVarSet a c => NLPSort -> FreeM a c Source #
Free NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods freeVars' :: IsVarSet a c => NLPType -> FreeM a c Source #
Free NLPat Source # | Only computes free variables that are not bound (see `nlPatVars`), i.e., those in a `PTerm`.
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinPattern Methods freeVars' :: IsVarSet a c => NLPat -> FreeM a c Source #
Free t => Free (Arg t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Arg t -> FreeM a c Source #
Free t => Free (Ranged t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Ranged t -> FreeM a c Source #
Free t => Free (WithHiding t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => WithHiding t -> FreeM a c Source #
Free t => Free (Abs t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Abs t -> FreeM a c Source #
Free t => Free (Dom t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Dom t -> FreeM a c Source #
Free t => Free (PlusLevel' t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => PlusLevel' t -> FreeM a c Source #
Free t => Free (Tele t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Tele t -> FreeM a c Source #
Free t => Free (Type' t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Type' t -> FreeM a c Source #
Free t => Free (Elim' t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Elim' t -> FreeM a c Source #
Free t => Free (SingleLevel' t) Source # |
Instance details Defined in Agda.TypeChecking.Level Methods freeVars' :: IsVarSet a c => SingleLevel' t -> FreeM a c Source #
Free t => Free (List1 t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => List1 t -> FreeM a c Source #
Free t => Free (Maybe t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Maybe t -> FreeM a c Source #
Free t => Free [t] Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => [t] -> FreeM a c Source #
Free t => Free (Named nm t) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => Named nm t -> FreeM a c Source #
(Free t, Free u) => Free (t, u) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => (t, u) -> FreeM a c Source #
(Free t, Free u, Free v) => Free (t, u, v) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet a c => (t, u, v) -> FreeM a c Source #

# Orphan instances

Singleton MetaId () Source # |
Instance details Methods singleton :: MetaId -> () Source #