Parse Typed Jerboa effect annotations
ober
6044c16ac950f76324e8a36dfef362b770c11c95
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -291,6 +291,10 @@ Typed Jerboa effects should influence generated Rust: - `qt`: only callable through Qt-thread wrapper - `unsafe`: requires generated unsafe block with audit marker +Current landing: typed def forms can carry parsed `#:effects (...)` +annotations. The Rust backend does not use them yet; effect checking and +effect-aware lowering remain future work. + The Rust backend should avoid `panic!` for Typed Jerboa errors. Use explicit `Result` values and convert failures into Jerboa conditions at the boundary. --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -195,7 +195,8 @@ Current landing: 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 and `:` or `->` return markers. + `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 @@ -402,6 +403,10 @@ Example: Pure functions should not call effectful functions. Effectful functions can call pure functions. Higher-level functions should accumulate effects from callees. +Current landing: the parser preserves optional `#:effects (...)` annotations on +typed defs as `typed-def-effects`. The checker does not yet enforce pure versus +effectful call relationships; that is the next Milestone 5 step. + ## Memory Model Typed Jerboa should not copy Rust's ownership model wholesale. It should use a @@ -876,7 +881,8 @@ Minimum excluded features: ### Milestone 5: Effects and Resources -- Add effect annotations. +- Add effect annotations. Parsed `#:effects (...)` lists now land on typed def + AST nodes as `typed-def-effects`. - Check pure/effectful call relationships. - Add linear resource types. - Model FFI handles. The current generated wrapper layer models same-module --- a/lib/jerboa/typed/parser.ss +++ b/lib/jerboa/typed/parser.ss @@ -35,7 +35,8 @@ typed-param-name typed-param-type typed-def? make-typed-def - typed-def-name typed-def-params typed-def-return-type typed-def-body) + typed-def-name typed-def-params typed-def-return-type + typed-def-effects typed-def-body) (import (chezscheme) ; jerboa-security: suppress direct-chezscheme-import-user-code -- trusted typed compiler front-end module (only (jerboa core) def defstruct) @@ -48,7 +49,7 @@ (defstruct typed-variant (name cases)) (defstruct typed-variant-case (name fields)) (defstruct typed-param (name type)) - (defstruct typed-def (name params return-type body)) + (defstruct typed-def (name params return-type effects body)) (def (strip-source-annotations datum) (cond @@ -210,6 +211,35 @@ head)) (values (car head) (map parse-param (cdr head)))) + (def (effects-marker? value) + (and (symbol? value) + (gensym? value) + (string=? (symbol->string value) "effects"))) + + (def (parse-effects-form form) + (expect-proper-list 'parse-typed-def form) + (unless (symbol-list? form) + (error 'parse-typed-def + "effects must be symbols" + form)) + form) + + (def (parse-def-effects-and-body body) + (if (and (pair? body) (effects-marker? (car body))) + (begin + (unless (pair? (cdr body)) + (error 'parse-typed-def + "expected an effects list after #:effects" + body)) + (let ([effects (parse-effects-form (cadr body))] + [rest (cddr body)]) + (when (null? rest) + (error 'parse-typed-def + "def with effects still needs a body" + body)) + (values effects rest))) + (values '() body))) + (def (parse-def form) (expect-proper-list 'parse-typed-def form) (unless (>= (length form) 5) @@ -225,11 +255,14 @@ "expected : or -> before return type" form)) (let-values ([(name params) (parse-def-head head)]) - (make-typed-def - name - params - (parse-typed-type return-type) - body)))) + (let-values ([(effects parsed-body) + (parse-def-effects-and-body body)]) + (make-typed-def + name + params + (parse-typed-type return-type) + effects + parsed-body))))) (def (parse-type-decl form) (expect-length 'parse-typed-type-decl form 2) --- a/tests/test-typed-parser.ss +++ b/tests/test-typed-parser.ss @@ -60,6 +60,11 @@ (define variant-decl (list-ref declarations 2)) (define make-leaf-def (list-ref declarations 3)) (define split-size-def (list-ref declarations 4)) +(define effects-def + (parse-typed-declaration + '(def (read-file-bytes (path : String)) : (Result Bytes String) + #:effects (io alloc) + path))) (printf "--- Typed Jerboa parser tests ---~%") @@ -143,6 +148,18 @@ (typed-def-return-type split-size-def) 'Nat) +(test "def default effects" + (typed-def-effects make-leaf-def) + '()) + +(test "def effects annotation" + (typed-def-effects effects-def) + '(io alloc)) + +(test "def effects body" + (typed-def-body effects-def) + '(path)) + (test "compound type expression" (parse-typed-type '(Result String (Option Nat))) '(Result String (Option Nat))) @@ -160,6 +177,17 @@ (parse-typed-declaration '(import (jerboa prelude)))) +(test-error "rejects bad effects list" + (parse-typed-declaration + '(def (f) : Nat + #:effects io + 0))) + +(test-error "rejects effects without body" + (parse-typed-declaration + '(def (f) : Nat + #:effects (io)))) + (printf "~%Typed parser: ~a passed, ~a failed~%" pass fail) (when (> fail 0) (exit 1))