From 82213f0df8e160982aed8204877af1c7932885a4 Mon Sep 17 00:00:00 2001 From: William Ball Date: Wed, 14 Aug 2024 10:13:45 -0700 Subject: [PATCH] reorganization in preparation for ProofParser --- .../proof-checker/parser/FormulaParser.sml | 45 +++++----- .../wball/proof-checker/parser/PARSER.sig | 2 +- .../wball/proof-checker/parser/ParseUtils.sml | 21 ++++- .../wball/proof-checker/parser/SCANNER.sig | 23 +---- .../wball/proof-checker/parser/Scanner.sml | 47 ++-------- .../wball/proof-checker/parser/TOKEN.sig | 51 +++++++++++ .../wball/proof-checker/parser/TermParser.sml | 10 +-- .../wball/proof-checker/parser/Token.sml | 86 +++++++++++++++++++ .../wball/proof-checker/parser/parser.mlb | 2 + 9 files changed, 190 insertions(+), 97 deletions(-) create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TOKEN.sig create mode 100644 lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Token.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 index 83e031b..3cbd108 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml @@ -15,25 +15,20 @@ struct 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 - exception NotOperator of token + exception NotOperator of Token.t val infix_table = - fn AND => (40, 41, Conj) - | OR => (30, 31, Disj) - | RARROW => (21, 20, Impl) - | LRARROW => (10, 10, Iff) + fn Token.AND => (40, 41, Conj) + | Token.OR => (30, 31, Disj) + | Token.RARROW => (21, 20, Impl) + | Token.LRARROW => (10, 10, Iff) | t => (100, 100, fn _ => raise NotOperator t) val prefix_table = - fn NEG => ((), 50, Neg) | t => ((), 100, fn _ => raise NotOperator t) + fn Token.NEG => ((), 50, Neg) | t => ((), 100, fn _ => raise NotOperator t) exception NotOperator @@ -53,20 +48,20 @@ struct fun parse_full ts = parse state ts fun equal_p ts = - ((term_p >>- eat EQ >>> term_p) oo Equal) ts + ((term_p >>- eat Token.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 ((Token.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) + "expecting identifier but found token " ^ Token.pp_token t) - val bottom_p = eat HASH oo (fn () => Bottom) + val bottom_p = eat Token.HASH oo (fn () => Bottom) fun forall_p ts = - ((eat FORALL ->> ident_p >>- eat DOT) + ((eat (Token.KEYWORD Token.Forall) ->> ident_p >>- eat Token.DOT) >>= (fn id => parse @@ -77,7 +72,7 @@ struct } oo Forall)) ts fun exists_p ts = - ((eat EXISTS ->> ident_p >>- eat DOT) + ((eat (Token.KEYWORD Token.Exists) ->> ident_p >>- eat Token.DOT) >>= (fn id => parse @@ -88,19 +83,19 @@ struct } oo Exists)) ts fun args_p ts = - (eat LPAREN + (eat Token.LPAREN ->> - ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p)) - (Utils.flip op::) >>- eat RPAREN) ts + ((term_p oo (fn x => [x])) ??* (eat Token.COMMA ->> term_p)) + (Utils.flip op::) >>- eat Token.RPAREN) ts - fun relation_p ((Scanner.IDENT id, r) :: rest) = + fun relation_p ((Token.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) + "expected identifier but found token " ^ Token.pp_token t) | relation_p [] = NO (Region.botloc, fn () => "expecting identifier but reached the end") @@ -112,7 +107,7 @@ struct fun atomic_p ts = (equal_p || bottom_p || relation_p || forall_p || exists_p - || (eat LPAREN ->> formula_p 0 >>- eat RPAREN)) ts + || (eat Token.LPAREN ->> formula_p 0 >>- eat Token.RPAREN)) ts and formula_p mprec [] = NO (Region.botloc, fn () => "expecting formula but reached the end") @@ -120,7 +115,7 @@ struct let (* get first term atomic or prefix *) val (lhs, r, rest') = unwrap - (if prefix_connective t then + (if Token.prefix_connective t then let val ((), rp, comb) = prefix_table t in (formula_p rp oo comb) rest end @@ -130,7 +125,7 @@ struct (* 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 + if Token.infix_connective t then let val (lp, rp, comb) = infix_table t in diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/PARSER.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/PARSER.sig index 287878d..8cb8abb 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/PARSER.sig +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/PARSER.sig @@ -2,5 +2,5 @@ signature PARSER = sig type result type state - val parse : state -> result ParseUtils.p + val parse: state -> result ParseUtils.p end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/ParseUtils.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/ParseUtils.sml index a6f2555..91a548c 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/ParseUtils.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/ParseUtils.sml @@ -1,2 +1,19 @@ -structure ParseUtils = - Parse (type token = Scanner.token val pp_token = Scanner.pp_token) +signature PARSEUTILS = +sig + include PARSE + val >>= : 'a p * ('a -> 'b p) -> 'b p +end + +structure ParseUtils: PARSEUTILS = +struct + structure ParseUtilsTemp = + Parse (type token = Token.t val pp_token = Token.pp_token) + open ParseUtilsTemp + + infix >>= + + fun (p >>= q) ts = + case p ts of + OK (v, r, ts') => q v ts' + | NO e => NO e +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 4068e91..1740dbd 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig @@ -1,25 +1,4 @@ signature SCANNER = sig - datatype token = - LPAREN - | RPAREN - | NEG - | AND - | OR - | EQ - | RARROW - | LRARROW - | DOT - | COMMA - | HASH - | FORALL - | EXISTS - | IDENT of string - | ERR - - val scan: {srcname: string, input: string} -> (token * Region.reg) list - val pp_token: token -> string - - val infix_connective: token -> bool - val prefix_connective: token -> bool + val scan: {srcname: string, input: string} -> (Token.t * Region.reg) list 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 a10f69d..0ced7d1 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml @@ -1,23 +1,7 @@ structure Scanner: SCANNER = struct open SimpleToken - - datatype token = - LPAREN - | RPAREN - | NEG - | AND - | OR - | EQ - | RARROW - | LRARROW - | DOT - | COMMA - | HASH - | FORALL - | EXISTS - | IDENT of string - | ERR + open Token fun map_token (Symb "(") = LPAREN | map_token (Symb ")") = RPAREN @@ -31,9 +15,10 @@ struct | map_token (Symb "=>") = RARROW | map_token (Symb "<=>") = LRARROW | map_token (Symb _) = ERR - | map_token (Id "forall") = FORALL - | map_token (Id "exists") = EXISTS - | map_token (Id id) = IDENT id + | map_token (Id id) = + (case KeywordMap.get (keywordMap, id) of + SOME keyword => KEYWORD keyword + | NONE => IDENT id) | map_token (Num _) = ERR fun const k _ = k @@ -47,26 +32,4 @@ struct , is_id = (List.all Char.isAlphaNum) o String.explode , is_num = const false } - - val pp_token = - fn LPAREN => "(" - | RPAREN => ")" - | NEG => "~" - | AND => "&" - | OR => "|" - | EQ => "=" - | RARROW => "=>" - | LRARROW => "<=>" - | DOT => "." - | COMMA => "," - | FORALL => "forall" - | EXISTS => "exists" - | ERR => "unk" - | HASH => "#" - | IDENT s => s - - val infix_connective = - fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false - - val prefix_connective = fn NEG => true | _ => false end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TOKEN.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TOKEN.sig new file mode 100644 index 0000000..7b711db --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TOKEN.sig @@ -0,0 +1,51 @@ +signature TOKEN = +sig + datatype keyword = + (* labels *) + Axiom + | AndI + | AndE + | OrI + | OrE + | ArrI + | ArrE + | NegI + | NegE + | RAA + | IffI + | IffE + | EqI + | EqE + | ForallI + | ForallE + | ExistsI + | ExistsE + + (* formulas *) + | Forall + | Exists + + structure KeywordMap: MAP where type key = string and type value = keyword + val keywordMap: KeywordMap.t + + datatype t = + LPAREN + | RPAREN + | NEG + | AND + | OR + | EQ + | RARROW + | LRARROW + | DOT + | COMMA + | HASH + | KEYWORD of keyword + | IDENT of string + | ERR + + val pp_token: t -> string + + val infix_connective: t -> bool + val prefix_connective: t -> bool +end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TermParser.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TermParser.sml index f0df4e1..2522382 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TermParser.sml +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/TermParser.sml @@ -19,7 +19,7 @@ struct fun term_p nil = NO (Region.botloc, fn () => "expecting identifier but reached the end") - | term_p ((Scanner.IDENT id, r) :: rest) = + | term_p ((Token.IDENT id, r) :: rest) = (case Utils.findIndex (id, binders) of SOME i => OK (Var i, r, rest) | NONE => @@ -31,13 +31,13 @@ struct OK (Free id, r, rest)) | term_p ((t, r) :: rest) = NO (#1 r, fn () => - "expecting variable but found token " ^ pp_token t) + "expecting variable but found token " ^ Token.pp_token t) and args_p ts = - (eat LPAREN + (eat Token.LPAREN ->> - ((term_p oo (fn x => [x])) ??* (eat COMMA ->> term_p)) - (Utils.flip op::) >>- eat RPAREN) ts + ((term_p oo (fn x => [x])) ??* (eat Token.COMMA ->> term_p)) + (Utils.flip op::) >>- eat Token.RPAREN) ts in term_p end diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Token.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Token.sml new file mode 100644 index 0000000..166238d --- /dev/null +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Token.sml @@ -0,0 +1,86 @@ +structure Token: TOKEN = +struct + datatype keyword = + Axiom + | AndI + | AndE + | OrI + | OrE + | ArrI + | ArrE + | NegI + | NegE + | RAA + | IffI + | IffE + | EqI + | EqE + | ForallI + | ForallE + | ExistsI + | ExistsE + | Forall + | Exists + + datatype t = + LPAREN + | RPAREN + | NEG + | AND + | OR + | EQ + | RARROW + | LRARROW + | DOT + | COMMA + | HASH + | KEYWORD of keyword + | IDENT of string + | ERR + + structure KeywordMap = Map (structure Ord = StringOrd type value = keyword) + val keywordMap = KeywordMap.fromList + [ ("Axiom", Axiom) + , ("AndI", AndI) + , ("AndE", AndE) + , ("OrI", OrI) + , ("OrE", OrE) + , ("ArrI", ArrI) + , ("ArrE", ArrE) + , ("NegI", NegI) + , ("NegE", NegE) + , ("RAA", RAA) + , ("IffI", IffI) + , ("IffE", IffE) + , ("EqI", EqI) + , ("EqE", EqE) + , ("ForallI", ForallI) + , ("ForallE", ForallE) + , ("ExistsI", ExistsI) + , ("ExistsE", ExistsE) + , ("Forall", Forall) + , ("Exists", Exists) + ] + + val pp_token = + fn LPAREN => "(" + | RPAREN => ")" + | NEG => "~" + | AND => "&" + | OR => "|" + | EQ => "=" + | RARROW => "=>" + | LRARROW => "<=>" + | DOT => "." + | COMMA => "," + | FORALL => "forall" + | EXISTS => "exists" + | ERR => "unk" + | HASH => "#" + | IDENT s => s + + val infix_connective = + fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false + + val prefix_connective = fn NEG => true | _ => false +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 639270d..570e6aa 100644 --- a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb +++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb @@ -3,6 +3,8 @@ $(SML_LIB)/basis/basis.mlb ../utils/utils.mlb ../../../../github.com/diku-dk/sml-parse/parse.mlb ../../../../github.com/diku-dk/sml-parse/simple_token.mlb +TOKEN.sig +Token.sml SCANNER.sig Scanner.sml ParseUtils.sml