adapter API

The adapter package has no public items. It is a contract-test package: its white-box tests define a small downstream-style AST, implement @syntax.BindingSyntax for it, and check that generic substitution and generic rewriting behave as documented on an AST that is not Term[T].

package "Luna-Flow/type_theory/adapter"

// Values

// Errors

// Types and methods

// Type aliases

// Traits

The interface you implement to adapt your own AST is @syntax.BindingSyntax; the algorithms you then get are @syntax.generic_free_variables, @substitution.GenericSubstitution and @rewrite.generic_top_down_once. The contract is explained in the adapter design, and the adapter tutorial builds an adapter step by step.

What the tests check

The test file src/adapter/poly_adapter_wbtest.mbt uses a private AST with four node kinds: integer literals (projected as Opaque), variables, an n-ary sum node (projected as Apply) and a scope node (projected as Bind). It checks that

• GenericSubstitution::apply_once substitutes simultaneously and in one pass: $\{x \mapsto y,\ y \mapsto 2\}$ applied to $x + y$ gives $y + 2$;
• substitution leaves variables outside its domain in place (partial evaluation);
• generic_top_down_once finds a redex inside an argument, rebuilds the parent through the trait constructors, and reports the path [ApplyArgument(0)].