Add further information on compilation-and-readback.md

[In-Veritas]

Feedback on Document Completeness

The document is incomplete regarding the nodes Eraser, Reference, and Match, and only briefly mentions Number and Operation.

Suggestions for Improvement

To render the document more complete, the following could be added:

1. Description and Model of Each Type of Node
   Provide detailed descriptions and formal models for each node type.

2. Interaction Rules Between Nodes
   Specify the rules and constraints that govern how different node types interact with each other.

3. Pattern Matching Implementation
   Elaborate on how pattern matching is implemented, covering:

   • Algorithms used
   • Examples illustrating the process
   • Edge cases and handling strategies

[developedby]

Bend core terms directly compile to HVM nodes.
Application -> CON node with --+ polarization.
Lambda -> CON node with ++- polarization.
Duplication -> DUP node with -++ polarization.
Superposition -> DUP node with +-- polarization
Pairs -> CON node with +-- polarization.
Pair elimination -> CON node with -++ polarization.
Erasure values (as in λx *) -> ERA node with + polarization.
Erased variables (as in λ* x) -> ERA node with + polarization.
Numbers -> NUM node (always + polarization).
Switches -> MAT node (--+) + CON node (+--) on port 1 that links to the if 0 and if >= 1 cases.
Numeric operations -> an OPR node (--+) plus a NUM that holds the kind of operation as per the HVM2 paper.
References to top level functions -> REF node (+).

Matches get compiled to the above core constructs according to the adt-encoding option.

The rest of the compilation process is (should be) described in the other documents. We have the following (relevant to this document) compiler passes:

• encode_adt : create functions for constructors
• desugar_open : convert open terms into match terms
• encode_builtins : convert sugars for builtin types (list, string, etc) into function calls.
• desugar_match_def : convert equational-style pattern matching functions into trees of match and switch terms.
• fix_match_terms : puts all match and switch terms into a normalized form.
• lift_local_defs : converts def terms into top-level functions.
• desugar_bend : converts bend terms into top-level functions.
• desugar_fold : converts fold terms into top-level functions.
• desugar_with_blocks : converts with terms and ask (<-) terms into monadic bind and unit (wrap).
• make_var_names_unique : Give a unique name to each variable in each function.
• desugar_use : resolve alias terms (use) by substituting their occurences by the aliased term (syntatic duplication).
• linearize_matches : linearize the variables in match and switch terms according to the linearize-matches option.
• linearize_match_with : linearize the variables specified in with clauses of match and switch if they haven't already been linearized by linearize_matches.
• type_check_book : runs the type checker (no elaboration, only inference/checking).
• encode_matches : transform match terms into their lambda-calculus forms specified by the adt-encoding option.
• linearize_vars : linearizes the occurences of variables by placing dups when variables are used more than once, erasing unused variables and inlining let terms whose variables only occur once.
• float_combinators : converts combinator terms into top-level functions according to the size heuristic described in the source code and probably in another document.
• prune : removes unused functions according to the prune option.
• merge_definitions : merge identical top level functions.
• expand_main : expands the term of the main function by dereferencing so that it includes some computation and isn't only lazy refs or data containing lazy refs.
• book_to_hvm : the lowering to hvm described in the compilation-and-readback file.
• eta : runs eta-reduction on the inet level, without reducing nodes with ERA or NUM at both ports (logically equivalent but for users it looks wrong).
• check_cycles : a heuristic check for mutually recursive cycles of function calls that would cause loops in the HVM.
• inline_hvm_book : inlines REFs to networks that are just nullary nodes.
• prune_hvm_book : another layer of pruning (new things can pop up after eta-reducing at the inet level).
• check_net_sizes : ensures that no generated definition will be too large to run on the cuda runtime.
• add_recursive_priority : marks some binary recursive calls with a flag at the inet level so that the gpu runtime can properly distribute work.

The documentation should also link to the HVM2 paper instead of the old hvm-64.