From c15d5e55d8b63b14669c3aed52213c3c0d682571 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 11 Nov 2024 04:56:38 +0100 Subject: [PATCH] close quotes terminate comments --- tools/Holmake/HolLex | 73 ++++++++++++------- tools/Holmake/HolParser.sml | 31 ++++---- .../Holmake/tests/quote-filter/expected-mosml | 14 ++-- .../Holmake/tests/quote-filter/expected-poly | 14 ++-- tools/Holmake/tests/quote-filter/input | 6 +- 5 files changed, 75 insertions(+), 63 deletions(-) diff --git a/tools/Holmake/HolLex b/tools/Holmake/HolLex index 21af58fa64..38c7bec40e 100644 --- a/tools/Holmake/HolLex +++ b/tools/Holmake/HolLex @@ -37,6 +37,7 @@ and antiq and qdecl = QuoteAntiq of int * antiq | DefinitionLabel of int * string + | QuoteComment of int * int and qbody = QBody of {start: int, toks: qdecl list, stop: int} @@ -44,15 +45,15 @@ datatype token = Decl of decl * token option (* from INITIAL *) | CloseParen of int (* from INITIAL *) | QED of int (* from INITIAL *) - | EndTok of int (* from INITIAL, quote *) + | EndTok of int (* from INITIAL, quote, holcomment *) | Comment (* from comment *) | Antiq of antiq * token option (* from ANTIQ *) | StringEnd of int (* from string *) | HolStrLitEnd of int * string (* from holstrlit *) - | ProofLine of int * string (* from quote *) - | TerminationTok of int (* from quote *) - | QuoteEnd of int * string (* from quote *) - | FullQuoteEnd of int * string (* from quote *) + | ProofLine of int * string (* from quote, holcomment *) + | TerminationTok of int (* from quote, holcomment *) + | QuoteEnd of int * string (* from quote, holcomment *) + | FullQuoteEnd of int * string (* from quote, holcomment *) | QDecl of qdecl * token option (* from quote *) | EOF of int (* from every state *) @@ -61,7 +62,8 @@ type lexresult = token datatype state = STATE of { parseError: int * int -> string -> unit, pardepth: int ref, - comdepth: int ref + comdepth: int ref, + comstart: (int * int) option ref } fun noDecls pos = Decls {start = pos, decls = [], stop = pos} @@ -69,10 +71,19 @@ fun noDecls pos = Decls {start = pos, decls = [], stop = pos} exception Unreachable datatype 'a test_result = TestOk of 'a | TestBad | TestSkip -fun parseQuoteBody (STATE {parseError, ...}) continue pos test = let +fun forceCloseComment (STATE {parseError, comdepth, comstart, ...}) stop buf = + case !comstart of + SOME pos => ( + parseError pos "unterminated comment"; + comdepth := 0; comstart := NONE; + QuoteComment (#1 pos, stop) :: buf) + | _ => buf + +fun parseQuoteBody (arg as STATE {parseError, ...}) continue pos test = let fun go buf lookahead = let val tk = case lookahead of SOME tk => tk | NONE => continue() - fun finish stop = QBody {start = #2 pos, toks = rev buf, stop = stop} + fun finish stop = + QBody {start = #2 pos, toks = rev (forceCloseComment arg stop buf), stop = stop} fun cont (p, t) strong = case test tk of TestBad => @@ -127,8 +138,11 @@ fun strlitMatch "\"" "\"" = true | strlitMatch _ _ = false fun parseQuoteEndDef yyarg continue pos text mk = let - val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue - (pos, pos + size text) (fn EndTok p => TestOk p | _ => TestBad) + val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue (pos, pos + size text) (fn + EndTok p => TestOk p + | QuoteEnd _ => TestSkip + | FullQuoteEnd _ => TestSkip + | _ => TestBad) in Decl (mk {head = (pos, text), quote = q, end_tok = end_tok, stop = stop}, extra) end @@ -164,8 +178,8 @@ fun eof (_:state) = EOF %% %structure HolLex -%s string stringlbrk comment quote holstrlit holstrlitlbrk ANTIQ; -%arg (UserDeclarations.STATE {pardepth, comdepth, parseError}); +%s string stringlbrk comment holcomment quote holstrlit holstrlitlbrk ANTIQ; +%arg (UserDeclarations.STATE {pardepth, comdepth, comstart, parseError}); %full %posarg %eofpos @@ -230,7 +244,11 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] {Theorempfx}{ws}*":" => (let val _ = YYBEGIN quote val (q, proof_tok, stop, extra) = - parseQuoteBody yyarg continue (yypos, yyend) (fn ProofLine l => TestOk l | _ => TestBad) + parseQuoteBody yyarg continue (yypos, yyend) (fn + ProofLine l => TestOk l + | QuoteEnd _ => TestSkip + | FullQuoteEnd _ => TestSkip + | _ => TestBad) val _ = YYBEGIN INITIAL val (decls, qed, stop, extra) = case extra of @@ -248,6 +266,8 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] val (q, tok, stop, extra) = parseQuoteBody yyarg continue (yypos, yypos + size yytext) (fn TerminationTok p => TestOk (p, true) | EndTok p => TestOk (p, false) + | QuoteEnd _ => TestSkip + | FullQuoteEnd _ => TestSkip | _ => TestBad) val _ = YYBEGIN INITIAL val (termination, end_tok, stop, extra) = @@ -325,7 +345,7 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] "\\" => (YYBEGIN string; continue()); -"(*" => (inc comdepth; continue()); +"(*" => (inc comdepth; continue()); "*)" => (dec comdepth; if !comdepth < 1 then Comment else continue()); [^\n()*]{1,10} => (continue()); @@ -350,17 +370,11 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] val ss = Substring.dropl Char.isSpace (Substring.full yytext) val n = yypos + #2 (Substring.base ss) in QDecl (DefinitionLabel (n, Substring.string ss), NONE) end); -"(*" => ( - comdepth := 1; YYBEGIN comment; - case continue() of - Comment => (YYBEGIN quote; continue()) - | EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p) - | _ => raise Unreachable -); -{quoteend} => (QuoteEnd (yypos, yytext)); -{newline}"End" => (EndTok (yyend-3)); -{newline}"Termination" => (TerminationTok (yyend-11)); -{fullquoteend} => (FullQuoteEnd (yypos, yytext)); +"(*" => (comdepth := 1; comstart := SOME (yypos, yyend); YYBEGIN holcomment; continue()); +{quoteend} => (QuoteEnd (yypos, yytext)); +{newline}"End" => (EndTok (yyend-3)); +{newline}"Termination" => (TerminationTok (yyend-11)); +{fullquoteend} => (FullQuoteEnd (yypos, yytext)); "^" => ( YYBEGIN ANTIQ; case continue() of @@ -370,6 +384,15 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"] ); {ws}+ => (continue()); +"*)" => ( + dec comdepth; + if !comdepth < 1 then + case !comstart of + SOME (pos, _) => (comstart := NONE; YYBEGIN quote; QDecl (QuoteComment (pos, yyend), NONE)) + | _ => raise Unreachable + else continue() +); + "\\"{HOLSTRLITend} => (continue()); {HOLSTRLITend} => (HolStrLitEnd (yypos, yytext)); "\\\\" => (continue()); diff --git a/tools/Holmake/HolParser.sml b/tools/Holmake/HolParser.sml index 2b8ea47ad0..9f57ba5a16 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, pardepth = ref 0, parseError = parseError}) + comdepth = ref 0, comstart = ref NONE, pardepth = ref 0, parseError = parseError}) val lookahead = ref NONE fun go () = case (case !lookahead of SOME tk => tk | NONE => lex ()) of @@ -342,6 +342,7 @@ structure ToSML = struct aux ",local]") fun doQuoteCore start ds stop f = case ds of [] => quote (start, stop) + | QuoteComment _ :: rest => doQuoteCore start rest stop f | QuoteAntiq (_, BadAntiq _) :: rest => doQuoteCore start rest stop f | QuoteAntiq (p, Ident (idstart, id)) :: rest => ( quote (start, p); @@ -363,20 +364,20 @@ structure ToSML = struct | SOME g => (quote (start, p); g l; doQuoteCore (p + size t) rest stop f) and doQuote (QBody {start, toks, stop}) = (aux "[QUOTE \""; doQuoteCore start toks stop NONE; aux "\"]") - and doQuoteConj (QBody {start, toks, stop}) f = ( - aux "[QUOTE \"("; - case toks of - DefinitionLabel (l as (p, t)) :: rest => let - val _ = locpragma start - val first = ref true - fun strcode1 (p as (_, s)) = ( - if !first then first := Substring.isEmpty (Substring.dropl Char.isSpace s) else (); - strcode0 p) - val _ = wrap strcode1 (start, p) - val _ = f (!first) l - in doQuoteCore (p + size t) rest stop (SOME (f false)) end - | _ => doQuoteCore start toks stop (SOME (f false)); - aux ")\"]") + and doQuoteConj (QBody {start, toks, stop}) f = let + val first = ref true + val strcode1 = wrap (fn (p as (_, s)) => ( + if !first then first := Substring.isEmpty (Substring.dropl Char.isSpace s) else (); + strcode0 p)) + fun doQuote0 start toks = + case toks of + DefinitionLabel (l as (p, t)) :: rest => ( + strcode1 (start, p); f (!first) l; + doQuoteCore (p + size t) rest stop (SOME (f false))) + | QuoteComment (p, stop) :: rest => + (strcode1 (start, p); strcode (p, stop); doQuote0 stop rest) + | _ => doQuoteCore start toks stop (SOME (f false)) + in aux "[QUOTE \"("; locpragma start; doQuote0 start toks; aux ")\"]" end and doDecl eager pos d = case d of DefinitionDecl {head = (p, head), quote, termination, stop, ...} => let val {keyword, name, attrs, name_attrs} = parseDefinitionPfx head diff --git a/tools/Holmake/tests/quote-filter/expected-mosml b/tools/Holmake/tests/quote-filter/expected-mosml index 4cc3306bc0..8564dbfa06 100644 --- a/tools/Holmake/tests/quote-filter/expected-mosml +++ b/tools/Holmake/tests/quote-filter/expected-mosml @@ -4,7 +4,7 @@ [QUOTE " (*#loc 4 2*)foo = #\"^`\""] [QUOTE " (*#loc 5 2*)\"\\\"\""] (Parse.Term [QUOTE " (*#loc 6 3*)\009"]) -(Parse.Term [QUOTE " (*#loc 7 3*)(* foo *)"]) +(Parse.Term [QUOTE " (*#loc 7 3*)(* foo"]) [QUOTE " (*#loc 8 2*)^^"] "\"" (Parse.Term [QUOTE " (*#loc 9 8*)foo"]) "\\" [QUOTE " (*#loc 10 7*)foo"] @@ -37,7 +37,7 @@ val foo = TotalDefn.qDefine "foo" [QUOTE " (*#loc 34 16*)\n\ val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)\n\ \ (* (* *) *)\n\ -\) /\\ ( (*#loc 40 8*)\n\ +\ (*#loc 40 8*)\n\ \ compile_rel foo bar\n\ \) /\\ ( (*#loc 42 8*)\n\ \ compile_rel foo bar\n\ @@ -67,7 +67,7 @@ val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#l \ !x y. reln x y ==> reln y x\n\ \) /\\ ( (*#loc 68 9*)\n\ \ !x. reln x 0\n\ -\)"]; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH); +\)"]; val reln_strongind = DB.fetch "-" "reln_strongind" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH); val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)\n\ \ (*#loc 73 10*) !x y. x < y ==> reln (x + 1) y\n\ @@ -87,13 +87,9 @@ val thmname = boolLib.save_thm("thmname", expression );val _ = bar_x [QUOTE " (*#loc 87 13*)\n\ \ another quotation (* with unfinished comment\n\ \ and bare \" with ^foo and ^\n\ -\End\n\ -\\n\ -\Quote another_one:\n\ -\ jk this is the end of the comment *)\n\ \"]; -val x = 91 + 10; +val x = 92 + 10; val y = 11 -val s = "" +val s = "" val s' = "foo.sml" (* #(FNAME) *) diff --git a/tools/Holmake/tests/quote-filter/expected-poly b/tools/Holmake/tests/quote-filter/expected-poly index 67c45eb65b..7b816eb143 100644 --- a/tools/Holmake/tests/quote-filter/expected-poly +++ b/tools/Holmake/tests/quote-filter/expected-poly @@ -4,7 +4,7 @@ [QUOTE " (*#loc 4 2*)foo = #\"^`\""] [QUOTE " (*#loc 5 2*)\"\\\"\""] (Parse.Term [QUOTE " (*#loc 6 3*)\009"]) -(Parse.Term [QUOTE " (*#loc 7 3*)(* foo *)"]) +(Parse.Term [QUOTE " (*#loc 7 3*)(* foo"]) [QUOTE " (*#loc 8 2*)^^"] "\"" (Parse.Term [QUOTE " (*#loc 9 8*)foo"]) "\\" [QUOTE " (*#loc 10 7*)foo"] @@ -37,7 +37,7 @@ val foo = TotalDefn.qDefine "foo" [QUOTE " (*#loc 34 16*)\n\ val (compile_rel_rules,compile_rel_ind,compile_rel_cases) = IndDefLib.xHol_reln "compile_rel" [QUOTE "( (*#loc 38 23*)\n\ \ (* (* *) *)\n\ -\) /\\ ( (*#loc 40 8*)\n\ +\ (*#loc 40 8*)\n\ \ compile_rel foo bar\n\ \) /\\ ( (*#loc 42 8*)\n\ \ compile_rel foo bar\n\ @@ -67,7 +67,7 @@ val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#l \ !x y. reln x y ==> reln y x\n\ \) /\\ ( (*#loc 68 9*)\n\ \ !x. reln x 0\n\ -\)"]; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 2 reln_rules handle HOL_ERR _ => boolTheory.TRUTH); +\)"]; val _ = CompilerSpecific.quietbind "val reln_strongind = DB.fetch \"-\" \"reln_strongind\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"; val reln_zero = boolLib.save_thm("reln_zero", Drule.cj 3 reln_rules handle HOL_ERR _ => boolTheory.TRUTH); val (reln_rules,reln_ind,reln_cases) = IndDefLib.xHol_reln "reln" [QUOTE "( (*#loc 72 16*)\n\ \ (*#loc 73 10*) !x y. x < y ==> reln (x + 1) y\n\ @@ -87,13 +87,9 @@ val thmname = boolLib.save_thm("thmname", expression );val _ = bar_x [QUOTE " (*#loc 87 13*)\n\ \ another quotation (* with unfinished comment\n\ \ and bare \" with ^foo and ^\n\ -\End\n\ -\\n\ -\Quote another_one:\n\ -\ jk this is the end of the comment *)\n\ \"]; -val x = 91 + 10; +val x = 92 + 10; val y = 11 -val s = "" +val s = "" val s' = "foo.sml" (* #(FNAME) *) diff --git a/tools/Holmake/tests/quote-filter/input b/tools/Holmake/tests/quote-filter/input index c6a563b569..4ec879d5ed 100644 --- a/tools/Holmake/tests/quote-filter/input +++ b/tools/Holmake/tests/quote-filter/input @@ -4,7 +4,7 @@ `foo = #"^`"` `"\""` `` `` -``(* foo *)`` +``(* foo`` `^^` "\"" ``foo`` "\\" `foo` @@ -89,10 +89,6 @@ Quote bar_x: and bare " with ^foo and ^ End -Quote another_one: - jk this is the end of the comment *) -End - val x = #(LINE) + 10; val #(LINE=11) y = #(LINE) val s = #(FNAME) #(FNAME=foo.sml)