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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Conversion

Contents

- Types
- Sorts and levels
- Definitions

Synopsis

- type MonadConversion m = (PureTCM m, MonadConstraint m, MonadMetaSolver m, MonadError TCErr m, MonadWarning m, MonadStatistics m, MonadFresh ProblemId m, MonadFresh Int m, MonadFail m)
- tryConversion :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m () -> m Bool
- tryConversion' :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m a -> m (Maybe a)
- sameVars :: Elims -> Elims -> Bool
- intersectVars :: Elims -> Elims -> Maybe [Bool]
- blockOnError :: MonadError TCErr m => Blocker -> m a -> m a
- equalTerm :: MonadConversion m => Type -> Term -> Term -> m ()
- equalAtom :: MonadConversion m => CompareAs -> Term -> Term -> m ()
- equalType :: MonadConversion m => Type -> Type -> m ()
- convError :: TypeError -> TCM ()
- compareTerm :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
- compareAs :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
- assignE :: MonadConversion m => CompareDirection -> MetaId -> Elims -> Term -> CompareAs -> (Term -> Term -> m ()) -> m ()
- compareAsDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
- compareAs' :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
- compareTerm' :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
- compareAtomDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m ()
- computeElimHeadType :: MonadConversion m => QName -> Elims -> Elims -> m Type
- compareAtom :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m ()
- compareDom :: (MonadConversion m, Free c) => Comparison -> Dom Type -> Dom Type -> Abs b -> Abs c -> m () -> m () -> m () -> m () -> m () -> m ()
- compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
- compareQuantity :: Comparison -> Quantity -> Quantity -> Bool
- compareCohesion :: Comparison -> Cohesion -> Cohesion -> Bool
- antiUnify :: MonadConversion m => ProblemId -> Type -> Term -> Term -> m Term
- antiUnifyArgs :: MonadConversion m => ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term)
- antiUnifyType :: MonadConversion m => ProblemId -> Type -> Type -> m Type
- antiUnifyElims :: MonadConversion m => ProblemId -> Type -> Term -> Elims -> Elims -> m Term
- compareElims :: forall m. MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> m ()
- compareIrrelevant :: MonadConversion m => Type -> Term -> Term -> m ()
- compareWithPol :: MonadConversion m => Polarity -> (Comparison -> a -> a -> m ()) -> a -> a -> m ()
- polFromCmp :: Comparison -> Polarity
- compareArgs :: MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> m ()
- compareType :: MonadConversion m => Comparison -> Type -> Type -> m ()
- leqType :: MonadConversion m => Type -> Type -> m ()
- coerce :: (MonadConversion m, MonadTCM m) => Comparison -> Term -> Type -> Type -> m Term
- coerceSize :: MonadConversion m => (Type -> Type -> m ()) -> Term -> Type -> Type -> m ()
- compareLevel :: MonadConversion m => Comparison -> Level -> Level -> m ()
- compareSort :: MonadConversion m => Comparison -> Sort -> Sort -> m ()
- leqSort :: forall m. MonadConversion m => Sort -> Sort -> m ()
- leqLevel :: MonadConversion m => Level -> Level -> m ()
- equalLevel :: forall m. MonadConversion m => Level -> Level -> m ()
- equalSort :: forall m. MonadConversion m => Sort -> Sort -> m ()
- forallFaceMaps :: MonadConversion m => Term -> (Map Int Bool -> Blocker -> Term -> m a) -> (Substitution -> m a) -> m [a]
- compareInterval :: MonadConversion m => Comparison -> Type -> Term -> Term -> m ()
- type Conj = (Map Int (Set Bool), [Term])
- isCanonical :: [Conj] -> Bool
- leqInterval :: MonadConversion m => [Conj] -> [Conj] -> m Bool
- leqConj :: MonadConversion m => Conj -> Conj -> m Bool
- equalTermOnFace :: MonadConversion m => Term -> Type -> Term -> Term -> m ()
- compareTermOnFace :: MonadConversion m => Comparison -> Term -> Type -> Term -> Term -> m ()
- compareTermOnFace' :: MonadConversion m => (Comparison -> Type -> Term -> Term -> m ()) -> Comparison -> Term -> Type -> Term -> Term -> m ()
- bothAbsurd :: MonadConversion m => QName -> QName -> m Bool

# Documentation

type MonadConversion m = (PureTCM m, MonadConstraint m, MonadMetaSolver m, MonadError TCErr m, MonadWarning m, MonadStatistics m, MonadFresh ProblemId m, MonadFresh Int m, MonadFail m) Source #

tryConversion :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m () -> m Bool Source #

Try whether a computation runs without errors or new constraints (may create new metas, though). Restores state upon failure.

tryConversion' :: (MonadConstraint m, MonadWarning m, MonadError TCErr m, MonadFresh ProblemId m) => m a -> m (Maybe a) Source #

Try whether a computation runs without errors or new constraints (may create new metas, though). Return `Just` the result upon success. Return `Nothing` and restore state upon failure.

sameVars :: Elims -> Elims -> Bool Source #

Check if to lists of arguments are the same (and all variables). Precondition: the lists have the same length.

intersectVars :: Elims -> Elims -> Maybe [Bool] Source #

`intersectVars us vs` checks whether all relevant elements in `us` and `vs` are variables, and if yes, returns a prune list which says `True` for arguments which are different and can be pruned.

blockOnError :: MonadError TCErr m => Blocker -> m a -> m a Source #

Run the given computation but turn any errors into blocked computations with the given blocker

equalTerm :: MonadConversion m => Type -> Term -> Term -> m () Source #

equalAtom :: MonadConversion m => CompareAs -> Term -> Term -> m () Source #

equalType :: MonadConversion m => Type -> Type -> m () Source #

convError :: TypeError -> TCM () Source #

Ignore errors in irrelevant context.

compareTerm :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m () Source #

Type directed equality on values.

compareAs :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m () Source #

Type directed equality on terms or types.

assignE :: MonadConversion m => CompareDirection -> MetaId -> Elims -> Term -> CompareAs -> (Term -> Term -> m ()) -> m () Source #

Try to assign meta. If meta is projected, try to eta-expand and run conversion check again.

compareAsDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m () Source #

compareAs' :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m () Source #

compareTerm' :: forall m. MonadConversion m => Comparison -> Type -> Term -> Term -> m () Source #

compareAtomDir :: MonadConversion m => CompareDirection -> CompareAs -> Term -> Term -> m () Source #

computeElimHeadType :: MonadConversion m => QName -> Elims -> Elims -> m Type Source #

Compute the head type of an elimination. For projection-like functions this requires inferring the type of the principal argument.

compareAtom :: forall m. MonadConversion m => Comparison -> CompareAs -> Term -> Term -> m () Source #

Syntax directed equality on atomic values

compareDom Source #

Arguments

:: (MonadConversion m, Free c) |
=> Comparison | `cmp` The comparison direction
-> Dom Type | `a1` The smaller domain.
-> Dom Type | `a2` The other domain.
-> Abs b | `b1` The smaller codomain.
-> Abs c | `b2` The bigger codomain.
-> m () | Continuation if mismatch in `Hiding`.
-> m () | Continuation if mismatch in `Relevance`.
-> m () | Continuation if mismatch in `Quantity`.
-> m () | Continuation if mismatch in `Cohesion`.
-> m () | Continuation if comparison is successful.
-> m () |

Check whether `a1 `cmp` a2` and continue in context extended by `a1`.

compareRelevance :: Comparison -> Relevance -> Relevance -> Bool Source #

compareQuantity :: Comparison -> Quantity -> Quantity -> Bool Source #

compareCohesion :: Comparison -> Cohesion -> Cohesion -> Bool Source #

antiUnify :: MonadConversion m => ProblemId -> Type -> Term -> Term -> m Term Source #

When comparing argument spines (in compareElims) where the first arguments don't match, we keep going, substituting the anti-unification of the two terms in the telescope. More precisely:

@`(u = v : A)[pid] w = antiUnify pid A u v us = vs : Δ[w/x] ------------------------------------------------------------- u us = v vs : (x : A) Δ` @

The simplest case of anti-unification is to return a fresh metavariable (created by blockTermOnProblem), but if there's shared structure between the two terms we can expose that.

This is really a crutch that lets us get away with things that otherwise would require heterogenous conversion checking. See for instance issue #2384.

antiUnifyArgs :: MonadConversion m => ProblemId -> Dom Type -> Arg Term -> Arg Term -> m (Arg Term) Source #

antiUnifyType :: MonadConversion m => ProblemId -> Type -> Type -> m Type Source #

antiUnifyElims :: MonadConversion m => ProblemId -> Type -> Term -> Elims -> Elims -> m Term Source #

compareElims :: forall m. MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> m () Source #

`compareElims pols a v els1 els2` performs type-directed equality on eliminator spines. `t` is the type of the head `v`.

compareIrrelevant :: MonadConversion m => Type -> Term -> Term -> m () Source #

Compare two terms in irrelevant position. This always succeeds. However, we can dig for solutions of irrelevant metas in the terms we compare. (Certainly not the systematic solution, that'd be proof search...)

compareWithPol :: MonadConversion m => Polarity -> (Comparison -> a -> a -> m ()) -> a -> a -> m () Source #

polFromCmp :: Comparison -> Polarity Source #

compareArgs :: MonadConversion m => [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> m () Source #

Type-directed equality on argument lists

# Types

compareType :: MonadConversion m => Comparison -> Type -> Type -> m () Source #

Equality on Types

leqType :: MonadConversion m => Type -> Type -> m () Source #

coerce :: (MonadConversion m, MonadTCM m) => Comparison -> Term -> Type -> Type -> m Term Source #

`coerce v a b` coerces `v : a` to type `b`, returning a `v' : b` with maybe extra hidden applications or hidden abstractions.

In principle, this function can host coercive subtyping, but currently it only tries to fix problems with hidden function types.

coerceSize :: MonadConversion m => (Type -> Type -> m ()) -> Term -> Type -> Type -> m () Source #

Account for situations like `k : (Size< j) <= (Size< k + 1)`

Actually, the semantics is `(Size<= k) ∩ (Size< j) ⊆ rhs` which gives a disjunctive constraint. Mmmh, looks like stuff TODO.

For now, we do a cheap heuristics.

# Sorts and levels

compareLevel :: MonadConversion m => Comparison -> Level -> Level -> m () Source #

compareSort :: MonadConversion m => Comparison -> Sort -> Sort -> m () Source #

leqSort :: forall m. MonadConversion m => Sort -> Sort -> m () Source #

Check that the first sort is less or equal to the second.

We can put `SizeUniv` below `Inf`, but otherwise, it is unrelated to the other universes.

leqLevel :: MonadConversion m => Level -> Level -> m () Source #

equalLevel :: forall m. MonadConversion m => Level -> Level -> m () Source #

equalSort :: forall m. MonadConversion m => Sort -> Sort -> m () Source #

Check that the first sort equal to the second.

forallFaceMaps :: MonadConversion m => Term -> (Map Int Bool -> Blocker -> Term -> m a) -> (Substitution -> m a) -> m [a] Source #

compareInterval :: MonadConversion m => Comparison -> Type -> Term -> Term -> m () Source #

type Conj = (Map Int (Set Bool), [Term]) Source #

isCanonical :: [Conj] -> Bool Source #

leqInterval :: MonadConversion m => [Conj] -> [Conj] -> m Bool Source #

leqInterval r q = r ≤ q in the I lattice. (∨ r_i) ≤ (∨ q_j) iff ∀ i. ∃ j. r_i ≤ q_j

leqConj :: MonadConversion m => Conj -> Conj -> m Bool Source #

leqConj r q = r ≤ q in the I lattice, when r and q are conjuctions. ' (∧ r_i) ≤ (∧ q_j) iff ' (∧ r_i) ∧ (∧ q_j) = (∧ r_i) iff ' {r_i | i} ∪ {q_j | j} = {r_i | i} iff ' {q_j | j} ⊆ {r_i | i}

equalTermOnFace :: MonadConversion m => Term -> Type -> Term -> Term -> m () Source #

equalTermOnFace φ A u v = _ , φ ⊢ u = v : A

compareTermOnFace :: MonadConversion m => Comparison -> Term -> Type -> Term -> Term -> m () Source #

compareTermOnFace' :: MonadConversion m => (Comparison -> Type -> Term -> Term -> m ()) -> Comparison -> Term -> Type -> Term -> Term -> m () Source #

# Definitions

bothAbsurd :: MonadConversion m => QName -> QName -> m Bool Source #