From 9cf96669e1cbe77a4ff234ab789863b896c7fc5a Mon Sep 17 00:00:00 2001 From: William Ball Date: Tue, 13 Aug 2024 14:03:32 -0700 Subject: [PATCH] mostly? done with parsing formulas --- .../proof-checker/parser/FormulaParser.sml | 131 ++++++++++++++++++ .../wball/proof-checker/parser/SCANNER.sig | 1 + .../wball/proof-checker/parser/Scanner.sml | 5 +- .../wball/proof-checker/parser/parser.mlb | 1 + .../wball/proof-checker/parser/repl.sml | 19 ++- 5 files changed, 149 insertions(+), 8 deletions(-) create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml new file mode 100644 index 0000000..c649e60 --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml @@ -0,0 +1,131 @@ +structure FormulaParser: PARSER = +struct + type result = Formula.t + + structure StringSet = Utils.StringSet + structure ArityMap = Utils.ArityMap + + type state = + { binders: string list + , constants: StringSet.t + , functions: ArityMap.t + , relations: ArityMap.t + } + + open ParseUtils + infix >>> ->> >>- ?? ??? || oo oor ??* >>= + + fun ((p: 'a p) >>= (q: 'a -> 'b p)) ts = + case p ts of + OK (v, r, ts') => q v ts' + | NO e => NO e + + open Formula + open Scanner + + val prec = + fn AND => (6, 7) + | OR => (4, 5) + | RARROW => (3, 2) + | LRARROW => (1, 2) + | _ => (~1, ~1) + + 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 + }) = + let + val termState = + {binders = binders, constants = constants, functions = functions} + + val term_p = TermParser.parse termState + + fun formula_p ts = parse state ts + + fun equal_p ts = + ((term_p >>- eat EQ >>> term_p) oo Equal) ts + + fun ident_p nil = + NO (Region.botloc, fn () => + "expecting identifier but reached the end") + | ident_p ((Scanner.IDENT id, r) :: rest) = OK (id, r, rest) + | ident_p ((t, r) :: rest) = + NO (#1 r, fn () => + "expecting identifier but found token " ^ pp_token t) + + val bottom_p = eat HASH oo (fn () => Bottom) + + fun forall_p ts = + ((eat FORALL ->> ident_p >>- eat DOT) + >>= + (fn id => + parse + { binders = id :: binders + , constants = constants + , functions = functions + , relations = relations + } oo Forall)) ts + + fun exists_p ts = + ((eat EXISTS ->> ident_p >>- eat DOT) + >>= + (fn id => + parse + { binders = id :: binders + , constants = constants + , functions = functions + , relations = relations + } oo Exists)) ts + + fun args_p ts = + (eat LPAREN + ->> + ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p)) + (Utils.flip op::) >>- eat RPAREN) ts + + fun relation_p ((Scanner.IDENT id, r) :: rest) = + if ArityMap.member (relations, id) then + (args_p oo (fn args => Relation (id, rev args))) rest + else + NO (#1 r, fn () => "identifier '" ^ id ^ "' is not a relation") + | relation_p ((t, r) :: _) = + NO (#1 r, fn () => + "expected identifier but found token " ^ pp_token t) + | relation_p [] = + 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) + + fun comb_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 OK (v, r1, ts) + else ((comb_p rprec) oo (fn res => comb (v, res))) rest + end + in + comb_p 0 + 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 6532085..bbba13c 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig @@ -10,6 +10,7 @@ sig | LRARROW | DOT | COMMA + | HASH | FORALL | EXISTS | IDENT of string 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 7ee94cb..2c7779f 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml @@ -12,6 +12,7 @@ struct | LRARROW | DOT | COMMA + | HASH | FORALL | EXISTS | IDENT of string @@ -21,6 +22,7 @@ struct | map_token (Symb ")") = RPAREN | map_token (Symb ".") = DOT | map_token (Symb ",") = COMMA + | map_token (Symb "#") = HASH | map_token (Symb "&") = AND | map_token (Symb "|") = OR | map_token (Symb "=") = EQ @@ -38,7 +40,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 @@ -57,5 +59,6 @@ struct | FORALL => "forall" | EXISTS => "exists" | ERR => "unk" + | HASH => "#" | IDENT s => s end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb index 5ce090c..639270d 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb @@ -8,4 +8,5 @@ Scanner.sml ParseUtils.sml PARSER.sig TermParser.sml +FormulaParser.sml repl.sml diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml index db31f3a..f058689 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/repl.sml @@ -1,29 +1,34 @@ open Scanner -structure TermTesting: +structure Testing: sig val parse_repl: string -> unit end = struct - open TermParser + open FormulaParser open Utils open ParseUtils open Scanner - val binders = ["y", "x"] val functions = ArityMap.fromList [("S", 1), ("plus", 2)] val constants = StringSet.fromList ["zero"] - val state = {binders = binders, functions = functions, constants = constants} + val relations = ArityMap.fromList [("lt", 2)] + val state = + { binders = [] + , functions = functions + , constants = constants + , relations = relations + } fun parse_repl s = let val toks = scan {input = s, srcname = "repl"} in case parse state toks of - OK (t, _, []) => print ("Parsed successfully: " ^ Term.ppd 2 t ^ "\n") + OK (t, _, []) => print ("Parsed successfully: " ^ Formula.pp t ^ "\n") | OK (t, r, rest) => print - ("Parsed '" ^ Term.ppd 2 t ^ "' up to " ^ Region.pp r ^ ", but " + ("Parsed '" ^ Formula.pp t ^ "' up to " ^ Region.pp r ^ ", but " ^ Int.toString (length rest) ^ " tokens remain unparsed\n") | NO (r, err) => print ("ERROR: " ^ Region.ppLoc r ^ ", " ^ err () ^ "\n") end @@ -32,7 +37,7 @@ end fun repl () = ( print "> " ; case (TextIO.inputLine TextIO.stdIn) of - SOME s => (TermTesting.parse_repl s; repl ()) + SOME s => (Testing.parse_repl s; repl ()) | NONE => () )