org: proof tree blocksHEADmain

2 files changed, 86 insertions, 1 deletions

diff --git a/config.el b/config.el
index deb5fa3..949a101 100644
--- a/config.el
+++ b/config.el
@@ -1,6 +1,5 @@
 ;;; -*- lexical-binding: t; -*-
 
-
 ;; fish as default confuses some sub processes of emacs
 (setq shell-file-name (executable-find "bash"))
 
@@ -34,6 +33,91 @@
           ("[?]"  . +org-todo-onhold)
           ("KILL" . +org-todo-cancel))))
 
+(after! org-special-block-extras
+
+  ; center a single-line string in a block of width
+  (defun prooftree--center-string (width str)
+    (-let* ((padding (- width (length str)))
+            (half (/ padding 2))
+            (other (- padding half)))
+      (s-concat (s-repeat half " ")
+                (if (eq str nil) "" str)
+                (s-repeat other " "))))
+
+  ;; helper
+  (defun join-stuff (w1 lines1 lines2)
+    (if (and (eq nil (car lines1)) (eq nil (car lines2)))
+        ""
+      (-let ((previous (join-stuff w1 (cdr lines1) (cdr lines2))))
+        (s-concat previous (if (equal previous "") "" "\n")
+                  (car lines1) (s-repeat (- w1 (length (car lines1))) " ")
+                  (car lines2)))))
+
+  ;; join two proof trees line-wise, with some spacing in between
+  (defun prooftree--linewise-join (tree1 tree2)
+    (-let* (((w1 . str1) tree1)
+            ((w2 . str2) tree2)
+            (lines1 (reverse (s-split "\n" str1)))
+            (lines2 (reverse (s-split "\n" str2)))
+            (spacing (if (< (+ w1 w2) 4) 2 4)))
+      `(,(+ w1 spacing w2) . ,(join-stuff (+ spacing w1) lines1 lines2))))
+
+  ;; join two proof trees line-wise, without any spacing
+  (defun prooftree--linewise-block-join (tree1 tree2)
+    (-let* (((w1 . str1) tree1)
+            ((w2 . str2) tree2)
+            (lines1 (reverse (s-split "\n" str1)))
+            (lines2 (reverse (s-split "\n" str2))))
+      `(,(+ w1 w2) . ,(join-stuff w1 lines1 lines2))))
+
+  ;; center a proof tree in a block of width
+  (defun prooftree--center-tree (width tree)
+    (-let* (((w . _) tree)
+            (padding (/ (- width w) 2)))
+      (prooftree--linewise-block-join `(,padding . "") tree)
+      ))
+
+  ;; prooftree--linewise-join, but for arbitrarily many proof trees in a list
+  (defun prooftree--join-trees (trees)
+    (if (equal (length trees) 1) (car trees)
+      (prooftree--join-trees `(,(prooftree--linewise-join (car trees) (cadr trees)) . ,(cddr trees)))))
+
+  ;; produce readable plain text representations of proof trees
+  (defun org--list-to-plaintext-tree (lst)
+    (cond
+     ((symbolp lst) '(0 . ""))
+     ((symbolp (car lst)) (org--list-to-plaintext-tree (cadr lst)))
+     (t
+      (-let* (((conclusion₀ children) lst)
+              ((name named?) (s-split " :: " conclusion₀))
+              (conclusion (or named? conclusion₀)))
+        (if (not children)
+            (-let ((rendered (if named? (format "%s(%s)\n%s" (s-repeat (length conclusion) "-") name conclusion) conclusion))
+                   (width (if named? (+ (length conclusion) 2 (length name)) (length conclusion))))
+              `(,width . ,rendered))
+          (-let* ((premises (cdr (mapcar #'org--list-to-plaintext-tree children)))
+                  (premises-width (+ (* 4 (- (length premises) 1)) (apply '+ (mapcar #'car premises))))
+                  (width (+ 2 (max premises-width (length conclusion)))))
+            `(,width .
+              ,(format "%s\n%s%s\n%s"
+                    (cdr (prooftree--center-tree width (prooftree--join-trees premises)))
+                    (s-repeat width "-")
+                    (if named? (format "(%s)" name) "")
+                    (prooftree--center-string width conclusion)))))))))
+
+  ;; same as the "tree" block, but with more than just LaTeX
+  (org-defblock prooftree (main-arg)
+    (let ((proof (cdr (with-temp-buffer
+                       (org-mode) ; otherwise org-list-to-lisp is unhappy
+                       (insert raw-contents)
+                       (goto-char (point-min))
+                       (org-list-to-lisp)))))
+      (pcase backend
+        (`latex (s-join "" (--map (format "\\[%s\\]" (org--list-to-math it)) proof)))
+        (_ (format "<pre>%s</pre>"
+                   (s-join "\n\n" (--map (format "%s" (cdr (org--list-to-plaintext-tree it))) proof)))))))
+  )
+
 (setq org-agenda-files '("~/org" "~/org/roam"))
 (setq org-roam-directory "~/org/roam")
 (setq org-roam-v2-ack t)
diff --git a/packages.el b/packages.el
index 54886c1..92bc71b 100644
--- a/packages.el
+++ b/packages.el
@@ -20,6 +20,7 @@
 (package! helm-dictionary)
 (package! org-drill)
 (package! org-drill-table)
+(package! org-special-block-extras)
 
 (package! pulseaudio-control)
 (package! desktop-environment)