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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Free

Contents

- Orphan instances

Description

Computing the free variables of a term.

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

If you need the occurrence information for all free variables, you can use `freeVars` which has amoungst others this instance `freeVars :: Term -> VarMap` From `VarMap`, specific information can be extracted, e.g., `relevantVars :: VarMap -> VarSet relevantVars = filterVarMap isRelevant`

To just check the status of a single free variable, there are more efficient methods, e.g., `freeIn :: Nat -> Term -> Bool`

Tailored optimized variable checks can be implemented as semimodules to `VarOcc`, see, for example, `VarCounts` or `SingleFlexRig`.

Synopsis

- newtype VarCounts = VarCounts {
  - varCounts :: IntMap Int
  }
- class Free t
- class (Singleton MetaId a, Semigroup a, Monoid a, Semigroup c, Monoid c) => IsVarSet a c | c -> a where
  - withVarOcc :: VarOcc' a -> c -> c
- data IgnoreSorts
  - = IgnoreNot
  - | IgnoreInAnnotations
  - | IgnoreAll
- freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c
- freeVars' :: (Free t, IsVarSet a c) => t -> FreeM a c
- filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet
- filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Variable]
- runFree :: (IsVarSet a c, Free t) => SingleVar c -> IgnoreSorts -> t -> c
- rigidVars :: VarMap -> VarSet
- stronglyRigidVars :: VarMap -> VarSet
- unguardedVars :: VarMap -> VarSet
- allVars :: VarMap -> VarSet
- flexibleVars :: VarMap -> IntMap MetaSet
- allFreeVars :: Free t => t -> VarSet
- allRelevantVars :: Free t => t -> VarSet
- allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet
- freeVarsIgnore :: (IsVarSet a c, Singleton Variable c, Free t) => IgnoreSorts -> t -> c
- freeIn :: Free a => Nat -> a -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- isBinderUsed :: Free a => Abs a -> Bool
- relevantIn :: Free t => Nat -> t -> Bool
- relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool
- 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
- isStronglyRigid :: LensFlexRig o a => o -> Bool
- isWeaklyRigid :: LensFlexRig o a => o -> Bool
- data VarOcc' a = VarOcc {
  - varFlexRig :: FlexRig' a
  - varModality :: Modality
  }
- type VarOcc = VarOcc' MetaSet
- varOccurrenceIn :: Free a => Nat -> a -> Maybe VarOcc
- flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe FlexRig
- closed :: Free t => t -> Bool
- data MetaSet
- insertMetaSet :: MetaId -> MetaSet -> MetaSet
- foldrMetaSet :: (MetaId -> a -> a) -> a -> MetaSet -> a
- metaSetToBlocker :: MetaSet -> Blocker

# Documentation

newtype VarCounts Source #

Constructors

VarCounts |

Fields

- varCounts :: IntMap Int

#### Instances

Instances details

Monoid VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods mempty :: VarCounts Source # mappend :: VarCounts -> VarCounts -> VarCounts Source # mconcat :: [VarCounts] -> VarCounts Source #
Semigroup VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods (<>) :: VarCounts -> VarCounts -> VarCounts Source # sconcat :: NonEmpty VarCounts -> VarCounts Source # stimes :: Integral b => b -> VarCounts -> VarCounts Source #
IsVarSet () VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc' () -> VarCounts -> VarCounts Source #
Singleton Variable VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods singleton :: Variable -> VarCounts Source #

class Free t Source #

Gather free variables in a collection.

#### 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 #

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 #

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 #

freeVars :: (IsVarSet a c, Singleton Variable c, Free t) => t -> c Source #

Collect all free variables together with information about their occurrence.

Doesn't go inside solved metas, but collects the variables from a metavariable application `X ts` as `flexibleVars`.

freeVars' :: (Free t, IsVarSet a c) => t -> FreeM a c Source #

filterVarMap :: (VarOcc -> Bool) -> VarMap -> VarSet Source #

filterVarMapToList :: (VarOcc -> Bool) -> VarMap -> [Variable] Source #

runFree :: (IsVarSet a c, Free t) => SingleVar c -> IgnoreSorts -> t -> c Source #

Compute free variables.

rigidVars :: VarMap -> VarSet Source #

Rigid variables: either strongly rigid, unguarded, or weakly rigid.

stronglyRigidVars :: VarMap -> VarSet Source #

Variables under only and at least one inductive constructor(s).

unguardedVars :: VarMap -> VarSet Source #

Variables at top or only under inductive record constructors λs and Πs. The purpose of recording these separately is that they can still become strongly rigid if put under a constructor whereas weakly rigid ones stay weakly rigid.

allVars :: VarMap -> VarSet Source #

flexibleVars :: VarMap -> IntMap MetaSet Source #

Variables occuring in arguments of metas. These are only potentially free, depending how the meta variable is instantiated. The set contains the id's of the meta variables that this variable is an argument to.

allFreeVars :: Free t => t -> VarSet Source #

Collect all free variables.

allRelevantVars :: Free t => t -> VarSet Source #

Collect all relevant free variables, excluding the "unused" ones.

allRelevantVarsIgnoring :: Free t => IgnoreSorts -> t -> VarSet Source #

Collect all relevant free variables, possibly ignoring sorts.

freeVarsIgnore :: (IsVarSet a c, Singleton Variable c, Free t) => IgnoreSorts -> t -> c Source #

freeIn :: Free a => Nat -> a -> Bool Source #

freeInIgnoringSorts :: Free a => Nat -> a -> Bool Source #

isBinderUsed :: Free a => Abs a -> Bool Source #

Is the variable bound by the abstraction actually used?

relevantIn :: Free t => Nat -> t -> Bool Source #

relevantInIgnoringSortAnn :: Free t => Nat -> t -> Bool Source #

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 #

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

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

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 #

varOccurrenceIn :: Free a => Nat -> a -> Maybe VarOcc Source #

Get the full occurrence information of a free variable.

flexRigOccurrenceIn :: Free a => Nat -> a -> Maybe FlexRig Source #

Get the full occurrence information of a free variable.

closed :: Free t => t -> Bool Source #

Is the term entirely closed (no free variables)?

data MetaSet Source #

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

#### 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 #

# Orphan instances

IsVarSet () All Source # |
Instance details Methods withVarOcc :: VarOcc' () -> All -> All Source #
IsVarSet () Any Source # |
Instance details Methods withVarOcc :: VarOcc' () -> Any -> Any Source #
IsVarSet () [Int] Source # |
Instance details Methods withVarOcc :: VarOcc' () -> [Int] -> [Int] Source #