Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Free

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 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.
flexibleVars :: VarSet: Variables occuring in arguments of metas. These are only 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 UnusedArguments.

Instances

Monoid FreeVars

Free variable sets form a monoid under union.

class Free a Source

Minimal complete definition

freeVars'

Instances

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

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
Show IgnoreSorts

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

allVars :: FreeVars -> VarSet Source

allVars fv includes irrelevant variables.

relevantVars :: FreeVars -> VarSet Source

All but the irrelevant variables.

rigidVars :: FreeVars -> VarSet Source

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

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

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

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	In arguments of metas.
Unused

Instances

Eq Occurrence
Show Occurrence

occurrence :: Nat -> FreeVars -> Occurrence Source