Safe Haskell | None |
---|---|
Language | Haskell98 |
Computing the free variables of a term.
- data FreeVars = FV {}
- class Free a where
- data FreeConf = FreeConf {}
- data IgnoreSorts
- freeVars :: Free a => 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
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
Free variables of a term, (disjointly) partitioned into strongly and and weakly rigid variables, flexible variables and irrelevant variables.
FV | |
|
FreeConf | |
|
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. |
freeVars :: Free a => a -> FreeVars Source
Doesn't go inside solved metas, but collects the variables from a
metavariable application X ts
as flexibleVars
.
relevantVars :: FreeVars -> VarSet Source
All but the irrelevant variables.
isBinderUsed :: Free a => Abs a -> Bool Source
Is the variable bound by the abstraction actually used?
freeInIgnoringSorts :: Free a => Nat -> a -> Bool Source
freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool Source
relevantIn :: Free a => Nat -> a -> Bool Source
relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool Source
data Occurrence Source
occurrence :: Nat -> FreeVars -> Occurrence Source