added negation and cleaned up/fixed parsing

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

@@ -23,36 +23,34 @@ struct
   open Formula
   open Scanner
 
-  val prec =
-    fn AND => (7, 6)
-     | OR => (5, 4)
-     | RARROW => (2, 3)
-     | LRARROW => (1, 1)
-     | _ => (~1, ~1)
+  exception NotOperator of token
+
+  val infix_table =
+    fn AND => (40, 41, Conj)
+     | OR => (30, 31, Disj)
+     | RARROW => (21, 20, Impl)
+     | LRARROW => (10, 10, Iff)
+     | t => (100, 100, fn _ => raise NotOperator t)
+
+  val prefix_table =
+    fn NEG => ((), 50, Neg) | t => ((), 100, fn _ => raise NotOperator t)
 
   exception NotOperator
 
-  val comb_func =
-    fn AND => Conj
-     | OR => Disj
-     | RARROW => Impl
-     | LRARROW => Iff
-     | _ => fn (_, _) => raise NotOperator
-
   fun parse
     (state as
        { binders = binders
        , constants = constants
        , functions = functions
        , relations = relations
-       }) =
+       }) ts =
     let
       val termState =
         {binders = binders, constants = constants, functions = functions}
 
       val term_p = TermParser.parse termState
 
-      fun formula_p ts = parse state ts
+      fun parse_full ts = parse state ts
 
       fun equal_p ts =
         ((term_p >>- eat EQ >>> term_p) oo Equal) ts
@@ -107,30 +105,49 @@ struct
             NO (Region.botloc, fn () =>
               "expecting identifier but reached the end")
 
-      val atomic_p =
-        bottom_p || equal_p || forall_p || exists_p || relation_p
-        || (eat LPAREN ->> formula_p >>- eat RPAREN)
+      exception ParseError of locerr
 
-      fun comb_p mprec [] =
+      fun unwrap (OK c) = c
+        | unwrap (NO l) = raise ParseError l
+
+      fun atomic_p ts =
+        (equal_p || bottom_p || relation_p || forall_p || exists_p
+         || (eat LPAREN ->> formula_p 0 >>- eat RPAREN)) ts
+
+      and formula_p mprec [] =
             NO (Region.botloc, fn () => "expecting formula but reached the end")
-        | comb_p mprec ts =
-            case atomic_p ts of
-              NO e => NO e
-            | OK (v, r, []) => OK (v, r, [])
-            | OK (v, r1, ts as (t, r) :: rest) =>
-                let
-                  val (lprec, rprec) = prec t
-                  val comb = comb_func t
-                in
-                  if lprec < mprec then
-                    if connective t then
-                      ((comb_p 0) oo (fn res => comb (v, res))) rest
+        | formula_p mp (ts as ((t, r) :: rest)) =
+            let
+              (* get first term atomic or prefix *)
+              val (lhs, r, rest') = unwrap
+                (if prefix_connective t then
+                   let val ((), rp, comb) = prefix_table t
+                   in (formula_p rp oo comb) rest
+                   end
+                 else
+                   atomic_p ts)
+
+              (* loop through the rest while the precedence is high enough *)
+              fun loop (lhs, r, []) = OK (lhs, r, [])
+                | loop (lhs, r, ts as (t, _) :: rest) =
+                    if infix_connective t then
+                      let
+                        val (lp, rp, comb) = infix_table t
+                      in
+                        if lp < mp then
+                          OK (lhs, r, ts)
+                        else
+                          let val (rhs, r'', rest') = unwrap (formula_p rp rest)
+                          in loop (comb (lhs, rhs), r'', rest')
+                          end
+                      end
                     else
-                      OK (v, r1, ts)
-                  else
-                    ((comb_p rprec) oo (fn res => comb (v, res))) rest
-                end
+                      OK (lhs, r, ts)
+            in
+              loop (lhs, r, rest')
+            end
     in
-      comb_p 0
+      formula_p 0 ts
+      handle ParseError l => NO l
     end
 end

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

@@ -3,6 +3,7 @@ sig
   datatype token =
     LPAREN
   | RPAREN
+  | NEG
   | AND
   | OR
   | EQ
@@ -19,5 +20,6 @@ sig
   val scan: {srcname: string, input: string} -> (token * Region.reg) list
   val pp_token: token -> string
 
-  val connective: token -> bool
+  val infix_connective: token -> bool
+  val prefix_connective: token -> bool
 end

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

@@ -5,6 +5,7 @@ struct
   datatype token =
     LPAREN
   | RPAREN
+  | NEG
   | AND
   | OR
   | EQ
@@ -23,6 +24,7 @@ struct
     | map_token (Symb ".") = DOT
     | map_token (Symb ",") = COMMA
     | map_token (Symb "#") = HASH
+    | map_token (Symb "~") = NEG
     | map_token (Symb "&") = AND
     | map_token (Symb "|") = OR
     | map_token (Symb "=") = EQ
@@ -40,7 +42,7 @@ struct
     map (fn (t, r) => (map_token t, r))
     o
     tokenise
-      { sep_chars = "(),&|.#"
+      { sep_chars = "(),&|.#~"
       , symb_chars = "<=>"
       , is_id = (List.all Char.isAlphaNum) o String.explode
       , is_num = const false
@@ -49,6 +51,7 @@ struct
   val pp_token =
     fn LPAREN => "("
      | RPAREN => ")"
+     | NEG => "~"
      | AND => "&"
      | OR => "|"
      | EQ => "="
@@ -62,6 +65,8 @@ struct
      | HASH => "#"
      | IDENT s => s
 
-  val connective =
+  val infix_connective =
     fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false
+
+  val prefix_connective = fn NEG => true | _ => false
 end