Reference evaluator

The reference evaluator takes a well-typed Deep program and reduces it step by step according to the operational semantics. Each reduction step corresponds to a single rule in the semantics, making the execution trace directly readable against the formal definition.

How it works

Hull implements the small-step operational semantics as a Chelis function from Deep AST terms to Deep AST terms. At each step, it identifies the active redex, applies the matching reduction rule, and produces the next term. Evaluation continues until the term is a value or until no rule applies (a stuck state, which indicates a bug in the spec or a violation of the type-safety property).

Usage

Evaluate a program to its final value:

chelis hull eval myprogram.deep

Print every intermediate step:

chelis hull eval --steps myprogram.deep

The --steps flag outputs each reduction with the name of the rule applied. This is useful for understanding evaluation order and for comparing against the compiler's runtime behavior.

Comparing against the compiler

Run the same program through both the compiler's evaluator and Hull's reference evaluator:

chelis eval myprogram.deep > compiler.out
chelis hull eval myprogram.deep > spec.out
diff compiler.out spec.out

Identical final values confirm that the compiler's runtime matches the spec for that program. Different results surface a semantic divergence: either the compiler reduces a term incorrectly, or the spec's rules produce an unintended result.

Stuck states

If evaluation reaches a term where no reduction rule applies, Hull reports the stuck term and the set of rules it attempted. A stuck state in a well-typed program is a violation of the progress property and always indicates a bug (either in the type checker or in the reduction rules).