Safe Haskell | None |
---|---|
Language | Haskell2010 |
Computing the free variables of a term.
This is the old version of 'Free'
, using
IntSet
s for the separate variable categories.
We keep it as a specification.
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 {}
- class Free a
- data IgnoreSorts
- freeVars :: Free a => a -> FreeVars
- freeVarsIgnore :: Free a => IgnoreSorts -> a -> FreeVars
- allVars :: FreeVars -> VarSet
- relevantVars :: FreeVars -> VarSet
- rigidVars :: FreeVars -> VarSet
- freeIn :: Free a => Nat -> a -> Bool
- isBinderUsed :: Free a => Abs a -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool
- relevantIn :: Free a => Nat -> a -> Bool
- relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool
- data Occurrence
- occurrence :: Nat -> FreeVars -> Occurrence
Documentation
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
FV | |
|
freeVars'
Instances
data IgnoreSorts Source #
Where should we skip sorts in free variable analysis?
IgnoreNot | Do not skip. |
IgnoreInAnnotations | Skip when annotation to a type. |
IgnoreAll | Skip unconditionally. |
Instances
Eq IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Old (==) :: IgnoreSorts -> IgnoreSorts -> Bool # (/=) :: IgnoreSorts -> IgnoreSorts -> Bool # | |
Show IgnoreSorts Source # | |
Defined in Agda.TypeChecking.Free.Old showsPrec :: Int -> IgnoreSorts -> ShowS # show :: IgnoreSorts -> String # showList :: [IgnoreSorts] -> ShowS # |
freeVars :: Free a => a -> FreeVars Source #
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
freeVarsIgnore :: Free a => IgnoreSorts -> a -> FreeVars Source #
relevantVars :: FreeVars -> VarSet Source #
All but the irrelevant variables.
rigidVars :: FreeVars -> VarSet Source #
Rigid variables: either strongly rigid, unguarded, or weakly rigid.
isBinderUsed :: Free a => Abs a -> Bool Source #
Is the variable bound by the abstraction actually used?
data Occurrence Source #
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 | In arguments of metas. |
Instances
Eq Occurrence Source # | |
Defined in Agda.TypeChecking.Free.Old (==) :: Occurrence -> Occurrence -> Bool # (/=) :: Occurrence -> Occurrence -> Bool # | |
Show Occurrence Source # | |
Defined in Agda.TypeChecking.Free.Old showsPrec :: Int -> Occurrence -> ShowS # show :: Occurrence -> String # showList :: [Occurrence] -> ShowS # |
occurrence :: Nat -> FreeVars -> Occurrence Source #