Agda.TypeChecking.Free

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

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 [MetaId]

  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

Eq FreeVars

Methods

(==) :: FreeVars -> FreeVars -> Bool

(/=) :: FreeVars -> FreeVars -> Bool

Show FreeVars

Methods

showsPrec :: Int -> FreeVars -> ShowS

show :: FreeVars -> String

showList :: [FreeVars] -> ShowS

Monoid FreeVars

Free variable sets form a monoid under union.

Methods

mempty :: FreeVars

mappend :: FreeVars -> FreeVars -> FreeVars

mconcat :: [FreeVars] -> FreeVars

Null FreeVars

Methods

empty :: FreeVars

null :: FreeVars -> Bool

Singleton Variable FreeVars

Methods

singleton :: Variable -> FreeVars

type Free a = Free' a Any

class Free' a c

Gather free variables in a collection.

Minimal complete definition

freeVars'

Instances

Free' EqualityView c

Methods

freeVars' :: EqualityView -> FreeM c

Free' ClauseBody c

Methods

freeVars' :: ClauseBody -> FreeM c

Free' Clause c

Methods

freeVars' :: Clause -> FreeM c

Free' LevelAtom c

Methods

freeVars' :: LevelAtom -> FreeM c

Free' PlusLevel c

Methods

freeVars' :: PlusLevel -> FreeM c

Free' Level c

Methods

freeVars' :: Level -> FreeM c

Free' Sort c

Methods

freeVars' :: Sort -> FreeM c

Free' Type c

Methods

freeVars' :: Type -> FreeM c

Free' Term c

Methods

freeVars' :: Term -> FreeM c

Free' a c => Free' [a] c

Methods

freeVars' :: [a] -> FreeM c

Free' a c => Free' (Maybe a) c

Methods

freeVars' :: Maybe a -> FreeM c

Free' a c => Free' (Dom a) c

Methods

freeVars' :: Dom a -> FreeM c

Free' a c => Free' (Arg a) c

Methods

freeVars' :: Arg a -> FreeM c

Free' a c => Free' (Tele a) c

Methods

freeVars' :: Tele a -> FreeM c

Free' a c => Free' (Abs a) c

Methods

freeVars' :: Abs a -> FreeM c

Free' a c => Free' (Elim' a) c

Methods

freeVars' :: Elim' a -> FreeM c

(Free' a c, Free' b c) => Free' (a, b) c

Methods

freeVars' :: (a, b) -> FreeM c

type FreeV a = Free' a FreeVars

type FreeVS a = Free' a VarSet

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 :: (Monoid c, Free' a c) => SingleVar c -> IgnoreSorts -> a -> c

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 VarSet => a -> VarSet

Collect all free variables.

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

Collect all relevant free variables.

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

Collect all relevant free variables, 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 [MetaId]

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 :: FreeV a => Nat -> a -> Occurrence

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

closed :: Free' a All => a -> Bool

Is the term entirely closed (no free variables)?

freeVars :: (Monoid c, Singleton Variable c, Free' a c) => a -> c

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