Add Typed Jerboa typecheck target
ober
d038747c26d98d6553f49bdb4584059bd158f1ef
--- a/Makefile +++ b/Makefile @@ -26,8 +26,9 @@ CHEZ_EXT_LIBDIRS = $(CHEZ_EXT_DIR)/chez-https/src:$(CHEZ_EXT_DIR)/chez-ssl/src:$ CHEZ_EXT_LDPATH = $(CHEZ_EXT_DIR)/chez-ssl:$(CHEZ_EXT_DIR)/chez-zlib:$(CHEZ_EXT_DIR)/chez-pcre2:$(CHEZ_EXT_DIR)/chez-leveldb:$(CHEZ_EXT_DIR)/chez-epoll:$(CHEZ_EXT_DIR)/chez-inotify:$(CHEZ_EXT_DIR)/chez-crypto:$(CHEZ_EXT_DIR)/chez-sqlite:$(CHEZ_EXT_DIR)/chez-postgresql PURE_AUDIT_ROOT ?= $(HOME)/mine PURE_AUDIT_ARGS ?= --summary --discover $(PURE_AUDIT_ROOT) +TYPED_SOURCES ?= tests/fixtures/typed/valid-split-tree.ss -.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 +.PHONY: help chez chez-cross build binary binary-cross native-cross pure-audit typecheck typed-test typed-clean 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>" @@ -41,6 +42,9 @@ help: @echo " binary-cross Build a jerboa-bin for a foreign target (same args as chez-cross)" @echo " native-cross Cross-build Rust native lib for a target" @echo " Args: CHEZ_TARGET_MACHINE=<mt> CROSS_CC=<cc> [CROSS_NATIVE_FEATURES=tls,...]" + @echo " typecheck Typecheck Typed Jerboa sources" + @echo " typed-test Run Typed Jerboa front-end tests" + @echo " typed-clean Remove generated typed build artifacts" @echo " native Build Rust native library" @echo " clean Remove compiled .so and .wpo artifacts" @echo " clean-native Remove Rust build artifacts" @@ -296,6 +300,14 @@ binary-cross: chez build chez-cross 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 +typecheck: + @$(SCHEME) --libdirs $(LIBDIRS) --script support/typecheck.ss $(TYPED_SOURCES) + +typed-test: test-typed-parser test-typed-checker typecheck + +typed-clean: + @rm -rf build/typed + pure-audit: @$(SCHEME) --libdirs $(LIBDIRS) --script support/pure-audit.ss $(PURE_AUDIT_ARGS) --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -140,6 +140,8 @@ Current landing: - `(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. +- `support/typecheck.ss` and the `make typecheck` / `make typed-test` targets + run the parser/checker over typed source files without invoking Rust. - 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. @@ -602,10 +604,12 @@ typed-llvm Initial meanings: -- `typecheck`: parse and type check typed modules. +- `typecheck`: parse and type check typed modules. Initial target landed for + parser/checker validation over `TYPED_SOURCES`. - `typed-rust`: generate Rust for typed modules. - `typed-build`: generate Rust, compile artifacts, generate wrappers. -- `typed-test`: run typed compiler tests and runtime boundary tests. +- `typed-test`: run typed compiler tests and runtime boundary tests. Initial + target runs parser, checker, and `typecheck`. - `typed-llvm`: reserved until the LLVM backend exists. ## Generated Files new file mode 100644 --- /dev/null +++ b/support/typecheck.ss @@ -0,0 +1,80 @@ +#!chezscheme +;;; typecheck.ss -- run Typed Jerboa parser/checker over source files +;;; +;;; Usage: +;;; scheme --libdirs lib --script support/typecheck.ss file.ss ... + +(import (chezscheme) ; jerboa-security: suppress direct-chezscheme-import-user-code -- trusted build/typecheck script + (jerboa reader) + (jerboa typed parser) + (jerboa typed checker)) + +(define (usage) + (display "Usage: scheme --libdirs lib --script support/typecheck.ss file.ss ...\n")) + +(define (read-all-forms path) + (jerboa-read-file path)) + +(define (typed-library-forms forms) + (let loop ([rest forms] [out '()]) + (cond + [(null? rest) (reverse out)] + [(typed-library-form? (car rest)) + (loop (cdr rest) (cons (car rest) out))] + [else + (loop (cdr rest) out)]))) + +(define (display-check-error path module-name err) + (printf "~a: ~s: ~s: ~a: ~s~%" + path + module-name + (typed-check-error-kind err) + (typed-check-error-message err) + (typed-check-error-detail err))) + +(define (check-typed-form path form) + (let* ([module (parse-typed-library form)] + [errors (check-typed-module module)] + [module-name (typed-module-name module)]) + (for-each + (lambda (err) + (display-check-error path module-name err)) + errors) + (length errors))) + +(define (check-file path) + (guard (exn + [#t + (printf "~a: failed to typecheck: ~a~%" + path + (if (message-condition? exn) + (condition-message exn) + exn)) + 1]) + (let ([forms (typed-library-forms (read-all-forms path))]) + (let loop ([rest forms] [count 0]) + (if (null? rest) + count + (loop (cdr rest) + (+ count (check-typed-form path (car rest))))))))) + +(define args (command-line-arguments)) + +(when (null? args) + (usage) + (exit 2)) + +(let loop ([rest args] [errors 0]) + (if (null? rest) + (begin + (when (= errors 0) + (printf "Typed Jerboa typecheck: ok (~a file~a)~%" + (length args) + (if (= (length args) 1) "" "s"))) + (when (> errors 0) + (printf "Typed Jerboa typecheck: ~a error~a~%" + errors + (if (= errors 1) "" "s")) + (exit 1))) + (loop (cdr rest) + (+ errors (check-file (car rest)))))) new file mode 100644 --- /dev/null +++ b/tests/fixtures/typed/valid-split-tree.ss @@ -0,0 +1,14 @@ +(typed-library (sample typed split-tree) + (export make-Pane Pane? Pane-id Pane-focused? Pane-focused?-set! + split-size EditOp? Insert Noop) + + (record Pane + ((id : Nat) + (mut focused? : Bool))) + + (variant EditOp + (Insert (at : Nat) (text : String)) + (Noop)) + + (def (split-size (pane : Pane)) : Nat + 0))