019 auto discharge branch constructor

✓ Passing This code compiles and runs correctly.

Code

// TEST: Auto-discharge with branch constructor termination (NOT using _)
//
// EXPOSES GAP: Auto-discharge currently only triggers on `_` terminal nodes.
// Flows that terminate with branch constructors should ALSO auto-discharge!
//
// Here: open() returns *File[opened!], we return a branch constructor
// WITHOUT calling close(). The obligation should be auto-discharged.
//
// Expected: Auto-discharge inserts close() before the branch constructor

~import "$app/fs"

// Event that wraps file opening and returns a status
~event check_file { path: []const u8 }
| result { status: []const u8 }

// Subflow: opens file, returns status - SHOULD auto-discharge the file!
// Using _ for binding since auto-discharge should synthesize _auto_N
~check_file = app.fs:open(path: path)
| opened _ |> result { status: "file exists" }  // obligation should be auto-discharged before returning!

// Main flow
~check_file(path: "test.txt")
| result _ |> _

pub fn main() void {}

input.kz

Expected Output

Opening file: test.txt
Closing file (auto-discharged)

Imported Files

const std = @import("std");
const File = struct { handle: i32 };

~pub event open { path: []const u8 }
| opened { file: *File[opened!] }

~proc open {
    std.debug.print("Opening file: {s}\n", .{path});
    const f = std.heap.page_allocator.create(File) catch unreachable;
    f.* = File{ .handle = 42 };
    return .{ .opened = .{ .file = f } };
}

~pub event close { file: *File[!opened] }
| closed {}

~proc close {
    std.debug.print("Closing file (auto-discharged)\n", .{});
    return .{ .closed = .{} };
}

fs.kz

Test Configuration

MUST_RUN

← 018 auto discharge escaped obligation 019 for manual done ok →