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

Documentation

data FreeVars #

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.
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.
unusedVars :: VarSet
Variables in UnusedArguments.

Instances

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

class Free a where #

Gather free variables in a collection.

Minimal complete definition

freeVars'

Methods

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

Instances

Free EqualityView #
Methods freeVars' :: IsVarSet c => EqualityView -> FreeM c #
Free Clause #
Methods freeVars' :: IsVarSet c => Clause -> FreeM c #
Free LevelAtom #
Methods freeVars' :: IsVarSet c => LevelAtom -> FreeM c #
Free PlusLevel #
Methods freeVars' :: IsVarSet c => PlusLevel -> FreeM c #
Free Level #
Methods freeVars' :: IsVarSet c => Level -> FreeM c #
Free Sort #
Methods freeVars' :: IsVarSet c => Sort -> FreeM c #
Free Term #
Methods freeVars' :: IsVarSet c => Term -> FreeM c #
Free Candidate #
Methods freeVars' :: IsVarSet c => Candidate -> FreeM c #
Free DisplayTerm #
Methods freeVars' :: IsVarSet c => DisplayTerm -> FreeM c #
Free DisplayForm #
Methods freeVars' :: IsVarSet c => DisplayForm -> FreeM c #
Free Constraint #
Methods freeVars' :: IsVarSet c => Constraint -> FreeM c #
Free a => Free [a] #
Methods freeVars' :: IsVarSet c => [a] -> FreeM c #
Free a => Free (Maybe a) #
Methods freeVars' :: IsVarSet c => Maybe a -> FreeM c #
Free a => Free (Dom a) #
Methods freeVars' :: IsVarSet c => Dom a -> FreeM c #
Free a => Free (Arg a) #
Methods freeVars' :: IsVarSet c => Arg a -> FreeM c #
Free a => Free (Tele a) #
Methods freeVars' :: IsVarSet c => Tele a -> FreeM c #
Free a => Free (Type' a) #
Methods freeVars' :: IsVarSet c => Type' a -> FreeM c #
Free a => Free (Abs a) #
Methods freeVars' :: IsVarSet c => Abs a -> FreeM c #
Free a => Free (Elim' a) #
Methods freeVars' :: IsVarSet c => Elim' a -> FreeM c #
(Free a, Free b) => Free (a, b) #
Methods freeVars' :: IsVarSet c => (a, b) -> FreeM c #

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

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

Minimal complete definition

withVarOcc

Methods

withVarOcc :: VarOcc -> a -> a #

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 VarMap #
Methods withVarOcc :: VarOcc -> VarMap -> VarMap #
IsVarSet FreeVars #
Methods withVarOcc :: VarOcc -> FreeVars -> FreeVars #

data IgnoreSorts #

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 #
Methods (==) :: IgnoreSorts -> IgnoreSorts -> Bool # (/=) :: IgnoreSorts -> IgnoreSorts -> Bool #
Show IgnoreSorts #
Methods showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS #

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

Compute free variables.

rigidVars :: FreeVars -> VarSet #

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

relevantVars :: FreeVars -> VarSet #

All but the irrelevant variables.

allVars :: FreeVars -> VarSet #

allVars fv includes irrelevant variables.

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

Collect all free variables.

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

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

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

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

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

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

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

Is the variable bound by the abstraction actually used?

relevantIn :: Free a => Nat -> a -> Bool #

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

data Occurrence #

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

Instances

Eq Occurrence #
Methods (==) :: Occurrence -> Occurrence -> Bool # (/=) :: Occurrence -> Occurrence -> Bool #
Show Occurrence #
Methods showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS #

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

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

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

Is the term entirely closed (no free variables)?

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

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 #

Orphan instances

IsVarSet All #
Methods withVarOcc :: VarOcc -> All -> All #
IsVarSet Any #
Methods withVarOcc :: VarOcc -> Any -> Any #
IsVarSet [Int] #
Methods withVarOcc :: VarOcc -> [Int] -> [Int] #