HVM4 is a term rewrite system / runtime for the Interaction Calculus.
- The theoretical spec is in
README.md. - The C implementation is in
clang/. - The C spec is in
clang/README.md.
# Build
cd clang && clang -O2 -o main main.c
# Run a file
./clang/main test/file.hvm4 -s -C10
Where:
- `-s` shows performance stats
- `-C10` collapses and flattens superpositions
- Note: use collapse mode it by default
- Note: limit it to 10 lines to avoid infinite streams
# Run all tests
./test/_all_.shThe file path IS the function name. Replace / with _, drop .c:
term/tag.c → term_tag()
term/new/lam.c → term_new_lam()
prim/add.c → prim_add()
wnf/app_lam.c → wnf_app_lam()
_.c represents the directory itself:
snf/_.c → snf()
collapse/_.c → collapse()
parse/term/_.c → parse_term()
This is strictly enforced. Read clang/STYLE.md before writing any code.
hvm4.c— root file that#includes everythingmain.c— CLI entry pointterm/— term representation (tag, val, ext, constructors)parse/— parser (source → AST)wnf/— weak normal form evaluator (interaction rules)snf/— strong normal form evaluatorprim/— primitive operations (add, mul, eq, etc.)collapse/— superposition extraction
64-bit term pointer: SUB(1) | TAG(7) | EXT(24) | VAL(32)
- SUB: is this heap entry a substitution?
- TAG: term type (APP, LAM, SUP, etc.)
- EXT: label/name (24-bit, base64-encoded)
- VAL: heap address or immediate value
Stack-based WNF evaluator in wnf/_.c.
Interaction rules are in wnf/ named by pattern:
app_lam.chandles(λx.f a)dup_sup.chandles! X &L = &R{a,b}- etc.
Tests are .hvm4 files with expected output in trailing // comments:
@main = ((@add 1) 2)
//3
@main = (&L{1,2} + 3)
//4
//5
Always run all tests after each change.