From 9f80fc1bcfdb11cfa35290a498106594fddc123a Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Thu, 20 Feb 2025 23:38:00 -0500
Subject: [PATCH] feat: prettification

---
 formal.scm | 43 +++++++++++++++++++++++++++++++++++--------
 1 file changed, 35 insertions(+), 8 deletions(-)

diff --git a/formal.scm b/formal.scm
index 9f0e0e0..929b353 100644
--- a/formal.scm
+++ b/formal.scm
@@ -1,6 +1,6 @@
 ;; okay, i'll keep these procedures for the sake of nesting
 
-(define (make-pand p q) `(and ,p ,q))
+(define (make-pand p q) `(∧ ,p ,q))
 
 (define pand
   (case-lambda
@@ -8,7 +8,7 @@
     [(p) p]
     [(p . qs) (fold-left make-pand p qs)]))
 
-(define (make-por p q) `(or ,p ,q))
+(define (make-por p q) `(∨ ,p ,q))
 
 (define por
   (case-lambda
@@ -17,7 +17,7 @@
     [(p . qs) (fold-left make-por p qs)]))
 
 ;; iirc, or: (not p) or q
-(define (make-p-> p q) `(-> ,p ,q))
+(define (make-p-> p q) `(→ ,p ,q))
 
 ;; could fold but laziness
 (define p->
@@ -121,6 +121,30 @@
         i
         (loop (add1 i)))))
 
+;; so over-general lel
+(define proof-variable
+  (let* ([bases '#(p q r s t u)]
+         [bases-count (vector-length bases)])
+    (lambda (n)
+      (define base (vector-ref bases (mod n bases-count)))
+      (define num  (floor (/ n bases-count)))
+      (string->symbol
+       (format "~a~a"
+               base
+               (if (zero? num) "" num))))))
+
+;; i think i prefer the turnstile to therefore
+(define (argument-pp arg port)
+  (define prems (argument-premises arg))
+  (define concls (argument-conclusions arg))
+  (format port "~{~a\n~}~{⊢ ~a\n~}"
+          prems concls))
+
+(define (general-argument-pp arg% port)
+  ;; map iota is bad but convenient (macro so needed)
+  (define arg (apply arg% (map proof-variable (iota (procedure-arity arg%)))))
+  (argument-pp arg port))
+
 (define (proof-valid? proof%)
   (define (gensyms n xs)
     (if (zero? n)
@@ -140,17 +164,20 @@
         (let ([concl (step-conclusion step)]
               [rule  (step-rule step)])
           (unless (follows? prems concl rule)
-            (format #t "fool, ~a does not follow from ~a and ~a!\n"
-                    concl (reverse prems) rule)
+            (printf "Failed to apply rule:\n")
+            (argument-pp rule #t)
+            (printf "Proof state:\n~{~a\n~}⊢ ~a\n"
+                    (reverse prems) concl)
             (return #f)) 
           (set! prems (cons concl prems))))
       (proof-steps proof))
-     (when (premises<=? goals prems)
+     (when (or (member #f prems) (premises<=? goals prems))
        (return #t))
-     (format #t "forgetting something? you're trying to prove ~a, but you've only got ~a\n"
-             goals prems))))
+     (format #t "Proof incomplete:\n~{~a\n~}~{⊢ ~a\n~}\n"
+             prems goals))))
 
 ;; TODO: i can just guess lol
+;; this really isn't far from the macroless version....
 (define and-comm
   (proof (p q)
     (argument (p q)