; SPDX-FileCopyrightText: In 2026, Chris Pressey, the creator of this work, placed it into the public domain.
; For more information, please refer to <https://unlicense.org/>
; SPDX-License-Identifier: Unlicense

; example usage with Chicken Scheme: csi -q -b hilbert-system.scm

(load "define-opaque-0.3.scm")

(define-opaque-adt theorem make-theorem open-theorem formula 'nil
  (
    (a1 (lambda (phi psi)
      (make-theorem (list '-> phi (list '-> psi phi)))))

    (a2 (lambda (phi psi chi)
      (make-theorem (list '->
        (list '-> phi (list '-> psi chi))
        (list '-> (list '-> phi psi) (list '-> phi chi))))))

    ; Modus ponens: from a proof of P and a proof of P->Q, derive a
    ; proof of Q.
    ;
    ; open-theorem verifies that thm-p and thm-impl are genuine theorems.
    ; Passing any non-theorem value here raises an error.
    (modus-ponens (lambda (thm-p thm-impl)
      (let* (
        (given-p    (open-theorem thm-p))
        (given-impl (open-theorem thm-impl))
      )
        (if (and (pair? given-impl)
                 (equal? (car given-impl) '->)
                 (equal? (cadr given-impl) given-p))
          (make-theorem (caddr given-impl))
          (error "Cannot apply modus ponens:" given-p given-impl)))))

    (repr (lambda () formula))
  )
)

(define demo (lambda ()
  ; Derive p -> p using only A1, A2, and modus ponens.
  (let* (
    ; t1: p -> (p -> p)         by A1(p, p)
    (t1 (theorem 'a1 'p 'p))
    ; t2: p -> ((p->p) -> p)    by A1(p, p->p)
    (t2 (theorem 'a1 'p '(-> p p)))
    ; t3: (p -> ((p->p) -> p)) -> ((p -> (p->p)) -> (p -> p))
    ;                            by A2(p, p->p, p)
    (t3 (theorem 'a2 'p '(-> p p) 'p))
    ; t4: (p -> (p->p)) -> (p -> p)   by MP(t2, t3)
    (t4 (theorem 'modus-ponens t2 t3))
    ; t5: p -> p                by MP(t1, t4)
    (t5 (theorem 'modus-ponens t1 t4))
  )
    (display "Derived theorem: ")
    (display (t5 'repr))
    (newline)
  )))

(demo)

; --------------------------------------------------------------------------

; Demonstration that other data structures are rejected (even in the case
; that they define the same operations - duck-typing would not reject this.)

(define-opaque-adt ersatz-theorem make-theorem open-theorem formula 'nil
  (
    (a1 (lambda (phi psi)
      (make-theorem (list '-> phi (list '-> psi phi)))))

    (a2 (lambda (phi psi chi)
      (make-theorem (list '->
        (list '-> phi (list '-> psi chi))
        (list '-> (list '-> phi psi) (list '-> phi chi))))))

    (modus-ponens (lambda (thm-p thm-impl)
      (let* (
        (given-p    (open-theorem thm-p))
        (given-impl (open-theorem thm-impl))
      )
        (if (and (pair? given-impl)
                 (equal? (car given-impl) '->)
                 (equal? (cadr given-impl) given-p))
          (make-theorem (caddr given-impl))
          (error "Cannot apply modus ponens:" given-p given-impl)))))
  )
)

(define errorful-demo (lambda ()
  (let* (
    (t1 (theorem 'a1 'p 'p))
    (t2 (theorem 'a1 'p '(-> p p)))
    (t3 (theorem 'a2 'p '(-> p p) 'p))
    (t4 (theorem 'modus-ponens t2 t3))
    (t5 (ersatz-theorem 'modus-ponens t1 t4))
  )
    (display "Derived theorem: ")
    (display (t5 'repr))
    (newline)
  )))