--- /dev/null
+;;;; Copyright (C) 2024 Vouivre Digital Corporation
+;;;;
+;;;; This file is part of Vouivre.
+;;;;
+;;;; Vouivre is free software: you can redistribute it and/or
+;;;; modify it under the terms of the GNU General Public
+;;;; License as published by the Free Software Foundation, either
+;;;; version 3 of the License, or (at your option) any later version.
+;;;;
+;;;; Vouivre is distributed in the hope that it will be useful,
+;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+;;;; General Public License for more details.
+;;;;
+;;;; You should have received a copy of the GNU General Public
+;;;; License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
+
+(define-module (vouivre type rules)
+ #:use-module (vouivre type system))
+
+;;;; Structural Rules
+
+(define-rule formation-1 ()
+ ((Γ ⊢ (type A))
+ (Γ (: x A) ⊢ (type (B x)))))
+
+(define-rule formation-2 ()
+ ((Γ ⊢ (type A))
+ (Γ ⊢ (≐ A B))))
+
+(define-rule formation-3 ()
+ ((Γ ⊢ (type B))
+ (Γ ⊢ (≐ A B))))
+
+(define-rule formation-4 ()
+ ((Γ ⊢ (type A))
+ (Γ ⊢ (: a A))))
+
+(define-rule formation-5 ()
+ ((Γ ⊢ (: a A))
+ (Γ ⊢ (≐ a b A))))
+
+(define-rule formation-6 ()
+ ((Γ ⊢ (: b A))
+ (Γ ⊢ (≐ a b A))))
+
+(define-rule type-reflexive ()
+ ((Γ ⊢ (≐ A A))
+ (Γ ⊢ (type A))))
+
+(define-rule type-symmetric ()
+ ((Γ ⊢ (≐ B A))
+ (Γ ⊢ (≐ A B))))
+
+(define-rule type-transitive ()
+ ((Γ ⊢ (≐ A C))
+ (Γ ⊢ (≐ A B))
+ (Γ ⊢ (≐ B C))))
+
+(define-rule :-reflexive ()
+ ((Γ ⊢ (≐ a a A))
+ (Γ ⊢ (: a A))))
+
+(define-rule :-symmetric ()
+ ((Γ ⊢ (≐ b a A))
+ (Γ ⊢ (≐ a b A))))
+
+(define-rule :-transitive ()
+ ((Γ ⊢ (≐ a c A))
+ (Γ ⊢ (≐ a b A))
+ (Γ ⊢ (≐ b c A))))
+
+(define-rule variable-conversion ()
+ ((Γ (: x A') Δ ⊢ J)
+ (Γ ⊢ (≐ A A'))
+ (Γ (: x A) Δ ⊢ J)))
+
+(define-rule substitution ()
+ ((Γ (/ Δ a x) ⊢ (/ J a x))
+ (Γ ⊢ (: a A))
+ (Γ (: x A) Δ ⊢ J)))
+
+(define-rule substitution-type-congruence ()
+ ((Γ (/ Δ a x) ⊢ (≐ (/ B a x) (/ B a' x)))
+ (Γ ⊢ (≐ a a' A))
+ (Γ (: x A) Δ ⊢ (type B))))
+
+(define-rule substitution-:-congruence ()
+ ((Γ (/ Δ a x) ⊢ (≐ (/ b a x) (/ b a' x) (/ B a x)))
+ (Γ ⊢ (≐ a a' A))
+ (Γ (: x A) Δ ⊢ (: b B))))
+
+(define-rule weakening ()
+ ((Γ (: x A) Δ ⊢ J)
+ (Γ ⊢ (type A))
+ (Γ Δ ⊢ J)))
+
+(define-rule generic-element ()
+ ((Γ (: x A) ⊢ (: x A))
+ (Γ ⊢ (type A))))
+
+;;;; Ordinary Function Type
+
+(define-rule → ()
+ ((Γ ⊢ (type (→ A B)))
+ (Γ ⊢ (type A))
+ (Γ ⊢ (type B))))
+
+(define-rule →-eq ()
+ ((Γ ⊢ (≐ (→ A B)
+ (→ A' B')))
+ (Γ ⊢ (≐ A A'))
+ (Γ ⊢ (≐ B B'))))
+
+(define-rule λ ()
+ ((Γ ⊢ (: (λ x (b x))
+ (→ A B)))
+ (Γ ⊢ (type B))
+ (Γ (: x A) ⊢ (: (b x) B))))
+
+(define-rule λ-eq ()
+ ((Γ ⊢ (≐ (λ x (b x))
+ (λ x (b' x))
+ (→ A B)))
+ (Γ (: x A) ⊢ (≐ (b x) (b' x) B))))
+
+(define-rule ev ()
+ ((Γ (: x A) ⊢ (: (f x) B))
+ (Γ ⊢ (: f (→ A B)))))
+
+(define-rule ev-eq ()
+ ((Γ (: x A) ⊢ (≐ (f x) (f' x) B))
+ (Γ ⊢ (≐ f f' (→ A B)))))
+
+(define-rule β ()
+ ((Γ (: x A) ⊢ (≐ ((λ y (b y)) x)
+ (b x)
+ B))
+ (Γ ⊢ (type B))
+ (Γ (: x A) ⊢ (: (b x) B))))
+
+(define-rule η ()
+ ((Γ ⊢ (≐ (λ x (f x))
+ f
+ (→ A B)))
+ (Γ ⊢ (: f (→ A B)))))
+
+;;;; Boolean Type
+
+(define-rule bool-formation ()
+ ((⊢ (type Bool))))
+
+(define-rule bool-introduction-1 ()
+ ((⊢ (: true Bool))))
+
+(define-rule bool-introduction-2 ()
+ ((⊢ (: false Bool))))
+
+(define-rule bool-elimination ()
+ ((⊢ (: if (→ Bool (→ A (→ A A)))))
+ (⊢ (type A))))
+
+(define-rule bool-computation-1 ()
+ ((⊢ (≐ (((if true) x) y)
+ x
+ Bool))))
+
+(define-rule bool-computation-2 ()
+ ((⊢ (≐ (((if false) x) y)
+ y
+ Bool))))
+
+;;;; Ordinary Pair Type
+
+(define-rule pair-formation ()
+ ((⊢ (type (Pair A B)))
+ (⊢ (type A))
+ (⊢ (type B))))
+
+(define-rule pair-introduction ()
+ ((⊢ (: (pair a b) (Pair A B)))
+ (⊢ (: a A))
+ (⊢ (: b B))))
+
+(define-rule pair-elimination-1 ()
+ ((⊢ (: first (→ (Pair A B)
+ A)))
+ (⊢ (type A))
+ (⊢ (type B))))
+
+(define-rule pair-elimination-2 ()
+ ((⊢ (: second (→ (Pair A B)
+ B)))
+ (⊢ (type A))
+ (⊢ (type B))))
+
+(define-rule pair-computation-1 ()
+ ((⊢ (≐ (first (pair a b))
+ a A))
+ (⊢ (: a A))
+ (⊢ (: b B))))
+
+(define-rule pair-computation-2 ()
+ ((⊢ (≐ (second (pair a b))
+ b B))
+ (⊢ (: a A))
+ (⊢ (: b B))))
+
+;;;; Derivations
+
+(define-derivation change-of-variables ((Γ (: x' A) Δ ⊢ J)
+ (Γ ⊢ (type A))
+ (Γ (: x A) Δ ⊢ J))
+ (substitution #:index 2 a x' x x A A)
+ (generic-element #:index 1)
+ (exact)
+ (weakening #:index 1)
+ (exact)
+ (exact))
+
+(define-derivation interchange ((Γ (: y B) (: x A) Δ ⊢ J)
+ (Γ ⊢ (type B))
+ (Γ ⊢ (type A))
+ (Γ (: x A) (: y B) Δ ⊢ J))
+ (substitution #:index 3 a y x y' A B)
+ (weakening #:index 2)
+ (weakening #:index 1)
+ (exact)
+ (exact)
+ (generic-element #:index 1)
+ (exact)
+ (weakening #:index 1)
+ (exact)
+ (substitution #:index 3 a y' x y A B)
+ (weakening #:index 1)
+ (exact)
+ (generic-element #:index 1)
+ (exact)
+ (weakening #:index 2)
+ (weakening #:index 1)
+ (exact)
+ (exact)
+ (exact))
+
+(define-derivation element-conversion ((Γ ⊢ (: a A'))
+ (Γ ⊢ (: a A))
+ (Γ ⊢ (≐ A A')))
+ (substitution a a x a' A A)
+ (exact)
+ (variable-conversion #:index 1 A A')
+ (type-symmetric)
+ (exact)
+ (generic-element #:index 1)
+ (formation-3 A A)
+ (exact))
+
+(define-derivation congruence ((Γ ⊢ (≐ a b A'))
+ (Γ ⊢ (≐ a b A))
+ (Γ ⊢ (≐ A A')))
+ (substitution-:-congruence #:index 1 a a a' b x x A A)
+ (exact)
+ (variable-conversion #:index 1 A A')
+ (type-symmetric)
+ (exact)
+ (generic-element #:index 1)
+ (formation-3)
+ (exact))
+
+(define-derivation identity ((Γ ⊢ (: (λ x x) (→ A A)))
+ (Γ ⊢ (type A)))
+ (λ)
+ (exact)
+ (generic-element #:index 1)
+ (exact))
+
+(define-derivation not ((⊢ (: (λ x (((if x) false) true))
+ (→ Bool Bool))))
+ (λ)
+ (bool-formation)
+ (substitution a true x y A Bool)
+ (weakening #:index 0)
+ (bool-formation)
+ (bool-introduction-1)
+ (ev #:index 1)
+ (substitution a false x y A Bool)
+ (weakening #:index 0)
+ (bool-formation)
+ (bool-introduction-2)
+ (ev #:index 1)
+ (ev #:index 0)
+ (bool-elimination)
+ (bool-formation))
--- /dev/null
+;;;; Copyright (C) 2024 Vouivre Digital Corporation
+;;;;
+;;;; This file is part of Vouivre.
+;;;;
+;;;; Vouivre is free software: you can redistribute it and/or
+;;;; modify it under the terms of the GNU General Public
+;;;; License as published by the Free Software Foundation, either
+;;;; version 3 of the License, or (at your option) any later version.
+;;;;
+;;;; Vouivre is distributed in the hope that it will be useful,
+;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+;;;; General Public License for more details.
+;;;;
+;;;; You should have received a copy of the GNU General Public
+;;;; License along with Vouivre. If not, see <https://www.gnu.org/licenses/>.
+
+(define-module (vouivre type system)
+ #:use-module (ice-9 match)
+ #:use-module (ice-9 receive)
+ #:use-module (srfi srfi-1)
+ #:use-module (srfi srfi-9)
+ #:use-module (vouivre misc)
+ #:export
+ (*rules*
+ apply-rule
+ apply-rules
+ conclusion
+ d
+ define-derivation
+ define-rule
+ exact
+ list-hypotheses))
+
+(define *rules* (make-hash-table))
+(define reserved-symbols '(: ≐ ⊢ type /))
+
+(define-record-type derivation
+ (make-derivation tree points)
+ derivation?
+ (tree derivation-tree)
+ (points derivation-points derivation-points-set!))
+
+(define-record-type evaluation
+ (make-evaluation function value)
+ evaluation?
+ (function evaluation-function)
+ (value evaluation-value))
+
+(define (papply proc . args)
+ (lambda (. rest)
+ (apply proc (append args rest))))
+
+(define (all pred lst)
+ "Like `every', but return the list of all `pred' return values on success."
+ (call/cc
+ (lambda (break)
+ (reverse
+ (fold
+ (lambda (x prev)
+ (if-let (y (pred x))
+ (cons y prev)
+ (break #f)))
+ '() lst)))))
+
+(define (unreserved-symbol? x)
+ (and (symbol? x)
+ (not (member x reserved-symbols))))
+
+(define (parse-unreserved-symbol expr)
+ (if (and (symbol? expr)
+ (not (member expr reserved-symbols)))
+ expr
+ #f))
+
+(define (parse-type-variable expr)
+ (parse-unreserved-symbol expr))
+
+(define (parse-type expr)
+ (match expr
+ ((? parse-unreserved-symbol A)
+ expr)
+ (((? parse-unreserved-symbol B)
+ (? parse-type x)
+ ..1)
+ expr)
+ (_ #f)))
+
+(define (parse-type-variable-declaration expr)
+ (match expr
+ ((': (? parse-type-variable x)
+ (? parse-type A))
+ (list ': x A))
+ (_ #f)))
+
+(define (parse-context expr)
+ (match expr
+ (((? parse-type-variable-declaration X) ...)
+ expr)
+ (((? parse-unreserved-symbol Γ)
+ (? parse-type-variable-declaration X)
+ ...
+ (? parse-unreserved-symbol Δ))
+ expr)
+ (((? parse-unreserved-symbol Γ)
+ (? parse-type-variable-declaration X)
+ ...
+ ('/ (? parse-unreserved-symbol Δ)
+ (? unreserved-symbol? x)
+ (? unreserved-symbol? y)))
+ expr)
+ (((? parse-unreserved-symbol Γ)
+ (? parse-type-variable-declaration X)
+ ...)
+ expr)
+ (_ #f)))
+
+(define (parse-element expr)
+ (match expr
+ ((? parse-unreserved-symbol a)
+ expr)
+ (((? parse-unreserved-symbol b)
+ (? parse-element x)
+ ...)
+ expr)
+ (((? parse-element b)
+ (? parse-type-variable x))
+ expr)
+ (_ #f)))
+
+(define (parse-judgment expr)
+ (match expr
+ ((context ... '⊢ J)
+ (and (parse-context context)
+ (match J
+ ;; generic judgment thesis
+ ((? unreserved-symbol? J)
+ expr)
+ (('/ (? unreserved-symbol? J)
+ (? unreserved-symbol? a)
+ (? unreserved-symbol? x))
+ expr)
+ ;; type
+ (('type (? parse-type A))
+ expr)
+ ;; judgmentally equal types
+ (('≐ ('/ (? parse-type A)
+ (? unreserved-symbol? x)
+ (? unreserved-symbol? y))
+ ('/ (? parse-type B)
+ (? unreserved-symbol? x')
+ (? unreserved-symbol? y)))
+ expr)
+ (('≐ (? parse-type A)
+ (? parse-type B))
+ expr)
+ ;; judgmentally equal elements of a type
+ (('≐ ('/ (? parse-element a)
+ (? unreserved-symbol? x)
+ (? unreserved-symbol? y))
+ ('/ (? parse-element b)
+ (? unreserved-symbol? x')
+ (? unreserved-symbol? y))
+ ('/ (? parse-type A)
+ (? unreserved-symbol? x)
+ (? unreserved-symbol? y)))
+ expr)
+ (('≐ (? parse-element a)
+ (? parse-element b)
+ (? parse-type A))
+ expr)
+ ;; element of a type
+ ((': (? parse-element a)
+ (? parse-type A))
+ expr)
+ ;;
+ (_ #f))))
+ (_ #f)))
+
+(define (parse literals judgments)
+ "Parse literals and judgments of a rule returning them as a cons cell on
+success and `#f' on failure."
+ (and (list? literals)
+ (every symbol? literals)
+ (match judgments
+ ((C Hs ...)
+ (and=> (all parse-judgment judgments)
+ (papply cons literals)))
+ (_ #f))))
+
+(defmacro define-rule (name literals judgments)
+ (let ((x (parse literals judgments)))
+ (ifn x
+ (error "SYNTAX ERROR")
+ (begin
+ (hash-set! *rules* name `,x)
+ `(hash-set! *rules* ',name ',x)))))
+
+(define* (apply-rule derivation name #:key index . args)
+ (if (eq? name 'exact)
+ (exact derivation)
+ (if-let (rule (hash-ref *rules* name))
+ (match-let (((literals . (C Hs ...)) rule))
+ (let* ((ps (derivation-points derivation))
+ (p (car ps))
+ (expr (car p)))
+ (and=>
+ (match-judgment
+ expr C
+ ;; When `#:index' is provided the evaluator adds it to
+ ;; the head of the `args' list (see the documentation
+ ;; `define*') followed by its value, and they must be
+ ;; removed.
+ (alist<-plist (ifn index args (cddr args)))
+ index)
+ (lambda (bindings)
+ (and=>
+ (call/cc
+ (lambda (break)
+ ;; Each hypothesis, with bindings replaced, is wrapped
+ ;; in a cons cell, to be added to the derivation
+ ;; points.
+ (map (lambda (hypothesis)
+ (list (or (replace-in-judgment hypothesis bindings)
+ (break #f))))
+ Hs)))
+ (lambda (points)
+ (set-cdr! p points)
+ ;; Remove the current point, adding its leaves as new
+ ;; points.
+ (derivation-points-set! derivation (append points
+ (cdr ps)))
+ derivation))))))
+ (error "Rule undefined."))))
+
+(define (apply-rules derivation rules)
+ (call/cc
+ (lambda (break)
+ (fold (lambda (rule prev)
+ (if-let (x (apply apply-rule prev (car rule) (cdr rule)))
+ x
+ (break #f)))
+ derivation rules))))
+
+(define (split-in-three lst start end)
+ "Split the given list in three with `start' and `end' the indices delimiting
+the resulting middle list e.g. (a b c d e) 2 3 => (a b) (c) (d e)."
+ (let rec ((i 0)
+ (xs '())
+ (ys '())
+ (zs lst))
+ (if (= i end)
+ (values (reverse xs)
+ (reverse ys)
+ zs)
+ (if (< i start)
+ (rec (1+ i)
+ (cons (car zs) xs)
+ ys
+ (cdr zs))
+ (rec (1+ i)
+ xs
+ (cons (car zs) ys)
+ (cdr zs))))))
+
+(define (sub e x y)
+ (define (sub% e x y)
+ (if (eq? e x)
+ y
+ (if (symbol? e)
+ e
+ (map (lambda (e) (sub e x y)) e))))
+ (ifn x e (sub% e x y)))
+
+(define* (match-context expr pattern bindings #:optional index)
+ "Match a context pattern to a context expression, binding symbols in the
+process. Return `#f' if the pattern fails to match or the updated bindings
+otherwise.
+
+expr: Context expression.
+
+pattern: Context pattern. For examples, look at the left side of `⊢' in
+ instances of `define-rule'.
+
+bindings: Association list of symbols to matched sub-expressions.
+
+index: Index of the first type variable in the expression that corresponds to
+ an explicit type variable in the pattern. This is for cases like the
+ expression (: x1 A1) ... (: xn An) with the pattern (Γ (: x X) Δ)
+ where it is unclear from the pattern alone which variable `x'
+ corresponds to."
+ ;; NOTE: By construction, `expr' has the proper syntax.
+ (let* ((m (length expr))
+ (index (or index m))
+ (bind-symbols
+ (lambda* (Γ xs As Δ #:optional u v)
+ (let ((n (length xs)))
+ (if (> n (- m index))
+ #f
+ (receive (gammas explicit deltas)
+ (split-in-three expr index (+ index n))
+ (fold (lambda (x A z prev)
+ (match-let (((': x' A') z))
+ (acons x x' (acons A A' prev))))
+ (ifn Γ
+ (ifn Δ
+ bindings
+ (acons Δ (sub deltas u v)
+ bindings))
+ (ifn Δ
+ (acons Γ gammas bindings)
+ (acons Γ gammas (acons Δ (sub deltas u v)
+ bindings))))
+ xs As explicit)))))))
+ (match pattern
+ (()
+ (and (= 0 m) bindings))
+ (((? symbol? Γ) (': x A) ...)
+ (bind-symbols Γ x A #f))
+ (((? symbol? Γ) (': x A) ... ('/ Δ u v))
+ (bind-symbols Γ x A Δ u v))
+ (((? symbol? Γ) (': x A) ... Δ)
+ (bind-symbols Γ x A Δ))
+ (((': x A) ...)
+ (bind-symbols #f x A #f))
+ (((': x A) ... ('/ Δ u v))
+ (bind-symbols #f x A Δ u v))
+ (((': x A) ... Δ)
+ (bind-symbols #f x A Δ))
+ (_ (error "Unsupported context pattern syntax.")))))
+
+(define (match-content expr pattern bindings)
+ "See the documentation for `match-context', only here we match the content of
+judgments, i.e. anything right of a `⊢' in instances of `define-rule', and no
+ambiguity arises."
+ ;; NOTE: By construction, `expr' has the proper syntax.
+ (define (equal-expr? v e x y)
+ (or (and (not y)
+ (eq? v e))
+ (and (eq? v y)
+ (eq? e x))
+ (and (list? v)
+ (list? e)
+ (= (length v)
+ (length e))
+ (every (lambda (v e)
+ (equal-expr? v e x y))
+ v e))))
+ (define* (bind-symbols expr pattern bindings
+ #:optional generic-judgment? x y)
+ (cond
+ ((member pattern reserved-symbols)
+ (and (eq? pattern expr)
+ bindings))
+ (generic-judgment?
+ (if (assoc-ref bindings pattern)
+ (error "Generic judgment thesis already bound.")
+ (acons pattern (sub expr x y) bindings)))
+ ((symbol? pattern)
+ (if-let (val (assoc-ref bindings pattern))
+ (and (equal-expr? val expr x y)
+ bindings)
+ (acons pattern (sub expr x y) bindings)))
+ ((list? pattern)
+ (match pattern
+ (('/ B x' y')
+ (let ((x' (assoc-ref bindings x'))
+ (y' (assoc-ref bindings y')))
+ (unless (and x' y')
+ (error "Unbound substitution element."))
+ (bind-symbols expr B bindings #f x' y')))
+ (((? unreserved-symbol? b)
+ x)
+ (if (list? expr)
+ (and
+ (= 2 (length expr))
+ (or (not (assoc-ref bindings b))
+ (equal-expr? (first expr)
+ (assoc-ref bindings b)
+ #f #f))
+ (or (not (assoc-ref bindings x))
+ (equal-expr? (second expr)
+ (assoc-ref bindings x)
+ #f #f))
+ (acons b
+ (make-evaluation (first expr)
+ (second expr))
+ bindings))
+ ;; a symbol
+ (acons b
+ (make-evaluation #f expr)
+ bindings)))
+ (else
+ (and (list? expr)
+ (= (length pattern)
+ (length expr))
+ (call/cc
+ (lambda (break)
+ (fold-right (lambda (e p prev)
+ (if prev
+ (bind-symbols e p prev #f x y)
+ (break #f)))
+ bindings expr pattern)))))))))
+ (define* (match-content% expr pattern bindings
+ #:optional generic-judgment? x y)
+ (match pattern
+ (('type A)
+ (bind-symbols expr pattern bindings #f x y))
+ ((': a A)
+ (bind-symbols expr pattern bindings #f x y))
+ (('≐ A B)
+ (bind-symbols expr pattern bindings #f x y))
+ (('≐ a b A)
+ (bind-symbols expr pattern bindings #f x y))
+ ((? symbol? J)
+ (bind-symbols expr J bindings #t x y))
+ (('/ J (? symbol? x) (? symbol? y))
+ (let ((x (assoc-ref bindings x))
+ (y (assoc-ref bindings y)))
+ (unless (and x y)
+ (error "Unbound substitution element."))
+ (match-content% expr J bindings (symbol? J) x y)))
+ (_ (error "Unsupported content pattern syntax."))))
+ (match-content% expr pattern bindings))
+
+(define* (match-judgment expr pattern bindings #:optional index)
+ ;; NOTE: By construction, `expr' has the proper syntax.
+ (match pattern
+ ((ctx ... '⊢ J)
+ (match expr
+ ((ctx' ... '⊢ J')
+ (and=> (match-context ctx' ctx bindings index)
+ (lambda (bindings)
+ (match-content J' J bindings))))))
+ (_ (error "Unsupported judgment pattern syntax."))))
+
+(define (replace-in-judgment pattern bindings)
+ "Replace all bound symbols (leaves) in the pattern (tree)."
+ (define (replace-in-ctx x)
+ (if (symbol? x)
+ (or (assoc-ref bindings x)
+ x)
+ (map replace-in-ctx x)))
+ (define (replace-in-content x)
+ (match x
+ ((? symbol? x)
+ (if-let (y (assoc-ref bindings x))
+ (ifn (evaluation? y)
+ y
+ (if (evaluation-function y)
+ (evaluation-function y)
+ (error "Can't separate function from value.")))
+ x))
+ (((? unreserved-symbol? b)
+ (? symbol? y))
+ (let ((z (assoc-ref bindings b)))
+ (ifn (evaluation-function z)
+ (evaluation-value z)
+ (list (evaluation-function z)
+ (evaluation-value z)))))
+ (else
+ (map replace-in-content x))))
+ (match pattern
+ ((ctx ... '⊢ J)
+ (append
+ (concatenate
+ (map (lambda (x)
+ (if (list? x)
+ (list (replace-in-ctx x))
+ (let ((y (replace-in-ctx x)))
+ (if (symbol? y)
+ (list y)
+ y))))
+ ctx))
+ (list '⊢ (replace-in-content J))))
+ (_ (error "Unsupported judgment pattern syntax."))))
+
+(define (d expr)
+ (let ((tree (list expr)))
+ (make-derivation tree (list tree))))
+
+(define (exact derivation)
+ (let* ((ps (derivation-points derivation))
+ (p (car ps)))
+ (set-cdr! p '.)
+ (derivation-points-set! derivation (cdr ps))
+ derivation))
+
+(define (list-hypotheses derivation)
+ (delete-duplicates
+ (let rec ((tree (derivation-tree derivation)))
+ (if (eq? '. (cdr tree))
+ (list (car tree))
+ (fold-right
+ (lambda (x prev)
+ (append (rec x) prev))
+ '()
+ (cdr tree))))
+ equal?))
+
+(define conclusion (compose car derivation-tree))
+
+(defmacro define-derivation% (name conclusion hypotheses . rules)
+ (let ((C (parse-judgment conclusion))
+ (Hs (all parse-judgment hypotheses)))
+ (ifn (and C Hs)
+ (error "SYNTAX")
+ (if-let (derivation (apply-rules (d C) rules))
+ (let ((Hs' (list-hypotheses derivation)))
+ (ifn (and (null? (lset-difference equal? Hs' Hs))
+ (null? (lset-difference equal? Hs Hs')))
+ (error "DERIVATION 1")
+ (begin
+ (hash-set! *rules*
+ name
+ (cons '() `(,conclusion ,@hypotheses)))
+ `(hash-set! *rules*
+ ',name
+ (cons '() '(,conclusion ,@hypotheses))))))
+ (error "DERIVATION 2")))))
+
+(define-syntax-rule (define-derivation name
+ (conclusion hypothesis ...)
+ (rule arg ...) ...)
+ (define-derivation% name conclusion (hypothesis ...)
+ (rule arg ...)
+ ...))
projects / vouivre.git / commitdiff