Skip to content

Commit

Permalink
close quotes terminate comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0
digama0 committed Nov 11, 2024
1 parent 5b303c3 commit c15d5e5
Show file tree
Hide file tree
Showing 5 changed files with 75 additions and 63 deletions.
73 changes: 48 additions & 25 deletions tools/Holmake/HolLex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,22 +37,23 @@ 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}

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 *)

Expand All @@ -61,18 +62,28 @@ 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}

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 =>
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -230,7 +244,11 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
<INITIAL>{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
Expand All @@ -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) =
Expand Down Expand Up @@ -325,7 +345,7 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]

<stringlbrk>"\\" => (YYBEGIN string; continue());

<comment>"(*" => (inc comdepth; continue());
<comment,holcomment>"(*" => (inc comdepth; continue());
<comment>"*)" => (dec comdepth; if !comdepth < 1 then Comment else continue());
<comment>[^\n()*]{1,10} => (continue());

Expand All @@ -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);
<quote>"(*" => (
comdepth := 1; YYBEGIN comment;
case continue() of
Comment => (YYBEGIN quote; continue())
| EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p)
| _ => raise Unreachable
);
<quote>{quoteend} => (QuoteEnd (yypos, yytext));
<quote>{newline}"End" => (EndTok (yyend-3));
<quote>{newline}"Termination" => (TerminationTok (yyend-11));
<quote>{fullquoteend} => (FullQuoteEnd (yypos, yytext));
<quote>"(*" => (comdepth := 1; comstart := SOME (yypos, yyend); YYBEGIN holcomment; continue());
<quote,holcomment>{quoteend} => (QuoteEnd (yypos, yytext));
<quote,holcomment>{newline}"End" => (EndTok (yyend-3));
<quote,holcomment>{newline}"Termination" => (TerminationTok (yyend-11));
<quote,holcomment>{fullquoteend} => (FullQuoteEnd (yypos, yytext));
<quote>"^" => (
YYBEGIN ANTIQ;
case continue() of
Expand All @@ -370,6 +384,15 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
);
<quote>{ws}+ => (continue());

<holcomment>"*)" => (
dec comdepth;
if !comdepth < 1 then
case !comstart of
SOME (pos, _) => (comstart := NONE; YYBEGIN quote; QDecl (QuoteComment (pos, yyend), NONE))
| _ => raise Unreachable
else continue()
);

<holstrlit>"\\"{HOLSTRLITend} => (continue());
<holstrlit>{HOLSTRLITend} => (HolStrLitEnd (yypos, yytext));
<holstrlit>"\\\\" => (continue());
Expand Down
31 changes: 16 additions & 15 deletions tools/Holmake/HolParser.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand All @@ -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
Expand Down
14 changes: 5 additions & 9 deletions tools/Holmake/tests/quote-filter/expected-mosml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down Expand Up @@ -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\
Expand Down Expand Up @@ -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\
Expand All @@ -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) *)
14 changes: 5 additions & 9 deletions tools/Holmake/tests/quote-filter/expected-poly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
Expand Down Expand Up @@ -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\
Expand Down Expand Up @@ -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\
Expand All @@ -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) *)
6 changes: 1 addition & 5 deletions tools/Holmake/tests/quote-filter/input
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
`foo = #"^`"`
`"\""`
`` ``
``(* foo *)``
``(* foo``
`^^`
"\"" ``foo``
"\\" `foo`
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit c15d5e5

Please sign in to comment.