feat: complete evidence threading in C backend
C backend now fully threads evidence through effectful function calls:
- Track effectful functions via effectful_functions HashSet
- Add has_evidence flag to track context during code generation
- Add LuxEvidence* ev parameter to effectful function signatures
- Transform effect operations to use ev->console->print() when evidence available
- Update function calls to pass evidence (ev or &default_evidence)
- Update main entry point to pass &default_evidence
Generated code now uses zero-cost evidence passing:
void greet_lux(LuxEvidence* ev) {
ev->console->print(ev->console->env, "Hello!");
}
This completes the evidence passing implementation for both interpreter
(O(1) HashMap lookup) and C backend (direct function pointer calls).
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
This commit is contained in:
@@ -251,13 +251,23 @@ Koka also compiles to C with algebraic effects. Key differences:
|
||||
|
||||
## Current Progress
|
||||
|
||||
### Evidence Passing (Zero-Cost Effects) - PARTIALLY COMPLETE
|
||||
### Evidence Passing (Zero-Cost Effects) ✅ COMPLETE
|
||||
|
||||
**Interpreter:** ✅ Complete - O(1) HashMap lookup instead of O(n) stack search.
|
||||
|
||||
**C Backend Infrastructure:** ✅ Complete - Handler structs and evidence types generated.
|
||||
**C Backend:** ✅ Complete - Full evidence threading through function calls.
|
||||
|
||||
**C Backend Threading:** 🔜 Planned - Passing evidence through function calls.
|
||||
**Generated code example:**
|
||||
```c
|
||||
void greet_lux(LuxEvidence* ev) {
|
||||
ev->console->print(ev->console->env, "Hello!");
|
||||
}
|
||||
|
||||
int main(int argc, char** argv) {
|
||||
greet_lux(&default_evidence);
|
||||
return 0;
|
||||
}
|
||||
```
|
||||
|
||||
See [docs/EVIDENCE_PASSING.md](EVIDENCE_PASSING.md) for details.
|
||||
|
||||
@@ -265,28 +275,6 @@ See [docs/EVIDENCE_PASSING.md](EVIDENCE_PASSING.md) for details.
|
||||
|
||||
## Future Roadmap
|
||||
|
||||
### Phase 1: Complete Evidence Passing in C Backend
|
||||
|
||||
**Goal:** Thread evidence through all effectful function calls.
|
||||
|
||||
**Current state:** Handler types (`LuxConsoleHandler`, etc.) and `LuxEvidence` struct
|
||||
are generated, but not yet used. Effect calls still use hardcoded `lux_console_print()`.
|
||||
|
||||
**Required changes:**
|
||||
```c
|
||||
// Current (hardcoded):
|
||||
void greet_lux(LuxString name) {
|
||||
lux_console_print(name);
|
||||
}
|
||||
|
||||
// Target (evidence passing):
|
||||
void greet_lux(LuxEvidence* ev, LuxString name) {
|
||||
ev->console->print(ev->console->env, name);
|
||||
}
|
||||
```
|
||||
|
||||
**Expected speedup:** 10-20x for effect-heavy code (based on Koka benchmarks).
|
||||
|
||||
### Phase 2: Perceus Reference Counting
|
||||
|
||||
**Goal:** Deterministic memory management without GC pauses.
|
||||
|
||||
@@ -181,16 +181,39 @@ let handler = self.evidence.get(&request.effect)
|
||||
|
||||
4. Added `default_evidence` global with built-in handlers
|
||||
|
||||
### Phase 3: C Backend Evidence Threading 🔜 PLANNED
|
||||
### Phase 3: C Backend Evidence Threading ✅ COMPLETE
|
||||
|
||||
**Goal:** Thread evidence through effectful function calls.
|
||||
|
||||
**Required changes:**
|
||||
**Changes made to `c_backend.rs`:**
|
||||
|
||||
1. Add `LuxEvidence* ev` parameter to effectful functions
|
||||
2. Transform effect operations to use `ev->console->print(...)`
|
||||
3. Generate handler structs for user-defined handlers in `run` blocks
|
||||
4. Pass evidence through call chain
|
||||
1. Track effectful functions in `effectful_functions: HashSet<String>`
|
||||
2. Add `has_evidence: bool` flag to track context
|
||||
3. For effectful functions:
|
||||
- Add `LuxEvidence* ev` parameter to forward declarations
|
||||
- Add `LuxEvidence* ev` parameter to function definitions
|
||||
4. Transform effect operations:
|
||||
- When `has_evidence` is true: `ev->console->print(ev->console->env, msg)`
|
||||
- When `has_evidence` is false: `lux_console_print(msg)` (fallback)
|
||||
5. Update function calls:
|
||||
- Effectful calls inside effectful functions: pass `ev`
|
||||
- Effectful calls outside: pass `&default_evidence`
|
||||
6. Update main function generation to pass `&default_evidence`
|
||||
|
||||
**Example generated code:**
|
||||
```c
|
||||
// Function signature includes evidence
|
||||
void greet_lux(LuxEvidence* ev) {
|
||||
// Effect operations use evidence
|
||||
ev->console->print(ev->console->env, "Hello, World!");
|
||||
}
|
||||
|
||||
int main(int argc, char** argv) {
|
||||
// Entry point uses default evidence
|
||||
greet_lux(&default_evidence);
|
||||
return 0;
|
||||
}
|
||||
```
|
||||
|
||||
## Performance Characteristics
|
||||
|
||||
|
||||
Reference in New Issue
Block a user