Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




Computing the free variables of a term lazily.

We implement a reduce (traversal into monoid) over internal syntax for a generic collection (monoid with singletons). This should allow a more efficient test for the presence of a particular variable.

Worst-case complexity does not change (i.e. the case when a variable does not occur), but best case-complexity does matter. For instance, see mkAbs: each time we construct a dependent function type, we check it is actually dependent.

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



data FlexRig Source

Depending on the surrounding context of a variable, it's occurrence can be classified as flexible or rigid, with finer distinctions.

The constructors are listed in increasing order (wrt. information content).



In arguments of metas.


In arguments to variables and definitions.


In top position, or only under inductive record constructors.


Under at least one and only inductive constructors.

composeFlexRig :: FlexRig -> FlexRig -> FlexRig Source

FlexRig composition. For accumulating the context of a variable.

Flexible is dominant. Once we are under a meta, we are flexible regardless what else comes.

WeaklyRigid is next in strength. Destroys strong rigidity.

StronglyRigid is still dominant over Unguarded.

Unguarded is the unit. It is the top (identity) context.

data VarOcc Source

Occurrence of free variables is classified by several dimensions. Currently, we have FlexRig and Relevance.



maxVarOcc :: VarOcc -> VarOcc -> VarOcc Source

When we extract information about occurrence, we care most about about StronglyRigid Relevant occurrences.

Collecting free variables.

data IgnoreSorts Source

Where should we skip sorts in free variable analysis?



Do not skip.


Skip when annotation to a type.


Skip unconditionally.

data FreeEnv c Source

The current context.




feIgnoreSorts :: !IgnoreSorts

Ignore free variables in sorts.

feBinders :: !Int

Under how many binders have we stepped?

feFlexRig :: !FlexRig

Are we flexible or rigid?

feRelevance :: !Relevance

What is the current relevance?

feSingleton :: SingleVar c

Method to return a single variable.


type SingleVar c = Variable -> c Source

initFreeEnv :: SingleVar c -> FreeEnv c Source

The initial context.

type FreeM c = Reader (FreeEnv c) c Source

variable :: Monoid c => Int -> FreeM c Source

Base case: a variable.

bind :: FreeM a -> FreeM a Source

Going under a binder.

go :: FlexRig -> FreeM a -> FreeM a Source

Changing the FlexRig context.

goRel :: Relevance -> FreeM a -> FreeM a Source

Changing the Relevance.

underConstructor :: ConHead -> FreeM a -> FreeM a Source

What happens to the variables occurring under a constructor?

class Free' a c where Source

Gather free variables in a collection.


freeVars' :: Monoid c => a -> FreeM c Source


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