✓
Passing This code compiles and runs correctly.
Code
// 690_056 — the *File<open!> proof: the owned-column generalization on a REAL
// pre-existing corpus resource (app/fs's *File<opened!>, open!/close — green
// across 330_006/013/…), not a purpose-built type. A store column holds
// *app/lib/fs:File<opened!>; insert moves ownership IN, take moves it OUT (then
// close), and store teardown auto-CLOSES each still-live file via the DISCOVERED
// canonical discharger `close`. Resource-agnostic: the store hardcodes nothing.
import std/io
import std/store
import app/lib/fs
std/store:new(files, capacity: 8) { handle: *app/lib/fs:File<opened!> }
app/lib/fs:open(path: "a"): f |> std/store:insert(files) { handle: f }
| row r |> std/store:take(files[r])
| item it |> app/lib/fs:close(file: it.handle) |> std/io:print.ln("took-and-closed")
app/lib/fs:open(path: "b"): kept |> std/store:insert(files) { handle: kept }
| row _ |> _
Actual
open a
close 42
took-and-closed
open b
close 42
Expected output
open a
close 42
took-and-closed
open b
close 42
Flows
flow ~new click a branch to expand · @labels scroll to their anchor
new (expr: files, capacity: 8, source: handle: *app/lib/fs:File<opened!>)
flow ~open click a branch to expand · @labels scroll to their anchor
open (path: "a")
flow ~open click a branch to expand · @labels scroll to their anchor
open (path: "b")
Imported Files
// The app/fs File resource, verbatim from the corpus (330_006/013/…): an owned
// *File<opened!> with a VOID canonical discharger `close` consuming <!opened>.
// This is a REAL pre-existing obligation type — the store owns it unchanged.
const std = @import("std");
const File = struct { handle: i32 };
~pub tor open { path: string } -> *File<opened!>
~proc open|zig {
std.debug.print("open {s}\n", .{path});
const f = std.heap.page_allocator.create(File) catch unreachable;
f.* = File{ .handle = 42 };
return f;
}
// Canonical discharger: consumes <!opened>, closes (void).
~pub tor close { file: *File<!opened> }
~proc close|zig {
std.debug.print("close {d}\n", .{file.handle});
std.heap.page_allocator.destroy(file);
}
Test Configuration
MUST_RUN