Created
December 7, 2025 16:13
-
-
Save VictorTaelin/57d8082c7ffb97bd4755dd39815bd0cc to your computer and use it in GitHub Desktop.
HM4 commit history
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> | |
| ... |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment