From 83f21428b2f3a012f9c9bf9c4b385433030af1df Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 23 Sep 2026 09:57:45 +0000 Subject: [PATCH 1/2] examples: call uncurried globals with all arguments at once (#11) ds_uncurry compiles `lambdas (a b ...)` definitions into multi-argument functions, so a single-argument call_global now runs the body with missing arguments instead of returning a partial closure. The eval example failed decoding that result as a closure, and fsm hit a match failure. Pass all arguments in one call_global instead. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011Vsc7gM2NbYCYBxR6BsFqG --- examples/eval/src/main.rs | 18 ++---------------- examples/fsm/src/main.rs | 8 +++----- 2 files changed, 5 insertions(+), 21 deletions(-) diff --git a/examples/eval/src/main.rs b/examples/eval/src/main.rs index 74d356f..01f35b1 100644 --- a/examples/eval/src/main.rs +++ b/examples/eval/src/main.rs @@ -6,8 +6,6 @@ use cortex_m_semihosting::{debug, hprintln}; use panic_halt as _; use encore_vm::error::ExternError; -use encore_vm::ffi::VmCallable; -use encore_vm::value::GlobalAddress; use encore_vm::vm::Vm; #[path = "../../common/qemu_clock.rs"] @@ -31,19 +29,6 @@ enum OptionNat { #[ctor(ctors::SOME)] Some(i32), } -// step : curried 3-argument call (TEST_ADD is a -> b -> fuel -> Option nat) -fn call3( - vm: &mut Vm, - global: GlobalAddress, - a: i32, - b: i32, - fuel: i32, -) -> Result { - let f1: VmCallable = vm.call_global(global, (a,))?; - let f2: VmCallable = vm.call_closure(&f1, (b,))?; - vm.call_closure(&f2, (fuel,)) -} - #[entry] fn main() -> ! { qemu_clock::start(cortex_m::Peripherals::take().unwrap().SYST); @@ -52,7 +37,8 @@ fn main() -> ! { vm.set_clock(qemu_clock::now_ns); for &(a, b, fuel) in &[(1i32, 1i32, 500i32), (1, 2, 1000), (2, 2, 3000)] { - let result: OptionNat = call3(&mut vm, funcs::TEST_ADD, a, b, fuel) + // TEST_ADD : a -> b -> fuel -> Option nat, uncurried into a 3-ary function. + let result: OptionNat = vm.call_global(funcs::TEST_ADD, (a, b, fuel)) .unwrap_or_else(|e| vm_exit_err(e)); match result { diff --git a/examples/fsm/src/main.rs b/examples/fsm/src/main.rs index 1acd2f2..9d918df 100644 --- a/examples/fsm/src/main.rs +++ b/examples/fsm/src/main.rs @@ -6,7 +6,7 @@ use cortex_m_semihosting::{debug, hprintln}; use panic_halt as _; use encore_vm::error::ExternError; -use encore_vm::ffi::{VmCallable, VmList}; +use encore_vm::ffi::VmList; use encore_vm::vm::Vm; encore_vm::encore_program!(env!("OUT_DIR")); @@ -51,10 +51,8 @@ fn vm_exit_err(e: ExternError) -> ! { } fn run_step(vm: &mut Vm, state: i32, event: Event) -> StepResult { - let partial: VmCallable = vm - .call_global(funcs::STEP, (state,)) - .unwrap_or_else(|e| vm_exit_err(e)); - vm.call_closure(&partial, (event,)) + // STEP : State -> Event -> Pair, uncurried into a 2-ary function. + vm.call_global(funcs::STEP, (state, event)) .unwrap_or_else(|e| vm_exit_err(e)) } From a369192438e6f816de6d7a82c7f6208ffc7a0586 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 23 Sep 2026 09:57:45 +0000 Subject: [PATCH 2/2] examples/eval: shift down after beta substitution (#11) beta computed shift(+1, subst(0, shift(+1, arg), body)), but de Bruijn beta reduction needs a downward shift after substituting, to account for the removed binder. Free variables drifted upward, so read_church never recognized a numeral and every test_add reported "timeout". Add an unshift and use it in beta; church 1+1, 1+2 and 2+2 now evaluate to 2, 3 and 4. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011Vsc7gM2NbYCYBxR6BsFqG --- examples/eval/eval.scm | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/examples/eval/eval.scm b/examples/eval/eval.scm index e6aacaa..7c7305f 100644 --- a/examples/eval/eval.scm +++ b/examples/eval/eval.scm @@ -28,8 +28,17 @@ (@ shift `((lambda (n) (+ n 1)) ,`(0)) `(0) s) body))) ((App t1 t2) `(App ,(@ subst j s t1) ,(@ subst j s t2)))))) +(define unshift (lambdas (c t) + (match t + ((Var n) + (match (@ leb c n) + ((True) `(Var ,(- n 1))) + ((False) `(Var ,n)))) + ((Abs body) `(Abs ,(@ unshift `((lambda (n) (+ n 1)) ,c) body))) + ((App t1 t2) `(App ,(@ unshift c t1) ,(@ unshift c t2)))))) + (define beta (lambdas (body arg) - (@ shift `((lambda (n) (+ n 1)) ,`(0)) `(0) + (@ unshift `(0) (@ subst `(0) (@ shift `((lambda (n) (+ n 1)) ,`(0)) `(0) arg) body)))) (define whnf (lambdas (fuel t)