Agda.TypeChecking.Pretty

For debugging only.

Assumes we are in the right context.

Print masked things in double parentheses.

Bound names in first argument scope over second argument.

Hiding is an idempotent partial monoid, with unit NotHidden. Instance and NotHidden are incompatible.

Semigroup computes if any of several is an AbstractDef.

Conjunctive semigroup (NotMain is absorbing).

Just for the Hiding instance. Should never combine different overlapping.

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

Right-biased composition, because the left quantity acts as context, and the right one as occurrence.

NameKind in Name can get more precise.

Some NameKinds are more informative than others.

Invariant: the KindOfName components should be equal whenever we have to concrete renderings of an abstract name.

Hereditary Semigroup instance for Maybe. (The default instance for Maybe may not be the hereditary one.)

Hereditary Semigroup instance for Maybe. (The default instance for Maybe may not be the hereditary one.)

The semigroup laws only hold up to flattening of Concat.

Partial ordering forms a monoid under sequencing.

Beware: stimes will crash if the given number does not fit into an Int.

Concatenation of StrictBuilder is right-biased: the right builder will be run first. This allows a builder to run tail-recursively when it was accumulated left-to-right.

Additive

Additive

ORs the flags.

ORs the masks.

Favorites forms a Monoid under empty and 'union.

Cohesion forms a semigroup under addition.

Pointwise addition.

Cohesion forms a semigroup under composition.

Pointwise composition.

Composition of quantities (multiplication).

Quantity0 is dominant. Quantity1 is neutral.

Right-biased for origin.

Relevance forms a semigroup under composition.

ReallyNotBlocked is the unit. MissingClauses is dominant. StuckOn{} should be propagated, if tied, we take the left.

CallGraph is a monoid under union.

This instance is more specific than a generic instance Semigroup a => Semigroup (TCM a).

(<>) on comparisons combines results with (<>) @Ordering. Without newtypes this equals liftA2 (liftA2 (<>)).

(<>) :: Comparison a -> Comparison a -> Comparison a
Comparison cmp <> Comparison cmp' = Comparison a a' ->
  cmp a a' <> cmp a a'

(<>) on equivalences uses logical conjunction (&&) on the results. Without newtypes this equals liftA2 (liftA2 (&&)).

(<>) :: Equivalence a -> Equivalence a -> Equivalence a
Equivalence equiv <> Equivalence equiv' = Equivalence a b ->
  equiv a b && equiv' a b

(<>) on predicates uses logical conjunction (&&) on the results. Without newtypes this equals liftA2 (&&).

(<>) :: Predicate a -> Predicate a -> Predicate a
Predicate pred <> Predicate pred' = Predicate a ->
  pred a && pred' a

Proper monoid instance for VarMap rather than inheriting the broken one from IntMap. We combine two occurrences of a variable using mappend.

The default way of aggregating free variable info from subterms is by adding the variable occurrences. For instance, if we have a pair (t₁,t₂) then and t₁ has o₁ the occurrences of a variable x and t₂ has o₂ the occurrences of the same variable, then (t₁,t₂) has mappend o₁ o₂ occurrences of that variable.

From counting Quantity, we extrapolate this to FlexRig and Relevance: we care most about about StronglyRigid Relevant occurrences. E.g., if t₁ has a StronglyRigid occurrence and t₂ a Flexible occurrence, then (t₁,t₂) still has a StronglyRigid occurrence. Analogously, Relevant occurrences count most, as we wish e.g. to forbid relevant occurrences of variables that are declared to be irrelevant.

VarOcc forms a semiring, and this monoid is the addition of the semiring.

Merges RangeMaps by inserting every "piece" of the smaller one into the larger one.

Only defined by async for base >= 4.9

This constraint is arguably too strong. However, as some types (such as Natural) have undefined complement, this is the only safe choice.

AlphaColour forms a monoid with over and transparent.

<> = union

O(n+m)

To obtain good performance, the smaller set must be presented as the first argument.

Examples

>>> fromList [1,2] <> fromList [2,3]fromList [1,2,3]

Either the combination of the successful results, or the first failure.

(<>) @(Op a b) without newtypes is (<>) @(b->a) = liftA2 (<>). This lifts the Semigroup operation (<>) over the output of a.

(<>) :: Op a b -> Op a b -> Op a b
Op f <> Op g = Op a -> f a <> g a

<> = union

If a key occurs in both maps, the mapping from the first will be the mapping in the result.

Examples

>>> fromList [(1,'a'),(2,'b')] <> fromList [(2,'c'),(3,'d')]fromList [(1,'a'),(2,'b'),(3,'d')]

Strict (non-shortcut) semigroup.

Note that there might be a lazy alternative, e.g., for TCM All we might want and2M as concatenation, to shortcut conjunction in case we already have False.

The Semigroup instance for ParsecT is used to append the result of several parsers, for example:

(many $ char a) <> (many $ char b)

The above will parse a string like "aabbb" and return a successful parse result "aabbb". Compare against the below which will produce a result of "bbb" for the same input:

(many $ char a) >> (many $ char b)
(many $ char a) *> (many $ char b)