Serene

A graph-based compilation pipeline

lscz2's pipeline is now organised around a graph. Namespaces are the graph's nodes, terms are added to it as they are checked, and evaluated values are fed back into the graph as values.

This end-to-end loop — Syntax → Expr (Semantic) → core terms → values — replaces the old linear pass structure and better matches how a dependently typed program is actually elaborated.