Agda.TypeChecking.Free.Lazy

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

Documentation

data FlexRig

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

Constructors

Flexible [MetaId]

In arguments of metas.

WeaklyRigid

In arguments to variables and definitions.

Unguarded

In top position, or only under inductive record constructors.

StronglyRigid

Under at least one and only inductive constructors.

Instances

Eq FlexRig

Methods

(==) :: FlexRig -> FlexRig -> Bool

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

Ord FlexRig

Methods

compare :: FlexRig -> FlexRig -> Ordering

(<) :: FlexRig -> FlexRig -> Bool

(<=) :: FlexRig -> FlexRig -> Bool

(>) :: FlexRig -> FlexRig -> Bool

(>=) :: FlexRig -> FlexRig -> Bool

max :: FlexRig -> FlexRig -> FlexRig

min :: FlexRig -> FlexRig -> FlexRig

Show FlexRig

Methods

showsPrec :: Int -> FlexRig -> ShowS

show :: FlexRig -> String

showList :: [FlexRig] -> ShowS

Arbitrary FlexRig

Methods

arbitrary :: Gen FlexRig

shrink :: FlexRig -> [FlexRig]

composeFlexRig :: FlexRig -> FlexRig -> FlexRig

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

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

Constructors

VarOcc

Fields

• varFlexRig :: FlexRig
• varRelevance :: Relevance

Instances

Eq VarOcc

Methods

(==) :: VarOcc -> VarOcc -> Bool

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

Show VarOcc

Methods

showsPrec :: Int -> VarOcc -> ShowS

show :: VarOcc -> String

showList :: [VarOcc] -> ShowS

Arbitrary VarOcc

Methods

arbitrary :: Gen VarOcc

shrink :: VarOcc -> [VarOcc]

Singleton Variable FreeVars

Methods

singleton :: Variable -> FreeVars

maxVarOcc :: VarOcc -> VarOcc -> VarOcc

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

topVarOcc :: VarOcc

botVarOcc :: VarOcc

type VarMap = IntMap VarOcc

Collecting free variables.

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

data FreeEnv c

The current context.

Constructors

FreeEnv

Fields

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

Instances

Monoid c => Monoid (FreeM c)

Methods

mempty :: FreeM c

mappend :: FreeM c -> FreeM c -> FreeM c

mconcat :: [FreeM c] -> FreeM c

type Variable = (Int, VarOcc)

type SingleVar c = Variable -> c

initFreeEnv :: SingleVar c -> FreeEnv c

The initial context.

type FreeM c = Reader (FreeEnv c) c

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

Base case: a variable.

bind :: FreeM a -> FreeM a

Going under a binder.

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

Changing the FlexRig context.

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

Changing the Relevance.

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

What happens to the variables occurring under a constructor?

class Free' a c where

Gather free variables in a collection.

Minimal complete definition

freeVars'

Methods

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

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