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

Agda.TypeChecking.Free.Old

Description

Computing the free variables of a term.

This is the old version of 'Free', using IntSets 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

# 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 FieldsstronglyRigidVars :: VarSetVariables under only and at least one inductive constructor(s).unguardedVars :: VarSetVariables 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 :: VarSetOrdinary rigid variables, e.g., in arguments of variables.flexibleVars :: VarSetVariables occuring in arguments of metas. These are only potentially free, depending how the meta variable is instantiated.irrelevantVars :: VarSetVariables in irrelevant arguments and under a DontCare, i.e., in irrelevant positions.
Instances
 Source # Instance detailsDefined in Agda.TypeChecking.Free.Old Methods Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsshowList :: [FreeVars] -> ShowS # Source # Free variable sets form a monoid under union. Instance detailsDefined in Agda.TypeChecking.Free.Old Methodsstimes :: Integral b => b -> FreeVars -> FreeVars # Source # Instance detailsDefined in Agda.TypeChecking.Free.Old Methodsmconcat :: [FreeVars] -> FreeVars #

class Free a Source #

Minimal complete definition

freeVars'

Instances
 Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Clause -> FreeT Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: LevelAtom -> FreeT Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: PlusLevel -> FreeT Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Level -> FreeT Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Sort -> FreeT Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Type -> FreeT Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Term -> FreeT Free a => Free [a] Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: [a] -> FreeT Free a => Free (Maybe a) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Maybe a -> FreeT Free a => Free (Dom a) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Dom a -> FreeT Free a => Free (Arg a) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Arg a -> FreeT Free a => Free (Tele a) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Tele a -> FreeT Free a => Free (Abs a) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Abs a -> FreeT Free a => Free (Elim' a) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: Elim' a -> FreeT (Free a, Free b) => Free (a, b) Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsfreeVars' :: (a, b) -> FreeT

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
 Source # Instance detailsDefined in Agda.TypeChecking.Free.Old Methods Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsshowList :: [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.

allVars fv includes irrelevant variables.

All but the irrelevant variables.

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?

relevantIn :: Free a => Nat -> a -> Bool 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.
Instances
 Source # Instance detailsDefined in Agda.TypeChecking.Free.Old Methods Source # Instance detailsDefined in Agda.TypeChecking.Free.Old MethodsshowList :: [Occurrence] -> ShowS #