Safe Haskell | None |
---|---|
Language | Haskell98 |
- tryConversion :: TCM () -> TCM Bool
- 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 ()
- 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. Restores 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.
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
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
equalLevel :: Level -> Level -> TCM () Source