fixed parser ignoring tokens and flipped associativity the right way round

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

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml

@@ -24,10 +24,10 @@ struct
   open Scanner
 
   val prec =
-    fn AND => (6, 7)
-     | OR => (4, 5)
-     | RARROW => (3, 2)
-     | LRARROW => (1, 2)
+    fn AND => (7, 6)
+     | OR => (5, 4)
+     | RARROW => (2, 3)
+     | LRARROW => (1, 1)
      | _ => (~1, ~1)
 
   exception NotOperator
@@ -122,8 +122,13 @@ struct
                   val (lprec, rprec) = prec t
                   val comb = comb_func t
                 in
-                  if lprec < mprec then OK (v, r1, ts)
-                  else ((comb_p rprec) oo (fn res => comb (v, res))) rest
+                  if lprec < mprec then
+                    if connective t then
+                      ((comb_p 0) oo (fn res => comb (v, res))) rest
+                    else
+                      OK (v, r1, ts)
+                  else
+                    ((comb_p rprec) oo (fn res => comb (v, res))) rest
                 end
     in
       comb_p 0

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig

@@ -18,4 +18,6 @@ sig
 
   val scan: {srcname: string, input: string} -> (token * Region.reg) list
   val pp_token: token -> string
+
+  val connective: token -> bool
 end

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml

@@ -61,4 +61,7 @@ struct
      | ERR => "unk"
      | HASH => "#"
      | IDENT s => s
+
+  val connective =
+    fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false
 end