Agda-2.6.0.1: 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).

Synopsis

- data FreeVars = FV {
  - stronglyRigidVars :: VarSet
  - unguardedVars :: VarSet
  - weaklyRigidVars :: VarSet
  - flexibleVars :: IntMap MetaSet
  - irrelevantVars :: VarSet
  }
- newtype VarCounts = VarCounts {
  - varCounts :: IntMap Int
  }
- class Free a
- class (Semigroup a, Monoid a) => IsVarSet a where
  - withVarOcc :: VarOcc -> a -> a
- data IgnoreSorts
  - = IgnoreNot
  - | IgnoreInAnnotations
  - | IgnoreAll
- runFree :: (IsVarSet c, Free a) => SingleVar c -> IgnoreSorts -> a -> c
- rigidVars :: FreeVars -> VarSet
- relevantVars :: FreeVars -> VarSet
- allVars :: FreeVars -> VarSet
- allFreeVars :: Free a => a -> VarSet
- allFreeVarsWithOcc :: Free a => a -> TheVarMap
- allRelevantVars :: Free a => a -> VarSet
- allRelevantVarsIgnoring :: Free a => IgnoreSorts -> a -> VarSet
- freeIn :: Free a => Nat -> a -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- isBinderUsed :: Free a => Abs a -> Bool
- relevantIn :: Free a => Nat -> a -> Bool
- relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool
- data Occurrence
  - = NoOccurrence
  - | Irrelevantly
  - | StronglyRigid
  - | Unguarded
  - | WeaklyRigid
  - | Flexible MetaSet
- data VarOcc = VarOcc {
  - varFlexRig :: FlexRig
  - varRelevance :: Relevance
  }
- occurrence :: Free a => Nat -> a -> Occurrence
- closed :: Free a => a -> Bool
- freeVars :: (IsVarSet c, Singleton Variable c, Free a) => a -> c
- freeVars' :: (Free a, IsVarSet c) => a -> FreeM c
- type MetaSet = Set MetaId

# Documentation

data FreeVars Source #

Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.

Constructors

FV |

Fields

- stronglyRigidVars :: VarSet

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

- unguardedVars :: VarSet

  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.

- weaklyRigidVars :: VarSet

  Ordinary rigid variables, e.g., in arguments of variables or functions.

- flexibleVars :: IntMap MetaSet

  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.

- irrelevantVars :: VarSet

  Variables in irrelevant arguments and under a `DontCare`, i.e., in irrelevant positions.

Instances

Eq FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods (==) :: FreeVars -> FreeVars -> Bool Source # (/=) :: FreeVars -> FreeVars -> Bool Source #
Show FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods showsPrec :: Int -> FreeVars -> ShowS Source # show :: FreeVars -> String Source # showList :: [FreeVars] -> ShowS Source #
Semigroup FreeVars Source # | Free variable sets form a monoid under `union`.
Instance details Defined in Agda.TypeChecking.Free Methods (<>) :: FreeVars -> FreeVars -> FreeVars Source # sconcat :: NonEmpty FreeVars -> FreeVars Source # stimes :: Integral b => b -> FreeVars -> FreeVars Source #
Monoid FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods mempty :: FreeVars Source # mappend :: FreeVars -> FreeVars -> FreeVars Source # mconcat :: [FreeVars] -> FreeVars Source #
Null FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods empty :: FreeVars Source # null :: FreeVars -> Bool Source #
IsVarSet FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> FreeVars -> FreeVars Source #
Singleton Variable FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods singleton :: Variable -> FreeVars Source #

newtype VarCounts Source #

Constructors

VarCounts |

Fields

- varCounts :: IntMap Int

Instances

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 #
Monoid VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods mempty :: VarCounts Source # mappend :: VarCounts -> VarCounts -> VarCounts Source # mconcat :: [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 a Source #

Gather free variables in a collection.

Minimal complete definition

freeVars'

Instances

Free EqualityView Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => EqualityView -> FreeM c Source #
Free Clause Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Clause -> FreeM c Source #
Free LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => LevelAtom -> FreeM c Source #
Free PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => PlusLevel -> FreeM c Source #
Free Level Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Level -> FreeM c Source #
Free Sort Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Sort -> FreeM c Source #
Free Term Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Term -> FreeM c Source #
Free Candidate Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Candidate -> FreeM c Source #
Free NLPType Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods freeVars' :: IsVarSet c => NLPType -> FreeM c Source #
Free NLPat Source # |
Instance details Defined in Agda.TypeChecking.Rewriting Methods freeVars' :: IsVarSet c => NLPat -> FreeM c Source #
Free DisplayTerm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayTerm -> FreeM c Source #
Free DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayForm -> FreeM c Source #
Free Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Constraint -> FreeM c Source #
Free a => Free [a] Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => [a] -> FreeM c Source #
Free a => Free (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Maybe a -> FreeM c Source #
Free a => Free (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Dom a -> FreeM c Source #
Free a => Free (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Arg a -> FreeM c Source #
Free a => Free (Tele a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Tele a -> FreeM c Source #
Free a => Free (Type' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Type' a -> FreeM c Source #
Free a => Free (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Abs a -> FreeM c Source #
Free a => Free (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => Elim' a -> FreeM c Source #
(Free a, Free b) => Free (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => (a, b) -> FreeM c Source #

class (Semigroup a, Monoid a) => IsVarSet a where Source #

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

Methods

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

Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition ``` withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ```

Instances

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 VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc -> VarMap -> VarMap Source #
IsVarSet VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> VarCounts -> VarCounts Source #
IsVarSet FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> FreeVars -> FreeVars Source #
IsVarSet [Int] Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> [Int] -> [Int] 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

Eq IgnoreSorts Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: IgnoreSorts -> IgnoreSorts -> Bool Source # (/=) :: IgnoreSorts -> IgnoreSorts -> Bool Source #
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 #

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

Compute free variables.

rigidVars :: FreeVars -> VarSet Source #

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

relevantVars :: FreeVars -> VarSet Source #

All but the irrelevant variables.

allVars :: FreeVars -> VarSet Source #

`allVars fv` includes irrelevant variables.

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

Collect all free variables.

allFreeVarsWithOcc :: Free a => a -> TheVarMap Source #

Collect all free variables together with information about their occurrence.

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

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

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

Collect all relevant free variables, possibly ignoring sorts.

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 a => Nat -> a -> Bool Source #

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

data Occurrence Source #

Constructors

NoOccurrence |
Irrelevantly |
StronglyRigid | Under at least one and only inductive constructors.
Unguarded | In top position, or only under inductive record constructors.
WeaklyRigid | In arguments to variables and definitions.
Flexible MetaSet | In arguments of metas.

Instances

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

data VarOcc Source #

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

Constructors

VarOcc |

Fields

- varFlexRig :: FlexRig
- varRelevance :: Relevance

Instances

Eq VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: VarOcc -> VarOcc -> Bool Source # (/=) :: VarOcc -> VarOcc -> Bool Source #
Show VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> VarOcc -> ShowS Source # show :: VarOcc -> String Source # showList :: [VarOcc] -> ShowS Source #
LensRelevance VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getRelevance :: VarOcc -> Relevance Source # setRelevance :: Relevance -> VarOcc -> VarOcc Source # mapRelevance :: (Relevance -> Relevance) -> VarOcc -> VarOcc Source #
Singleton (Variable, VarOcc) VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: (Variable, VarOcc) -> VarMap Source #

occurrence :: Free a => Nat -> a -> Occurrence Source #

Compute an occurrence of a single variable in a piece of internal syntax.

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

Is the term entirely closed (no free variables)?

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

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

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

type MetaSet = Set MetaId 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 #