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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Free.Lazy

Contents

- Collecting free variables.

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

- type MetaSet = Set MetaId
- data FlexRig
  - = Flexible MetaSet
  - | WeaklyRigid
  - | Unguarded
  - | StronglyRigid
- composeFlexRig :: FlexRig -> FlexRig -> FlexRig
- data VarOcc = VarOcc {
  - varFlexRig :: FlexRig
  - varRelevance :: Relevance
  }
- maxVarOcc :: VarOcc -> VarOcc -> VarOcc
- topVarOcc :: VarOcc
- botVarOcc :: VarOcc
- composeVarOcc :: VarOcc -> VarOcc -> VarOcc
- class (Semigroup a, Monoid a) => IsVarSet a where
  - withVarOcc :: VarOcc -> a -> a
- type TheVarMap = IntMap VarOcc
- newtype VarMap = VarMap {
  - theVarMap :: TheVarMap
  }
- mapVarMap :: (TheVarMap -> TheVarMap) -> VarMap -> VarMap
- data IgnoreSorts
  - = IgnoreNot
  - | IgnoreInAnnotations
  - | IgnoreAll
- data FreeEnv c = FreeEnv {
  - feIgnoreSorts :: !IgnoreSorts
  - feFlexRig :: !FlexRig
  - feRelevance :: !Relevance
  - feSingleton :: Maybe Variable -> c
  }
- type Variable = Int
- type SingleVar c = Variable -> c
- initFreeEnv :: Monoid c => SingleVar c -> FreeEnv c
- type FreeM c = Reader (FreeEnv c) c
- runFreeM :: IsVarSet c => SingleVar c -> IgnoreSorts -> FreeM c -> c
- variable :: IsVarSet c => Int -> FreeM c
- subVar :: Int -> Maybe Variable -> Maybe Variable
- bind :: FreeM a -> FreeM a
- bind' :: Nat -> FreeM a -> FreeM a
- go :: FlexRig -> FreeM a -> FreeM a
- goRel :: Relevance -> FreeM a -> FreeM a
- underConstructor :: ConHead -> FreeM a -> FreeM a
- class Free a where
  - freeVars' :: IsVarSet c => a -> FreeM c

# Documentation

type MetaSet = Set MetaId Source #

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 Source # (/=) :: FlexRig -> FlexRig -> Bool Source #
Ord FlexRig Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods compare :: FlexRig -> FlexRig -> Ordering Source # (<) :: FlexRig -> FlexRig -> Bool Source # (<=) :: FlexRig -> FlexRig -> Bool Source # (>) :: FlexRig -> FlexRig -> Bool Source # (>=) :: FlexRig -> FlexRig -> Bool Source # max :: FlexRig -> FlexRig -> FlexRig Source # min :: FlexRig -> FlexRig -> FlexRig Source #
Show FlexRig Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> FlexRig -> ShowS Source # show :: FlexRig -> String Source # showList :: [FlexRig] -> ShowS Source #

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 |

Fields

- varFlexRig :: FlexRig
- varRelevance :: Relevance

Instances

Eq VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: VarOcc -> VarOcc -> Bool Source # (/=) :: VarOcc -> VarOcc -> Bool Source #
Show VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> VarOcc -> ShowS Source # show :: VarOcc -> String Source # showList :: [VarOcc] -> ShowS Source #
LensRelevance VarOcc Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods getRelevance :: VarOcc -> Relevance Source # setRelevance :: Relevance -> VarOcc -> VarOcc Source # mapRelevance :: (Relevance -> Relevance) -> VarOcc -> VarOcc Source #
Singleton (Variable, VarOcc) VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: (Variable, VarOcc) -> VarMap Source #

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

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

topVarOcc :: VarOcc Source #

botVarOcc :: VarOcc Source #

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 Methods withVarOcc :: VarOcc -> VarMap -> VarMap Source #
IsVarSet VarCounts Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> VarCounts -> VarCounts Source #
IsVarSet FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> FreeVars -> FreeVars Source #
IsVarSet [Int] Source # |
Instance details Defined in Agda.TypeChecking.Free Methods withVarOcc :: VarOcc -> [Int] -> [Int] Source #

type TheVarMap = IntMap VarOcc Source #

newtype VarMap Source #

Constructors

VarMap |

Fields

- theVarMap :: TheVarMap

Instances

Show VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> VarMap -> ShowS Source # show :: VarMap -> String Source # showList :: [VarMap] -> ShowS Source #
Semigroup VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: VarMap -> VarMap -> VarMap Source # sconcat :: NonEmpty VarMap -> VarMap Source # stimes :: Integral b => b -> VarMap -> VarMap Source #
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 Methods mempty :: VarMap Source # mappend :: VarMap -> VarMap -> VarMap Source # mconcat :: [VarMap] -> VarMap Source #
IsVarSet VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods withVarOcc :: VarOcc -> VarMap -> VarMap Source #
Singleton (Variable, VarOcc) VarMap Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods singleton :: (Variable, VarOcc) -> VarMap Source #

mapVarMap :: (TheVarMap -> TheVarMap) -> VarMap -> VarMap Source #

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

Instances

Eq IgnoreSorts Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (==) :: IgnoreSorts -> IgnoreSorts -> Bool Source # (/=) :: IgnoreSorts -> IgnoreSorts -> Bool Source #
Show IgnoreSorts Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods showsPrec :: Int -> IgnoreSorts -> ShowS Source # show :: IgnoreSorts -> String Source # showList :: [IgnoreSorts] -> ShowS Source #

data FreeEnv c Source #

The current context.

Constructors

FreeEnv |

Fields

- feIgnoreSorts :: !IgnoreSorts

  Ignore free variables in sorts.

- feFlexRig :: !FlexRig

  Are we flexible or rigid?

- feRelevance :: !Relevance

  What is the current relevance?

- feSingleton :: Maybe Variable -> c

  Method to return a single variable.

Instances

Semigroup c => Semigroup (FreeM c) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods (<>) :: FreeM c -> FreeM c -> FreeM c Source # sconcat :: NonEmpty (FreeM c) -> FreeM c Source # stimes :: Integral b => b -> FreeM c -> FreeM c Source #
(Semigroup c, Monoid c) => Monoid (FreeM c) Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods mempty :: FreeM c Source # mappend :: FreeM c -> FreeM c -> FreeM c Source # mconcat :: [FreeM c] -> FreeM c Source #

type Variable = Int Source #

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 Methods freeVars' :: IsVarSet c => EqualityView -> FreeM c Source #
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 Methods freeVars' :: IsVarSet c => LevelAtom -> FreeM c Source #
Free PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Free.Lazy Methods freeVars' :: IsVarSet c => PlusLevel -> FreeM c Source #
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 Methods freeVars' :: IsVarSet c => Candidate -> FreeM c Source #
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 Methods freeVars' :: IsVarSet c => DisplayTerm -> FreeM c Source #
Free DisplayForm Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => DisplayForm -> FreeM c Source #
Free Constraint Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods freeVars' :: IsVarSet c => Constraint -> FreeM c Source #
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 #