Safe Haskell | None |
---|---|

Language | Haskell98 |

- tryConversion :: TCM () -> TCM Bool
- tryConversion' :: TCM a -> TCM (Maybe a)
- sameVars :: Elims -> Elims -> Bool
- intersectVars :: Elims -> Elims -> Maybe [Bool]
- equalTerm :: Type -> Term -> Term -> TCM ()
- equalAtom :: Type -> Term -> Term -> TCM ()
- equalType :: Type -> Type -> TCM ()
- convError :: TypeError -> TCM ()
- compareTerm :: Comparison -> Type -> Term -> Term -> TCM ()
- unifyPointers :: Comparison -> Term -> Term -> TCM () -> TCM ()
- assignE :: CompareDirection -> MetaId -> Elims -> Term -> (Term -> Term -> TCM ()) -> TCM ()
- compareTermDir :: CompareDirection -> Type -> Term -> Term -> TCM ()
- compareTerm' :: Comparison -> Type -> Term -> Term -> TCM ()
- compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM ()
- etaInequal :: Comparison -> Type -> Term -> Term -> TCM ()
- compareAtomDir :: CompareDirection -> Type -> Term -> Term -> TCM ()
- compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()
- compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
- compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
- compareIrrelevant :: Type -> Term -> Term -> TCM ()
- compareWithPol :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM ()
- polFromCmp :: Comparison -> Polarity
- compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM ()
- compareType :: Comparison -> Type -> Type -> TCM ()
- leqType :: Type -> Type -> TCM ()
- coerce :: Term -> Type -> Type -> TCM Term
- coerceSize :: Term -> Type -> Type -> TCM Term
- compareLevel :: Comparison -> Level -> Level -> TCM ()
- compareSort :: Comparison -> Sort -> Sort -> TCM ()
- leqSort :: Sort -> Sort -> TCM ()
- leqLevel :: Level -> Level -> TCM ()
- equalLevel :: Level -> Level -> TCM ()
- equalSort :: Sort -> Sort -> TCM ()
- bothAbsurd :: QName -> QName -> TCM Bool

# Documentation

tryConversion :: TCM () -> TCM Bool Source

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

tryConversion' :: TCM a -> TCM (Maybe a) Source

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.

compareTerm :: Comparison -> Type -> Term -> Term -> TCM () Source

Type directed equality on values.

unifyPointers :: Comparison -> Term -> Term -> TCM () -> TCM () Source

assignE :: CompareDirection -> MetaId -> Elims -> Term -> (Term -> Term -> TCM ()) -> TCM () Source

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

compareTermDir :: CompareDirection -> Type -> Term -> Term -> TCM () Source

compareTerm' :: Comparison -> Type -> Term -> Term -> TCM () Source

compareTel :: Type -> Type -> Comparison -> Telescope -> Telescope -> TCM () Source

`compareTel t1 t2 cmp tel1 tel1`

checks whether pointwise
`tel1 `cmp` tel2`

and complains that `t2 `cmp` t1`

failed if
not.

etaInequal :: Comparison -> Type -> Term -> Term -> TCM () Source

Raise `UnequalTerms`

if there is no hope that by
meta solving and subsequent eta-contraction these
terms could become equal.
Precondition: the terms are in reduced form
(with no top-level pointer) and
failed to be equal in the `compareAtom`

check.

By eta-contraction, a lambda or a record constructor term can become anything.

compareAtomDir :: CompareDirection -> Type -> Term -> Term -> TCM () Source

compareAtom :: Comparison -> Type -> Term -> Term -> TCM () Source

Syntax directed equality on atomic values

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

compareElims :: [Polarity] -> Type -> Term -> [Elim] -> [Elim] -> TCM () Source

`compareElims pols a v els1 els2`

performs type-directed equality on eliminator spines.
`t`

is the type of the head `v`

.

compareIrrelevant :: Type -> Term -> Term -> TCM () 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 :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM () Source

polFromCmp :: Comparison -> Polarity Source

compareArgs :: [Polarity] -> Type -> Term -> Args -> Args -> TCM () Source

Type-directed equality on argument lists

# Types

compareType :: Comparison -> Type -> Type -> TCM () Source

Equality on Types

coerce :: Term -> Type -> Type -> TCM 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 :: Term -> Type -> Type -> TCM Term 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 :: Comparison -> Level -> Level -> TCM () Source

compareSort :: Comparison -> Sort -> Sort -> TCM () Source

leqSort :: Sort -> Sort -> TCM () 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.

equalLevel :: Level -> Level -> TCM () Source