Skip to content

Edofication part 2: more comb support in backend

Tom Jack requested to merge edofication2 into dev

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; ... (because PAIR 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)

Edited by Rémi

Merge request reports