Edofication part 2: more comb support in backend
This adds support for Edo , PAIR k
GET k
, and UPDATE k
on combs.
A guide to the important parts of the diff:
src/stages/6-mini_c/types.ml
Mini_c now has a T_tuple type (translate to comb pairs in Michelson) and E_tuple, E_proj, E_update operators. T_tuple
and E_tuple
are now used for all pairs, but the length will be 2 except for comb tuples.
src/passes/12-spilling/compiler.ml
Translates Ast_typed to Mini_c, new behavior for comb layout only:
- E_record to E_tuple
- E_record_accessor to E_proj
- E_record_update to E_update
(non-comb cases are left as is
src/passes/13-self_mini_c/self_mini_c.ml
Updated to account for new operators and to perform compile-time beta-reduction for tuple projection and destructuring, and eta-contraction of tuples, which are now easy.
src/passes/13-self_mini_c/uncurry.ml
Now works with tuple types and operators, making things significantly easier and benefiting from compile-time beta-reduction
src/passes/14-scoping/scoping.ml
Translates Mini_c E_tuple, E_proj, E_update to the Coq IR
src/coq/ligo.v
Coq IR now has corresponding E_tuple, E_proj, E_update operators. These operate directly on comb pair types for now, since Coq IR uses Michelson types directly.
src/coq/compiler.v
Compiles:
- E_tuple to
SWAP; PAIR; SWAP; PAIR; ...
(becausePAIR k
is not usable yet) - E_proj to
GET k
- E_update to
UPDATE k
src/passes/16-self_michelson/self_michelson.ml
Needed updates to account for the fact that the arity of GET
is different from the arity of GET k
, etc. Also shrinks GET 0/1/2
.
relates to #1152 (closed)