Auxiliary elaboration functions: AKA custom elaborators #
The elaborator for expression trees of
At a high level, the elaborator tries to solve for a type that each of the operands in the expression tree can be coerced to, while taking into account the expected type for the entire expression tree. Once this type is computed (and if it exists), it inserts coercions where needed.
Here are brief descriptions of each of the operator types:
binop% f a belaborates
f a bas a binary operator with two operands
b, and each operand participates in the protocol.
binop_lazy% f a bis like
binop%but elaborates as
f a (fun () => b).
unop% f aelaborates
f aas a unary operator with one operand
a, which participates in the protocol.
leftact% f a belaborates
f a bas a left action (the
aoperand "acts upon" the
bparticipates in the protocol since
acan have an unrelated type, for example scalar multiplication of vectors.
rightact% f a belaborates
f a bas a right action (the
boperand "acts upon" the
aparticipates in the protocol since
bcan have an unrelated type. This is used by
HPowsince, for example, there are both
Real -> Nat -> Realand
Real -> Real -> Realexponentiation functions, and we prefer the former in the case of
x ^ 2, but
binop%would choose the latter. (#2220)
- There are also
binrel_no_prop%(see the docstring for
The elaborator works as follows:
1- Expand macros.
Syntax object corresponding to the
binop%/... term into a
toTree method visits nested
binop%/... terms and parentheses.
3- Synthesize pending metavariables without applying default instances and using the
(mayPostpone := true).
4- Tries to compute a maximal type for the tree computed at step 2.
We say a type α is smaller than type β if there is a (nondependent) coercion from α to β.
We are currently ignoring the case we may have cycles in the coercion graph.
If there are "uncomparable" types α and β in the tree, we skip the next step.
We say two types are "uncomparable" if there isn't a coercion between them.
Note that two types may be "uncomparable" because some typing information may still be missing.
5- We traverse the tree and inject coercions to the "maximal" type when needed.
Recall that the coercions are expanded eagerly by the elaborator.
b) The coercions are inserted in the "leaves" like in Lean 3.
c) There are no coercions "hidden" inside instances, and we can elaborate
axiom Int.add_comm (i j : Int) : i + j = j + i example (n : Nat) (i : Int) : n + i = i + n := by rw [Int.add_comm]
Recall that the
rw tactic used to fail because our old
binop% elaborator would hide
coercions inside of a
In the new
binop%and related elaborators the decision whether a coercion will be inserted or not is made at
binop%elaboration time. This was not the case in the old elaborator. For example, an instance, such as
HAdd Int ?m ?n, could be created when executing the
binop%elaborator, and only resolved much later. We try to minimize this problem by synthesizing pending metavariables at step 3.
For types containing heterogeneous operators (e.g., matrix multiplication), step 4 will fail and we will skip coercion insertion. For example,
x : Matrix Real 5 4and
y : Matrix Real 4 8, there is no coercion
Matrix Real 5 4from
Matrix Real 4 8and vice-versa, but
x * yis elaborated successfully and has type
Matrix Real 5 8.
rightact%elaborators are to handle binary operations where only one of the arguments participates in the protocol. For example, in
2 ^ n + ywith
n : Natand
y : Real, we do not want to coerce
nto be a real as well, but we do want to elaborate
2 : Real.
Elaboration functions for
We use the infrastructure for
binop% to make sure we propagate information between the left and right hand sides
of a binary relation.
binrel% R x yelaborates
R x yusing the
binop%/...expression trees in both
y. It is similar to how
binop% R x yelaborates but with a significant difference: it does not use the expected type when computing the types of the operads.
binrel_no_prop% R x yelaborates
R x ylike
binrel% R x y, but if the resulting type for
Propthey are coerced to
Bool. This is used for relations such as
==which do not support
Prop, but we still want to be able to write
(5 > 2) == (2 > 1)for example.
- One or more equations did not get rendered due to their size.