Brummel
aaa70d4c35
The strict linearity check (use-after-consume / consume-while-borrowed, linearity.rs) runs today only on the ~45 of 258 all-explicit-mode fns; its activation gate skips any fn with a bare/Implicit param. Deleting ParamMode::Implicit (#55) would turn it on universally and surface ~21% false positives in two classes. This closes both, making the core ownership analysis sharp across the whole codebase for the first time — the precondition for #55. Diagnostic-only: no schema, no hash, no codegen change; the two existing diagnostic codes simply fire on a smaller, more correct set. Fix 1 — value-type exemption. A new is_value_type predicate (ailang-core::primitives) names the unboxed set {Int,Bool,Float,Unit}; BinderState gains an is_value flag seeded from the binder's locally available type (param signatures, ctor field types for pattern binders, lam typed-params), and use_var short-circuits the Consume arm for it. A value type has no refcount and is never consumed, so multi-read is always legal. Str is deliberately NOT in the value set, though is_primitive_name includes it: drop.rs:490-492 lowers only Int/Bool/Float/Unit to non-ptr; Str is a ptr, RC-dec'd, so a multi-consume of Str without clone is a real use-after-free. is_value_type is the Str-excluding subset of is_primitive_name, pinned by a unit test. is_heap_type and the over-strict-mode lint are left untouched (separate concern). Fix 2 — application is a borrow. Term::App walks its callee in Position::Borrow (was Consume). Applying a function value reads it; it stays live for further applications. Global fn-refs are untracked (no-op); a tracked function-typed binder (a HOF param) is no longer consumed by application. This fixes both the own-f-param use-after-consume and the borrow-f-param consume-while-borrowed in the recursion-passing HOF shape (map_int f t). Passing a function value as an arg is unchanged — it follows the callee param_modes. Scope decision: value-typed let-binders stay conservatively tracked as heap (their type is inferred, not annotated, and the linearity walk does not re-run inference). This is soundness-safe — over-strict, never unsound — and not a measured corpus shape; lifting it would need a full binder->type table out of the type-checker. Verification: all three false-positive classes reproduced today against explicit-mode fns and shipped as RED->GREEN fixtures (examples/fp_{value,hof,map}.ail); examples/real_consume.ail stays RED (heap double-consume still fires) to prove the exemption is type-gated. 715 workspace tests green; bench/check.py 0/34 and bench/compile_check.py 0/24 regressed. merge_states carries is_value so the flag survives branch merges. RED-first verified per task. closes #56
15 lines
540 B
Plaintext
15 lines
540 B
Plaintext
(module fp_map
|
|
(data IntList
|
|
(doc "boxed list")
|
|
(ctor Nil)
|
|
(ctor Cons (con Int) (con IntList)))
|
|
(fn map_int
|
|
(doc "recursive HOF: f applied AND passed to the recursive call")
|
|
(type (fn-type
|
|
(params (borrow (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con IntList)))
|
|
(ret (own (con IntList)))))
|
|
(params f xs)
|
|
(body (match xs
|
|
(case (pat-ctor Nil) (term-ctor IntList Nil))
|
|
(case (pat-ctor Cons h t) (term-ctor IntList Cons (app f h) (app map_int f t)))))))
|