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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Free.Lazy

Contents

Description

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

Synopsis

Documentation

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

Constructors

Flexible MetaSet

In arguments of metas. The set of metas is used by 'NonLinMatch' to generate the right blocking information.

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 Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

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

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

Ord FlexRig Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Show FlexRig Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

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.

Constructors

VarOcc 

maxVarOcc :: VarOcc -> VarOcc -> VarOcc Source #

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

composeVarOcc :: VarOcc -> VarOcc -> VarOcc Source #

First argument is the outer occurrence and second is the inner.

class (Semigroup a, Monoid a) => IsVarSet a where Source #

Any representation of a set of variables need to be able to be modified by a variable occurrence. This is to ensure that free variable analysis is compositional. For instance, it should be possible to compute `fv (v [u/x])` from `fv v` and `fv u`.

Methods

withVarOcc :: VarOcc -> a -> a Source #

Laws * Respects monoid operations: ``` withVarOcc o mempty == mempty withVarOcc o (x <> y) == withVarOcc o x <> withVarOcc o y ``` * Respects VarOcc composition ``` withVarOcc (composeVarOcc o1 o2) = withVarOcc o1 . withVarOcc o2 ```

Instances
IsVarSet All Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc -> All -> All Source #

IsVarSet Any Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc -> Any -> Any Source #

IsVarSet VarMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

IsVarSet VarCounts Source # 
Instance details

Defined in Agda.TypeChecking.Free

IsVarSet FreeVars Source # 
Instance details

Defined in Agda.TypeChecking.Free

IsVarSet [Int] Source # 
Instance details

Defined in Agda.TypeChecking.Free

Methods

withVarOcc :: VarOcc -> [Int] -> [Int] Source #

newtype VarMap Source #

Constructors

VarMap 

Fields

Instances
Show VarMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Semigroup VarMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Monoid VarMap Source #

Proper monoid instance for VarMap rather than inheriting the broken one from IntMap. We combine two occurrences of a variable using maxVarOcc.

Instance details

Defined in Agda.TypeChecking.Free.Lazy

IsVarSet VarMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Singleton (Variable, VarOcc) VarMap Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Collecting free variables.

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.

data FreeEnv c Source #

The current context.

Constructors

FreeEnv 

Fields

Instances
Semigroup c => Semigroup (FreeM c) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

(<>) :: FreeM c -> FreeM c -> FreeM c #

sconcat :: NonEmpty (FreeM c) -> FreeM c #

stimes :: Integral b => b -> FreeM c -> FreeM c #

(Semigroup c, Monoid c) => Monoid (FreeM c) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

mempty :: FreeM c #

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

mconcat :: [FreeM c] -> FreeM c #

type SingleVar c = Variable -> c Source #

initFreeEnv :: Monoid c => SingleVar c -> FreeEnv c Source #

The initial context.

type FreeM c = Reader (FreeEnv c) c Source #

runFreeM :: IsVarSet c => SingleVar c -> IgnoreSorts -> FreeM c -> c Source #

Run function for FreeM.

variable :: IsVarSet c => Int -> FreeM c Source #

Base case: a variable.

subVar :: Int -> Maybe Variable -> Maybe Variable Source #

Subtract, but return Nothing if result is negative.

bind :: FreeM a -> FreeM a Source #

Going under a binder.

bind' :: Nat -> FreeM a -> FreeM a Source #

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 where Source #

Gather free variables in a collection.

Methods

freeVars' :: IsVarSet c => a -> FreeM c Source #

Instances
Free EqualityView Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Free Clause Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Clause -> FreeM c Source #

Free LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Free PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Free Level Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Level -> FreeM c Source #

Free Sort Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Sort -> FreeM c Source #

Free Term Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Term -> FreeM c Source #

Free Candidate Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free NLPType Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Methods

freeVars' :: IsVarSet c => NLPType -> FreeM c Source #

Free NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting

Methods

freeVars' :: IsVarSet c => NLPat -> FreeM c Source #

Free DisplayTerm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free DisplayForm Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free Constraint Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Base

Free a => Free [a] Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => [a] -> FreeM c Source #

Free a => Free (Maybe a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Maybe a -> FreeM c Source #

Free a => Free (Dom a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Dom a -> FreeM c Source #

Free a => Free (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Arg a -> FreeM c Source #

Free a => Free (Tele a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Tele a -> FreeM c Source #

Free a => Free (Type' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Type' a -> FreeM c Source #

Free a => Free (Abs a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Abs a -> FreeM c Source #

Free a => Free (Elim' a) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => Elim' a -> FreeM c Source #

(Free a, Free b) => Free (a, b) Source # 
Instance details

Defined in Agda.TypeChecking.Free.Lazy

Methods

freeVars' :: IsVarSet c => (a, b) -> FreeM c Source #