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

Safe Haskell | None

Agda.TypeChecking.Free

Description

Computing the free variables of a term.

Synopsis

- data FreeVars = FV {
  - stronglyRigidVars :: VarSet
  - weaklyRigidVars :: VarSet
  - flexibleVars :: VarSet
  - irrelevantVars :: VarSet
  - unusedVars :: VarSet
  }
- class Free a
- 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
  - = NoOccurrence
  - | Irrelevantly
  - | StronglyRigid
  - | WeaklyRigid
  - | Flexible
  - | Unused
- occurrence :: Nat -> FreeVars -> Occurrence

# Documentation

data FreeVars

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.

Constructors

FV |
Fields stronglyRigidVars :: VarSet variables at top and under constructors weaklyRigidVars :: VarSet ord. rigid variables, e.g., in arguments of variables flexibleVars :: VarSet variables occuring in arguments of metas. These are potentially free, depending how the meta variable is instantiated. irrelevantVars :: VarSet variables in irrelevant arguments and under a `DontCare`, i.e., in irrelevant positions unusedVars :: VarSet variables in `UnusedArg`uments

class Free a

Instances

Free ClauseBody |
Free LevelAtom |
Free PlusLevel |
Free Level |
Free Sort |
Free Type |
Free Term |
Free a => Free [a] |
Free a => Free (Maybe a) |
Free a => Free (Arg a) |
Free a => Free (Dom a) |
Free a => Free (Tele a) |
Free a => Free (Abs a) |
(Free a, Free b) => Free (a, b) |

freeVars :: Free a => a -> FreeVars

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

allVars :: FreeVars -> VarSet

`allVars fv` includes irrelevant variables.

relevantVars :: FreeVars -> VarSet

All but the irrelevant variables.

rigidVars :: FreeVars -> VarSet

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

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

Is the variable bound by the abstraction actually used?

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

Constructors

NoOccurrence |
Irrelevantly |
StronglyRigid |
WeaklyRigid |
Flexible |
Unused |

Instances

Eq Occurrence |
Show Occurrence |

occurrence :: Nat -> FreeVars -> Occurrence