Struct Book 

pub struct Book {
    pub defs: Definitions,
    pub hvm_defs: HvmDefinitions,
    pub adts: Adts,
    pub ctrs: Constructors,
    pub entrypoint: Option<Name>,
    pub imports: Vec<Import>,
}

The representation of a program.

Fields

defs: Definitions

Function definitions.

hvm_defs: HvmDefinitions

HVM native function definitions.

adts: Adts

Algebraic datatype definitions.

ctrs: Constructors

Map of constructor name to type name.

entrypoint: Option<Name>

A custom or default “main” entrypoint.

imports: Vec<Import>

Imports declared in the program.

Implementations

impl Book

pub fn encode_builtins(&mut self)

impl Book

pub fn display_pretty(&self) -> impl Display + '_

impl Book

pub fn merge_definitions(&mut self)

Merges definitions that have the same structure into one definition. Expects variables to be linear.

Some of the origins of the rules will be lost in this stage, Should not be preceded by passes that cares about the origins.

impl Book

pub fn desugar_use(&mut self)

Inline copies of the declared bind in the use expression.

Example:

use id = λx x
(id id id)

// Transforms to:
(λx x λx x λx x)

pub fn desugar_ctr_use(&mut self)

Inline copies of the declared bind in Fold, Mat and Open inside use expressions.

impl Book

pub fn encode_adts(&mut self, adt_encoding: AdtEncoding)

Defines a function for each constructor in each ADT in the book.

impl Book

pub fn encode_matches(&mut self, adt_encoding: AdtEncoding)

Encodes pattern matching expressions in the book into their core form. Must be run after [Ctr::fix_match_terms].

ADT matches are encoded based on adt_encoding.

Num matches are encoded as a sequence of native num matches (on 0 and 1+).

impl Book

pub fn recursive_defs(&self) -> BTreeSet<Name>

impl Book

pub fn expand_main(&mut self)

Expands the main function so that it is not just a reference. While technically correct, directly returning a reference is never what users want.

impl Book

pub fn float_combinators(&mut self, max_size: usize)

Extracts combinator terms into new definitions.

Precondition: Variables must have been sanitized.

The floating algorithm follows these rules: For each child of the term:

• Recursively float every grandchild term.
• If the child is a combinator:
  • If the child is not “safe”, extract it.
  • If the term is a combinator and it’s “safe”:
    • If the term is currently larger than max_size, extract the child.
  • Otherwise, always extract the child to a new definition.
• If the child is not a combinator, we can’t extract it since it would generate an invalid term.

Terms are considered combinators if they have no free vars, no unmatched unscoped binds/vars and are not references (to avoid infinite recursion).

See Term::is_safe for what is considered safe here.

See Term::size for the measurement of size. It should more or less correspond to the compiled inet size.

impl Book

pub fn lift_local_defs(&mut self)

impl Book

pub fn linearize_match_binds(&mut self)

Linearization of binds preceding match/switch terms, up to the first bind used in either the scrutinee or the bind.

Example:

@a @b @c let d = (b c); switch a {
  0: (A b c d)
  _: (B a-1 b c d)
}
// Since `b`, `c` and `d` would be eta-reducible if linearized,
// they get pushed inside the match.
@a switch a {
  0: @b @c let d = (b c); (A b c d)
  _: @b @c let d = (b c); (B a-1 b c d)
}

impl Book

pub fn linearize_matches(&mut self)

Linearizes all variables used in a matches’ arms.

impl Book

pub fn linearize_match_with(&mut self)

Linearizes all variables specified in the with clauses of match terms.

impl Book

Erases variables that weren’t used, dups the ones that were used more than once. Substitutes lets into their variable use. In details: For all var declarations: If they’re used 0 times: erase the declaration If they’re used 1 time: leave them as-is If they’re used more times: insert dups to make var use affine For all let vars: If they’re used 0 times: Discard the let If they’re used 1 time: substitute the body in the var use If they’re use more times: add dups for all the uses, put the let body at the root dup. Precondition: All variables are bound and have unique names within each definition.

pub fn linearize_vars(&mut self)

impl Book

pub fn make_var_names_unique(&mut self)

Makes all variables in each definition have a new unique name. Skips unbound variables. Precondition: Definition references have been resolved.

impl Book

pub fn hvm_entrypoint(&self) -> &str

Trait Implementations

impl Clone for Book

fn clone(&self) -> Book

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Book

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Book

fn default() -> Book

Returns the “default value” for a type.

impl Display for Book

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.