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

Safe Haskell | None

Agda.TypeChecking.MetaVars.Occurs

Contents

- Getting rid of flexible occurrences

Synopsis

- modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()
- initOccursCheck :: MetaVariable -> TCM ()
- defNeedsChecking :: QName -> TCM Bool
- tallyDef :: QName -> TCM ()
- data OccursCtx
  - = Flex
  - | Rigid
  - | StronglyRigid
  - | Top
  - | Irrel
- data UnfoldStrategy
  - = YesUnfold
  - | NoUnfold
- defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx
- unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)
- leaveTop :: OccursCtx -> OccursCtx
- weakly :: OccursCtx -> OccursCtx
- strongly :: OccursCtx -> OccursCtx
- abort :: OccursCtx -> TypeError -> TCM a
- type Vars = ([Nat], [Nat])
- goIrrelevant :: Vars -> Vars
- allowedVar :: Nat -> Vars -> Bool
- takeRelevant :: Vars -> [Nat]
- liftUnderAbs :: Vars -> Vars
- class Occurs t where
  - occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t
  - metaOccurs :: MetaId -> t -> TCM ()
- occursCheck :: MetaId -> Vars -> Term -> TCM Term
- prune :: MetaId -> Args -> [Nat] -> TCM PruneResult
- hasBadRigid :: [Nat] -> Term -> TCM Bool
- rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool
- data PruneResult
  - = NothingToPrune
  - | PrunedNothing
  - | PrunedSomething
  - | PrunedEverything
- killArgs :: [Bool] -> MetaId -> TCM PruneResult
- killedType :: [(Dom (String, Type), Bool)] -> Type -> ([Arg Bool], Type)
- performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()

# Documentation

modifyOccursCheckDefs :: (Set QName -> Set QName) -> TCM ()

initOccursCheck :: MetaVariable -> TCM ()

Set the names of definitions to be looked at to the defs in the current mutual block.

defNeedsChecking :: QName -> TCM Bool

Is a def in the list of stuff to be checked?

tallyDef :: QName -> TCM ()

Remove a def from the list of defs to be looked at.

data OccursCtx

Constructors

Flex | we are in arguments of a meta
Rigid | we are not in arguments of a meta but a bound var
StronglyRigid | we are at the start or in the arguments of a constructor
Top | we are at the term root (this turns into `StronglyRigid`)
Irrel | we are in an irrelevant argument

Instances

Eq OccursCtx |
Show OccursCtx |

data UnfoldStrategy

Constructors

YesUnfold |
NoUnfold |

Instances

Eq UnfoldStrategy |
Show UnfoldStrategy |

defArgs :: UnfoldStrategy -> OccursCtx -> OccursCtx

unfold :: UnfoldStrategy -> Term -> TCM (Blocked Term)

leaveTop :: OccursCtx -> OccursCtx

Leave the top position.

weakly :: OccursCtx -> OccursCtx

Leave the strongly rigid position.

strongly :: OccursCtx -> OccursCtx

abort :: OccursCtx -> TypeError -> TCM a

type Vars = ([Nat], [Nat])

Distinguish relevant and irrelevant variables in occurs check.

goIrrelevant :: Vars -> Vars

allowedVar :: Nat -> Vars -> Bool

takeRelevant :: Vars -> [Nat]

liftUnderAbs :: Vars -> Vars

class Occurs t where

Extended occurs check.

Methods

occurs :: UnfoldStrategy -> OccursCtx -> MetaId -> Vars -> t -> TCM t

metaOccurs :: MetaId -> t -> TCM ()

Instances

Occurs QName |
Occurs Clause |
Occurs LevelAtom |
Occurs PlusLevel |
Occurs Level |
Occurs Sort |
Occurs Type |
Occurs Term |
Occurs Defn |
Occurs a => Occurs [a] |
Occurs a => Occurs (Arg a) |
Occurs a => Occurs (Dom a) |
(Occurs a, Subst a) => Occurs (Abs a) |
(Occurs a, Occurs b) => Occurs (a, b) |

occursCheck :: MetaId -> Vars -> Term -> TCM Term

When assigning `m xs := v`, check that `m` does not occur in `v` and that the free variables of `v` are contained in `xs`.

# Getting rid of flexible occurrences

prune :: MetaId -> Args -> [Nat] -> TCM PruneResult

`prune m' vs xs` attempts to remove all arguments from `vs` whose free variables are not contained in `xs`. If successful, `m'` is solved by the new, pruned meta variable and we return `True` else `False`.

hasBadRigid :: [Nat] -> Term -> TCM Bool

`hasBadRigid xs v = True` iff one of the rigid variables in `v` is not in `xs`. Actually we can only prune if a bad variable is in the head. See issue 458. Or in a non-eliminateable position (see succeed/PruningNonMillerPattern).

rigidVarsNotContainedIn :: Free a => a -> [Nat] -> Bool

data PruneResult

Constructors

NothingToPrune | the kill list is empty or only `False`s
PrunedNothing | there is no possible kill (because of type dep.)
PrunedSomething | managed to kill some args in the list
PrunedEverything | all prescribed kills where performed

Instances

Eq PruneResult |
Show PruneResult |

killArgs :: [Bool] -> MetaId -> TCM PruneResult

`killArgs [k1,...,kn] X` prunes argument `i` from metavar `X` if `ki==True`. Pruning is carried out whenever > 0 arguments can be pruned. `True` is only returned if all arguments could be pruned.

killedType :: [(Dom (String, Type), Bool)] -> Type -> ([Arg Bool], Type)

`killedType [((x1,a1),k1)..((xn,an),kn)] b = ([k'1..k'n],t')` (ignoring `Dom`). Let `t' = (xs:as) -> b`. Invariant: `k'i == True` iff `ki == True` and pruning the `i`th argument from type `b` is possible without creating unbound variables. `t'` is type `t` after pruning all `k'i==True`.

performKill :: [Arg Bool] -> MetaId -> Type -> TCM ()