From 607b9f1d7d68f4dfc6c1379c510fb1ec8b8d0c95 Mon Sep 17 00:00:00 2001
From: William Ball <williampi103@gmail.com>
Date: Tue, 13 Aug 2024 16:08:08 -0700
Subject: [PATCH] fixed parser ignoring tokens and flipped associativity the
 right way round

---
 .../proof-checker/parser/FormulaParser.sml      | 17 +++++++++++------
 .../wball/proof-checker/parser/SCANNER.sig      |  2 ++
 .../wball/proof-checker/parser/Scanner.sml      |  3 +++
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml
index c649e60..50f4dd5 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml
+++ b/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
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig
index bbba13c..76d61b4 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig
+++ b/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
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml
index 2c7779f..8be1c30 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml
+++ b/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