Add Typed Jerboa checker skeleton
ober
e020904f2ed7bc2c37c3931754dde44d9f816584
--- a/Makefile +++ b/Makefile @@ -27,7 +27,7 @@ CHEZ_EXT_LDPATH = $(CHEZ_EXT_DIR)/chez-ssl:$(CHEZ_EXT_DIR)/chez-zlib:$(CHEZ_EXT_ PURE_AUDIT_ROOT ?= $(HOME)/mine PURE_AUDIT_ARGS ?= --summary --discover $(PURE_AUDIT_ROOT) -.PHONY: help chez chez-cross build binary binary-cross native-cross pure-audit test test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded test-contract test-ergo test-typed-parser test-pure-audit test-features test-wrappers test-phase4a test-phase4b test-phase4c test-phase4d test-phase4e test-phase4f test-phase5 test-phase5e test-phase6 test-phase7 test-phase8 test-functional test-repl test-security test-security-profile test-native test-gaps native clean-native audit-native clean security security-production security-profile fuzz fuzz-smoke fuzz-deep fuzz-reader-fuzz fuzz-json-fuzz fuzz-http2-fuzz fuzz-websocket-fuzz fuzz-dns-fuzz fuzz-pregexp-fuzz fuzz-csv-fuzz fuzz-base64-fuzz fuzz-hex-fuzz fuzz-uri-fuzz fuzz-format-fuzz fuzz-router-fuzz fuzz-sandbox-fuzz test-rawstring test-regex test-rx test-peg test-regex-all check-docs check-docs-strict docker-build docker-push +.PHONY: help chez chez-cross build binary binary-cross native-cross pure-audit test test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded test-contract test-ergo test-typed-parser test-typed-checker test-pure-audit test-features test-wrappers test-phase4a test-phase4b test-phase4c test-phase4d test-phase4e test-phase4f test-phase5 test-phase5e test-phase6 test-phase7 test-phase8 test-functional test-repl test-security test-security-profile test-native test-gaps native clean-native audit-native clean security security-production security-profile fuzz fuzz-smoke fuzz-deep fuzz-reader-fuzz fuzz-json-fuzz fuzz-http2-fuzz fuzz-websocket-fuzz fuzz-dns-fuzz fuzz-pregexp-fuzz fuzz-csv-fuzz fuzz-base64-fuzz fuzz-hex-fuzz fuzz-uri-fuzz fuzz-format-fuzz fuzz-router-fuzz fuzz-sandbox-fuzz test-rawstring test-regex test-rx test-peg test-regex-all check-docs check-docs-strict docker-build docker-push help: @echo "Usage: make <target>" @@ -67,6 +67,7 @@ help: @echo " test-contract Runtime contract tests" @echo " test-ergo Ergonomic contract marker tests" @echo " test-typed-parser Typed Jerboa parser tests" + @echo " test-typed-checker Typed Jerboa checker tests" @echo " test-pure-audit Pure Jerboa migration scanner tests" @echo "" @echo "Test (features):" @@ -293,7 +294,7 @@ binary-cross: chez build chez-cross CC="$(CROSS_CC)" \ support/build-binary.sh $(BINARY_ENTRY) $(BINARY_OUTPUT)-$(CHEZ_TARGET_MACHINE) -test: test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded test-regex-all test-contract test-ergo test-typed-parser test-pure-audit +test: test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded test-regex-all test-contract test-ergo test-typed-parser test-typed-checker test-pure-audit pure-audit: @$(SCHEME) --libdirs $(LIBDIRS) --script support/pure-audit.ss $(PURE_AUDIT_ARGS) @@ -347,6 +348,9 @@ test-ergo: test-typed-parser: @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-typed-parser.ss +test-typed-checker: + @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-typed-checker.ss + test-pure-audit: @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-pure-audit.ss --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -137,11 +137,14 @@ Current landing: - `(jerboa typed parser)` parses and validates `(typed-library ...)` datums into a first AST layer. +- `(jerboa typed checker)` performs the first backend-neutral validation pass: + duplicate names, export resolution, type-reference resolution, compound type + arities, duplicate fields, duplicate params, and duplicate variant cases. - 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. -- This is a front-end milestone only. It does not yet typecheck expressions, - resolve imports, lower to typed core IR, or emit Rust/LLVM. +- This is still a front-end milestone. It does not yet typecheck function + bodies, resolve imports, lower to typed core IR, or emit Rust/LLVM. ## Surface Syntax @@ -725,9 +728,10 @@ Minimum excluded features: ### Milestone 2: Type Checker -- Resolve names. +- Resolve names. Initial declaration/export/type-reference validation landed + as `(jerboa typed checker)`. - Build module environment. -- Check primitive expressions. +- Check primitive expressions. Not yet landed. - Check function applications. - Check records and variants. - Check match exhaustiveness. new file mode 100644 --- /dev/null +++ b/lib/jerboa/typed/checker.ss @@ -0,0 +1,234 @@ +#!chezscheme +;;; (jerboa typed checker) -- first Typed Jerboa validation pass +;;; +;;; This checker validates names and type references over the parser AST. +;;; It intentionally does not typecheck function bodies yet. + +(library (jerboa typed checker) + (export + typed-check-error? make-typed-check-error + typed-check-error-kind typed-check-error-message typed-check-error-detail + check-typed-module + typecheck-typed-library-form + typed-module-valid?) + + (import (chezscheme) ; jerboa-security: suppress direct-chezscheme-import-user-code -- trusted typed compiler checker module + (only (jerboa core) def defstruct) + (jerboa typed parser)) + + (defstruct typed-check-error (kind message detail)) + + (def builtin-type-names + '(Unit Bool Char Int Nat Fixnum Float String Bytes Symbol Keyword)) + + (def compound-type-arities + '((List . 1) + (Vector . 1) + (Option . 1) + (Result . 2) + (Pair . 2))) + + (def (make-check-error kind message detail) + (make-typed-check-error kind message detail)) + + (def (append-map f xs) + (let loop ([rest xs] [out '()]) + (if (null? rest) + (reverse out) + (loop (cdr rest) (append (reverse (f (car rest))) out))))) + + (def (symbol-append . parts) + (string->symbol + (apply string-append + (map (lambda (p) + (cond + [(symbol? p) (symbol->string p)] + [(string? p) p] + [else (error 'symbol-append "expected symbol or string" p)])) + parts)))) + + (def (add-unique x xs) + (if (memq x xs) xs (cons x xs))) + + (def (duplicates xs) + (let loop ([rest xs] [seen '()] [dups '()]) + (cond + [(null? rest) (reverse dups)] + [(memq (car rest) seen) + (loop (cdr rest) seen (add-unique (car rest) dups))] + [else + (loop (cdr rest) (cons (car rest) seen) dups)]))) + + (def (duplicate-errors kind message xs) + (map (lambda (x) (make-check-error kind message x)) + (duplicates xs))) + + (def (type-declaration-name decl) + (cond + [(typed-type-decl? decl) (typed-type-decl-name decl)] + [(typed-record? decl) (typed-record-name decl)] + [(typed-variant? decl) (typed-variant-name decl)] + [else #f])) + + (def (declared-type-names declarations) + (let loop ([rest declarations] [out '()]) + (cond + [(null? rest) (reverse out)] + [else + (let ([name (type-declaration-name (car rest))]) + (loop (cdr rest) (if name (cons name out) out)))]))) + + (def (record-value-names record) + (let* ([name (typed-record-name record)] + [prefix (symbol->string name)] + [fields (typed-record-fields record)] + [field-names + (append-map + (lambda (field) + (let ([base (symbol-append prefix "-" (typed-field-name field))]) + (if (typed-field-mutable? field) + (list base (symbol-append base "-set!")) + (list base)))) + fields)]) + (append + (list (symbol-append "make-" name) + (symbol-append name "?")) + field-names))) + + (def (variant-value-names variant) + (cons (symbol-append (typed-variant-name variant) "?") + (map typed-variant-case-name + (typed-variant-cases variant)))) + + (def (declaration-value-names decl) + (cond + [(typed-def? decl) (list (typed-def-name decl))] + [(typed-record? decl) (record-value-names decl)] + [(typed-variant? decl) (variant-value-names decl)] + [else '()])) + + (def (declared-value-names declarations) + (append-map declaration-value-names declarations)) + + (def (known-type? name type-names) + (or (memq name builtin-type-names) + (memq name type-names))) + + (def (check-compound-type type type-names) + (let* ([head (car type)] + [args (cdr type)] + [arity-entry (assq head compound-type-arities)]) + (cond + [(eq? head '->) + (if (< (length args) 2) + (list (make-check-error 'bad-type-arity + "function type needs at least one argument and a result" + type)) + (append-map (lambda (arg) (check-type arg type-names)) args))] + [(not arity-entry) + (list (make-check-error 'unknown-type-constructor + "unknown compound type constructor" + head))] + [(not (= (length args) (cdr arity-entry))) + (list (make-check-error 'bad-type-arity + "wrong number of type arguments" + type))] + [else + (append-map (lambda (arg) (check-type arg type-names)) args)]))) + + (def (check-type type type-names) + (cond + [(symbol? type) + (if (known-type? type type-names) + '() + (list (make-check-error 'unknown-type + "unknown type name" + type)))] + [(pair? type) + (check-compound-type type type-names)] + [else + (list (make-check-error 'bad-type + "invalid type expression" + type))])) + + (def (check-fields fields type-names) + (append + (duplicate-errors 'duplicate-field + "duplicate field name" + (map typed-field-name fields)) + (append-map + (lambda (field) (check-type (typed-field-type field) type-names)) + fields))) + + (def (check-record record type-names) + (check-fields (typed-record-fields record) type-names)) + + (def (check-variant-case case type-names) + (check-fields (typed-variant-case-fields case) type-names)) + + (def (check-variant variant type-names) + (append + (duplicate-errors 'duplicate-variant-case + "duplicate variant case name" + (map typed-variant-case-name (typed-variant-cases variant))) + (append-map + (lambda (case) (check-variant-case case type-names)) + (typed-variant-cases variant)))) + + (def (check-def def type-names) + (append + (duplicate-errors 'duplicate-param + "duplicate parameter name" + (map typed-param-name (typed-def-params def))) + (append-map + (lambda (param) (check-type (typed-param-type param) type-names)) + (typed-def-params def)) + (check-type (typed-def-return-type def) type-names))) + + (def (check-declaration decl type-names) + (cond + [(typed-record? decl) (check-record decl type-names)] + [(typed-variant? decl) (check-variant decl type-names)] + [(typed-def? decl) (check-def decl type-names)] + [else '()])) + + (def (check-exports exports value-names) + (append + (duplicate-errors 'duplicate-export + "duplicate export" + exports) + (let loop ([rest exports] [out '()]) + (cond + [(null? rest) (reverse out)] + [(memq (car rest) value-names) + (loop (cdr rest) out)] + [else + (loop (cdr rest) + (cons (make-check-error 'undefined-export + "export is not provided by a def, record, or variant" + (car rest)) + out))])))) + + (def (check-typed-module module) + (let* ([declarations (typed-module-declarations module)] + [type-names (declared-type-names declarations)] + [value-names (declared-value-names declarations)]) + (append + (duplicate-errors 'duplicate-type + "duplicate type declaration" + type-names) + (duplicate-errors 'duplicate-value + "duplicate value declaration" + value-names) + (check-exports (typed-module-exports module) value-names) + (append-map + (lambda (decl) (check-declaration decl type-names)) + declarations)))) + + (def (typecheck-typed-library-form form) + (check-typed-module (parse-typed-library form))) + + (def (typed-module-valid? module) + (null? (check-typed-module module))) + +) ;; end library --- a/support/build.ss +++ b/support/build.ss @@ -18,6 +18,7 @@ (jerboa modules) (jerboa build) (jerboa typed parser) + (jerboa typed checker) ;; Regex / rx / peg tier — compiled independently so errors are isolated (std srfi srfi-115) (std regex) new file mode 100644 --- /dev/null +++ b/tests/test-typed-checker.ss @@ -0,0 +1,145 @@ +#!chezscheme +;;; Tests for (jerboa typed checker) + +(import (chezscheme) + (jerboa typed parser) + (jerboa typed checker)) + +(define pass 0) +(define fail 0) + +(define-syntax test + (syntax-rules () + [(_ name expr expected) + (guard (exn [#t (set! fail (+ fail 1)) + (printf "FAIL ~a: exception ~a~%" name + (if (message-condition? exn) (condition-message exn) exn))]) + (let ([got expr]) + (if (equal? got expected) + (begin (set! pass (+ pass 1)) + (printf " ok ~a~%" name)) + (begin (set! fail (+ fail 1)) + (printf "FAIL ~a: got ~s expected ~s~%" name got expected)))))])) + +(define (error-kinds form) + (map typed-check-error-kind + (typecheck-typed-library-form form))) + +(define valid-form + '(typed-library (sample typed pane) + (export make-Pane Pane? Pane-id Pane-focused? Pane-focused?-set! + make-pane-size EditOp? Insert Noop) + + (type Split) + + (record Pane + ((id : Nat) + (mut focused? : Bool))) + + (variant EditOp + (Insert (at : Nat) (text : String)) + (Noop)) + + (def (make-pane-size (p : Pane)) : Nat + 0))) + +(printf "--- Typed Jerboa checker tests ---~%") + +(test "valid module has no errors" + (error-kinds valid-form) + '()) + +(test "typed-module-valid?" + (typed-module-valid? (parse-typed-library valid-form)) + #t) + +(test "unknown param type" + (error-kinds + '(typed-library (bad unknown) + (export f) + (def (f (x : Missing)) : Nat + 0))) + '(unknown-type)) + +(test "unknown return type" + (error-kinds + '(typed-library (bad unknown-return) + (export f) + (def (f (x : Nat)) : Missing + x))) + '(unknown-type)) + +(test "unknown compound type constructor" + (error-kinds + '(typed-library (bad compound) + (export f) + (def (f (x : (Map String Nat))) : Nat + 0))) + '(unknown-type-constructor)) + +(test "bad compound type arity" + (error-kinds + '(typed-library (bad arity) + (export f) + (def (f (x : (Option Nat String))) : Nat + 0))) + '(bad-type-arity)) + +(test "duplicate type declarations" + (error-kinds + '(typed-library (bad duplicate-type) + (export f) + (type T) + (record T ((x : Nat))) + (def (f (x : T)) : T + x))) + '(duplicate-type)) + +(test "duplicate def declarations" + (error-kinds + '(typed-library (bad duplicate-def) + (export f) + (def (f (x : Nat)) : Nat x) + (def (f (x : Nat)) : Nat x))) + '(duplicate-value)) + +(test "duplicate field declarations" + (error-kinds + '(typed-library (bad duplicate-field) + (export make-R R?) + (record R ((x : Nat) (x : Nat))))) + '(duplicate-value duplicate-field)) + +(test "duplicate params" + (error-kinds + '(typed-library (bad duplicate-param) + (export f) + (def (f (x : Nat) (x : Nat)) : Nat x))) + '(duplicate-param)) + +(test "duplicate variant case" + (error-kinds + '(typed-library (bad duplicate-case) + (export V? A) + (variant V + (A) + (A)))) + '(duplicate-value duplicate-variant-case)) + +(test "duplicate export" + (error-kinds + '(typed-library (bad duplicate-export) + (export f f) + (def (f (x : Nat)) : Nat x))) + '(duplicate-export)) + +(test "undefined export" + (error-kinds + '(typed-library (bad undefined-export) + (export f missing) + (def (f (x : Nat)) : Nat x))) + '(undefined-export)) + +(printf "~%Typed checker: ~a passed, ~a failed~%" pass fail) +(when (> fail 0) + (exit 1))