Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- 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 ()
- 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 ()
- computeElimHeadType :: QName -> Elims -> Elims -> TCM Type
- compareAtom :: Comparison -> Type -> Term -> Term -> TCM ()
- compareDom :: Free c => Comparison -> Dom Type -> Dom Type -> Abs b -> Abs c -> TCM () -> TCM () -> TCM () -> TCM ()
- compareRelevance :: Comparison -> Relevance -> Relevance -> Bool
- antiUnify :: ProblemId -> Type -> Term -> Term -> TCM Term
- antiUnifyType :: ProblemId -> Type -> Type -> TCM Type
- antiUnifyElims :: ProblemId -> Type -> Term -> Elims -> Elims -> TCM Term
- compareElims :: [Polarity] -> [IsForced] -> Type -> Term -> [Elim] -> [Elim] -> TCM ()
- compareIrrelevant :: Type -> Term -> Term -> TCM ()
- compareWithPol :: Polarity -> (Comparison -> a -> a -> TCM ()) -> a -> a -> TCM ()
- polFromCmp :: Comparison -> Polarity
- compareArgs :: [Polarity] -> [IsForced] -> Type -> Term -> Args -> Args -> TCM ()
- compareType :: Comparison -> Type -> Type -> TCM ()
- leqType :: Type -> Type -> TCM ()
- coerce :: Comparison -> Term -> Type -> Type -> TCM Term
- coerceSize :: (Type -> Type -> TCM ()) -> Term -> Type -> Type -> TCM ()
- compareLevel :: Comparison -> Level -> Level -> TCM ()
- compareSort :: Comparison -> Sort -> Sort -> TCM ()
- leqSort :: Sort -> Sort -> TCM ()
- leqLevel :: Level -> Level -> TCM ()
- equalLevel :: Level -> Level -> TCM ()
- equalLevel' :: Level -> Level -> TCM ()
- equalSort :: Sort -> Sort -> TCM ()
- forallFaceMaps :: Term -> (Map Int Bool -> MetaId -> Term -> TCM a) -> (Substitution -> TCM a) -> TCM [a]
- compareInterval :: Comparison -> Type -> Term -> Term -> TCM ()
- type Conj = (Map Int (Set Bool), [Term])
- isCanonical :: [Conj] -> Bool
- leqInterval :: [Conj] -> [Conj] -> TCM Bool
- leqConj :: Conj -> Conj -> TCM Bool
- equalTermOnFace :: Term -> Type -> Term -> Term -> TCM ()
- compareTermOnFace :: Comparison -> Term -> Type -> Term -> Term -> TCM ()
- compareTermOnFace' :: (Comparison -> Type -> Term -> Term -> TCM ()) -> Comparison -> Term -> Type -> Term -> Term -> 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.
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.
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 #
computeElimHeadType :: QName -> Elims -> Elims -> TCM Type Source #
Compute the head type of an elimination. For projection-like functions this requires inferring the type of the principal argument.
compareAtom :: Comparison -> Type -> Term -> Term -> TCM () Source #
Syntax directed equality on atomic values
:: Free c | |
=> Comparison |
|
-> Dom Type |
|
-> Dom Type |
|
-> Abs b |
|
-> Abs c |
|
-> TCM () | Continuation if mismatch in |
-> TCM () | Continuation if mismatch in |
-> TCM () | Continuation if comparison is successful. |
-> TCM () |
Check whether a1
and continue in context extended by cmp
a2a1
.
compareRelevance :: Comparison -> Relevance -> Relevance -> Bool Source #
antiUnify :: ProblemId -> Type -> Term -> Term -> TCM 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.
compareElims :: [Polarity] -> [IsForced] -> 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] -> [IsForced] -> Type -> Term -> Args -> Args -> TCM () Source #
Type-directed equality on argument lists
Types
compareType :: Comparison -> Type -> Type -> TCM () Source #
Equality on Types
coerce :: Comparison -> 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.
Precondition: a
and b
are reduced.
coerceSize :: (Type -> Type -> TCM ()) -> Term -> Type -> Type -> TCM () 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.
Precondition: types are reduced.
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.
forallFaceMaps :: Term -> (Map Int Bool -> MetaId -> Term -> TCM a) -> (Substitution -> TCM a) -> TCM [a] Source #
compareInterval :: Comparison -> Type -> Term -> Term -> TCM () Source #
isCanonical :: [Conj] -> Bool Source #
leqInterval :: [Conj] -> [Conj] -> TCM Bool Source #
leqInterval r q = r ≤ q in the I lattice. (∨ r_i) ≤ (∨ q_j) iff ∀ i. ∃ j. r_i ≤ q_j
leqConj :: Conj -> Conj -> TCM 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 :: Term -> Type -> Term -> Term -> TCM () Source #
equalTermOnFace φ A u v = _ , φ ⊢ u = v : A
compareTermOnFace :: Comparison -> Term -> Type -> Term -> Term -> TCM () Source #
compareTermOnFace' :: (Comparison -> Type -> Term -> Term -> TCM ()) -> Comparison -> Term -> Type -> Term -> Term -> TCM () Source #