Created
December 7, 2025 16:15
-
-
Save VictorTaelin/71e9b2ffeba3a9402afba76f8735d0b8 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| commit 4ffb261f8a43be0c5891e0725f1ea709147eeb7e | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Dec 7 11:53:52 2025 -0300 | |
| Make commas and semicolons optional in parser | |
| - Superposition: &L{A,B} or &L{A B} | |
| - Fork params: &Lλx,y,z{...} or &Lλx y z{...} | |
| - Fork branches: semicolons now optional between and after branches | |
| - Constructor args: #Foo{a,b} or #Foo{a b} | |
| - Lists: [a,b,c] or [a b c] | |
| - Function application: f(a,b) or f(a b) | |
| - Unscoped binding: ${f,v} or ${f v} | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com> | |
| commit 65d9cef686b7fae63f15e105ad0341b81df8f181 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 17:46:29 2025 -0300 | |
| Allow optional &₀: and &₁: labels in fork branches | |
| For clarity, fork branches can now be prefixed with side labels: | |
| &Lλx{&₀:F;&₁:G} | |
| This makes it explicit which branch produces CO0 vs CO1 refs. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| ... | |
| commit 52d3c259466eccdf92942add6c116852167b3461 | |
| Merge: 66c2cbc 1ba369b | |
| Author: Victor Taelin <victor.taelin@gmail.com> | |
| Date: Fri Dec 5 17:23:16 2025 -0300 | |
| Merge pull request #6 from HigherOrderCO/col-optim | |
| optimize | |
| commit 66c2cbce3866057301c6193b9bd06cfb60f6f342 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 17:15:57 2025 -0300 | |
| Add fork notation syntax for parallel branching | |
| New syntax: &Lλx,y,z{A;B} (static) or &(L)λx,y,z{A;B} (dynamic) | |
| Desugars to: λx&L.λy&L.λz&L.&L{A';B'} | |
| Variables used in the left branch A automatically become CO0 refs | |
| (x₀,y₀,z₀) and variables in the right branch B become CO1 refs | |
| (x₁,y₁,z₁), eliminating the need for explicit subscripts. | |
| Example: | |
| &Lλx,y{(x+y);(x*y)} | |
| desugars to: | |
| λx&L.λy&L.&L{(x₀+y₀);(x₁*y₁)} | |
| which desugars to: | |
| λx.!x&L=x;λy.!y&L=y;&L{(x₀+y₀);(x₁*y₁)} | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit d13584f038d14034de898910e31e17312f830b33 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 17:09:38 2025 -0300 | |
| polish | |
| commit 1a55024e9188409af987a4d71023b61182f1696f | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 16:46:34 2025 -0300 | |
| comprehensive README | |
| commit 3977f4ba4377daf7347b1b8a33bf81227eef4daf | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 11:52:45 2025 -0300 | |
| Fix de Bruijn index bug in dynamic lambda-dup label parsing | |
| The dynamic label in λx&(L).body was parsed at depth D instead of D+1, | |
| causing variables to get wrong indices. For λ&L.λB&(L).body, L got | |
| index 0 instead of 1, referencing the wrong lambda. | |
| Also add supgen_mul test (as collapse_supgen_mul for proper limiting). | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit c36ce46ee76abb7d5fa778ea4003fa9a0a093beb | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 11:52:15 2025 -0300 | |
| instructions | |
| ... | |
| commit 7b20204f7101ad7cfbc4e7c7fbc1ca3dd0a0f730 | |
| Merge: 7bb9a04 de4ff55 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 10:54:16 2025 -0300 | |
| Merge remote-tracking branch 'origin/main' | |
| Resolved conflict in clang/parse/term/var.c: | |
| - Kept local version using parse_error_var helper | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 7bb9a047a730b6ac0cde3f1fa172798331513c64 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 10:50:55 2025 -0300 | |
| Add multi-argument lambda syntax: λx,y,z.f | |
| Supports comma-separated args with any modifier combination: | |
| - λx,y,z.f → λx.λy.λz.f | |
| - λ&x,y&L,z&(L).f → mixed cloned/dup forms | |
| - λx&L,y&M.f → each arg with own dup label | |
| Uses recursive parsing - no separate code path for single vs multi-arg. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 857c35e5023252d8108200896cdf0348412782e2 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 10:17:01 2025 -0300 | |
| Extract parse error helpers to reduce repetition | |
| Add parse/error_var.c with two helpers: | |
| - parse_error_var(fmt, nam): for variable-related errors with name lookup | |
| - parse_error_affine(nam, uses, is_dup, hint): for affinity violation errors | |
| Simplifies 5 error sites across var.c, lam.c, dup.c from verbose | |
| multi-line fprintf sequences to single function calls. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 3f137aaef6733fd6a78afcc59c77d8f0e805a9bd | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 09:48:36 2025 -0300 | |
| Add lambda-dup syntax sugar: λx&L. λx&(L). λx&. | |
| New syntax for inline dup in lambda bindings: | |
| λx&L. F desugars to λx. ! x &L = x; F | |
| λx&(L). F desugars to λx. ! x &(L) = x; F | |
| λx&. F desugars to λx. ! x & = x; F | |
| This allows concise splitting of lambda arguments: | |
| (λx&L.[x₀,x₁])(7) → [7,7] | |
| (λx&L.[x₀,x₁])(&L{1,2}) → [1,2] | |
| Implementation extracts shared dup-parsing logic into parse_dup_body() | |
| helper, which both parse_term_dup and parse_term_lam now use. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit bfcb46538e868a7b2f205d6ea52e36b837df4061 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Fri Dec 5 09:42:53 2025 -0300 | |
| fix test example | |
| commit 9a98b1b40a1d02e6b34a67e61e2eb7704e015512 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Thu Dec 4 15:01:49 2025 -0300 | |
| Remove spaces around <> in improper list printing | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit de4ff55e50047b4608a77997f496442fd1e0a319 | |
| Author: Nicolas Abril <nicolas@higherorderco.com> | |
| Date: Thu Dec 4 15:16:16 2025 +0100 | |
| Print location on unbound var parse error | |
| ... | |
| commit 713c63bcaaab986ab4c4630110f614628731f493 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Thu Dec 4 07:44:45 2025 -0300 | |
| Use NUM(0) instead of ERA for missing λ-match default case | |
| Previously, λ{#A:a;#B:b} desugared to λ{#A:a;λ{#B:b;&{}}} with ERA | |
| as the sentinel for "no default case". This caused superpositions | |
| inside λ-matches to disappear during collapse, because collapse | |
| treated ERA specially (any subterm collapsing to ERA makes the whole | |
| node ERA). | |
| Now the sentinel is NUM(0) instead: λ{#A:a;λ{#B:b;0}}. This allows | |
| the generic collapse handler to process MAT nodes like any other | |
| arity-2 node, properly lifting superpositions through the match. | |
| Changes: | |
| - parse/term/lam.c: Use term_new_num(0) for missing default | |
| - print/term.c: Recognize NUM(0) as "no default" when printing | |
| - collapse/_.c: Remove special MAT/SWI case, use generic handler | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit c151ef1d59a539250750172a2e76c3790fa0d7ab | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 23:50:09 2025 -0300 | |
| Skip ERA terms in collapse mode output | |
| ERA represents a destroyed universe and should not be printed as a | |
| collapsed value. Previously, terms like &L{1,λx.&{}} would incorrectly | |
| output both "1" and "&{}" - now only "1" is printed. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit d6e701ce5a5f968269ed987c50b0276b393f27e1 | |
| Merge: fa855f1 a9ffcb4 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 23:43:44 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit fa855f1c5204b002e80a6567cc0d3f299a84f543 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 23:43:16 2025 -0300 | |
| Add runtime errors for app-num and app-ctr, warn about dup-app | |
| - Applying a number or constructor is now a runtime error | |
| - Added warning comment that DUP does not interact with APP | |
| - Rewrote autodup_nightmare test to use lambda variables (well-typed) | |
| - Removed bug_co_app test (was testing ill-typed behavior) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit a9ffcb4084c83d67c58220277779d7f4afb72d52 | |
| Merge: 9012033 8f69498 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 23:17:56 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 9012033e56ec1f59b2ab2973281a03aac707ce2c | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 23:17:19 2025 -0300 | |
| Fix collapse to propagate ERA through terms | |
| Terms containing ERA in value positions now collapse to ERA: | |
| - λx.&{} → &{} | |
| - #F{&{}} → &{} | |
| - [0, &{}] → &{} | |
| Special handling for MAT/SWI: ERA in chain position (meaning "no | |
| default case") does not poison the result. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 8f69498654bec1c9005ced7ea38b0902857019e2 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 23:14:30 2025 -0300 | |
| Add stress tests for auto-dup, discover CO app bug | |
| New tests: | |
| - autodup_nightmare: deep nesting with mixed cloned/non-cloned bindings | |
| - autodup_value_path: cloned refs inside dup VALUE positions | |
| - autodup_sup_mix: superpositions with cloned bindings | |
| - autodup_bound_vars: cloning lambdas that capture bound vars | |
| Bug discovered (separate from auto-dup): | |
| - bug_co_app: CO ref as function in dup value produces unresolved subs | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 1d012f864bc359cf23e1fd22922d62be62f4bfb8 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 22:50:31 2025 -0300 | |
| Simplify auto-dup: unify VAR and CO modes into single function | |
| - 92 lines (down from 178, was 4 duplicate functions) | |
| - Uses term_arity() for DRY | |
| - Unified threshold: dep for VAR mode, dep+1 for CO mode | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 8268aa0fb2b967cf2ede0f954c90f80fa99ee1d3 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 22:10:22 2025 -0300 | |
| Fix auto-dup incorrectly shifting inner lambda variables | |
| Variables bound by inner lambdas (like x in λx.x) were being shifted | |
| when they shouldn't. Use initial_idx to track depth into body and only | |
| shift variables pointing outside (val >= depth). | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 3d2ae39456fb03b4cd9a9e44b731ac3d0dd40895 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 21:52:41 2025 -0300 | |
| debug wip | |
| commit 970dd525afd017562ab2d97ace03279159d8d929 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 20:06:09 2025 -0300 | |
| Fix auto-dup crash with 3+ variable uses | |
| The CO1 terms in the dup chain were created with De Bruijn index 1, | |
| but should use index 0 since the parent DUP is always the immediately | |
| enclosing binder from the child's value position. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 3bdd60acd17cc6ecd0c72cd7bd5be7f82b36f924 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 19:51:08 2025 -0300 | |
| debug wip | |
| commit b6d97cc98c3913d1d5de9bbb89a1cf4ccb9fa13a | |
| Merge: 4fae3bc 309e68d | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 19:04:33 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 4fae3bc6dd2b66360cdf405c106e93e1a0c225ef | |
| Merge: 1cccd05 bec8797 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 18:59:16 2025 -0300 | |
| Implement lazy collapse for infinite structure enumeration | |
| Add collapse_step() which lifts SUPs one step at a time instead of | |
| eagerly collapsing the entire term. This allows enumerating infinite | |
| structures like `@X = &L{#Z, #S{@X}}` without stack overflow. | |
| The flatten() function now uses a BFS approach: collapse_step finds | |
| the first SUP, both branches are enqueued, and the process repeats. | |
| Non-SUP results are fully collapsed and normalized before printing. | |
| Also update test runner to infer collapse limit from number of expected | |
| output lines instead of requiring an explicit count. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| NOTE: this was implemented by lorenzo and just adjusted by Claude | |
| commit 309e68d35cbd8d95c396f4414ec2582fee7c4fdf | |
| Merge: 1cccd05 bec8797 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 18:59:16 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 1cccd0536db0d007c7134b7158cdb4f2b3bcc6a0 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 18:59:09 2025 -0300 | |
| rm | |
| commit f2bf39bb496c0b52f1ec8ff21751149c6b5ec242 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 18:58:03 2025 -0300 | |
| Implement lazy collapse for infinite structure enumeration | |
| Add collapse_step() which lifts SUPs one step at a time instead of | |
| eagerly collapsing the entire term. This allows enumerating infinite | |
| structures like `@X = &L{#Z, #S{@X}}` without stack overflow. | |
| The flatten() function now uses a BFS approach: collapse_step finds | |
| the first SUP, both branches are enqueued, and the process repeats. | |
| Non-SUP results are fully collapsed and normalized before printing. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit e075e9c9b1f05b1340d5f7b2a93237e4baf13ec4 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 18:18:47 2025 -0300 | |
| Fix auto-dup label collision with user-defined labels | |
| Start PARSE_FRESH_LAB at 2^23 (0x800000) to namespace auto-generated | |
| dup/sup labels away from user-defined labels which start from 0. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 2c9bb79a877a18b66219c467134351414f8fc440 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 18:05:13 2025 -0300 | |
| bug wip | |
| commit bec87977b43593e434df1e24e276c2563c056b01 | |
| Author: Nicolas Abril <nicolas@higherorderco.com> | |
| Date: Wed Dec 3 21:30:02 2025 +0100 | |
| Add primitive for unscoped lambdas. | |
| We want to be able to write terms like `[(λ$x.0)(1), $x]`, however since Alo terms require deBruijn index, this is not possible. | |
| We can circunvent this by first binding both the unscoped lambda and the unscoped variable to regular scoped variables before their unscoped uses. | |
| The added syntax is `! ${f,v}; t` which translates to the term Unscoped(Lam(f, Lam(v, t))). | |
| This term reduces like this: | |
| ``` | |
| ! ${f, v}; t | |
| ------------------- uns | |
| t(λy.λ$x.y, $x) | |
| ``` | |
| Where t is a term of form `λf. λv. t`. | |
| `f` is a function that receives the body of the lambda and returns the unscoped lambda. | |
| The unscoped lambda `λ$x.bod` is equivalent to `! ${f, v}; ... f(bod)`. | |
| The unscoped variable `$x` is simply `v` itself. | |
| The example given above thus becomes: `!${xf,xv};[xf(0, 1), xv]` which should give the result `[0,1]`. | |
| commit 6f4646f324321054272fe4293bf9755a57009d97 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 17:40:38 2025 -0300 | |
| Resugar MAT/SWI chains when printing | |
| Print chained pattern-matching lambdas in their sugared form: | |
| - λ{0:10;1:20} instead of λ{0:10;λ{1:20;&{}}} | |
| - λ{#A:1;#B:2;default} instead of nested lambdas | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 9be7d3962d2e015e657536abdf1101b92233b32b | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 16:53:03 2025 -0300 | |
| Implement structural equality (Eql) term variant | |
| Add === operator for structural comparison of arbitrary terms: | |
| - Returns #1 if equal, #0 if not | |
| - Strict on left argument first, then right | |
| - Handles all term types: NUM, LAM, CTR, MAT/SWI, USE, NAM, DRY | |
| - SUP/ERA propagate through equality checks | |
| New files: | |
| - clang/term/new/eql.c - EQL constructor | |
| - clang/wnf/eql_*.c - 9 interaction handlers | |
| 22 new tests covering numbers, lambdas, constructors, lists, | |
| strings, nats, nested structures, and superpositions. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 75f301674b6ab017ceb00e18904cb4f42e012eee | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 14:52:03 2025 -0300 | |
| Unify MAT/SWI interactions, keep tags for parser/printer | |
| SWI now shares all interaction code with MAT: | |
| - MAT frame handles both CTR and NUM matching inline | |
| - F_RED_MAT handles both guarded CTR and NUM matching | |
| - Removed 6 redundant SWI-specific interaction files | |
| - SWI tag retained only for parser/printer disambiguation | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit df2524438444534155198e105364861d743e5510 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 14:18:47 2025 -0300 | |
| typo | |
| commit f7af2671877ed0a8d497d1218700d41e17c450bc | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 14:16:51 2025 -0300 | |
| Rename DYS/DYD to DSU/DDU for DynSup/DynDup | |
| Consistent naming: DSU (DynSup) and DDU (DynDup). | |
| - Tags: DYS → DSU, DYD → DDU | |
| - Files: term/new/dys.c → dsu.c, term/new/dyd.c → ddu.c | |
| - Functions: term_new_dys → term_new_dsu, term_new_dyd → term_new_ddu | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit f542fd40e34c97d14d74e0e4b3024f20352bb408 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 14:10:37 2025 -0300 | |
| Split app_red.c into separate files per coding guidelines | |
| The file path must be the function name. Each interaction rule | |
| goes in its own file: | |
| - app_red_era.c: wnf_app_red_era() | |
| - app_red_sup.c: wnf_app_red_sup() | |
| - app_red_lam.c: wnf_app_red_lam() | |
| - app_red_red.c: wnf_app_red_red() | |
| - app_red_nam.c: wnf_app_red_nam() | |
| - app_red_dry.c: wnf_app_red_dry() | |
| - app_red_ctr.c: wnf_app_red_ctr() | |
| - app_red_mat_era.c: wnf_app_red_mat_era() | |
| - app_red_mat_sup.c: wnf_app_red_mat_sup() | |
| - app_red_mat_ctr.c: wnf_app_red_mat_ctr_match/miss() | |
| - app_red_swi_era.c: wnf_app_red_swi_era() | |
| - app_red_swi_sup.c: wnf_app_red_swi_sup() | |
| - app_red_swi_num.c: wnf_app_red_swi_match/miss() | |
| - app_red_use_era.c: wnf_app_red_use_era() | |
| - app_red_use_sup.c: wnf_app_red_use_sup() | |
| - app_red_use_val.c: wnf_app_red_use_val() | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 504c87155fe87339353b0646df66cb7177c2a649 | |
| Merge: 13a67b6 407a54f | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 13:59:36 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 13a67b67949b5ec3ad5389be01d83e1b3b743dd5 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 11:47:45 2025 -0300 | |
| Refactor wnf() with dedicated stack frame tags | |
| This commit refactors the WNF (weak normal form) evaluator to use a cleaner | |
| design with dedicated stack frame tags, eliminating the OP1 term type and | |
| improving the handling of RED (guarded reduction) interactions. | |
| ## Design Changes | |
| ### Stack Frame Tags (0x40+) | |
| Introduced dedicated frame tags separate from term tags: | |
| - F_APP_RED (0x40): ((f ~> □) x) - reducing g in guarded application | |
| - F_RED_MAT (0x41): ((f ~> mat) □) - reducing arg for guarded MAT | |
| - F_RED_SWI (0x42): ((f ~> swi) □) - reducing arg for guarded SWI | |
| - F_RED_USE (0x43): ((f ~> use) □) - reducing arg for guarded USE | |
| - F_OP2_NUM (0x44): (x op □) - reducing y after x reduced to NUM | |
| This separates reduction state from term representation, making the | |
| evaluator logic clearer: "enter only enters, apply only applies/dispatches." | |
| ### Heap Node Reuse | |
| Frames reuse existing heap nodes instead of allocating: | |
| - F_APP_RED stores app_loc; RED read from HEAP[app_loc+0] | |
| - F_RED_MAT/SWI/USE store mat/swi/use in RED's g slot (HEAP[red_loc+1]) | |
| - F_OP2_NUM stores x's numeric value and operator in the frame itself | |
| ### OP1 Elimination | |
| Removed the OP1 term type entirely. Previously OP2 reduced to OP1 when the | |
| first argument became a number. Now F_OP2_NUM frame handles this state | |
| internally without needing a separate term type. | |
| ### Heap Update for RED | |
| When APP's function evaluates to RED (e.g., from expanding a REF), we now | |
| write the RED back to HEAP[app_loc+0]. This ensures F_APP_RED can correctly | |
| read the RED term for recursive function calls like @add and @dbl. | |
| ### Correct Stuck Behavior | |
| When ((f ~> elim) arg) encounters a stuck argument: | |
| - Previously: returned APP(RED(f, elim), arg) - kept eliminator | |
| - Now: returns DRY(f, arg) - drops g, creates stuck application | |
| This produces the correct output format like `add(x, 2n)` instead of | |
| keeping the eliminator in the stuck result. | |
| ## Files Changed | |
| Modified: | |
| - hvm4.c: Added frame tag definitions, removed OP1 | |
| - wnf/_.c: Rewrote evaluator with new frame design | |
| - term/arity.c: Removed OP1 case | |
| - parse/auto_dup.c: Removed OP1 case | |
| - print/term.c: Removed OP1 printing | |
| Deleted: | |
| - term/new/op1.c: No longer needed | |
| - wnf/op1_*.c: Replaced by op2_num_*.c | |
| - wnf/op2_num.c: Logic moved inline to wnf/_.c | |
| Added: | |
| - wnf/op2_num_era.c: ERA interaction after first NUM | |
| - wnf/op2_num_num.c: NUM+NUM computation (renamed from op1_num.c) | |
| - wnf/op2_num_sup.c: SUP interaction after first NUM | |
| All 124 tests pass. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| ... | |
| commit aab8ef62002006d4936e6b6ca696bb6bfc035c3f | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 09:58:44 2025 -0300 | |
| Add operator precedence to parser | |
| Implements precedence climbing so that e.g. 2 * 3 + 4 parses as | |
| (2 * 3) + 4 instead of 2 * (3 + 4). Operators are left-associative. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit ea7c0dfc3a36de7e1654e92fa2abf72f24b3e499 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 09:39:01 2025 -0300 | |
| Replace @@opr syntax with infix operators | |
| - Add infix operator parsing: x + y, x * y, x == y, etc. | |
| - Add new operators: + - * / % && || ^ ~ << >> == != < <= > >= | |
| - Remove deprecated @@opr(x, y) syntax | |
| - Update all test files to use new syntax | |
| - Update README documentation | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| ... | |
| commit b27bf7a51300ec344f953f6b42749155770d82bf | |
| Merge: 2d90217 4b90228 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 08:41:42 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 2d90217144eaed66cf1cd77a789585fde7c32988 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 08:41:36 2025 -0300 | |
| thing | |
| commit ef43976be5025a8f5a8c5a680991ece6eb8ff928 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 08:35:00 2025 -0300 | |
| remove | |
| ... | |
| commit 00fe6013faaf77bee1bfe8ce481f9b39e10444d8 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 08:35:00 2025 -0300 | |
| remove | |
| commit 219ec18ef0f29c5329901cfea0da0313941a222d | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 08:14:17 2025 -0300 | |
| Replace prims with Op2/Op1 interactions | |
| - Remove prim/ directory entirely | |
| - Add OP2, OP1, DYS, DYD tags for numeric ops and dynamic sup/dup | |
| - Op2(opr, x, y): strict on x, creates Op1 when x is NUM | |
| - Op1(opr, x, y): strict on y, performs operation when y is NUM | |
| - DSu(lab, a, b): strict on lab, creates SUP when lab is NUM | |
| - DDu(lab, v, f): strict on lab, creates DUP when lab is NUM | |
| - Add proper wnf interaction files for all new operations | |
| - Add app_swi_* and use_* interaction files | |
| - Update README with new grammar and interaction rules | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit e8d2ece72ca55a8ced0cb596bff9fbfd361a8e60 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 07:49:50 2025 -0300 | |
| Remove prelude, implement ERA/SUP handling directly in C prims | |
| - Remove prelude wrappers (@add, @mul, etc.) - prims now called as @@add, @@mul directly | |
| - Add prim/op1.c and prim/op2.c generic handlers with ERA/SUP pattern matching | |
| - All numeric prims delegate to op1/op2 for consistent ERA/SUP handling | |
| - prim_dup and prim_sup now handle ERA/SUP on label argument | |
| - Parser generates @@dup/@@sup primitives directly for dynamic dup/sup syntax | |
| - Fix parse/auto_dup.c to recurse into P00..P16 primitive arguments | |
| - Update all tests to use @@ syntax for numeric primitives | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 17c8c76d7a9bd63d724ed8a1b212631a35bd65c7 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Wed Dec 3 00:12:47 2025 -0300 | |
| dynamic dup syntax fix wip | |
| commit 3c6203d04b9763cff0e70fca84d166431b4157b5 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 23:36:25 2025 -0300 | |
| dup prim before calling it | |
| as an improvement over the previous HVM4, pattern-matching isn't done on | |
| C prims; instead, we do them using native λ-matches, on prelude | |
| functions that wrap around the @@prim, like: | |
| @add = λ{λx.λ{λy.@@add(x,y)}} | |
| this greatly reduces complexity of the C prim files, since they're | |
| guaranteed to receive the terms they need, and not sups/eras. yet, this | |
| alonw isn't enough. consider: | |
| //(λ{λx.λ{λy.@@eq(x,y)}} &A{0,0} 0) | |
| //--------------------------------- | |
| //! F &A = λ{λx.λ{λy.@@eq(x,y)}} | |
| //(&A{(F₀ 0),(F₁ 0)} 0) | |
| //--------------------------------- | |
| //! F &A = λx.λ{λy.@@eq(x,y)} | |
| //(&A{(λ{F₀} 0),(λ{F₁} 0)} 0) | |
| //--------------------------------- | |
| //! F &A = λ{λy.@@eq(&A{x0,x1},y)} | |
| //(&A{(λ{λx0.F₀} 0),(λ{λx1.F₁} 0)} 0) | |
| //--------------------------------- | |
| //! F &A = λ{λy.@@eq(&A{0,0},y)} | |
| //(&A{F₀,F₁} 0) | |
| //--------------------------------- | |
| //! F &A = λy.@@eq(&A{0,0},y) | |
| //(&A{λ{F₀},λ{F₁}} 0) | |
| //--------------------------------- | |
| //! F &A = @@eq(&A{0,0},&A{y0,y1}) | |
| //(&A{λ{λy0.F₀},λ{λy1.F₁}} 0) | |
| //--------------------------------- | |
| //! F &A = @@eq(&A{0,0},&A{y0,y1}) | |
| //(&A{λ{λy0.F₀},λ{λy1.F₁}} 0) | |
| //--------------------------------- | |
| //! F &A = @@eq(&A{0,0},&A{y0,y1}) | |
| //&A{(λ{λy0.F₀} 0),(λ{λy1.F₁} 0)} | |
| //--------------------------------- | |
| //! F &A = @@eq(&A{0,0},&A{y0,y1}) | |
| //&A{(λ{λy0.F₀} 0),(λ{λy1.F₁} 0)} | |
| //--------------------------------- | |
| //! F &A = @@eq(&A{0,0},&A{0,0}) | |
| //&A{F₀,F₁} | |
| note how we still end up with sups on the @@eq call. the reason is that | |
| wnf will reduce it *before* the dup takes place, so, these sups will be | |
| passed to the C prim function. to avoid that, we block prim_call of a | |
| pri that is surrounded by a dup, and implement dup-pri interaction. this | |
| will force @@eq to be dup'd *before* prim_call is called, as needed. | |
| commit 887310ca8dd4827595e8b7f7b5cadb459e22a07d | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 21:28:55 2025 -0300 | |
| Make {} optional for nullary constructors | |
| #Foo now parses as #Foo{}, allowing cleaner syntax for constructors | |
| without arguments. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit e3f866e4024451244bc83aa955422318afd1baa8 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 20:25:55 2025 -0300 | |
| Add affine type checking and auto-dup for cloned variables | |
| This commit adds support for cloned variables that can be used multiple | |
| times, with automatic dup insertion at parse time. | |
| ## New Syntax | |
| - `λ&x. body` - Cloned lambda variable, allows multiple uses of x | |
| - `! &x = val; body` - Cloned let binding | |
| - `!! &x = val; body` - Cloned strict let binding | |
| ## How Auto-Dup Works | |
| When a cloned variable is used N times, the parser inserts N-1 dups to | |
| duplicate the value. For example: | |
| ``` | |
| λ&x. [x] → λx. [x] // 1 use: no dup | |
| λ&x. [x,x] → λx. !d0&=x; [d0₀,d0₁] // 2 uses: 1 dup | |
| λ&x. [x,x,x] → λx. !d0&=x; !d1&=d0₁; [d0₀,d1₀,d1₁] // 3 uses: 2 dups | |
| λ&x. [x,x,x,x] → λx. !d0&=x; !d1&=d0₁; !d2&=d1₁; [d0₀,d1₀,d2₀,d2₁] | |
| ``` | |
| The transformation walks the term, replacing VAR references with CO0/CO1 | |
| references to the appropriate dup, and shifting outer-scope references. | |
| ## Affine Checking | |
| - Non-cloned variables can only be used 0 or 1 times | |
| - Error if a non-cloned variable is used more than once | |
| - Error if an undefined variable is referenced | |
| ## Files Added | |
| - `clang/parse/auto_dup.c` - Auto-dup transformation | |
| - `clang/nick/b64_to_letter.c`, `to_str.c` - Name printing for errors | |
| - `test/autodup_*.hvm4` - Tests for auto-dup feature | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 5be0aae40d9f0af7fa4d57cf73b54e1f5b8350cd | |
| Merge: 1d90552 3714e52 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 19:05:53 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 1d90552718d280620b21acb9a5c3d1f915974b8b | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 19:05:22 2025 -0300 | |
| Fix NAM_* constants and add Unicode support | |
| Fix incorrect base-64 encoded constructor name constants: | |
| - NAM_SUC: 187165 (SRC) -> 187357 (SUC) | |
| - NAM_NIL: 166438 (NNL) -> 166118 (NIL) | |
| - NAM_CON: 121000 (CHN) -> 121448 (CON) | |
| - NAM_CHR: 120364 (CxR) -> 121004 (CHR) | |
| Add UTF-8 support for parsing and printing: | |
| - parse/utf8.c: decode UTF-8 codepoints from source | |
| - print/utf8.c: encode codepoints as UTF-8 for output | |
| - Strings and chars now store Unicode codepoints, not bytes | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 3714e52964fdc21817cbe46757938acee6717951 | |
| Author: Nicolas Abril <nicolas@higherorderco.com> | |
| Date: Tue Dec 2 22:57:28 2025 +0100 | |
| Add syntax for dynamic label sup and dup | |
| commit aa7e9e9642ea8285844fd63b42bda69839c5ef4c | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 18:46:06 2025 -0300 | |
| Add auto-label dup syntax | |
| !x& = val desugars to !x&N = val where N is a fresh global counter. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 393e1274d1a8f9adf9483c4408e83235f0bff705 | |
| Merge: 344e461 7cb151d | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 18:35:14 2025 -0300 | |
| Merge remote changes, update prelude | |
| Resolved conflict: keep prelude in prelude/_.c, update @dup and @sup | |
| to use simpler syntax without nested λ{} wrappers. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 344e4613420518d7dfea60ba5a0800aba16fceec | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 18:31:07 2025 -0300 | |
| Allow _: prefix for default case in match | |
| λ{0:f; _:g} is now equivalent to λ{0:f; g} | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 7cb151d180ca6a766aa52f3c4f39fa0a7fd57b12 | |
| Author: Nicolas Abril <nicolas@higherorderco.com> | |
| Date: Tue Dec 2 22:28:14 2025 +0100 | |
| Don't match on non-label parts of dynamic label dups and sups | |
| commit 077462e8936bf6d2f0bcb3da22e344351451dc3f | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 18:24:23 2025 -0300 | |
| Add let syntax sugar | |
| - `! x = val; body` desugars to `(λx.body)(val)` | |
| - `!!x = val; body` desugars to `(λ{λx.body(x)})(val)` (strict) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 19f654868a2b02a95e338a0842c3c24638f68e37 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 18:13:52 2025 -0300 | |
| Move prelude to prelude/_.c | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit d6afc786227a661fbe53c10b0e0a083dd383f8e6 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 17:48:52 2025 -0300 | |
| Add chained numeric switch syntax | |
| Support multiple cases in SWI like MAT: λ{0:a; 1:b; 2:c; default} | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit f8a846ce742b228a98851d93889365a8ef661fe5 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 17:31:30 2025 -0300 | |
| Move built-in name constants to nick/names.c | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit f6961cd0983a3fee62d55d6a8e1fffc4fa59dd42 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 17:08:38 2025 -0300 | |
| Add table module for function name lookups | |
| Introduces a global id→name table so functions can have arbitrarily | |
| long names. The EXT field now stores a unique ID that indexes into | |
| this table, rather than a 24-bit encoded name. | |
| - table/_.c: TABLE array and TABLE_LEN counter | |
| - table/find.c: name→id lookup (finds existing or creates new) | |
| - table/get.c: id→name lookup for printing | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit ba8e62e0cc49fdd3db03bf1c81b99d37cabf7ed0 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 16:04:51 2025 -0300 | |
| words | |
| commit bcd386bb0da1ea4255fa42a6ef2b29888a0ed087 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 13:02:27 2025 -0300 | |
| Add CLAUDE.md for Claude Code guidance | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 7c0f7ab99654a370e7f5a19cdae47f3667e67031 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 12:55:42 2025 -0300 | |
| Add file organization rules to style guide | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit e0aee16b7a29a85591b2ba16bdfba56117635f96 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 12:40:14 2025 -0300 | |
| remove title part of style.md | |
| commit 9886cf9b9ab7423d6c94b92dd133dad09aec5c16 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 11:55:33 2025 -0300 | |
| Add syntax sugar for Nat, List, Char, String | |
| Terms: | |
| - 0n, 3n → #ZER{}, #SUC{#SUC{#SUC{#ZER{}}}} | |
| - 3n+x → #SUC{#SUC{#SUC{x}}} | |
| - [] → #NIL{} | |
| - [a,b,c] → #CON{a,#CON{b,#CON{c,#NIL{}}}} | |
| - h <> t → #CON{h,t} | |
| - 'x' → #CHR{120} | |
| - "foo" → #CON{#CHR{102},#CON{#CHR{111},#CON{#CHR{111},#NIL{}}}} | |
| Pattern matching: | |
| - λ{0n: z; 1n+: s; d} → λ{#ZER: z; λ{#SUC: s; d}} | |
| - λ{[]: n; <>: c; d} → λ{#NIL: n; λ{#CON: c; d}} | |
| Stringification prints sugar forms when applicable. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 8e255eeaab9abc6b2bae126504f65d0c0859c45b | |
| Merge: 4392426 5634221 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 10:01:09 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 43924268ed4c4fd6c054aad54b826d702649905e | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 09:39:56 2025 -0300 | |
| Performance Regression Fix (back to 180 MIPS) | |
| After commits `12b022d` and `eb5727d`, the `bench/cnots.hvm4` benchmark dropped from ~180 MIPS to ~140 MIPS—a significant ~22% performance regression. | |
| The regression was caused by adding new term tags (SWI, USE, P00-P16) which expanded the tag range from 0-30 to 0-49. This affected the compiler's ability to generate efficient switch statements in the hot `wnf()` function, resulting in larger jump tables with worse cache behavior and branch prediction. | |
| Solution | |
| Three key optimizations recovered the lost performance: | |
| 1. **Tag Reordering** (`hvm4.c`): Moved the hottest tags to positions 0-7: | |
| - `APP=0, VAR=1, LAM=2, CO0=3, CO1=4, SUP=5, DUP=6, ALO=7` | |
| - This allows the compiler to generate a tighter, more cache-friendly jump table for the most frequently executed cases. | |
| 2. **Branch Prediction Hints** (`wnf/_.c`): Added `__builtin_expect(DEBUG, 0)` to both debug-print conditionals, telling the compiler the debug path is cold and should not pollute the hot instruction cache. | |
| 3. **Hot Function Attribute** (`wnf/_.c`): Added `__attribute__((hot))` to the `wnf()` function, hinting the compiler to prioritize optimization and code placement for this function. | |
| Additional Fixes for Correctness | |
| - Uncommented SWI/USE/P00-P16 handling code that was accidentally left commented | |
| - Fixed the apply loop condition from `while (S_POS > 0)` to `while (S_POS > base)` to support recursive `wnf()` calls needed by primitives | |
| Results | |
| - Before fix: ~140 MIPS | |
| - After fix: ~175 MIPS (peak ~177 MIPS) | |
| - All tests passing including `prim_add`, `swi_0`, `swi_1` | |
| note by taelin: actually getting 180 MIPS with my CPU cold! | |
| commit 56342215cca95e6a1747e54a936c41b9e0effedd | |
| Author: Nicolas Abril <nicolas@higherorderco.com> | |
| Date: Tue Dec 2 13:49:07 2025 +0100 | |
| Make sp0 and sp1 prelude fns use the primitives directly | |
| commit 4af67404788a22dec4fe504c54aaadd285d8fbe5 | |
| Author: Nicolas Abril <nicolas@higherorderco.com> | |
| Date: Tue Dec 2 13:47:17 2025 +0100 | |
| Add dynamic label dup and sup primitives, and split hash functions to the prelude | |
| commit bc40c8af8372a84c358fbdb6ea7b4ebc60e4182a | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Tue Dec 2 08:29:29 2025 -0300 | |
| perf regression debug prompt | |
| commit 3fe8da027ff6c46e9efce700de381a4c62d82077 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 22:29:51 2025 -0300 | |
| add lambda eval test | |
| commit 0e3c954a35926e795375aca717e5144ce597a27c | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 22:16:38 2025 -0300 | |
| Embed prelude statically in binary | |
| Previously the prelude was loaded dynamically from prelude/book.hvm4, | |
| which only worked when running from the project root directory. Running | |
| from other directories (e.g., test/) would fail to find the prelude. | |
| Now the prelude is embedded as a static string constant in the C binary, | |
| eliminating the external file dependency and making the executable | |
| self-contained. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit b19dc6597a429a0f6a16c7dac9fe7f79e3f54716 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 18:28:04 2025 -0300 | |
| Remove prim_add_nested (merged into prim_add) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit cb97d75422fc568a02b8f4fc97f698ed3f5518da | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 18:25:24 2025 -0300 | |
| Make primitive tests use nested calls | |
| Update prim_add, prim_mul, prim_sub, prim_eq_t, prim_lt_t to use | |
| nested primitive calls, testing that primitives properly reduce | |
| their arguments via wnf(). Remove separate prim_add_nested test. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 4ecc1102b87453aaaa4676b3b5c6020eeb5e7a27 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 18:21:56 2025 -0300 | |
| Add comprehensive primitive tests with descriptive names | |
| Replace prim_0/1/2/3 with named tests for all 17 primitives: | |
| - Arithmetic: add, add_nested, sub, mul, div, mod | |
| - Bitwise: and, or, xor, lsh, rsh, not | |
| - Comparison: eq_t/f, ne_t/f, lt_t/f, le_t/f, gt_t/f, ge_t/f | |
| Each comparison primitive has both true and false test cases. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 3b76d2b404ed812a49c8715291c1243974ffd545 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 18:09:06 2025 -0300 | |
| Add all u32 numeric primitives | |
| Arithmetic: | |
| - add, sub, mul, div, mod | |
| Bitwise: | |
| - and, or, xor, lsh, rsh, not | |
| Comparison (return 0 or 1): | |
| - eq, ne, lt, le, gt, ge | |
| Each primitive has its own file in clang/prim/ following the codebase | |
| style with interaction rule comments. All primitives call wnf() on | |
| their arguments internally and abort with an error if given non-NUMs. | |
| Prelude updated with wrapper functions for all primitives. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 8c45aee958adb0345fde2a2fec70b2eff8a49ded | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 17:54:02 2025 -0300 | |
| Add prelude with built-in functions | |
| - Create prelude/book.hvm4 containing built-in function definitions | |
| - Parse prelude automatically before user file in main.c | |
| - Move @add definition from test files to prelude | |
| The prelude provides standard library functions that are always available. | |
| User code can use @add directly without defining it. This keeps test files | |
| cleaner and ensures consistent primitive wrapper definitions. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 12b022d9271a4a0fc4d6b63e8e336b7ca3225139 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 17:26:24 2025 -0300 | |
| Add primitives (PRI), switch (SWI), and strict evaluation (USE) terms | |
| Primitives (PRI): | |
| - New term variant for calling C functions directly from HVM4 | |
| - Syntax: @@name(x,y,z,...) where name is 4 letters encoded as 24-bit value | |
| - Tags P00-P16 (values 33-49) encode arity in the tag itself | |
| - Primitives are entered directly in WNF - they have no strict arguments | |
| - Each primitive is responsible for calling wnf() on its arguments internally | |
| - First primitive: @@add(a,b) for addition of two NUMs | |
| Switch (SWI): | |
| - New term for number pattern matching: λ{123: f; g} | |
| - When applied to a NUM, if it equals the pattern return f, else return (g num) | |
| - Tag 31, stores match value in ext field, f and g in heap | |
| Strict evaluation (USE): | |
| - New term for forcing argument evaluation: λ{f} | |
| - Reduces its argument to WNF, then applies f to the result | |
| - Tag 32, stores f in heap | |
| - Used to build strict wrappers for primitives | |
| Primitive wrappers: | |
| - Primitives receive their arguments as ALO refs (book-level variables) | |
| - To get strict evaluation, wrap primitives with USE lambdas: | |
| @add = λ{λx.λ{λy.@@add(x,y)}} | |
| - The USE wrappers reduce arguments to WNF before binding them | |
| - The primitive then calls wnf() on its ALO args to get the actual values | |
| Re-entrant WNF: | |
| - wnf() now saves initial S_POS as 'base' instead of resetting to 0 | |
| - Apply phase loops while S_POS > base (not > 0) | |
| - This allows nested wnf() calls from within primitives without | |
| corrupting the outer evaluation's stack frames | |
| - Critical for primitives that need to reduce their arguments | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit eb5727d927d226c7426df37a31503db196e3a3ec | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 16:49:12 2025 -0300 | |
| prims WIP | |
| commit 744b69984da16becbf4cce148dc9ba92772a6b40 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 16:08:09 2025 -0300 | |
| remove haskell implementation | |
| I've learned what I had to and know the way forward | |
| commit d3fd0a2415a946e453f0598526de93d82f9654eb | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 14:11:33 2025 -0300 | |
| remove regression_0, turn this into an issue please | |
| commit 631079a1e416976f2ec527b30e6ef81306cf55e9 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 13:48:07 2025 -0300 | |
| Revert to NAM/DRY tags for stuck terms | |
| Brings back NAM and DRY as first-class tags instead of using #VAR/#APP | |
| constructors, which had issues for other reasons. | |
| C implementation: | |
| - Add NAM (tag 0) and DRY (tag 1) to tag definitions | |
| - Add term constructors: term/new/nam.c, term/new/dry.c | |
| - Add interaction rules: app_nam, app_dry, dup_nam, dup_dry, alo_nam, alo_dry | |
| - Update app_ctr to create DRY instead of Ctr _APP_ | |
| - Update snf to use NAM for stuck variables | |
| - Update printer to display NAM/DRY as regular variable/application syntax | |
| Haskell implementation: | |
| - Add Nam and Dry constructors to Term type | |
| - Add dup_nam, dup_dry, app_nam, app_dry interaction functions | |
| - Update app_ctr to create Dry | |
| - Update snf to use Nam for stuck variables | |
| - Update Show instance to print NAM/DRY like regular terms | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit e3b9344ee7b2aebcf40d11c01c5b0bb2d3cb8470 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 13:28:42 2025 -0300 | |
| Refactor print module: remove globals, use FILE* parameter | |
| - Remove stringifier globals (STR_MODE, TERM_BUF, TERM_BUF_POS, TERM_BUF_CAP) | |
| - Pass FILE* through print functions instead of using global state | |
| - Simplify by using standard stdio functions (fputc, fputs, fprintf) | |
| - Delete unused files: str_putc.c, str_puts.c, str_uint.c, is_app.c, | |
| term_to_str.c, term_buf_init.c, term_buf_free.c | |
| - Consolidate print/term.c and rename functions (remove _str_ infix) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit a0d9ed95fc99f489b1270b00dddb2b6c4e8f6d64 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Mon Dec 1 00:07:05 2025 -0300 | |
| Add interaction rule comments to WNF files, merge clone functions | |
| - Add interaction rule comments (from README.md) to all wnf/*.c files | |
| - Merge term_clone_at, term_clone, term_clone_many into term/clone.c | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 43efd4f37d394e6d05afe6903b47ef5bfd8ba53b | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 23:48:14 2025 -0300 | |
| Add compiled binaries to gitignore | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 21685e81460e6018a45705dd93a955e0513ee59b | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 23:43:42 2025 -0300 | |
| Fix lambda match body parsing for trailing } | |
| Handle the case where a lambda match body ends without a default | |
| term (just closing }), which returns ERA implicitly. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 0b0de04300fee91b7cd0790dcb639d2c25f01740 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 23:40:59 2025 -0300 | |
| Refactor C module structure and naming conventions | |
| - Move all type declarations, structs, #defines and globals to hvm4.c | |
| - Extract documentation to README.md and STYLE.md | |
| - Rename letter/ to nick/ with updated function names | |
| - Split parse/term.c into parse/term/*.c with parse_term_* naming | |
| - Move term constructors to term/new/ with term_new_* naming | |
| - Rename term_mark_sub/term_clear_sub to term_mark/term_unmark | |
| - Rename term_clone functions (not constructors, stay in term/) | |
| - Module files now contain only functions, no declarations | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 3fdd63f2b556141635d8d64630d9290337c63c34 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 23:01:07 2025 -0300 | |
| Modularize C implementation into separate files | |
| Split hvm4.c into modules with one function per file: | |
| - term/: types, tags, bit layout, constructors | |
| - heap/: allocation, substitution helpers | |
| - book/: book capacity and globals | |
| - letter/: base64 alphabet encoding | |
| - sys/: error, path_join, file_read | |
| - print/: stringifier functions | |
| - parse/: parser state and functions | |
| - wnf/: WNF evaluator and interactions | |
| - snf/: strong normal form | |
| - collapse/: collapse and inject | |
| Function naming convention: module_function (e.g., term_tag, heap_alloc) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit b18f310d87c6bc193b04630a86e3725a4cc64685 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 22:02:21 2025 -0300 | |
| pre split wip | |
| commit 70f46c204078240abebd09cd29369ede541e6581 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 21:35:29 2025 -0300 | |
| Remove NAM/DRY tags, use #VAR{} and #APP{} CTRs for stuck terms | |
| - Remove NAM and DRY tags, renumber remaining tags | |
| - Stuck variables now represented as #VAR{#name{}} | |
| - Stuck applications now represented as #APP{f,x} | |
| - Add _VAR_ and _APP_ constants for special CTR names | |
| - Extract str_app helper for shared application spine printing | |
| - Simplify arity_of, WNF, and stringifier | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 991125e5f1d18e3818e3779b7f8a4050c9400c48 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 21:19:51 2025 -0300 | |
| Replace CTR/CTR_MAX_ARI with individual C00-C16 tags | |
| - Define C00 through C16 (tags 13-29) for constructor arities 0-16 | |
| - Update all CTR ... CTR + CTR_MAX_ARI ranges to C00 ... C16 | |
| - Change arity calculation from tag(t) - CTR to tag(t) - C00 | |
| - Change constructor creation from CTR + ari to C00 + ari | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 64c3bc73538c896681b0a53efbf9a7288a5f2803 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 21:04:17 2025 -0300 | |
| Remove Dsp and Ddp, keep only Num | |
| - Remove Dsp (dynamic superposition) and Ddp (dynamic dup) from Term type | |
| - Remove DSP/DDP tags from C implementation | |
| - Remove parsing, stringification, and evaluation for Dsp/Ddp | |
| - Simplify arity_of, bruijn, wnf, snf functions | |
| - Renumber NUM tag from 32 to 30 | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 28aaba85734fb8339316d153c6ed4b34bffb0c1d | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 20:26:41 2025 -0300 | |
| Change Num contents from Int to Word32 | |
| - Import Data.Word (Word32) | |
| - Change Term's Num constructor from Int to Word32 | |
| - Add fromIntegral conversions when using Num value as Lab (in Dsp/Ddp) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 7bef28d580e4c01821581d16d243df705ce758eb | |
| Merge: 5440004 842f874 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 20:22:02 2025 -0300 | |
| Merge branch 'main' of github.com:victortaelin/hvm4-spec | |
| commit 54400047d04363481538c6bd35304dfe251b6414 | |
| Merge: 05d4dd4 8a45fbe | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 20:17:53 2025 -0300 | |
| Merge bendgen branch: add Dsp, Ddp, Num; remove Suc, Sp0, Sp1 | |
| - Reorder Term type to place Dsp, Ddp, Num at the end | |
| - Remove Suc (successor), Sp0, Sp1 (splitters) from both implementations | |
| - Keep only dynamic superposition (Dsp), dynamic dup (Ddp), and Num | |
| - Update all pattern-matching functions to respect new Term order | |
| - Add dup_num handler for duplicating numeric values | |
| - Add enum_regression test (currently fails due to removed /Sp0, /Sp1 syntax) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 05d4dd4cc2b300646a9ea02cb60c98b37fe68eb6 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 18:49:59 2025 -0300 | |
| align | |
| commit 010cded18054b62014e05843ce90fee71c26835a | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 10:29:03 2025 -0300 | |
| Simplify Term type by replacing Nam/Dry with Ctr VAR/APP | |
| Remove dedicated Nam and Dry term variants and represent them using | |
| the existing Ctr type instead: | |
| - Nam "x" becomes Ctr VAR [Ctr x []] | |
| - Dry f x becomes Ctr APP [f, x] | |
| Add special pretty-printing for VAR/APP constructors to maintain | |
| identical output. Add app_ctr interaction for (#Foo{...} x) -> #APP{...}. | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 842f87426d4ebda342e76987e1ae4f3cb402c1c8 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 07:40:02 2025 -0300 | |
| proper name | |
| commit a5ec60ffc448e1cd9937c658498bb5ec371746fc | |
| Merge: 90c522b 8a45fbe | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 07:38:32 2025 -0300 | |
| Merge branch 'bendgen' | |
| commit 90c522b61da64f1908f9512ff421b42964e31d42 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 07:20:29 2025 -0300 | |
| move gpu evaluators to another branch | |
| commit 39d702c9880279a0d79a9dcb5ef71764b73a096e | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 07:13:35 2025 -0300 | |
| metal adjusts | |
| commit 4e7b407f905946e950b062039574107475b9e38b | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sun Nov 30 06:51:16 2025 -0300 | |
| Revert "wip" | |
| This reverts commit 5e9e91b2edfedeea3dbb9660572a6c17a181a8a2. | |
| commit 5e9e91b2edfedeea3dbb9660572a6c17a181a8a2 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sat Nov 29 22:59:48 2025 -0300 | |
| wip | |
| commit 02541c48da3da53ca35d64f3ffb5094cf3d45a39 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sat Nov 29 22:40:09 2025 -0300 | |
| wip | |
| commit 0b43aef600e4bd919c81d620f7e342a355963a18 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sat Nov 29 22:17:09 2025 -0300 | |
| wip - adjust layout on metal | |
| commit 6f3aac355117c2c3c32b7588e5e33cdbe2e01c42 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sat Nov 29 21:09:01 2025 -0300 | |
| 40-bit metal wip | |
| commit 2dae12641057983bcb6b99dc3de949520ace6788 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sat Nov 29 16:57:56 2025 -0300 | |
| metal: optimize heap layout for direct physical addressing | |
| - Simplify Heap struct to just base pointer with direct base[idx] access | |
| - Move coalesced allocation logic to heap_alloc() which returns physical indices | |
| - Physical layout: thread N allocates at heap_base + k * simd_width for slot k | |
| - Update all multi-slot node accesses to use loc + i * simd_width stride | |
| - Remove unnecessary to_physical/to_local indirection | |
| Performance improvement: | |
| - Single thread: 0.91 MIPS (was 0.79, +15%) | |
| - 1024 threads: 619 MIPS (was 445, +39%) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> | |
| commit 94f7bb1c297365d270a3a2d3000d4b313a21c7b2 | |
| Author: VictorTaelin <victortaelin@gmail.com> | |
| Date: Sat Nov 29 11:17:20 2025 -0300 | |
| metal: remove single-threaded code, keep only GPU multi-threaded evaluator | |
| - Remove duplicate single-threaded kernel and helper functions | |
| - Unify to single hvm_run kernel with warp-coalesced memory layout | |
| - Simplify Swift host code to only support multi-threaded execution | |
| - File size reduced from 2320 to 941 lines (59% smaller) | |
| 🤖 Generated with [Claude Code](https://claude.com/claude-code) | |
| Co-Authored-By: Claude <noreply@anthropic.com> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment