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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Free.Old

Description

Computing the free variables of a term.

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

- data FreeVars = FV {
  - stronglyRigidVars :: VarSet
  - unguardedVars :: VarSet
  - weaklyRigidVars :: VarSet
  - flexibleVars :: VarSet
  - irrelevantVars :: VarSet
  }
- class Free a
- data IgnoreSorts
  - = IgnoreNot
  - | IgnoreInAnnotations
  - | IgnoreAll
- freeVars :: Free a => a -> FreeVars
- freeVarsIgnore :: Free a => IgnoreSorts -> a -> FreeVars
- allVars :: FreeVars -> VarSet
- relevantVars :: FreeVars -> VarSet
- rigidVars :: FreeVars -> VarSet
- freeIn :: Free a => Nat -> a -> Bool
- isBinderUsed :: Free a => Abs a -> Bool
- freeInIgnoringSorts :: Free a => Nat -> a -> Bool
- freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool
- relevantIn :: Free a => Nat -> a -> Bool
- relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool
- data Occurrence
  - = NoOccurrence
  - | Irrelevantly
  - | StronglyRigid
  - | Unguarded
  - | WeaklyRigid
  - | Flexible
- occurrence :: Nat -> FreeVars -> Occurrence

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

Fields

- stronglyRigidVars :: VarSet

  Variables under only and at least one inductive constructor(s).

- unguardedVars :: VarSet

  Variables 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 :: VarSet

  Ordinary rigid variables, e.g., in arguments of variables.

- flexibleVars :: VarSet

  Variables occuring in arguments of metas. These are only potentially free, depending how the meta variable is instantiated.

- irrelevantVars :: VarSet

  Variables in irrelevant arguments and under a `DontCare`, i.e., in irrelevant positions.

Instances

Eq FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods (==) :: FreeVars -> FreeVars -> Bool Source # (/=) :: FreeVars -> FreeVars -> Bool Source #
Show FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods showsPrec :: Int -> FreeVars -> ShowS Source # show :: FreeVars -> String Source # showList :: [FreeVars] -> ShowS Source #
Semigroup FreeVars Source # | Free variable sets form a monoid under `union`.
Instance details Defined in Agda.TypeChecking.Free.Old Methods (<>) :: FreeVars -> FreeVars -> FreeVars Source # sconcat :: NonEmpty FreeVars -> FreeVars Source # stimes :: Integral b => b -> FreeVars -> FreeVars Source #
Monoid FreeVars Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods mempty :: FreeVars Source # mappend :: FreeVars -> FreeVars -> FreeVars Source # mconcat :: [FreeVars] -> FreeVars Source #

class Free a Source #

Minimal complete definition

freeVars'

Instances

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

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.Old Methods (==) :: IgnoreSorts -> IgnoreSorts -> Bool Source # (/=) :: IgnoreSorts -> IgnoreSorts -> Bool Source #
Show IgnoreSorts Source # |
Instance details Defined in Agda.TypeChecking.Free.Old Methods showsPrec :: Int -> IgnoreSorts -> ShowS Source # show :: IgnoreSorts -> String Source # showList :: [IgnoreSorts] -> ShowS Source #

freeVars :: Free a => a -> FreeVars Source #

Doesn't go inside solved metas, but collects the variables from a metavariable application `X ts` as `flexibleVars`.

freeVarsIgnore :: Free a => IgnoreSorts -> a -> FreeVars Source #

allVars :: FreeVars -> VarSet Source #

`allVars fv` includes irrelevant variables.

relevantVars :: FreeVars -> VarSet Source #

All but the irrelevant variables.

rigidVars :: FreeVars -> VarSet Source #

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?

freeInIgnoringSorts :: Free a => Nat -> a -> Bool Source #

freeInIgnoringSortAnn :: Free a => Nat -> a -> Bool Source #

relevantIn :: Free a => Nat -> a -> Bool Source #

relevantInIgnoringSortAnn :: Free a => Nat -> a -> Bool Source #

data Occurrence 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

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

occurrence :: Nat -> FreeVars -> Occurrence Source #