From 55a1a9ce0ad3434bb200329ce1e7605207fa47cd Mon Sep 17 00:00:00 2001 From: William Ball Date: Tue, 13 Aug 2024 16:07:54 -0700 Subject: [PATCH] pretty printer now respects associativity --- .../wball/proof-checker/kernel/Formula.sml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml index 24c5902..2118f66 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml @@ -122,10 +122,12 @@ struct f ^ "(" ^ (String.concatWith ", " (map (Term.ppd d) args)) ^ ")" | Equal (t, s) => Term.ppd d t ^ " = " ^ Term.ppd d s | Neg (Equal (t, s)) => Term.ppd d t ^ " != " ^ Term.ppd d s - | Neg phi => "~" ^ ppd d np phi - | Conj (phi, psi) => ppd d np phi ^ " \226\136\167 " ^ ppd d np psi - | Disj (phi, psi) => ppd d np phi ^ " \226\136\168 " ^ ppd d np psi - | Impl (phi, psi) => ppd d np phi ^ " => " ^ ppd d np psi + | Neg phi => "\194\172" ^ ppd d np phi + | Conj (phi, psi) => + ppd d np phi ^ " \226\136\167 " ^ ppd d (np + 1) psi + | Disj (phi, psi) => + ppd d np phi ^ " \226\136\168 " ^ ppd d (np + 1) psi + | Impl (phi, psi) => ppd d (np + 1) phi ^ " => " ^ ppd d np psi | Iff (phi, psi) => ppd d np phi ^ " <=> " ^ ppd d np psi | Forall phi => "\226\136\128" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi | Exists phi => "\226\136\131" ^ Var.name d ^ ". " ^ ppd (d + 1) np phi