Parse Typed Jerboa resource types
ober
a0ccc117d5503725dc55e95d8e18157d1dccea58
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -315,6 +315,11 @@ Mappings: - Nullable FFI handles: `Option<NonNull<T>>` internally - Non-null FFI handles: `NonNull<T>` internally +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 but does not yet enforce linear movement, +borrowing, or Drop lowering. + At the C ABI boundary, references cannot cross directly. Use opaque handles. ## Runtime Handles --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -194,9 +194,10 @@ Current landing: wrappers under `build/typed/jerboa` and runs `cargo build` against the generated crate. - The parser currently recognizes explicit `export` forms, `type` declarations, - immutable and `mut` record fields, variants including nullary cases, and - `def` forms with typed parameters, `:` or `->` return markers, and optional - `#:effects (...)` annotations. + immutable and `mut` record fields, `resource` declarations with optional + `#:close` hooks, variants including nullary cases, and `def` forms with + typed parameters, `:` or `->` return markers, and optional `#:effects (...)` + annotations. - This is still a front-end milestone. Function-body checking currently covers literals, variables, `begin`, simple `let`, `if`, arithmetic primitives, numeric comparisons, boolean primitives, calls to typed functions defined in @@ -502,6 +503,12 @@ The compiler should reject: - Copying owned handles - Returning borrowed handles that cannot outlive their owner +Current landing: the front end recognizes `(resource Name)` and +`(resource Name #:close close-fn)` declarations. Resource names participate in +the type namespace, and `(Owned T)` / `(Borrow T)` / `(MutBorrow T)` are checked +compound type constructors. Linear move/borrow flow checks are still future +work. + ## FFI Types FFI should be typed and guarded. @@ -889,7 +896,9 @@ Minimum excluded features: - Check pure/effectful call relationships. Same-module calls now require the caller's effect list to cover the callee's effects; pure callers reject effectful callees. -- Add linear resource types. +- Add linear resource types. Resource declarations and Owned/Borrow/MutBorrow + type constructors are parsed and type-checked; movement and borrowing rules + are not enforced yet. - 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 @@ -33,7 +33,10 @@ (Vector . 1) (Option . 1) (Result . 2) - (Pair . 2))) + (Pair . 2) + (Owned . 1) + (Borrow . 1) + (MutBorrow . 1))) (def allowed-effects '(pure alloc mut io ffi throw block qt unsafe)) @@ -48,7 +51,7 @@ [(unknown-type) "Define the type in this typed-library, import it later when imports exist, or use a builtin type name."] [(unknown-type-constructor) - "Use a supported compound type constructor: List, Vector, Option, Result, Pair, or ->."] + "Use a supported compound type constructor: List, Vector, Option, Result, Pair, Owned, Borrow, MutBorrow, or ->."] [(bad-type-arity) "Check the number of type arguments for the compound type."] [(duplicate-type duplicate-value duplicate-field duplicate-param @@ -202,6 +205,7 @@ (cond [(typed-type-decl? decl) (typed-type-decl-name decl)] [(typed-record? decl) (typed-record-name decl)] + [(typed-resource? decl) (typed-resource-name decl)] [(typed-variant? decl) (typed-variant-name decl)] [else #f])) @@ -240,6 +244,7 @@ [(typed-def? decl) (list (typed-def-name decl))] [(typed-record? decl) (record-value-names decl)] [(typed-variant? decl) (variant-value-names decl)] + [(typed-resource? decl) '()] [else '()])) (def (declared-value-names declarations) --- a/lib/jerboa/typed/parser.ss +++ b/lib/jerboa/typed/parser.ss @@ -25,6 +25,9 @@ typed-record? make-typed-record typed-record-name typed-record-fields + typed-resource? make-typed-resource + typed-resource-name typed-resource-close + typed-variant? make-typed-variant typed-variant-name typed-variant-cases @@ -46,6 +49,7 @@ (defstruct typed-type-decl (name)) (defstruct typed-field (name type mutable?)) (defstruct typed-record (name fields)) + (defstruct typed-resource (name close)) (defstruct typed-variant (name cases)) (defstruct typed-variant-case (name fields)) (defstruct typed-param (name type)) @@ -203,6 +207,34 @@ (expect-symbol 'parse-typed-variant (cadr form) form) (map parse-variant-case (cddr form)))) + (def (keyword-marker? value name) + (and (symbol? value) + (gensym? value) + (string=? (symbol->string value) name))) + + (def (close-marker? value) + (keyword-marker? value "close")) + + (def (parse-resource form) + (expect-proper-list 'parse-typed-resource form) + (case (length form) + [(2) + (make-typed-resource + (expect-symbol 'parse-typed-resource (cadr form) form) + #f)] + [(4) + (unless (close-marker? (caddr form)) + (error 'parse-typed-resource + "expected #:close close-function" + form)) + (make-typed-resource + (expect-symbol 'parse-typed-resource (cadr form) form) + (expect-symbol 'parse-typed-resource (cadddr form) form))] + [else + (error 'parse-typed-resource + "expected (resource Name) or (resource Name #:close close-function)" + form)])) + (def (parse-def-head head) (expect-proper-list 'parse-typed-def head) (unless (and (pair? head) (symbol? (car head))) @@ -212,9 +244,7 @@ (values (car head) (map parse-param (cdr head)))) (def (effects-marker? value) - (and (symbol? value) - (gensym? value) - (string=? (symbol->string value) "effects"))) + (keyword-marker? value "effects")) (def (parse-effects-form form) (expect-proper-list 'parse-typed-def form) @@ -277,6 +307,7 @@ (case (car form) [(type) (parse-type-decl form)] [(record) (parse-record form)] + [(resource) (parse-resource form)] [(variant) (parse-variant form)] [(def) (parse-def form)] [else --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -98,6 +98,16 @@ x))) '(duplicate-type)) +(test "duplicate resource type declarations" + (error-kinds + '(typed-library (bad duplicate-resource) + (export f) + (resource FileHandle) + (record FileHandle ((id : Nat))) + (def (f (x : Nat)) : Nat + x))) + '(duplicate-type)) + (test "duplicate def declarations" (error-kinds '(typed-library (bad duplicate-def) @@ -143,6 +153,42 @@ (def (f (x : Nat)) : Nat x))) '(undefined-export)) +(test "resource owned type accepted" + (error-kinds + '(typed-library (resource owned) + (export id) + (resource FileHandle) + (def (id (fh : (Owned FileHandle))) : (Owned FileHandle) + fh))) + '()) + +(test "resource borrow type accepted" + (error-kinds + '(typed-library (resource borrow) + (export read) + (resource FileHandle) + (def (read (fh : (Borrow FileHandle))) : Nat + 0))) + '()) + +(test "resource mutable borrow type accepted" + (error-kinds + '(typed-library (resource mut-borrow) + (export read) + (resource FileHandle) + (def (read (fh : (MutBorrow FileHandle))) : Nat + 0))) + '()) + +(test "resource compound type arity" + (error-kinds + '(typed-library (resource arity) + (export read) + (resource FileHandle) + (def (read (fh : (Borrow FileHandle Nat))) : Nat + 0))) + '(bad-type-arity)) + (test "body can return parameter" (error-kinds '(typed-library (body param) --- a/tests/test-typed-parser.ss +++ b/tests/test-typed-parser.ss @@ -60,6 +60,10 @@ (define variant-decl (list-ref declarations 2)) (define make-leaf-def (list-ref declarations 3)) (define split-size-def (list-ref declarations 4)) +(define resource-decl + (parse-typed-declaration + '(resource FileHandle + #:close close-file-handle!))) (define effects-def (parse-typed-declaration '(def (read-file-bytes (path : String)) : (Result Bytes String) @@ -118,6 +122,15 @@ (typed-field-type (car (typed-record-fields record-decl))) 'Nat) +(test "resource declaration" + (and (typed-resource? resource-decl) + (typed-resource-name resource-decl)) + 'FileHandle) + +(test "resource close function" + (typed-resource-close resource-decl) + 'close-file-handle!) + (test "variant declaration" (and (typed-variant? variant-decl) (typed-variant-name variant-decl)) @@ -177,6 +190,10 @@ (parse-typed-declaration '(import (jerboa prelude)))) +(test-error "rejects bad resource close marker" + (parse-typed-declaration + '(resource FileHandle close close-file-handle!))) + (test-error "rejects bad effects list" (parse-typed-declaration '(def (f) : Nat