From 855acf6b984855646119551b39bffb4cf169dc40 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Sat, 22 May 2021 01:41:01 +0200
Subject: pretty printing formulae for sequence calculus

problem: minikanren may return a set of constraints, which aren't very
obvious for how to pretty-print them (currently they're just displayed
as an empty []).
---
 minikanren/sequentcalc.scm | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/minikanren/sequentcalc.scm b/minikanren/sequentcalc.scm
index e0099c0..fa882c9 100644
--- a/minikanren/sequentcalc.scm
+++ b/minikanren/sequentcalc.scm
@@ -18,6 +18,8 @@
 ;; always not terminate (as there are usually an infinite amount
 ;; of possible completions).
 
+(use-modules (ice-9 match))
+
 ;; goal: is q a member of the list l?
 (define
   (membero q l)
@@ -110,3 +112,16 @@
         (display "does not follow from sequent calculus")
         (display "follows from sequent calculus"))
     (newline)))
+
+
+(define (pretty formula)
+  (match formula
+    (('and a b) (string-append "(" (pretty a) " ∧ " (pretty b) ")"))
+    (('or a b) (string-append "(" (pretty a) " ∨ " (pretty b) ")"))
+    (('not a) (string-append "¬" (pretty a)))
+    (('arrow a b) (string-append "(" (pretty a) " → " (pretty b) ")"))
+    ('bottom "⊥")
+    (a (if (symbol? a) (symbol->string a) "[]"))))
+
+(define (prettylist formulae)
+  (map (lambda (f) (map pretty f)) formulae))
-- 
cgit v1.2.3