;; SPDX-FileCopyrightText: 2024 Artyom Bologov
;; SPDX-License-Identifier: MIT

;;; Permission is hereby granted, free of charge, to any person
;;; obtaining a copy of this software and associated documentation
;;; files (the "Software"), to deal in the Software without
;;; restriction, including without limitation the rights to use,
;;; copy, modify, merge, publish, distribute, sublicense, and/or
;;; sell copies of the Software, and to permit persons to whom the
;;; Software is furnished to do so, subject to the following
;;; conditions:
;;;
;;; The above copyright notice and this permission notice shall be
;;; included in all copies or substantial portions of the Software.
;;;
;;; THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
;;; EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
;;; OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
;;; NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
;;; HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
;;; WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
;;; FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
;;; OTHER DEALINGS IN THE SOFTWARE.

(import-for-syntax (chicken type))

(define-syntax assume
  (syntax-rules ()
    ((_ expr rest ...)
     (begin (assert expr rest ...) #t))))

(define-syntax check-arg
  (syntax-rules (pointer? check-impl?)
    ((_ pred val caller)
     (assume (pred val) "argument should match the specification" '(pred val) val caller))
    ((_ pointer? val)
     (when #f #f))
    ((_ (check-impl? type) val)
     (when #f #f))
    ((_ pred val)
     (check-arg pred val 'check-arg))))

(define-syntax values-checked
  (syntax-rules (the check-impl?
                     ;; Predicates
                     exact-integer? integer? boolean? char? complex?
                     fixnum? flonum?
                     eof? inexact? real?
                     list? null? number? pair?
                     input-port? output-port?
                     procedure? rational?
                     string? symbol? keyword? vector? pointer?
                     ;; Types
                     fixnum float boolean char cplxnum eof
                     list null number pair input-port output-port
                     procedure ratnum string symbol keyword vector pointer)
    ((_ (fixnum?) value)
     (let ((v value))
       (check-arg fixnum? v 'values-checked)
       (the fixnum value)))
    ((_ (flonum?) value)
     (let ((v value))
       (check-arg float? v 'values-checked)
       (the float value)))
    ((_ (exact-integer?) value)
     (let ((v value))
       (check-arg integer? v 'values-checked)
       (the integer value)))
    ((_ (integer?) value)
     (let ((v value))
       (check-arg integer? v 'values-checked)
       (the number value)))
    ((_ (boolean?) value)
     (let ((v value))
       (check-arg boolean? v 'values-checked)
       (the boolean value)))
    ((_ (char?) value)
     (let ((v value))
       (check-arg char? v 'values-checked)
       (the char value)))
    ((_ (complex?) value)
     (let ((v value))
       (check-arg complex? v 'values-checked)
       (the cplxnum value)))
    ((_ (eof-object?) value)
     (let ((v value))
       (check-arg eof-object? v 'values-checked)
       (the eof value)))
    ((_ (inexact?) value)
     (let ((v value))
       (check-arg inexact? v 'values-checked)
       (the float value)))
    ((_ (real?) value)
     (let ((v value))
       (check-arg real? v 'values-checked)
       (the number value)))
    ((_ (list?) value)
     (let ((v value))
       (check-arg list? v 'values-checked)
       (the list value)))
    ((_ (null?) value)
     (let ((v value))
       (check-arg null? v 'values-checked)
       (the null value)))
    ((_ (number?) value)
     (let ((v value))
       (check-arg number? v 'values-checked)
       (the number value)))
    ((_ (pair?) value)
     (let ((v value))
       (check-arg pair? v 'values-checked)
       (the pair value)))
    ((_ (input-port?) value)
     (let ((v value))
       (check-arg input-port? v 'values-checked)
       (the input-port value)))
    ((_ (output-port?) value)
     (let ((v value))
       (check-arg output-port? v 'values-checked)
       (the output-port value)))
    ((_ (procedure?) value)
     (let ((v value))
       (check-arg procedure? v 'values-checked)
       (the procedure value)))
    ((_ (rational?) value)
     (let ((v value))
       (check-arg rational? v 'values-checked)
       (the ratnum value)))
    ((_ (string?) value)
     (let ((v value))
       (check-arg string? v 'values-checked)
       (the string value)))
    ((_ (symbol?) value)
     (let ((v value))
       (check-arg symbol? v 'values-checked)
       (the symbol value)))
    ((_ (keyword?) value)
     (let ((v value))
       (check-arg keyword? v 'values-checked)
       (the keyword value)))
    ((_ (vector?) value)
     (let ((v value))
       (check-arg vector? v 'values-checked)
       (the vector value)))
    ((_ (pointer?) value)
     (let ((v value))
       ;; No check-arg—dummy predicate
       (the pointer value)))
    ((_ (check-impl? type) value)
     (let ((v value))
       ;; No check-arg—dummy predicate
       (the type value)))
    ((_ (predicate) value)
     (let ((v value))
       (check-arg predicate v 'values-checked)
       v))
    ((_ (predicate ...) value ...)
     (values (values-checked (predicate) value) ...))))

(cond-expand
  (csc
    (define-syntax %check-case
      (syntax-rules (else
                      ;; Predicates
                      fixnum? flonum? exact-integer? integer? boolean? char?
                      complex? eof? inexact? real? list? null? number? pair?
                      input-port? output-port? procedure? rational? string?
                      symbol? keyword? vector? pointer?
                      ;; Types
                      fixnum float integer number boolean char cplxnum eof list
                      null pair input-port output-port procedure ratnum string
                      symbol keyword vector pointer)
        ((_ val (typed-clause ...) ())
         (compiler-typecase val typed-clause ...))
        ((_ val () ((regular-check regular-body ...) ...))
         (cond
           (regular-check regular-body ...) ...
           (else (assume (or regular-check ...)))))
        ((_ val (typed-clause ...) ((regular-check regular-body ...) ...))
         (compiler-typecase
           val typed-clause ...
           (else
             (cond
               (regular-check regular-body ...) ...
               (else (assume (or regular-check ...)))))))
        ((_ val (typed-clause ...) () (else body ...))
         (compiler-typecase
           val typed-clause ...
           (else body ...)))
        ((_ val () (regular-clause ...) (else body ...))
         (cond
           regular-clause ...
           (else body ...)))
        ((_ val (typed ...) regular (fixnum? body ...) rest ...)
         (%check-case val (typed ... (fixnum body ...)) regular rest ...))
        ((_ val (typed ...) regular (flonum? body ...) rest ...)
         (%check-case val (typed ... (float body ...)) regular rest ...))
        ((_ val (typed ...) regular (exact-integer? body ...) rest ...)
         (%check-case val (typed ... (integer body ...)) regular rest ...))
        ((_ val (typed ...) regular (integer? body ...) rest ...)
         (%check-case val (typed ... (number body ...)) regular rest ...))
        ((_ val (typed ...) regular (boolean? body ...) rest ...)
         (%check-case val (typed ... (boolean body ...)) regular rest ...))
        ((_ val (typed ...) regular (char? body ...) rest ...)
         (%check-case val (typed ... (char body ...)) regular rest ...))
        ((_ val (typed ...) regular (complex? body ...) rest ...)
         (%check-case val (typed ... (cplxnum body ...)) regular rest ...))
        ((_ val (typed ...) regular (eof? body ...) rest ...)
         (%check-case val (typed ... (eof body ...)) regular rest ...))
        ((_ val (typed ...) regular (inexact? body ...) rest ...)
         (%check-case val (typed ... (float body ...)) regular rest ...))
        ((_ val (typed ...) regular (real? body ...) rest ...)
         (%check-case val (typed ... (number body ...)) regular rest ...))
        ((_ val (typed ...) regular (list? body ...) rest ...)
         (%check-case val (typed ... (list body ...)) regular rest ...))
        ((_ val (typed ...) regular (null? body ...) rest ...)
         (%check-case val (typed ... (null body ...)) regular rest ...))
        ((_ val (typed ...) regular (number? body ...) rest ...)
         (%check-case val (typed ... (number body ...)) regular rest ...))
        ((_ val (typed ...) regular (pair? body ...) rest ...)
         (%check-case val (typed ... (pair body ...)) regular rest ...))
        ((_ val (typed ...) regular (input-port? body ...) rest ...)
         (%check-case val (typed ... (input-port body ...)) regular rest ...))
        ((_ val (typed ...) regular (output-port? body ...) rest ...)
         (%check-case val (typed ... (output-port body ...)) regular rest ...))
        ((_ val (typed ...) regular (procedure? body ...) rest ...)
         (%check-case val (typed ... (procedure body ...)) regular rest ...))
        ((_ val (typed ...) regular (rational? body ...) rest ...)
         (%check-case val (typed ... (ratnum body ...)) regular rest ...))
        ((_ val (typed ...) regular (string? body ...) rest ...)
         (%check-case val (typed ... (string body ...)) regular rest ...))
        ((_ val (typed ...) regular (symbol? body ...) rest ...)
         (%check-case val (typed ... (symbol body ...)) regular rest ...))
        ((_ val (typed ...) regular (keyword? body ...) rest ...)
         (%check-case val (typed ... (keyword body ...)) regular rest ...))
        ((_ val (typed ...) regular (vector? body ...) rest ...)
         (%check-case val (typed ... (vector body ...)) regular rest ...))
        ((_ val (typed ...) regular (pointer? body ...) rest ...)
         (%check-case val (typed ... (pointer body ...)) regular rest ...))
        ((_ val typed (regular ...) (pred body ...) rest ...)
         (%check-case val typed (regular ... ((pred val) body ...)) rest ...))))
    (define-syntax check-case
      (syntax-rules (%check-case)
        ((_ value clause ...)
         (let ((v value))
           (%check-case v () () clause ...))))))
  (else
    (define-syntax %check-case
      (syntax-rules (else)
        ((_ val (clause ...) (else body ...))
         (cond
           clause ...
           (else body ...)))
        ((_ val ((clause-check clause-body ...) ...))
         (cond
           (clause-check clause-body ...)
           ...
           (else (assume (or clause-check ...)
                         "at least one branch of check-case should be true"
                         'clause-check ...))))
        ;; FIXME: pointer? not supported
        ((_ val (clause ...) (pred body ...) rest ...)
         (%check-case
           val
           (clause ... ((pred val) body ...))
           rest ...))))
    (define-syntax check-case
      (syntax-rules ()
        ((_ value clause ...)
         (let ((v value))
           (%check-case v () clause ...)))))))

(define-syntax %lambda-checked
  (syntax-rules (=> pointer? check-impl?)
    ((_ name (=> (return ...) body ...) args (checks ...))
     (lambda args
       checks ...
       (values-checked
         (return ...)
         (begin
           body ...))))
    ((_ name (body ...) args (checks ...))
     (lambda args
       checks ...
       body ...))
    ;; Special case: pointer? is a dummy predicate not having a procedure
    ((_ name body (args ...) (checks ...) (arg pointer?) rest ...)
     (%lambda-checked
       name body
       (args ... arg) (checks ...) rest ...))
    ;; Dummy check too
    ((_ name body (args ...) (checks ...) (arg (check-impl? type)) rest ...)
     (%lambda-checked
       name body
       (args ... arg) (checks ...) rest ...))
    ((_ name body (args ...) (checks ...) (arg pred) rest ...)
     (%lambda-checked
       name body
       (args ... arg) (checks ... (check-arg pred arg 'name)) rest ...))
    ((_ name body (args ...) (checks ...) arg rest ...)
     (%lambda-checked
       name body
       (args ... arg) (checks ...) rest ...))))

(define-syntax lambda-checked
  (syntax-rules (=>)
    ;; Regular (positional ...) arglist
    ((_ (args ...) body ...)
     (%lambda-checked lambda-checked (body ...) () () args ...))
    ;; arg->list lambda, but with return checking
    ((_ arg => (returns ...) body ...)
     (lambda arg
       (values-checked (returns ...) (begin body ...))))
    ;; Case of arg->list lambda, no-op.
    ((_ arg body ...)
     (lambda arg body ...))))

(define-syntax %case-lambda-checked
  (syntax-rules (=>)
    ;; Terminal case, generate the actual case-lambda
    ((_ (clauses-so-far ...)
        ()
        args-so-far (checks-so-far ...) (body ...))
     (case-lambda
       clauses-so-far ...
       (args-so-far
         checks-so-far ...
         body ...)))
    ;; Empty arglist with returns
    ((_ (clauses-so-far ...)
        ((() => (returns ...) body-to-process ...) clauses-to-process ...)
        args-so-far (checks-so-far ...) (body ...))
     (%case-lambda-checked
       (clauses-so-far ... (args-so-far checks-so-far ... body ...))
       (clauses-to-process ...)
       () () ((values-checked (returns ...) (begin body-to-process ...)))))
    ;; Empty args without returns
    ((_ (clauses-so-far ...)
        ((() body-to-process ...) clauses-to-process ...)
        args-so-far (checks-so-far ...) (body ...))
     (%case-lambda-checked
       (clauses-so-far ... (args-so-far checks-so-far ... body ...))
       (clauses-to-process ...)
       () () (body-to-process ...)))
    ;; Regular args with returns
    ((_ (clauses-so-far ...)
        (((args ...) => (returns ...) body-to-process ...) clauses-to-process ...)
        args-so-far (checks-so-far ...) (body ...))
     (%case-lambda-checked
       (clauses-so-far ... (args-so-far checks-so-far ... body ...))
       (clauses-to-process ...)
       () () ((values-checked (returns ...) (begin body-to-process ...))) args ...))
    ;; Regular args without returns
    ((_ (clauses-so-far ...)
        (((args ...) body-to-process ...) clauses-to-process ...)
        args-so-far (checks-so-far ...) (body ...))
     (%case-lambda-checked
       (clauses-so-far ... (args-so-far checks-so-far ... body ...))
       (clauses-to-process ...)
       () () (body-to-process ...) args ...))
    ;; Rest arg with returns
    ((_ (clauses-so-far ...)
        ((arg-to-process => (returns ...) body-to-process ...) clauses-to-process ...)
        args-so-far (checks-so-far ...) (body ...))
     (%case-lambda-checked
       (clauses-so-far ... (args-so-far checks-so-far ... body ...))
       (clauses-to-process ...)
       arg-to-process () ((values-checked (returns ...) (begin body-to-process ...)))))
    ;; Rest arg without returns
    ((_ (clauses-so-far ...)
        ((arg-to-process body-to-process ...) clauses-to-process ...)
        args-so-far (checks-so-far ...) (body ...))
     (%case-lambda-checked
       (clauses-so-far ... (args-so-far checks-so-far ... body ...))
       (clauses-to-process ...)
       arg-to-process () (body-to-process ...)))
    ;; Consume arg with predicate / check
    ((_ (clauses-so-far ...) (clauses-to-process ...)
        (args-so-far ...) (checks-so-far ...) (body ...) (arg pred) . args)
     (%case-lambda-checked
       (clauses-so-far ...) (clauses-to-process ...)
       (args-so-far ... arg)
       (checks-so-far ... (check-arg pred arg 'case-lambda-checked))
       (body ...) . args))
    ;; Consume regular arg
    ((_ (clauses-so-far ...) (clauses-to-process ...)
        (args-so-far ...) (checks-so-far ...) (body ...) arg args ...)
     (%case-lambda-checked
       (clauses-so-far ...) (clauses-to-process ...)
       (args-so-far ... arg) (checks-so-far ...) (body ...) args ...))))

(define-syntax case-lambda-checked
  (syntax-rules (=>)
    ;; First clause: empty args with returns
    ((_ (() => (returns ...) first-body ...) rest-clauses ...)
     (%case-lambda-checked () (rest-clauses ...) () () ((values-checked (returns ...) (begin first-body ...)))))
    ;; First clause: empty args without returns
    ((_ (() first-body ...) rest-clauses ...)
     (%case-lambda-checked () (rest-clauses ...) () () (first-body ...)))
    ;; First clause: args with returns
    ((_ ((args ...) => (returns ...) first-body ...) rest-clauses ...)
     (%case-lambda-checked
       () (rest-clauses ...) () ()
       ((values-checked (returns ...) (begin first-body ...)))
       args ...))
    ;; First clause: args without returns
    ((_ ((args ...) first-body ...) rest-clauses ...)
     (%case-lambda-checked () (rest-clauses ...) () () (first-body ...) args ...))
    ;; First clause: rest arg with returns
    ((_ (args-var => (returns ...) first-body ...) rest-clauses ...)
     (%case-lambda-checked () (rest-clauses ...) args-var () ((values-checked (returns ...) (begin first-body ...)))))
    ;; First clause: rest arg without returns
    ((_ (args-var first-body ...) rest-clauses ...)
     (%case-lambda-checked () (rest-clauses ...) args-var () (first-body ...)))))

(define-syntax %declare-checked-var
  (syntax-rules (: -> check-impl?
                   integer? exact-integer? boolean? char? complex?
                   fixnum? flonum?
                   eof? inexact? real?
                   list? null? number? pair?
                   input-port? output-port?
                   procedure? rational?
                   string? symbol? keyword? vector? pointer?
                   check-any? check-list-of? check-vector-of? check-pair-of? check-procedure-of?

                   integer boolean char cplxnum eof fixnum float
                   number list null number pair input-port output-port
                   procedure ratnum string symbol keyword vector pointer *)
    ((_ name check-any?)     (: name *))
    ((_ name fixnum?)        (: name fixnum))
    ((_ name flonum?)        (: name float))
    ((_ name integer?)       (: name number))
    ((_ name exact-integer?) (: name integer))
    ((_ name boolean?)       (: name boolean))
    ((_ name char?)          (: name char))
    ((_ name complex?)       (: name cplxnum))
    ((_ name eof?)           (: name eof))
    ((_ name inexact?)       (: name float))
    ((_ name real?)          (: name number))
    ((_ name list?)          (: name list))
    ((_ name (check-list-of? _)) (: name list))
    ((_ name (check-list-of? _ _)) (: name list))
    ((_ name null?)          (: name null))
    ((_ name number?)        (: name number))
    ((_ name pair?)          (: name pair))
    ((_ name (check-pair-of? _ _)) (: name pair))
    ((_ name input-port?)    (: name input-port))
    ((_ name output-port?)   (: name output-port))
    ((_ name procedure?)     (: name procedure))
    ((_ name (check-procedure-of? _ _)) (: name procedure))
    ((_ name rational?)      (: name ratnum))
    ((_ name string?)        (: name string))
    ((_ name symbol?)        (: name symbol))
    ((_ name keyword?)       (: name keyword))
    ((_ name vector?)        (: name vector))
    ((_ name (check-vector-of? _)) (: name vector))
    ((_ name pointer?)       (: name pointer))
    ((_ name (check-impl? type)) (: name type))
    ((_ name predicate)
     (when #f #f))))
(define-syntax %declare-checked-fn/return
  (syntax-rules (: -> check-impl?
                   integer? boolean? char? complex?
                   fixnum? flonum?
                   eof? inexact? real?
                   list? null? number? pair?
                   input-port? output-port?
                   procedure? rational?
                   string? symbol? keyword? vector? pointer?
                   check-any? check-list-of? check-vector-of? check-pair-of? check-procedure-of?

                   integer boolean char cplxnum eof fixnum float
                   number list null number pair input-port output-port
                   procedure ratnum string symbol keyword vector pointer *)
    ((_ name (arg-type ...) ())
     (: name (arg-type ...) -> *))
    ((_ name (arg-type ...) (return-type ...))
     (: name (arg-type ... -> return-type ...)))
    ((_ name (arg-type ...) (return-type ...) check-any? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... *) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) fixnum? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... fixnum) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) flonum? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... float) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) integer? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... integer) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) exact-integer? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... integer) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) boolean? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... boolean) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) char? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... char) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) complex? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... cmlxnum) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) eof? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... eof) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) inexact? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... float) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) real? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... number) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) list? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... list) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) (check-list-of? _) other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... list) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) null? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... null) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) number? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... number) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) pair? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... pair) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) (check-pair-of? _ _) other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... pair) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) input-port? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... input-port) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) output-port? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... output-port) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) procedure? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... procedure) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) (check-procedure-of? _ _) other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... procedure) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) rational? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... ratnum) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) string? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... string) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) symbol? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... symbol) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) keyword? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... keyword) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) vector? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... vector) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) (check-vector-of? _) other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... vector) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) pointer? other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... pointer) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) (check-impl? type) other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... type) other-returns ...))
    ((_ name (arg-type ...) (return-type ...) pred other-returns ...)
     (%declare-checked-fn/return name (arg-type ...) (return-type ... *) other-returns ...))))
(define-syntax %declare-checked-fn
  (syntax-rules (: -> check-impl?
                   integer? boolean? char? complex?
                   fixnum? flonum?
                   eof? inexact? real?
                   list? null? number? pair?
                   input-port? output-port?
                   procedure? rational?
                   string? symbol? keyword? vector? pointer?
                   check-any? check-list-of? check-vector-of? check-pair-of? check-procedure-of?

                   integer boolean char cplxnum eof fixnum float
                   number list null number pair input-port output-port
                   procedure ratnum string symbol keyword vector pointer *)
    ((_ name (return ...) () (type ...))
     (%declare-checked-fn/return name (type ...) () return ...))
    ((_ name return ((arg fixnum?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... fixnum)))
    ((_ name return ((arg flonum?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... float)))
    ((_ name return ((arg integer?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... number)))
    ((_ name return ((arg boolean?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... boolean)))
    ((_ name return ((arg char?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... char)))
    ((_ name return ((arg complex?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... cplxnum)))
    ((_ name return ((arg eof?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... eof)))
    ((_ name return ((arg inexact?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... float)))
    ((_ name return ((arg real?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... number)))
    ((_ name return ((arg list?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... list)))
    ((_ name return ((arg null?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... null)))
    ((_ name return ((arg number?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... number)))
    ((_ name return ((arg pair?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... pair)))
    ((_ name return ((arg input-port?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... input-port)))
    ((_ name return ((arg output-port?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... output-port)))
    ((_ name return ((arg procedure?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... procedure)))
    ((_ name return ((arg rational?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... ratnum)))
    ((_ name return ((arg string?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... string)))
    ((_ name return ((arg symbol?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... symbol)))
    ((_ name return ((arg keyword?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... keyword)))
    ((_ name return ((arg vector?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... vector)))
    ((_ name return ((arg pointer?) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... pointer)))
    ((_ name return ((arg (check-impl? impl-type)) check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... impl-type)))
    ((_ name return (arg check ...) (type ...))
     (%declare-checked-fn name return (check ...) (type ... *)))))

(define-syntax define-checked
  (syntax-rules (=>)
    ;; Function with return checks
    ((_ (name arg ...) => (return ...) body ...)
     (begin
       (%declare-checked-fn name (return ...) (arg ...) ())
       (define name (%lambda-checked name (=> (return ...) body ...) () () arg ...))))
    ;; Function
    ((_ (name arg ...) body ...)
     (begin
       (%declare-checked-fn name (check-any?) (arg ...) ())
       (define name (%lambda-checked name (body ...) () () arg ...))))
    ;; Variable
    ((_ name pred value)
     (begin
       (%declare-checked-var name pred)
       (define name (values-checked (pred) value))))))

(define-syntax %define-record-type-checked
  (syntax-rules ()
    ((_ type-name constructor predicate
        (fields ...) (field-wrappers ...))
     (begin
       (define-record-type
         type-name constructor predicate
         fields ...)
       field-wrappers ...))
    ((_ type-name constructor predicate
        (fields ...) (field-wrappers ...) (field pred accessor modifier)
        fields-to-process ...)
     (%define-record-type-checked
       type-name constructor predicate
       (fields ... (field internal-accessor internal-modifier))
       (field-wrappers
         ...
         (define-checked (accessor (record predicate))
           (internal-accessor record))
         (define-checked (modifier (record predicate) (val pred))
           (internal-modifier record val)))
       fields-to-process ...))
    ((_ type-name constructor predicate
        (fields ...) (field-wrappers ...) (field pred accessor)
        fields-to-process ...)
     (%define-record-type-checked
       type-name constructor predicate
       (fields ... (field internal-accessor))
       (field-wrappers
         ...
         (define-checked (accessor (record predicate))
           (internal-accessor record)))
       fields-to-process ...))))

(define-syntax %wrap-constructor
  (syntax-rules ()
    ((_ constructor internal-constructor (arg-names ...) (args ...))
     (define-checked (constructor args ...)
       (internal-constructor arg-names ...)))
    ((_ constructor internal-constructor (arg-names ...) (args ...)
        (name pred rest ...) fields-to-process ...)
     (%wrap-constructor constructor internal-constructor
                        (arg-names ... name) (args ... (name pred))
                        fields-to-process ...))))

(define-syntax define-record-type-checked
  (syntax-rules ()
    ((_ type-name (constructor constructor-args ...) predicate field ...)
     (begin
       (%define-record-type-checked
         type-name
         (internal-constructor constructor-args ...)
         predicate
         () () field ...)
       (%wrap-constructor constructor internal-constructor () () field ...)))))