Allow Typed Jerboa owned borrows
ober
cb4bb8e2bb5c77d18be2928933db89a9b3de7c3a
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -319,8 +319,9 @@ Current landing: the typed front end recognizes resource declarations and the `(Owned T)` / `(Borrow T)` / `(MutBorrow T)` type constructors. The checker validates those type references and catches first-order straight-line Owned movement errors: use after move and duplicate moves in one call. It does not -yet enforce path-sensitive movement, borrow lifetimes, borrowed-from-owned -coercions, or Drop lowering. +yet enforce path-sensitive movement, borrow lifetimes, mutable borrow +exclusivity, or Drop lowering. Owned values can satisfy Borrow parameters +before they move; borrowing them after a consuming call is rejected. At the C ABI boundary, references cannot cross directly. Use opaque handles. --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -509,8 +509,10 @@ the type namespace, and `(Owned T)` / `(Borrow T)` / `(MutBorrow T)` are checked compound type constructors. The checker now enforces a first straight-line linear rule: passing an Owned variable to a consuming call moves it, later uses of that variable in the same straight-line body are rejected, and moving the -same variable twice in one call is rejected. Path-sensitive branch joins, -borrow lifetimes, and borrowed-from-owned coercions are still future work. +same variable twice in one call is rejected. An Owned variable can satisfy a +Borrow parameter before it moves; attempting that borrow after the move is +rejected. Path-sensitive branch joins, borrow lifetimes, and mutable borrow +exclusivity are still future work. ## FFI Types @@ -902,7 +904,8 @@ Minimum excluded features: - Add linear resource types. Resource declarations and Owned/Borrow/MutBorrow type constructors are parsed and type-checked. The checker now catches straight-line use-after-move and duplicate moves for Owned variables; richer - movement and borrowing rules are not enforced yet. + movement and borrowing rules are not enforced yet. Owned-to-Borrow calls are + allowed before the owner moves and rejected after it moves. - Model FFI handles. The current generated wrapper layer models same-module record and variant handles as tagged opaque values, exposes explicit handle drops, clears dropped handle ids, and has boundary tests for stale use and --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -262,10 +262,20 @@ (let ([entry (assq name env)]) (and entry (cdr entry)))) + (def (borrow-type? type) + (and (pair? type) + (eq? (car type) 'Borrow))) + + (def (owned-to-borrow-assignable? actual expected) + (and (owned-type? actual) + (borrow-type? expected) + (equal? (cadr actual) (cadr expected)))) + (def (type-assignable? actual expected) (or (equal? actual expected) (eq? expected any-value-type) - (and (eq? actual 'Nat) (eq? expected 'Int)))) + (and (eq? actual 'Nat) (eq? expected 'Int)) + (owned-to-borrow-assignable? actual expected))) (def (owned-type? type) (and (pair? type) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -213,6 +213,36 @@ (size fh)))) '()) +(test "owned resource can be borrowed without moving" + (error-kinds + '(typed-library (resource borrow-owned) + (export ok) + (resource FileHandle) + (record Sink ((mut closed? : Bool))) + (def (size (fh : (Borrow FileHandle))) : Nat + 0) + (def (consume (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (Sink-closed?-set! sink #t)) + (def (ok (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (size fh) + (consume fh sink)))) + '()) + +(test "owned resource cannot be borrowed after move" + (error-kinds + '(typed-library (resource borrow-after-move) + (export bad) + (resource FileHandle) + (record Sink ((mut closed? : Bool))) + (def (size (fh : (Borrow FileHandle))) : Nat + 0) + (def (consume (fh : (Owned FileHandle)) (sink : Sink)) : Unit + (Sink-closed?-set! sink #t)) + (def (bad (fh : (Owned FileHandle)) (sink : Sink)) : Nat + (consume fh sink) + (size fh)))) + '(use-after-move)) + (test "owned resource use after move rejected" (error-kinds '(typed-library (resource use-after-move)