From b54197d9b48417d34c097384e9daf239618d0c2c Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 10 Nov 2024 05:33:21 +0100 Subject: [PATCH] cleanup --- tools/Holmake/HolLex | 54 +++++++----------------------- tools/Holmake/HolParser.sml | 2 +- tools/quote-filter/poly-unquote.ML | 1 + 3 files changed, 15 insertions(+), 42 deletions(-) diff --git a/tools/Holmake/HolLex b/tools/Holmake/HolLex index 9cf8e44170..a32fed8bc7 100644 --- a/tools/Holmake/HolLex +++ b/tools/Holmake/HolLex @@ -55,25 +55,12 @@ type lexresult = token datatype state = STATE of { parseError: int * int -> string -> unit, - linecount: (int * int) ref, pardepth: int ref, comdepth: int ref } fun noDecls pos = Decls {start = pos, decls = [], stop = pos} -fun linecol linecount pos = let val (line, start) = !linecount in (line, pos - start) end - -fun newline linecount pos = linecount := (#1 (!linecount) + 1, pos) - -fun newlines text linecount pos = let - fun go i = - if i < size text then ( - if String.sub(text, i) = #"\n" then newline linecount (pos + i + 1) else (); - go (i+1) - ) else () - in go 0 end - exception Unreachable datatype 'a test_result = TestOk of 'a | TestBad | TestSkip @@ -100,13 +87,6 @@ fun parseQuoteBody (STATE {parseError, ...}) continue pos test = let end in go [] NONE end -fun token_pos (EOF p) = p - | token_pos (EndTok p) = p - | token_pos (QED p) = p - | token_pos (ProofLine (p, _)) = p - | token_pos (TerminationTok p) = p - | token_pos _ = raise Unreachable (* only used for pushback tokens *) - fun parseDecls (STATE {parseError, pardepth, ...}) continue pos test = let fun go buf lookahead = let val tk = case lookahead of SOME tk => tk | NONE => continue() @@ -180,7 +160,7 @@ fun eof (_:state) = EOF %% %structure HolLex %s string stringlbrk comment quote holstrlit holstrlitlbrk ANTIQ; -%arg (UserDeclarations.STATE {pardepth, comdepth, linecount, parseError}); +%arg (UserDeclarations.STATE {pardepth, comdepth, parseError}); %full %posarg %eofpos @@ -243,7 +223,6 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] ^("Type"|"Overload"){ws}+({alphaMLid}|{quotedsymbolid})("["{alphaMLid_list}"]")?{ws}*"=" => (Decl (BeginType (yypos, yytext), NONE)); {Theorempfx}{ws}*":" => (let - val _ = newlines yytext linecount yypos val _ = YYBEGIN quote val (q, proof_tok, stop, extra) = parseQuoteBody yyarg continue (yypos, yyend) (fn ProofLine l => TestOk l | _ => TestBad) @@ -287,10 +266,7 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] YYBEGIN quote; parseQuoteEndDef yyarg continue yypos yytext QuoteEqnDecl before YYBEGIN INITIAL ); -{Theorempfx}({ws}|{newline})+"=" => ( - newlines yytext linecount yypos; - Decl (BeginSimpleThm (yypos, yytext), NONE) -); +{Theorempfx}({ws}|{newline})+"=" => (Decl (BeginSimpleThm (yypos, yytext), NONE)); ^{Inductivepfx} => ( YYBEGIN quote; parseQuoteEndDef yyarg continue yypos yytext InductiveDecl before YYBEGIN INITIAL @@ -328,12 +304,10 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] | _ => raise Unreachable); {declforms} => (if !pardepth = 0 then Decl (Chunk yypos, NONE) else continue()); {MLid} => (continue()); -{newline}"End" => (newline linecount (yyend-3); EndTok (yyend-3)); +{newline}"End" => (EndTok (yyend-3)); -"\\\\" => (continue()); -"\\\"" => (continue()); -"\\"{newline} => (newline linecount yyend; YYBEGIN stringlbrk; continue()); -"\\"{ws} => (YYBEGIN stringlbrk; continue()); +"\\\\"|"\\\"" => (continue()); +"\\"({ws}|{newline}) => (YYBEGIN stringlbrk; continue()); "\"" => (StringEnd yyend); [^\\""\n\015]{1,10} => (continue()); @@ -357,12 +331,12 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] in YYBEGIN holstrlit; go () end); "^"({symbol}|"^"*{ws}|[`^]) => (continue()); -"^"+{newline}"End" => (newline linecount (yyend-3); EndTok (yyend-3)); -"^"+{newline} => (newline linecount yyend; continue()); +"^"+{newline}"End" => (EndTok (yyend-3)); +"^"+{newline} => (continue()); {newline}{DefinitionLabel} => (let val ss = Substring.dropl Char.isSpace (Substring.full yytext) val n = yypos + #2 (Substring.base ss) - in newline linecount n; QDecl (DefinitionLabel (n, Substring.string ss), NONE) end); + in QDecl (DefinitionLabel (n, Substring.string ss), NONE) end); "(*" => ( comdepth := 1; YYBEGIN comment; case continue() of @@ -371,8 +345,8 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] | _ => raise Unreachable ); {quoteend} => (QuoteEnd (yypos, yytext)); -{newline}"End" => (newline linecount (yyend-3); EndTok (yyend-3)); -{newline}"Termination" => (newline linecount (yyend-11); TerminationTok (yyend-11)); +{newline}"End" => (EndTok (yyend-3)); +{newline}"Termination" => (TerminationTok (yyend-11)); {fullquoteend} => (FullQuoteEnd (yypos, yytext)); "^" => ( YYBEGIN ANTIQ; @@ -386,7 +360,7 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] "\\"{HOLSTRLITend} => (continue()); {HOLSTRLITend} => (HolStrLitEnd (yypos, yytext)); "\\\\" => (continue()); -"\\"{newline} => (newline linecount yyend; YYBEGIN holstrlitlbrk; continue()); +"\\"{newline} => (YYBEGIN holstrlitlbrk; continue()); "\\"{ws} => (YYBEGIN holstrlitlbrk; continue()); "\\" . => (continue()); @@ -398,13 +372,11 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] val (decls, end_tok, stop, extra) = parseDecls yyarg continue yyend (fn CloseParen p => SOME p | _ => NONE) in Antiq (Paren {start_tok = yypos, decls = decls, end_tok = end_tok, stop = stop}, extra) end); -{ws}+ => (continue()); -{newline} => (newline linecount yyend; continue()); +({ws}|{newline})+ => (continue()); . => ( parseError (yypos, yyend) "expected identifier or parenthesized group"; yybufpos := !yybufpos - 1; (* unread last character *) Antiq (BadAntiq yypos, NONE) ); -{newline} => (newline linecount yyend; continue()); -. => (continue()); +.|{newline} => (continue()); diff --git a/tools/Holmake/HolParser.sml b/tools/Holmake/HolParser.sml index 929c71b4b4..c0d21f9129 100644 --- a/tools/Holmake/HolParser.sml +++ b/tools/Holmake/HolParser.sml @@ -24,7 +24,7 @@ in fun mkParser {read, parseError, pos} = let val lex = HolLex.makeLexer (read, pos) (H.STATE { - comdepth = ref 0, linecount = ref (0, 0), pardepth = ref 0, parseError = parseError}) + comdepth = ref 0, pardepth = ref 0, parseError = parseError}) val lookahead = ref NONE fun go () = case (case !lookahead of SOME tk => tk | NONE => lex ()) of diff --git a/tools/quote-filter/poly-unquote.ML b/tools/quote-filter/poly-unquote.ML index f27d3a886c..b2aeb45d83 100644 --- a/tools/quote-filter/poly-unquote.ML +++ b/tools/quote-filter/poly-unquote.ML @@ -7,6 +7,7 @@ use "../../tools-poly/Holmake/Systeml.sml"; use "../Holmake/AttributeSyntax.sig"; use "../Holmake/AttributeSyntax.sml"; use "../Holmake/HolLex.sml"; +use "../Holmake/QuoteFilter.sml"; use "../Holmake/HM_SimpleBuffer.sig"; use "../Holmake/HM_SimpleBuffer.sml"; use "../Holmake/HOLFS_dtype.sml";