From 68de6a806b3ce85165dbfc32cf68fea412e9efa8 Mon Sep 17 00:00:00 2001 From: William Ball Date: Tue, 13 Aug 2024 18:55:21 -0700 Subject: [PATCH] added negation and cleaned up/fixed parsing --- .../proof-checker/parser/FormulaParser.sml | 89 +++++++++++-------- .../wball/proof-checker/parser/SCANNER.sig | 4 +- .../wball/proof-checker/parser/Scanner.sml | 9 +- 3 files changed, 63 insertions(+), 39 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 50f4dd5..83e031b 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml +++ b/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 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 76d61b4..4068e91 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig +++ b/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 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 8be1c30..a10f69d 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml +++ b/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