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

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

class Free a #

Minimal complete definition

freeVars'

Instances

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

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

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

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

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

allVars :: FreeVars -> VarSet #

allVars fv includes irrelevant variables.

relevantVars :: FreeVars -> VarSet #

All but the irrelevant variables.

rigidVars :: FreeVars -> VarSet #

Rigid variables: either strongly rigid, unguarded, or weakly rigid.

freeIn :: Free a => Nat -> a -> Bool #

isBinderUsed :: Free a => Abs a -> Bool #

Is the variable bound by the abstraction actually used?

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 #

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

occurrence :: Nat -> FreeVars -> Occurrence #