vouivre/system.scm

   1 ;;;; Copyright (C) 2024 Vouivre Digital Corporation
   2 ;;;;
   3 ;;;; This file is part of Vouivre.
   4 ;;;;
   5 ;;;; Vouivre is free software: you can redistribute it and/or
   6 ;;;; modify it under the terms of the GNU General Public
   7 ;;;; License as published by the Free Software Foundation, either
   8 ;;;; version 3 of the License, or (at your option) any later version.
   9 ;;;;
  10 ;;;; Vouivre is distributed in the hope that it will be useful,
  11 ;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
  12 ;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
  13 ;;;; General Public License for more details.
  14 ;;;;
  15 ;;;; You should have received a copy of the GNU General Public
  16 ;;;; License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
  17
  18 (define-module (vouivre type system)
  19   #:use-module (ice-9 match)
  20   #:use-module (ice-9 receive)
  21   #:use-module (srfi srfi-1)
  22   #:use-module (srfi srfi-9)
  23   #:use-module (vouivre misc)
  24   #:export
  25   (d
  26    apply-rule
  27    derivation?
  28    derivation-tree
  29    derivation-steps
  30    define-derivation
  31    define-rule
  32    define-derivation-list
  33    *rules*
  34    *definition-rules*))
  35
  36 ;;;; miscellaneous routines
  37
  38 (define (papply proc . args)
  39   (lambda (. rest)
  40     (apply proc (append args rest))))
  41
  42 (define-syntax-rule (second-value expr)
  43   (receive (x y . rest)
  44       expr y))
  45
  46 (define (unzip lst)
  47   (map reverse
  48    (let rec ((lst lst)
  49              (acc (map (const '())
  50                        (car lst))))
  51      (if (null? lst)
  52          acc
  53          (rec (cdr lst)
  54               (map cons (car lst) acc))))))
  55
  56 ;;;; data
  57
  58 (define *constructors* (make-hash-table))
  59 (define *rules* (make-hash-table))
  60 (define *definition-rules* (make-hash-table))
  61 (define *types* (make-hash-table))
  62 (define *ctxs* (make-parameter #f))
  63
  64 (define-record-type derivation
  65   (make-derivation tree steps)
  66   derivation?
  67   (tree derivation-tree)
  68   (steps derivation-steps))
  69
  70 (define-record-type substitution
  71   (make-substitution pattern source destination)
  72   substitution?
  73   (pattern substitution-pattern)
  74   (source substitution-source)
  75   (destination substitution-destination))
  76
  77 (define element-of-:xX second)
  78 (define judgment-context (papply take-while (compose not (papply eq? '⊢))))
  79 (define judgment-content last)
  80 (define meta-conclusion car)
  81 (define meta-hypotheses cdr)
  82 (define constructor-ref (papply hash-ref *constructors*))
  83 (define (context-ref ctx var)
  84   (find (lambda (:xX)
  85           (eq? var (element-of-:xX :xX)))
  86         ctx))
  87 (define rule-ref (papply hash-ref *rules*))
  88 (define type-ref (papply hash-ref *types*))
  89
  90 ;; NOTE: The requirement that for declared types and constructors we can list
  91 ;;       the kind of its arguments, if any, imposes additional constraints that
  92 ;;       must be checked in `define-rule'. Incidentally, we can dispense with
  93 ;;       some checks here because we know that interned metas satisfy these
  94 ;;       constraints.
  95 (define (meta-arguments-kinds meta)
  96   (let ((content (judgment-content (meta-conclusion meta))))
  97     (ifn (list? content)
  98          (parse-error
  99           "meta-arguments-kinds: requires a type kind of judgment.")
 100          (case (first content)
 101            ((type)
 102             (case (car (second content))
 103               ((→)
 104                '(type type))
 105               ((Π)
 106                '(binding type))
 107               ((=)
 108                '(element element))
 109               ((Σ)
 110                '(binding type))
 111               ((List)
 112                '(type))
 113               ((Vector)
 114                '(type element))
 115               (else (parse-error "unsupported type."))))
 116            (else
 117             (parse-error
 118              "meta-arguments-kinds: requires a type kind of judgment."))))))
 119
 120 (define (d judgment)
 121   (make-derivation (cons judgment #f) '()))
 122
 123 (define (derivation-point derivation)
 124   (call/cc
 125    (lambda (break)
 126      (let rec ((tree (derivation-tree derivation)))
 127        (ifn (cdr tree)
 128             (break (car tree))
 129             (ifn (list? (cdr tree))
 130                  #f
 131                  (fold (lambda (x _)
 132                          (rec x))
 133                        #f (cdr tree))))))))
 134
 135 (define (expand-derivation-point derivation step stuff)
 136   (match-let (((expanded? . tree)
 137                (let rec ((tree (derivation-tree derivation)))
 138                  (ifn (cdr tree)
 139                       (cons #t (cons (car tree) stuff))
 140                       (ifn (list? (cdr tree))
 141                            (cons #f tree)
 142                            (match-let (((expanded? . rlst)
 143                                         (fold (lambda (x prev)
 144                                                 (if (car prev)
 145                                                     (cons #t (cons x (cdr prev)))
 146                                                     (let ((r (rec x)))
 147                                                       (cons (car r)
 148                                                             (cons (cdr r) (cdr prev))))))
 149                                               '(#f . ())
 150                                               (cdr tree))))
 151                              (cons expanded? (cons (car tree) (reverse rlst)))))))))
 152     (values (make-derivation tree (cons step (derivation-steps derivation)))
 153             expanded?)))
 154
 155 (define (list-hypotheses derivation)
 156   (delete-duplicates
 157    (let rec ((tree (derivation-tree derivation))
 158              (lst '()))
 159      (if (or (not (cdr tree))
 160              (not (list? (cdr tree))))
 161          (cons (car tree) lst)
 162          (fold rec lst (cdr tree))))
 163    equal?))
 164
 165 ;;;; parsing routines
 166
 167 ;;; In what follows, we want to do for judgments what `map' and `fold' do for
 168 ;;; lists – to evaluate a function on the judgment's intrinsics. We proceed by
 169 ;;; implementing map/fold routines in a "Russian doll" kind of way from big to
 170 ;;; small (although they appear in this file in reverse order i.e from callee to
 171 ;;; caller): judgment, content and context, type, and element. For each of these
 172 ;;; we have a "dispatch" routine to abstract away the structural analysis and
 173 ;;; validation that is common to the corresponding map and fold. Follows, a
 174 ;;; simple application of `judgment-map'. The others work in a similar fashion.
 175 ;;;
 176 ;;; (define (prime x) (string->symbol (string-append (symbol->string x) "'")))
 177 ;;;
 178 ;;; (judgment-map (lambda (kind x y)
 179 ;;;             (case kind
 180 ;;;               ((type)
 181 ;;;                (prime y))
 182 ;;;               (else x)))
 183 ;;;           #f
 184 ;;;           '(Λ ⊢ (type A))
 185 ;;;           '(Ξ ⊢ (type B)))
 186 ;;; => (Λ ⊢ (type B'))
 187 ;;;
 188 ;;; As you can see, there are two differences with `map'. The first is `kind',
 189 ;;; which binds to the kind of intrinsics currently being mapped (either
 190 ;;; 'element, 'type, 'Γ, or 'Δ). The second is the range, `#f' here, which
 191 ;;; allows the split of variable declarations between Γs and Δs.
 192
 193 (define (parse-error str . format-args)
 194   (error (string-append "parsing error: "
 195                         (apply format #f str format-args))))
 196
 197 (define just cdr)
 198
 199 (define (pre-destruct kind expr)
 200   (define fmt "destruct: unknown expression ~a of kind ~a.")
 201   ;; Since the name can be any expression including `#f' we wrap it as a
 202   ;; "Maybe" so that we can distinguish the absence of a name from the name
 203   ;; `#f'.
 204   (ifn (list? expr)
 205        (values (cons 'just expr) '())
 206        (if (or (null? expr)
 207                (null? (cdr expr)))
 208            (parse-error fmt expr kind)
 209            (if (list? (car expr))
 210                (if (eq? kind 'type)
 211                    (parse-error fmt expr kind)
 212                    ;; When instead of a name we have an s-expression the
 213                    ;; expression must have a size of exactly two.
 214                    (ifn (null? (cddr expr))
 215                         (parse-error fmt expr kind)
 216                         (values #f (cdr expr))))
 217                (values (cons 'just (car expr))
 218                        (cdr expr))))))
 219
 220 (define (destruct kind expr)
 221   "Destructure an element or type into its head, tail, and meta data, raising an
 222    error if the expression has an unexpected format.
 223
 224    kind: The kind of expression to destructure. This is either 'type or
 225          'element.
 226
 227    expr: The expression to destructure.
 228
 229    Returns Maybe name, List arguments, and either `#f' or the name's meta data,
 230    as multiple values."
 231   (define referee (if (eq? kind 'element) constructor-ref type-ref))
 232   (define fmt "destruct: unknown expression ~a of kind ~a.")
 233   (receive (maybe-name args) (pre-destruct kind expr)
 234     (ifn maybe-name
 235          (values maybe-name args #f)
 236          (if-let (meta (referee (just maybe-name)))
 237                  (let ((n-args (length args))
 238                        (n-meta-args (length (second-value
 239                                              (pre-destruct
 240                                               kind
 241                                               (element-of-:xX
 242                                                (judgment-content
 243                                                 (meta-conclusion meta))))))))
 244                    (if (= n-args n-meta-args)
 245                        (values maybe-name args meta)
 246                        ;; We allow constructors declared with no arguments to be
 247                        ;; curried applications.
 248                        (if (and (eq? kind 'element)
 249                                 (= 1 n-args)
 250                                 (zero? n-meta-args))
 251                            (values maybe-name args meta)
 252                            (parse-error "destruct: declared expression ~a has ~a arguments, but expected ~a." expr n-args n-meta-args))))
 253                  (values maybe-name args #f)))))
 254
 255 (define (element-dispatch function exprs)
 256   "Dispatch a function based on the given elements or raise an error if they
 257    have an unexpcted format. There are three kinds of expressions: declared
 258    constructors, undeclared constructors, and curried application to an
 259    argument.
 260
 261    function: A function of one argument called with 'declared, 'undeclared, or
 262              'applied if, respectively, expressions are: all declared, any are
 263              undeclared, or all are applied.
 264
 265    exprs: List of expressions.
 266
 267    Returns the result of the function application."
 268   (define element-destruct (papply destruct 'element))
 269   (receive (maybe-names argss metas)
 270       (unzip3 (map (lambda (expr) (receive vals (element-destruct expr) vals))
 271                    exprs))
 272     ;; All declared constructors must have the same meta data and their number
 273     ;; of arguments must match.
 274     (unless (apply eq? (remove not metas))
 275       (parse-error "element-dispatch: declared constructors don't match."))
 276     (if (every (lambda (maybe-name args meta)
 277                  (or (not maybe-name)
 278                      (and meta
 279                           (= 1 (length args))
 280                           (zero? (length (second-value
 281                                           (pre-destruct
 282                                            'element
 283                                            (element-of-:xX
 284                                             (judgment-content
 285                                              (meta-conclusion meta))))))))))
 286                maybe-names argss metas)
 287         (function 'applied maybe-names argss metas)
 288         (if (every identity metas)
 289             (function 'declared maybe-names argss metas)
 290             (function 'undeclared maybe-names argss metas)))))
 291
 292 (define (element-map function expr . more)
 293   "Map a function on the given elements or raise an error if they have unexpected
 294    format.
 295
 296    function: A function that will always be called with 'element as its first
 297              argument, to be consistant with `type-map', and then with the
 298              corresponding intrinsics of each expression.
 299
 300    expr . more: One or more expressions.
 301
 302    Returns an element that is the result of mapping the function to the
 303    corresponding intrinsics."
 304   (let ((exprs (cons expr more)))
 305     (element-dispatch
 306      (lambda (kind maybe-names argss metas)
 307        (case kind
 308          ((declared)
 309           (if (null? (car argss))
 310               (apply function 'element exprs)
 311               (cons (just (car maybe-names)) ; all expressions have the same name
 312                     (apply map
 313                            (lambda formals
 314                              (apply element-map function formals))
 315                            argss))))
 316          ((undeclared)
 317           (apply function 'element exprs))
 318          ((applied)
 319           ;; Each expression is of the form '(f x).
 320           (list (apply element-map function (map first exprs))
 321                 (apply element-map function (map second exprs))))))
 322      exprs)))
 323
 324 (define (element-fold function init expr . more)
 325   "Fold a function over the given elements or raise an error if they have
 326    unexpected format.
 327
 328    function: A function that will always be called with 'element as its first
 329              argument, to be consistant with `type-fold', and then with the
 330              corresponding intrinsics of each expression, followed by the
 331              latest accumulator.
 332
 333    expr . more: One or more expressions.
 334
 335    Returns an element that is the result of folding the function over the
 336    corresponding intrinsics."
 337   (let ((exprs (cons expr more)))
 338     (element-dispatch
 339      (lambda (kind maybe-names argss metas)
 340        (case kind
 341          ((declared)
 342           (if (null? (car argss))
 343               (apply function 'element `(,@exprs ,init))
 344               (apply fold
 345                      (lambda formals
 346                        (apply element-fold function
 347                               (last formals)
 348                               (but-last formals)))
 349                      init argss)))
 350          ((undeclared)
 351           (apply function 'element `(,@exprs ,init)))
 352          ((applied)
 353           (apply element-fold function
 354                  (apply element-fold function init
 355                         (map first exprs))
 356                  (map second exprs)))))
 357      exprs)))
 358
 359 (define (type-dispatch function exprs)
 360   "Dispatch a function based on the given types or raise an error if they
 361    have an unexpcted format. There are two kinds of expressions: declared
 362    types, and undeclared types.
 363
 364    function: A function of one argument called with 'declared or 'undeclared if,
 365              respectively, expressions are: all declared, or any are undeclared.
 366
 367    exprs: List of expressions.
 368
 369    Returns the result of the function application."
 370   (define type-destruct (papply destruct 'type))
 371   (receive (maybe-names argss metas)
 372       (unzip3 (map (lambda (expr) (receive vals (type-destruct expr) vals)) exprs))
 373     ;; All declared types must have the same meta data and their number
 374     ;; of arguments must match.
 375     (unless (apply eq? (remove not metas))
 376       (parse-error "type-dispatch: declared types don't match."))
 377     (if (every identity metas)
 378         (function 'declared maybe-names argss metas)
 379         (function 'undeclared maybe-names argss metas))))
 380
 381 (define (type-map function expr . more)
 382   "Map a function to type-expressions. See the documentation of `element-map' which
 383    has analogous behaviour except for the function who's called on a kind that
 384    alternates between 'type and 'element based on the intrinsic."
 385   (let ((exprs (cons expr more)))
 386     (type-dispatch
 387      (lambda (kind maybe-names argss metas)
 388        (case kind
 389          ((declared)
 390           (if (null? (car argss))
 391               (apply function 'type exprs)
 392               (cons (just (car maybe-names)) ; all expressions have the same name
 393                     (apply map
 394                            (lambda formals
 395                              (if (eq? 'binding (car formals))
 396                                  (match (cdr formals)
 397                                    (((': xs Xs) ...)
 398                                     (list ':
 399                                           (apply element-map function xs)
 400                                           (apply type-map function Xs)))
 401                                    (_
 402                                     (parse-error "type-map: declared types don't match.")))
 403                                  (apply (case (car formals)
 404                                           ((element)
 405                                            element-map)
 406                                           ((type)
 407                                            type-map))
 408                                         function (cdr formals))))
 409                            (cons (meta-arguments-kinds (type-ref (car expr)))
 410                                  argss)))))
 411          ((undeclared)
 412           (apply function 'type exprs))))
 413      exprs)))
 414
 415 (define (type-fold function init expr . more)
 416   "Fold a function over type-expressions. See the documentation of `element-fold'
 417    which has analogous behaviour except for the function who's called on a kind
 418    that alternates between 'type and 'element based on the intrinsic."
 419   (let ((exprs (cons expr more)))
 420     (type-dispatch
 421      (lambda (kind maybe-names argss metas)
 422        (case kind
 423          ((declared)
 424           (if (null? (car argss))
 425               (apply function 'type `(,@exprs ,init))
 426               (apply fold
 427                      (lambda formals
 428                        (if (eq? 'binding (car formals))
 429                            (match (but-last (cdr formals))
 430                              (((': xs Xs) ...)
 431                               (apply element-fold function
 432                                      (apply type-fold function
 433                                             (last formals)
 434                                             Xs)
 435                                      xs))
 436                              (_
 437                               (parse-error "type-fold: declared types don't match.")))
 438                            (apply (case (car formals)
 439                                     ((element)
 440                                      element-fold)
 441                                     ((type)
 442                                      type-fold))
 443                                   function
 444                                   (last formals)
 445                                   (but-last (cdr formals)))))
 446                      init (cons (meta-arguments-kinds (type-ref (car expr)))
 447                                 argss))))
 448          ((undeclared)
 449           (apply function 'type `(,@exprs ,init)))))
 450      exprs)))
 451
 452 (define (split-in-three lst start end)
 453   "Split the given list in three with `start' and `end' the indices delimiting
 454 the resulting middle list e.g. (a b c d e) 2 3 => (a b) (c) (d e)."
 455   (let rec ((i 0)
 456             (xs '())
 457             (ys '())
 458             (zs lst))
 459     (if (= i end)
 460         (values (reverse xs)
 461                 (reverse ys)
 462                 zs)
 463         (if (< i start)
 464             (rec (1+ i)
 465                  (cons (car zs) xs)
 466                  ys
 467                  (cdr zs))
 468             (rec (1+ i)
 469                  xs
 470                  (cons (car zs) ys)
 471                  (cdr zs))))))
 472
 473 (define (context-dispatch function ranges exprs)
 474   (define (expand-range range start end)
 475     (ifn range
 476          (list start end)
 477          (list (or (first range) start)
 478                (or (second range) end))))
 479   (apply function
 480          (receive (Γs :xXss Δs)
 481              (unzip3
 482               (map (lambda (range expr)
 483                      (match expr
 484                        (((? symbol? Γ) :xXs ... (? symbol? Δ))
 485                         (receive (a b c)
 486                             (apply split-in-three
 487                                    :xXs
 488                                    (expand-range range 0 (length :xXs)))
 489                           (list (cons Γ a) b `(,@c ,Δ))))
 490                        (((? symbol? Γ) :xXs ... ('/ (? symbol? Δ) x y))
 491                         (receive (a b c)
 492                             (apply split-in-three
 493                                    :xXs
 494                                    (expand-range range 0 (length :xXs)))
 495                           (list (cons Γ a) b `(,@c ,Δ))))
 496                        (((? symbol? Γ) :xXs ...)
 497                         (receive (a b c)
 498                             (apply split-in-three
 499                                    :xXs
 500                                    (expand-range range 0 (length :xXs)))
 501                           (list (cons Γ a) b c)))
 502                        ((:xXs ...)
 503                         (receive (a b c)
 504                             (apply split-in-three
 505                                    :xXs
 506                                    (expand-range range 0 (length :xXs)))
 507                           (list a b c)))
 508                        (_ (parse-error "context-fold: unknown expression."))))
 509                    (or ranges (list-tabulate (length exprs) not))
 510                    exprs))
 511            (if (apply = (map length :xXss))
 512                (list Γs :xXss Δs)
 513                (parse-error "context-dispatch: contexts should have the same range, but got ~{~a~^ ~}." :xXss)))))
 514
 515 (define (context-map function ranges expr . more)
 516   (context-dispatch
 517    (lambda (Γs :xXss Δs)
 518      (append
 519       (if (null? (car Γs)) '() (apply function 'Γ Γs))
 520       (reverse
 521        (cdr
 522         (apply fold
 523                (lambda formals
 524                  (let* ((:xXs (but-last formals)) ; one decl per judgment
 525                         (z (last formals))
 526                         (ctxs (car z))
 527                         (prev (cdr z)))
 528                    (if (any identity (map (lambda (ctx :xX)
 529                                             (context-ref ctx (second :xX)))
 530                                           ctxs :xXs))
 531                        (parse-error "context-map: variable can only be declared once.")
 532                        (cons (map cons :xXs ctxs)
 533                              (cons
 534                               (list ':
 535                                     (apply function 'variable (map second :xXs))
 536                                     (apply type-map function (map third :xXs)))
 537                               prev)))))
 538                (cons (list-tabulate (length :xXss) (const '()))
 539                      '())
 540                :xXss)))
 541       (if (null? (car Δs)) '() (apply function 'Δ Δs))))
 542    ranges (cons expr more)))
 543
 544 (define (context-fold function ranges init expr . more)
 545   (context-dispatch
 546    (lambda (Γs :xXss Δs)
 547      ;; See `context-map' for the format of Γs :xXss Δs.
 548      (apply
 549       (ifn (null? (car Δs)) function (lambda formals (last formals)))
 550       'Δ
 551       `(,@Δs
 552         ,(apply fold
 553                 (lambda formals
 554                   (let* ((:xXs (but-last formals)) ; one decl per judgment
 555                          (prev (last formals)))
 556                     (if (any identity
 557                              (map (lambda (ctx :xX)
 558                                     (context-ref ctx (element-of-:xX :xX)))
 559                                   (*ctxs*)
 560                                   :xXs))
 561                         (parse-error "context-fold: variable can only be declared once.")
 562                         (begin
 563                           (*ctxs* (map cons :xXs (*ctxs*)))
 564                           (apply function 'variable
 565                                  `(,@(map element-of-:xX :xXs)
 566                                    ,(apply function 'type `(,@(map third :xXs)
 567                                                             ,prev))))))))
 568                 (apply (ifn (null? (car Γs)) function (lambda formals (last formals)))
 569                        'Γ `(,@Γs ,init))
 570                 :xXss))))
 571    ranges (cons expr more)))
 572
 573 (define (content-dispatch function exprs)
 574   (define (content-match expr)
 575     (match expr
 576       ;; generic judgment
 577       (('/ (? symbol? J) (? symbol? a) (? symbol? b))
 578        (list 'generic (make-substitution J a b)))
 579       ((? symbol? J)
 580        (list 'generic J))
 581       ;; type
 582       (('type A)
 583        (list 'type A))
 584       ;; judgmentally equal types
 585       (('≐ ('/ A
 586                (? symbol? x)
 587                (? symbol? y))
 588            ('/ B
 589                (? symbol? x')
 590                (? symbol? y)))
 591        (list 'type-eq
 592              (make-substitution A x y)
 593              (make-substitution B x' y)))
 594       (('≐ A B)
 595        (list 'type-eq A B))
 596       ;; judgmentally equal elements of a type
 597       (('≐ ('/ a
 598                (? symbol? x)
 599                (? symbol? y))
 600            ('/ b
 601                (? symbol? x')
 602                (? symbol? y))
 603            ('/ A
 604                (? symbol? x)
 605                (? symbol? y)))
 606        (list 'element-eq
 607              (make-substitution a x y)
 608              (make-substitution b x' y)
 609              (make-substitution A x y)))
 610       (('≐ a b A)
 611        (list 'element-eq a b A))
 612       ;; element of a type
 613       ((': a A)
 614        (list 'element a A))
 615       (_ (parse-error "content-dispatch: unknown expression."))))
 616   (let* ((xs (map content-match exprs))
 617          (generic? (papply eq? 'generic))
 618          (kinds (map car xs)))
 619     (unless (apply eq? (remove generic? kinds))
 620       (parse-error "content-dispatch: contents don't match."))
 621     (ifn (any generic? kinds)
 622          (apply function (find (compose not generic?)
 623                                kinds)
 624                 (unzip (map cdr xs)))
 625          (apply function 'generic
 626                 (map (lambda (kind x)
 627                        (if (generic? kind)
 628                            (second x)
 629                            (match x
 630                              (('type A)
 631                               x)
 632                              (('type-eq A B)
 633                               (list '≐ A B))
 634                              (('element-eq a b A)
 635                               (list '≐ a b A))
 636                              (('element a A)
 637                               (list ': a A)))))
 638                      kinds xs)))))
 639
 640 (define (content-map function expr . more)
 641   (content-dispatch
 642    (lambda (kind . args)
 643      (case kind
 644        ((generic)
 645         (apply function 'generic args))
 646        ((type)
 647         (list 'type (apply type-map function (first args))))
 648        ((element)
 649         (list ':
 650               (apply element-map function (first args))
 651               (apply type-map function (second args))))
 652        ((type-eq)
 653         (list '≐
 654               (apply type-map function (first args))
 655               (apply type-map function (second args))))
 656        ((element-eq)
 657         (list '≐
 658               (apply element-map function (first args))
 659               (apply element-map function (second args))
 660               (apply type-map function (third args))))))
 661    (cons expr more)))
 662
 663 (define (content-fold function init expr . more)
 664   (content-dispatch
 665    (lambda (kind . args)
 666      (case kind
 667        ((generic)
 668         (apply function 'generic `(,@args ,init)))
 669        ((type)
 670         (apply type-fold function init (first args)))
 671        ((element)
 672         (apply element-fold function
 673                (apply type-fold function init (second args))
 674                (first args)))
 675        ((type-eq)
 676         (apply type-fold function
 677                (apply type-fold function init (second args))
 678                (first args)))
 679        ((element-eq)
 680         (apply element-fold function
 681                (apply element-fold function
 682                       (apply type-fold function init (third args))
 683                       (first args))
 684                (second args)))))
 685    (cons expr more)))
 686
 687 (define (judgment-dispatch function exprs)
 688   (match exprs
 689     (((contexts ... '⊢ contents) ...)
 690      (function contexts contents))
 691     (_ (parse-error "judgment-dispatch: unknown expression."))))
 692
 693 (define (judgment-map function ranges expr . more)
 694   (judgment-dispatch (lambda (ctxs cnts)
 695                        (append (apply context-map function ranges ctxs)
 696                                (list '⊢)
 697                                (list (apply content-map function cnts))))
 698                      (cons expr more)))
 699
 700 (define (judgment-fold function ranges init expr . more)
 701   (parameterize ((*ctxs* (map (const '()) (cons expr more))))
 702    (judgment-dispatch (lambda (ctxs cnts)
 703                         (apply content-fold function
 704                                (apply context-fold function ranges init ctxs)
 705                                cnts))
 706                       (cons expr more))))
 707
 708 (defmacro define-rule (name judgment . more)
 709   (begin
 710     (when (eq? name 'exact)
 711       (parse-error "define-rule: the rule name \"exact\" is reserved."))
 712     (for-each (lambda (judgment)
 713                 (judgment-fold
 714                  (lambda (kind x prev)
 715                    prev)
 716                  #f #f judgment))
 717               (cons judgment more))
 718     ;; We declare types or constructors when they occur.
 719     (let ((content (judgment-content judgment)))
 720       (when (list? content)
 721         (let ((kind (case (first content)
 722                       ((type) 'type)
 723                       ((:) 'element)
 724                       (else 'else))))
 725           (when (member kind '(type element))
 726             (if-let (maybe-name (pre-destruct kind (second content)))
 727                     (unless (and (eq? 'element kind)
 728                                  (judgment-fold
 729                                   (lambda (kind' x prev)
 730                                     (ifn (eq? kind kind')
 731                                          prev
 732                                          (or prev (context-ref (car (*ctxs*))
 733                                                                (just maybe-name)))))
 734                                   #f #f judgment))
 735                       (unless (any (lambda (judgment)
 736                                      (judgment-fold
 737                                       (lambda (kind' x prev)
 738                                         (ifn (eq? kind kind')
 739                                              prev
 740                                              (or prev (equal? x (just maybe-name)))))
 741                                       #f #f judgment))
 742                                    more)
 743                         (hash-set! (if (eq? kind 'type)
 744                                        *types*
 745                                        *constructors*)
 746                                    (just maybe-name)
 747                                    (cons judgment more)))))))))
 748     (hash-set! *rules* name `,(cons judgment more))
 749     `(begin
 750        (hash-set! *rules* ',name ',(cons judgment more))
 751        (values))))
 752
 753 (define (replace-judgment mappings judgment)
 754   (judgment-map
 755    (lambda (kind x)
 756      (or
 757       (if (member kind '(Γ Δ))
 758           (assoc-ref mappings (car x))
 759           (if (member kind '(element variable type generic))
 760               (assoc-ref mappings x)
 761               x))
 762       (parse-error "replace-judgment: expression ~a not mapped in ~a." x mappings)))
 763    #f judgment))
 764
 765 (define (substitute mapper x y mapping)
 766   (acons (substitution-pattern x)
 767          (mapper
 768           (lambda (kind z)
 769             (if (and (eq? kind 'type)
 770                      (receive (maybe-name args meta) (destruct 'type z)
 771                        (and (not meta) (= 1 (length args)))))
 772                 (ifn (equal? (second z) (assoc-ref mapping (substitution-source x)))
 773                      z
 774                      (list (first z)
 775                            (assoc-ref mapping (substitution-destination x))))
 776                 (ifn (equal? z (assoc-ref mapping (substitution-source x)))
 777                      z
 778                      (assoc-ref mapping (substitution-destination x)))))
 779           y)
 780          mapping))
 781
 782 (define* (apply-rule derivation name #:key start end . args)
 783   (let ((err1 "apply-rule: derivation is pointless.")
 784         (err2 "apply-rule: substitutions are only allowed in rules.")
 785         (err3 "apply-rule: can't apply a specific judgment rule to a generic judgment expression.")
 786         (err4 "define-derivation: rule ~s is undefined."))
 787     (expand-derivation-point
 788      derivation
 789      (if start
 790          (if end
 791              `(,name #:start ,start #:end ,end ,@args)
 792              `(,name #:start ,start ,@args))
 793          `(,name ,@args))
 794      (let ((Jp (derivation-point derivation)))
 795        (unless Jp
 796          (parse-error err1))
 797        (if (eq? name 'exact)
 798            #t
 799            (if-let (m (ifn (eq? name 'definition)
 800                            (rule-ref name)
 801                            (hash-ref *definition-rules* (just (pre-destruct 'type (second (judgment-content Jp)))))))
 802                    ;; NOTE: Computing the mapping is essential to be sure
 803                    ;; the meta-conclusion matches the judgment point even
 804                    ;; in cases where there are no hypotheses.
 805                    (let ((mapping
 806                           (judgment-fold
 807                            (lambda (kind x y prev)
 808                              (case kind
 809                                ((Γ)
 810                                 (if (substitution? y)
 811                                     (parse-error err2)
 812                                     (ifn (substitution? x)
 813                                          (acons (car x) y prev)
 814                                          (ifn (null? (cdr y))
 815                                               (parse-error "TBD")
 816                                               (acons (substitution-pattern x)
 817                                                      y prev)))))
 818                                ((Δ)
 819                                 (if (substitution? y)
 820                                     (parse-error err2)
 821                                     (ifn (substitution? x)
 822                                          (acons (car x) y prev)
 823                                          (ifn (null? (cdr y))
 824                                               (parse-error "TBD")
 825                                               (acons (substitution-pattern x)
 826                                                      y prev)))))
 827                                ((element)
 828                                 (if (substitution? y)
 829                                     (parse-error err2)
 830                                     (ifn (substitution? x)
 831                                          (acons x y prev)
 832                                          (substitute element-map x y prev))))
 833                                ((type)
 834                                 (if (substitution? y)
 835                                     (parse-error err2)
 836                                     (ifn (substitution? x)
 837                                          (acons x y prev)
 838                                          (substitute type-map x y prev))))
 839                                ((generic)
 840                                 (if (and (not (list? y))
 841                                          (list? x))
 842                                     ;; if y is generic so must x.
 843                                     (parse-error err3)
 844                                     (ifn (substitution? x)
 845                                          (acons x y prev)
 846                                          (if (not (list? y))
 847                                              (acons (substitution-pattern x)
 848                                                     y prev)
 849                                              (substitute content-map x y prev)))))
 850                                ((variable)
 851                                 (acons x y prev))
 852                                (else
 853                                 prev)))
 854                            (list #f (list start end))
 855                            ;; When `#:start'/`#:end' is provided the evaluator
 856                            ;; adds it to the head of the `args' list (see the
 857                            ;; documentation for `define*') followed by its value,
 858                            ;; and must be removed.
 859                            (alist<-plist
 860                             (if start
 861                                 (if end
 862                                     (drop args 4)
 863                                     (drop args 2))
 864                                 (if end
 865                                     (drop args 2)
 866                                     args)))
 867
 868                            (meta-conclusion m)
 869                            Jp)))
 870                      (map
 871                       (lambda (judgment)
 872                         (cons (replace-judgment mapping judgment)
 873                               #f))
 874                       (meta-hypotheses m)))
 875                    (parse-error err4 name)))))))
 876
 877 (defmacro define-derivation% (name kind maybe-assignment conclusion hypotheses rule . more)
 878   (let ((derivation
 879          (fold (lambda (step derivation)
 880                  (apply apply-rule derivation step))
 881                (d conclusion)
 882                (cons rule more))))
 883     (ifn (lset= equal? hypotheses (list-hypotheses derivation))
 884          (parse-error
 885           "define-derivation: expected remaining hypotheses ~a, but got ~a."
 886           hypotheses (list-hypotheses derivation))
 887          (if maybe-assignment
 888              (begin
 889                (hash-set!
 890                 *rules*
 891                 name
 892                 (cons `(,@(judgment-context conclusion)
 893                         ⊢
 894                         ,(if (eq? kind 'type)
 895                              (list 'type (just maybe-assignment))
 896                              (list ':
 897                                    (just maybe-assignment)
 898                                    (third (judgment-content conclusion)))))
 899                       hypotheses))
 900                (hash-set!
 901                 *definition-rules*
 902                 name
 903                 (cons `(,@(judgment-context conclusion)
 904                         ⊢
 905                         ,(if (eq? kind 'type)
 906                              (list '≐
 907                                    (just maybe-assignment)
 908                                    (second (judgment-content conclusion)))
 909                              (list '≐
 910                                    (just maybe-assignment)
 911                                    (second (judgment-content conclusion))
 912                                    (third (judgment-content conclusion)))))
 913                       hypotheses))
 914                (hash-set! (if (eq? kind 'type) *types* *constructors*)
 915                           (just (pre-destruct 'type (just maybe-assignment)))
 916                           (rule-ref name))
 917                '(values)
 918                )
 919              (begin
 920                (hash-set! *rules* name (cons conclusion hypotheses))
 921                '(values))))))
 922
 923 ;; NOTE: A derivation must have at least one derivation rule (can't derive a
 924 ;;       statement out of nothing).
 925 (define-syntax define-derivation
 926   (syntax-rules (:= ⊢ type :)
 927     ((_ name ((Γ ⊢ (:= a (type expr)))
 928               hypothesis ...)
 929         (rule-1 arg-1 ...)
 930         (rule-2 arg-2 ...)
 931         ...)
 932      (define-derivation% name type (just . a) (Γ ⊢ (type expr)) (hypothesis ...)
 933        (rule-1 arg-1 ...)
 934        (rule-2 arg-2 ...)
 935        ...))
 936     ((_ name ((Γ ⊢ (:= a (: b B)))
 937               hypothesis ...)
 938         (rule-1 arg-1 ...)
 939         (rule-2 arg-2 ...)
 940         ...)
 941      (define-derivation% name element (just . a) (Γ ⊢ (: b B)) (hypothesis ...)
 942        (rule-1 arg-1 ...)
 943        (rule-2 arg-2 ...)
 944        ...))
 945     ((_ name (conclusion hypothesis ...)
 946         (rule-1 arg-1 ...)
 947         (rule-2 arg-2 ...)
 948         ...)
 949      (define-derivation% name #f #f conclusion (hypothesis ...)
 950        (rule-1 arg-1 ...)
 951        (rule-2 arg-2 ...)
 952        ...))))
 953
 954 (define (define-derivation-list name derivation)
 955   (let ((tree (derivation-tree derivation)))
 956    `(define-derivation ,name
 957       (,(car tree) ,@(list-hypotheses derivation))
 958       ,@(reverse (derivation-steps derivation)))))