summaryrefslogtreecommitdiff
path: root/minikanren
diff options
context:
space:
mode:
authorstuebinm2021-05-22 01:41:01 +0200
committerstuebinm2021-05-22 01:45:19 +0200
commit855acf6b984855646119551b39bffb4cf169dc40 (patch)
treed48a5488783e3d69f443c04f06ede76af0a01f0e /minikanren
parentd9ee055fb5ee77d3130372be29256878a06e2b93 (diff)
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 []).
Diffstat (limited to 'minikanren')
-rw-r--r--minikanren/sequentcalc.scm15
1 files changed, 15 insertions, 0 deletions
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))