Add Gerbil-style ergo contract markers
ober
8a76911345194bdc721274e1ba5d452105256fa0
--- a/docs/index.md +++ b/docs/index.md @@ -39,6 +39,7 @@ Updated 2026-03-22. ## Language Features - [typing.md](typing.md) — Gradual type system: inference, refinements, GADTs, HKTs +- [gerbil-contracts.md](gerbil-contracts.md) — Reference notes for Gerbil-style contracts and Jerboa's contract bridge - [pattern-matching.md](pattern-matching.md) — Pattern matching - [effects.md](effects.md) — Algebraic effects - [sequences.md](sequences.md) — Lazy sequences and iterators --- a/docs/typing.md +++ b/docs/typing.md @@ -37,6 +37,13 @@ types, type-directed compilation): (std typed advanced)) ``` +For Gerbil-style ergonomic casts, local `using` scopes, and predicate +contracts: + +```scheme +(import (std ergo)) +``` + --- ## Core API — `(std typed)` @@ -137,6 +144,59 @@ in code without annotating a whole function. --- +## Ergonomic Contract Markers — `(std ergo)` + +`(std ergo)` provides Gerbil-inspired contract markers for dynamic Jerboa code. +These are not a full static type system; they are boundary checks and local +assertions that bridge ordinary dynamic code toward Typed Jerboa. + +```scheme +(: expr type) ; checked type cast in debug mode +(:? expr type) ; #f or checked type in debug mode +(:- expr type) ; unchecked assertion, returns expr +(:~ expr pred) ; checked predicate contract +``` + +Examples: + +```scheme +(define maybe-name (:? raw-name string)) +(define fast-count (:- count fixnum)) +(define bounded-index (:~ idx (in-range? 0 len))) +``` + +`using` supports the same local markers: + +```scheme +(using (p maybe-point :? point) + (if p p.x 'none)) + +(using (n idx :~ (in-range? 0 len)) + (vector-ref values n)) + +(using (p value :- point) + p.x) +``` + +`:` and `:?` use the `(std typed)` type registry and follow +`*typed-mode*`. `:~` is a contract check and runs immediately. `:-` is an +unchecked assertion: use it only after a checked boundary has established the +invariant. + +Predicate helpers: + +```scheme +(maybe string?) ; #f or string +(list-of? fixnum?) ; list of fixnums +(in-range? 0 10) ; integer in [0, 10) +(in-range-inclusive? 0 10) ; integer in [0, 10] +``` + +This layer is the dynamic contract bridge. Typed Jerboa remains the stricter +tier for closed-world module checks, resources, effects, and native backends. + +--- + ### Built-in Type Names The following type names are recognized out of the box: --- a/lib/std/ergo.ss +++ b/lib/std/ergo.ss @@ -4,20 +4,29 @@ ;;; Gerbil-inspired type annotations with minimal friction. ;;; ;;; Type cast: -;;; (: expr type) — checked cast (raises in debug mode if wrong type) +;;; (: expr type) — checked cast (raises in debug mode if wrong type) +;;; (:? expr type) — checked nullable cast (#f or type) +;;; (:- expr type) — unchecked assertion, returns expr +;;; (:~ expr pred) — checked predicate contract ;;; ;;; Typed scopes with dot-access: -;;; (using (var expr : type) var.field ...) — checked type + dot-access -;;; (using (var expr as type) var.field ...) — unchecked, dot-access only +;;; (using (var expr : type) var.field ...) — checked type + dot-access +;;; (using (var expr :? type) body ...) — #f or checked type + dot-access +;;; (using (var expr :- type) var.field ...) — unchecked assertion + dot-access +;;; (using (var expr as type) var.field ...) — unchecked, dot-access only +;;; (using (var expr :~ pred) body ...) — checked predicate contract ;;; (using ((v1 e1 : t1) (v2 e2 as t2)) ...) — multiple bindings ;;; ;;; Contract predicates: -;;; (maybe pred) — returns predicate: #f or satisfies pred -;;; (list-of? pred) — returns predicate: list where all elements satisfy pred +;;; (maybe pred) — predicate: #f or satisfies pred +;;; (list-of? pred) — predicate: list whose elements satisfy pred +;;; (in-range? start end) — predicate: integer in [start, end) +;;; (in-range-inclusive? start end) — predicate: integer in [start, end] (library (std ergo) - (export using : maybe list-of?) - (import (chezscheme) + (export using : :? :- :~ + maybe list-of? in-range? in-range-inclusive?) + (import (chezscheme) ; jerboa-security: suppress direct-chezscheme-import-user-code -- trusted stdlib macro module (std typed) (only (jerboa core) def)) @@ -33,6 +42,37 @@ (check-type! ': 'expr v 'type-name) v)]))) + ;; (:? expr type) — checked nullable cast, allowing #f + (define-syntax :? + (lambda (stx) + (syntax-case stx () + [(kw expr type-name) + (identifier? #'type-name) + #'(let ([v expr]) + (when v + (check-type! ':? 'expr v 'type-name)) + v)]))) + + ;; (:- expr type) — unchecked assertion. Today this is runtime identity; + ;; compiler-facing metadata can be attached here later. + (define-syntax :- + (lambda (stx) + (syntax-case stx () + [(kw expr type-name) + (identifier? #'type-name) + #'expr]))) + + ;; (:~ expr pred) — checked predicate contract. + (define-syntax :~ + (lambda (stx) + (syntax-case stx () + [(kw expr pred) + #'(let ([v expr] + [p pred]) + (unless (p v) + (error ':~ "predicate contract failed" v)) + v)]))) + ;; ========== Contract Predicates ========== (def (maybe pred) @@ -41,6 +81,18 @@ (def (list-of? pred) (lambda (v) (and (list? v) (for-all pred v)))) + (def (in-range? start end) + (lambda (v) + (and (integer? v) + (>= v start) + (< v end)))) + + (def (in-range-inclusive? start end) + (lambda (v) + (and (integer? v) + (>= v start) + (<= v end)))) + ;; ========== using Macro ========== (define-syntax using @@ -101,28 +153,49 @@ (datum->syntax ctx (syntax->datum (transform b var-map ctx)))) (syntax->list body-stx))) - ;; Detect binding operator: : or as - (define (binding-op? stx) + ;; Detect binding operator. + (define (type-binding-op? stx) (let ([d (syntax->datum stx)]) - (or (eq? d ':) (eq? d 'as)))) + (or (eq? d ':) + (eq? d ':?) + (eq? d ':-) + (eq? d 'as)))) + + (define (predicate-binding-op? stx) + (eq? (syntax->datum stx) ':~)) (define (checked-op? stx) (eq? (syntax->datum stx) ':)) + (define (nullable-op? stx) + (eq? (syntax->datum stx) ':?)) + (syntax-case stx () - ;; Single binding: (using (var expr :/as type) body ...) + ;; Single binding: (using (var expr :/:?/:-/as type) body ...) [(_ (var expr op type) body ...) (and (identifier? #'var) - (identifier? #'type) - (binding-op? #'op)) - (let ([var-map (list (make-var-entry #'var #'type))]) - (with-syntax ([(tbody ...) (transform-body #'(body ...) var-map #'var)]) - (if (checked-op? #'op) - #'(let ([var expr]) - (check-type! 'using 'var var 'type) - tbody ...) - #'(let ([var expr]) - tbody ...))))] + (or (and (identifier? #'type) + (type-binding-op? #'op)) + (predicate-binding-op? #'op))) + (if (predicate-binding-op? #'op) + #'(let ([var expr]) + (:~ var type) + body ...) + (let ([var-map (list (make-var-entry #'var #'type))]) + (with-syntax ([(tbody ...) (transform-body #'(body ...) var-map #'var)]) + (cond + [(checked-op? #'op) + #'(let ([var expr]) + (check-type! 'using 'var var 'type) + tbody ...)] + [(nullable-op? #'op) + #'(let ([var expr]) + (when var + (check-type! 'using 'var var 'type)) + tbody ...)] + [else + #'(let ([var expr]) + tbody ...)]))))] ;; Multiple bindings: expand into nested using [(_ (first-binding rest-binding ...) body ...) @@ -130,8 +203,9 @@ (syntax-case #'first-binding () [(var expr op type) (and (identifier? #'var) - (identifier? #'type) - (binding-op? #'op)) + (or (and (identifier? #'type) + (type-binding-op? #'op)) + (predicate-binding-op? #'op))) #'(using (var expr op type) (using (rest-binding ...) body ...))]))] --- a/tests/test-ergo.ss +++ b/tests/test-ergo.ss @@ -44,6 +44,21 @@ (parameterize ([*typed-mode* 'release]) (test ": release mode no check" (: "oops" fixnum) "oops")) +;;; ========== :? / :- / :~ ========== + +(printf "~%-- Gerbil-style contract markers --~%") + +(parameterize ([*typed-mode* 'debug]) + (test ":? accepts #f" (:? #f string) #f) + (test ":? accepts typed value" (:? "hello" string) "hello") + (test-error ":? rejects wrong non-false value" (:? 42 string))) + +(parameterize ([*typed-mode* 'debug]) + (test ":- unchecked assertion returns value" (:- "not-a-fixnum" fixnum) "not-a-fixnum")) + +(test ":~ accepts predicate success" (:~ 4 even?) 4) +(test-error ":~ rejects predicate failure" (:~ 5 even?)) + ;;; ========== maybe / list-of? ========== (printf "~%-- contract predicates --~%") @@ -57,11 +72,17 @@ (test "list-of?: invalid" ((list-of? fixnum?) '(1 "x" 3)) #f) (test "list-of?: not list" ((list-of? fixnum?) 42) #f) +(test "in-range?: lower inclusive" ((in-range? 1 4) 1) #t) +(test "in-range?: upper exclusive" ((in-range? 1 4) 4) #f) +(test "in-range-inclusive?: upper inclusive" ((in-range-inclusive? 1 4) 4) #t) +(test "in-range-inclusive?: non-integer" ((in-range-inclusive? 1 4) 2.5) #f) + ;;; ========== using with : ========== (printf "~%-- using (checked) --~%") (defstruct point (x y)) +(register-type-predicate! 'point point?) (parameterize ([*typed-mode* 'debug]) ;; Basic dot-access @@ -92,6 +113,39 @@ (using (p "not a point" : point) p.x))) +;;; ========== using with :? / :- / :~ ========== + +(printf "~%-- using (contract markers) --~%") + +(parameterize ([*typed-mode* 'debug]) + (test "using :? accepts #f" + (using (p #f :? point) + (if p p.x 'none)) + 'none) + + (test "using :? dot-access" + (using (p (make-point 11 12) :? point) + (+ p.x p.y)) + 23) + + (test-error "using :? rejects wrong non-false value" + (using (p "bad" :? point) + p)) + + (test "using :- skips type check" + (using (p "not-a-point" :- point) + 99) + 99) + + (test "using :~ predicate success" + (using (n 7 :~ (in-range? 0 10)) + (+ n 1)) + 8) + + (test-error "using :~ predicate failure" + (using (n 12 :~ (in-range? 0 10)) + n))) + ;;; ========== using with as (unchecked) ========== (printf "~%-- using (unchecked) --~%") @@ -114,6 +168,7 @@ (printf "~%-- using (multiple bindings) --~%") (defstruct rect (w h)) +(register-type-predicate! 'rect rect?) (test "using: two bindings" (using ((p (make-point 1 2) : point)