diff --git a/Manual/Tools/polyscripter.sml b/Manual/Tools/polyscripter.sml index 7b43875cb5..af93c1483d 100644 --- a/Manual/Tools/polyscripter.sml +++ b/Manual/Tools/polyscripter.sml @@ -17,11 +17,11 @@ fun lnumdie linenum extra exn = val outputPrompt = ref "> " -val quote = QFRead.fromString +val quote = HolParser.fromString val default_linewidth = 77 fun quoteFile lnum fname = - QFRead.inputFile fname handle e => lnumdie lnum "" e + HolParser.inputFile fname handle e => lnumdie lnum "" e datatype lbuf = LB of { @@ -319,7 +319,7 @@ fun process_line debugp umap obuf origline lbuf = let end val assertcmd = "##assert " val assertcmdsz = size assertcmd - val stringCReader = #read o QFRead.stringToReader true + val stringCReader = #read o HolParser.stringToReader true fun compile exnhandle input = (if debugp then TextIO.output(TextIO.stdErr, input) diff --git a/developers/genUseScript.sml b/developers/genUseScript.sml index 59db24f688..a9b3138cec 100644 --- a/developers/genUseScript.sml +++ b/developers/genUseScript.sml @@ -39,9 +39,9 @@ in (push, read, reset) end; -val _ = use "../tools/Holmake/QuoteFilter.sml"; -val _ = use "../tools/Holmake/QFRead.sig"; -val _ = use "../tools/Holmake/QFRead.sml"; +val _ = use "../tools/Holmake/HolLex.sml"; +val _ = use "../tools/Holmake/HolParser.sig"; +val _ = use "../tools/Holmake/HolParser.sml"; val _ = use "../tools/Holmake/Holdep_tokens.sig" val _ = use "../tools/Holmake/Holdep_tokens.sml"; diff --git a/src/AI/sml_inspection/smlExecute.sml b/src/AI/sml_inspection/smlExecute.sml index e235aafcee..41788d20cf 100644 --- a/src/AI/sml_inspection/smlExecute.sml +++ b/src/AI/sml_inspection/smlExecute.sml @@ -29,7 +29,7 @@ val sml_thml_glob = ref [] fun quse_string s = let - val stream = TextIO.openString (QFRead.fromString false s) + val stream = TextIO.openString (HolParser.fromString false s) fun infn () = TextIO.input1 stream in ( diff --git a/src/probability/borelScript.sml b/src/probability/borelScript.sml index dc64287159..733e0d0368 100644 --- a/src/probability/borelScript.sml +++ b/src/probability/borelScript.sml @@ -8120,8 +8120,8 @@ Theorem IN_MEASURABLE_BOREL_POW_EXP: (!x. x IN space a ==> h x = (f x) pow (g x)) ==> h IN Borel_measurable a Proof rw[] >> simp[Once IN_MEASURABLE_BOREL_PLUS_MINUS] >> - ‘!P. {x | P (g x)} INTER space a IN subsets a` by (rw[] >> - `{x | P (g x)} INTER space a = BIGUNION {{x | g x = n} INTER space a | P n}’ by ( + ‘!P. {x | P (g x)} INTER space a IN subsets a’ by (rw[] >> + ‘{x | P (g x)} INTER space a = BIGUNION {{x | g x = n} INTER space a | P n}’ by ( rw[Once EXTENSION,IN_BIGUNION] >> eq_tac >> strip_tac >> gvs[] >> qexists_tac ‘{y | g y = g x} INTER space a’ >> simp[] >> qexists_tac ‘g x’ >> simp[]) >> pop_assum SUBST1_TAC >> irule SIGMA_ALGEBRA_COUNTABLE_UNION >> @@ -8130,11 +8130,11 @@ Proof map_every (fn (pos,tm,qex,ths) => irule_at pos tm >> qexistsl_tac qex >> simp ths) [ (Pos hd,IN_MEASURABLE_BOREL_ADD',[‘λx. fn_minus f x pow g x * indicator_fn {x | EVEN (g x)} x’, ‘λx. fn_plus f x pow g x * indicator_fn {x | $< 0 (g x)} x’],[]), - (Pos (el 2),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | EVEN (g x)}`,`λx. fn_minus f x pow g x’],[]), + (Pos (el 2),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | EVEN (g x)}’,‘λx. fn_minus f x pow g x’],[]), (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | EVEN (g x)} INTER space a’],[]), - (Pos (el 3),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | $< 0 (g x)}`,`λx. fn_plus f x pow g x’],[]), + (Pos (el 3),IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | $< 0 (g x)}’,‘λx. fn_plus f x pow g x’],[]), (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | $< 0 (g x)} INTER space a’],[]), - (Pos last,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | ODD (g x)}`,`λx. fn_minus f x pow g x’],[]), + (Pos last,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | ODD (g x)}’,‘λx. fn_minus f x pow g x’],[]), (Pos (el 2),IN_MEASURABLE_BOREL_INDICATOR,[‘{x | ODD (g x)} INTER space a’],[])] >> pop_assum kall_tac >> ‘!pf. pf IN Borel_measurable a /\ (!x. 0 <= pf x) ==> (λx. pf x pow g x) IN Borel_measurable a’ by ( @@ -8142,7 +8142,7 @@ Proof qexistsl_tac [‘λn x. pf x pow n * indicator_fn {x | g x = n} x’] >> simp[pow_pos_le,INDICATOR_FN_POS,le_mul] >> simp[RIGHT_AND_FORALL_THM] >> strip_tac >> map_every (fn (pos,tm,qex,ths) => irule_at pos tm >> simp[] >> qexistsl_tac qex >> simp ths) [ - (Any,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | g x = n}`,`λx. pf x pow n’],[]), + (Any,IN_MEASURABLE_BOREL_MUL',[‘indicator_fn {x | g x = n}’,‘λx. pf x pow n’],[]), (Pos hd,IN_MEASURABLE_BOREL_POW',[‘n’,‘pf’],[]), (Pos hd,IN_MEASURABLE_BOREL_INDICATOR,[‘{x | g x = n} INTER space a’],[indicator_fn_def])] >> rw[] >> qspecl_then [‘g x’,‘pf x pow g x’] mp_tac ext_suminf_sing_general >> diff --git a/src/tactictoe/examples/ttt_demoScript.sml b/src/tactictoe/examples/ttt_demoScript.sml index 623e78ef74..b9fc943a78 100644 --- a/src/tactictoe/examples/ttt_demoScript.sml +++ b/src/tactictoe/examples/ttt_demoScript.sml @@ -31,7 +31,7 @@ open listTheory (* ttt ([],``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``); *) val ex2 = store_thm("ex2", ``(!n. f n = c) ==> (MAP f ls = REPLICATE (LENGTH ls) c)``, - asm_simp_tac (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss)) [LIST_EQ_REWRITE] >> + asm_simp_tac (srw_ss () ++ boolSimps.LET_ss ++ ARITH_ss) [LIST_EQ_REWRITE] >> metis_tac [EL_MAP, rich_listTheory.EL_REPLICATE] ); diff --git a/src/tactictoe/src/tttToken.sml b/src/tactictoe/src/tttToken.sml index 281a4cf55d..dcb57a7bac 100644 --- a/src/tactictoe/src/tttToken.sml +++ b/src/tactictoe/src/tttToken.sml @@ -175,7 +175,7 @@ fun inst_term sterm stac = (* load "tttToken"; open tttToken; val stac = "EXISTS_TAC ``1:num``"; -val stac' = QFRead.fromString false stac; +val stac' = HolParser.fromString false stac; val (astac,sterm) = valOf (abstract_term stac'); val istac = inst_term "2:num" astac; *) diff --git a/src/tactictoe/src/tttUnfold.sml b/src/tactictoe/src/tttUnfold.sml index 0807d55fdd..2f03de6947 100644 --- a/src/tactictoe/src/tttUnfold.sml +++ b/src/tactictoe/src/tttUnfold.sml @@ -973,7 +973,7 @@ fun rm_spaces s = fun sketch_wrap thy file = let - val s1 = QFRead.inputFile file + val s1 = HolParser.inputFile file val s2 = rm_spaces (rm_comment s1) val sl = partial_sml_lexer s2 val lexdir = tactictoe_dir ^ "/log/lexer" diff --git a/tools-poly/configure.sml b/tools-poly/configure.sml index f4ea305ba2..e871e051ed 100644 --- a/tools-poly/configure.sml +++ b/tools-poly/configure.sml @@ -425,13 +425,13 @@ val _ = work_in_dir val _ = work_in_dir "Holmake" (fullPath [HOLDIR, "tools", "Holmake", "poly"]) (fn () => (OS.FileSys.chDir ".."; - systeml [lexer, "QuoteFilter"] ; + systeml [lexer, "HolLex"]; OS.FileSys.chDir "poly"; polyc_compile (SOME "../mlton/Holmake.mlb") "poly-Holmake.ML" hmakebin)) (* unquote - the quotation filter *) -val _ = work_in_dir "unquote." qfdir +val _ = work_in_dir "unquote" qfdir (fn () => (polyc_compile NONE "poly-unquote.ML" qfbin)) (* holdeptool *) diff --git a/tools-poly/holrepl.ML b/tools-poly/holrepl.ML index 28269c247c..5f3d8160a2 100644 --- a/tools-poly/holrepl.ML +++ b/tools-poly/holrepl.ML @@ -163,7 +163,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm, in fn () => let (* Create a new lexer for each command block. *) - val {read, ...} = QFRead.inputToReader true input; + val {read, ...} = HolParser.inputToReader true input; val endOfBlock = ref false; fun read' () = case read () of NONE => (endOfBlock := true; NONE) @@ -195,7 +195,7 @@ fun topLevel diag {nameSpace, exitLoop, exitOnError, isInteractive, zeroTerm, fun cgen() = !cgenref() fun bind_cgen () = let - val {read, ...} = QFRead.streamToReader true TextIO.stdIn + val {read, ...} = HolParser.streamToReader true TextIO.stdIn in cgenref := read end diff --git a/tools-poly/poly-build.ML b/tools-poly/poly-build.ML index 82c40a2492..0720da6bea 100644 --- a/tools-poly/poly-build.ML +++ b/tools-poly/poly-build.ML @@ -17,8 +17,8 @@ val _ = useC "HOLFileSys"; val _ = useC "Holdep_tokens"; val _ = useC "HM_SimpleBuffer"; val _ = useC "AttributeSyntax"; -val _ = use "../tools/Holmake/QuoteFilter.sml"; -val _ = useC "QFRead"; +val _ = use "../tools/Holmake/HolLex.sml"; +val _ = useC "HolParser"; val _ = useC "Holdep"; val _ = use "../tools/Holmake/Holmake_tools_dtype.sml"; val _ = use "../tools/Holmake/terminal_primitives.sig"; diff --git a/tools-poly/poly/poly-init2.ML b/tools-poly/poly/poly-init2.ML index c72df78410..8deea6fd15 100644 --- a/tools-poly/poly/poly-init2.ML +++ b/tools-poly/poly/poly-init2.ML @@ -6,7 +6,7 @@ val _ = use "Holmake/Systeml.sml" val _ = use "../tools/Holmake/AttributeSyntax.sig"; val _ = use "../tools/Holmake/AttributeSyntax.sml"; -val _ = use "../tools/Holmake/QuoteFilter.sml"; +val _ = use "../tools/Holmake/HolLex.sml"; val _ = use "../tools/Holmake/HM_SimpleBuffer.sig"; val _ = use "../tools/Holmake/HM_SimpleBuffer.sml"; val _ = use "../tools/Holmake/HOLFS_dtype.sml"; @@ -15,8 +15,8 @@ val _ = use "../tools/Holmake/poly/HFS_NameMunge.sml"; val _ = use "../tools/Holmake/HOLFS_dtype.sml"; val _ = use "../tools/Holmake/HOLFileSys.sig"; val _ = use "../tools/Holmake/HOLFileSys.sml"; -val _ = use "../tools/Holmake/QFRead.sig"; -val _ = use "../tools/Holmake/QFRead.sml"; +val _ = use "../tools/Holmake/HolParser.sig"; +val _ = use "../tools/Holmake/HolParser.sml"; val _ = use "poly/quse.sig"; val _ = use "poly/quse.sml"; diff --git a/tools-poly/poly/quse.sml b/tools-poly/poly/quse.sml index cf455f14c9..1c08a370b6 100644 --- a/tools-poly/poly/quse.sml +++ b/tools-poly/poly/quse.sml @@ -1,7 +1,7 @@ structure QUse :> QUse = struct -fun use_reader fname (reader as {read = infn0, eof, reset}) = +fun use_reader fname (reader as {read = infn0, eof}) = let val lineNo = ref 1 fun infn () = @@ -17,12 +17,12 @@ fun use_reader fname (reader as {read = infn0, eof, reset}) = Compiler.CPLineNo (fn () => !lineNo)]) () end -fun use fname = use_reader fname (QFRead.fileToReader fname) +fun use fname = use_reader fname (HolParser.fileToReader fname) fun useScript fname = let val istream = TextIO.openIn fname - val reader = QFRead.streamToReader true istream + val reader = HolParser.streamToReader true istream val _ = use_reader fname reader handle e => (TextIO.closeIn istream; raise e) in diff --git a/tools/Holmake/.gitignore b/tools/Holmake/.gitignore index 28bd1009d3..e2010ab40a 100644 --- a/tools/Holmake/.gitignore +++ b/tools/Holmake/.gitignore @@ -1 +1,2 @@ QuoteFilter.sml +HolLex.sml diff --git a/tools/Holmake/AttributeSyntax.sig b/tools/Holmake/AttributeSyntax.sig index d54da729e0..9c6bb6bd04 100644 --- a/tools/Holmake/AttributeSyntax.sig +++ b/tools/Holmake/AttributeSyntax.sig @@ -2,6 +2,7 @@ signature AttributeSyntax = sig val mk_strsafe : string -> string + val bslash_escape : char -> string val bslash_escape_s : string -> string val dest_ml_thm_binding : string -> {keyword: string, name : string, name_attr_original : string, diff --git a/tools/Holmake/HolLex b/tools/Holmake/HolLex new file mode 100644 index 0000000000..9cf8e44170 --- /dev/null +++ b/tools/Holmake/HolLex @@ -0,0 +1,410 @@ +(* this is an -*- sml -*- file, or near enough *) +fun inc r = (r := !r + 1) +fun dec r = (r := !r - 1) + +datatype decl + = DefinitionDecl of { + head: int * string, quote: qbody, termination: {tok: int, decls: decls} option, + end_tok: int option, stop: int} + | DatatypeDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int} + | QuoteDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int} + | QuoteEqnDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int} + | InductiveDecl of {head: int * string, quote: qbody, end_tok: int option, stop: int} + | BeginType of int * string + | BeginSimpleThm of int * string + | TheoremDecl of { + head: int * string, quote: qbody, proof_tok: (int * string) option, + body: decls, qed: int option, stop: int} + | Chunk of int + | FullQuote of { + head: int * string, type_q: int option, + quote: qbody, end_tok: (int * string) option, stop: int} + | Quote of {head: int * string, quote: qbody, end_tok: (int * string) option, stop: int} + | String of int * int + +and decls = Decls of {start: int, decls: decl list, stop: int} + +and antiq + = Ident of int * string + | Paren of {start_tok: int, decls: decls, end_tok: int option, stop: int} + | BadAntiq of int + +and qdecl + = QuoteAntiq of int * antiq + | DefinitionLabel of int * string + +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 *) + | 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 *) + | QDecl of qdecl * token option (* from quote *) + | EOF of int (* from every state *) + +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 + +fun parseQuoteBody (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 cont (p, t) strong = + case test tk of + TestBad => + if strong then (parseError pos "unterminated quote"; (finish p, NONE, p, SOME tk)) + else (parseError (p, p + size t) ("unexpected '"^t^"'"); go buf NONE) + | TestSkip => go buf NONE + | TestOk out => (finish p, SOME out, p + size t, NONE) + in case tk of + QDecl (qd, extra) => go (qd :: buf) extra + | QuoteEnd pt => cont pt false + | FullQuoteEnd pt => cont pt false + | ProofLine pt => cont pt true + | TerminationTok p => cont (p, "Termination") true + | EndTok p => cont (p, "End") true + | EOF p => (parseError pos "unterminated quote"; (finish p, NONE, p, SOME tk)) + | _ => raise Unreachable + 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() + fun finish stop = Decls {start = pos, decls = rev buf, stop = stop} + fun cont (p, t) strong = + case test tk of + NONE => + if strong then (finish p, NONE, p, SOME tk) + else (parseError (p, p + size t) ("unexpected '"^t^"'"); go buf NONE) + | out => (finish p, out, p + size t, NONE) + in case tk of + Decl (tk, look) => go (tk :: buf) look + | CloseParen p => cont (p, ")") false + | EndTok p => cont (p, "End") true + | QED p => cont (p, "QED") true + | EOF p => (finish p, NONE, p, SOME tk) + | _ => raise Unreachable + end + val n = !pardepth + in pardepth := 0; go [] NONE before pardepth := n end + +fun fullQuoteMatch "``" "``" = true + | fullQuoteMatch "\226\128\156" "\226\128\157" = true + | fullQuoteMatch _ _ = false + +fun quoteMatch "`" "`" = true + | quoteMatch "\226\128\152" "\226\128\153" = true + | quoteMatch _ _ = false + +fun strlitMatch "\"" "\"" = true + | strlitMatch "\226\128\185" "\226\128\186" = true + | strlitMatch "\194\171" "\194\187" = 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) + in + Decl (mk {head = (pos, text), quote = q, end_tok = end_tok, stop = stop}, extra) + end + +fun parseFullQuote (yyarg as STATE {parseError, ...}) continue pos yytext type_q = let + val qlen = if String.sub(yytext,0) = #"`" then 2 else 3 + val text = String.substring (yytext, 0, qlen) + val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue (pos, pos + qlen) (fn + FullQuoteEnd (tk as (p, t)) => ( + if fullQuoteMatch text t then () else parseError (p, p + size t) ("unexpected '"^t^"'"); + TestOk tk) + | QuoteEnd _ => TestSkip + | _ => TestBad) + in + Decl (FullQuote {head = (pos, text), type_q = type_q, + quote = q, end_tok = end_tok, stop = stop}, extra) + end + +fun parseQuote (yyarg as STATE {parseError, ...}) continue pos yytext = let + val qlen = if String.sub(yytext,0) = #"`" then 1 else 3 + val text = String.substring (yytext, 0, qlen) + val (q, end_tok, stop, extra) = parseQuoteBody yyarg continue (pos, pos + qlen) (fn + QuoteEnd (tk as (p, t)) => ( + if quoteMatch text t then () else parseError (p, p + size t) ("unexpected '"^t^"'"); + TestOk tk) + | FullQuoteEnd _ => TestSkip + | _ => TestBad) + in + Decl (Quote {head = (pos, text), quote = q, end_tok = end_tok, stop = stop}, extra) + end + +fun eof (_:state) = EOF + +%% +%structure HolLex +%s string stringlbrk comment quote holstrlit holstrlitlbrk ANTIQ; +%arg (UserDeclarations.STATE {pardepth, comdepth, linecount, parseError}); +%full +%posarg +%eofpos + +letter = [A-Za-z]; +digit = [0-9]; +nonspecial_symbol = [-!%&$+/<>?@~|#*\\^]; +symbol = {nonspecial_symbol} | [=:]; +symbolident = ":" {symbol}+ | "=" {symbol}+ | {nonspecial_symbol} {symbol}*; +alphaMLid_tailchar = ({letter} | {digit} | _ | "'"); +alphaMLid = {letter} {alphaMLid_tailchar}*; +alphaMLid_list = {alphaMLid} (","{alphaMLid})*; +quotedsymbolid = "\"" [^\034]+ "\""; +ws = [\ \t]; +newline = "\n" | "\013\n"; +optallws = ({ws}|{newline})*; +forcedallws = ({ws}|{newline})+; +attributeValue_tailchar = {alphaMLid_tailchar} | "."; +attributeValue = {letter} {attributeValue_tailchar}*; +attributeEqnRHS = {attributeValue}({forcedallws}{attributeValue})*; +defn_attribute = + {alphaMLid}{optallws} ("="{optallws}{attributeEqnRHS}{optallws})?; +defn_attribute_list = {defn_attribute} (","({ws}|{newline})*{defn_attribute})*; +MLid = {alphaMLid} | {symbolident}; +QUALMLid = {MLid} ("." {MLid})*; +QUALalphaMLid = {alphaMLid} ("." {alphaMLid})*; +locpragma = "(*#loc" {ws}+ {digit}* {ws}+ {digit}* {ws}* "*)"; +lowergreek = "\206" [\177-\191] | "\207" [\128-\137]; +fullquotebegin = "``" | "\226\128\156"; +fullquoteend = "``" | "\226\128\157"; +quotebegin = "`" | "\226\128\152"; +quoteend = "`" | "\226\128\153"; +Theorempfx = ("Theorem"|"Triviality"){ws}+{alphaMLid}({ws}*"["{alphaMLid_list}"]")?; +Quote_eqnpfx = "Quote"{ws}+{alphaMLid}{ws}*"="{ws}*{QUALalphaMLid}{ws}*":"; +Quote_pfx = "Quote"{ws}+{QUALalphaMLid}{ws}*":"; +HOLconjunction = "/\092" | "\226\136\167"; +DefinitionLabelID = {letter}{alphaMLid_tailchar}* | "~"{alphaMLid_tailchar}+ | {HOLconjunction}; +DefinitionLabel = "["{ws}*{DefinitionLabelID}?("["{alphaMLid_list}"]")?{ws}*":"?{ws}*"]"; +Definitionpfx = "Definition"{ws}+{alphaMLid}({ws}*"["{optallws}{defn_attribute_list}"]")?{ws}*":"; +declforms = "val"|"fun"|"structure"|"signature"|"functor"|"abstype"|"datatype"|"exception"|"open"|";"|"infix"[lr]?|"local"; +Inductivepfx = ("Co")?"Inductive"{ws}+{alphaMLid}{ws}*":"; +HOLSTRLITstart = "\"" | "\226\128\185" | "\194\171"; +HOLSTRLITend = "\"" | "\226\128\186" | "\194\187"; +ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]")?; +%% + +"(*" => ( + comdepth := 1; YYBEGIN comment; + case continue() of + Comment => (YYBEGIN INITIAL; continue()) + | EOF p => (parseError (yypos, yyend) "unterminated comment"; EOF p) + | _ => raise Unreachable +); +"(" => (inc pardepth; continue()); +")" => (if !pardepth < 1 then CloseParen yypos else (dec pardepth; continue())); +^"Datatype"{ws}*":" => ( + YYBEGIN quote; + parseQuoteEndDef yyarg continue yypos yytext DatatypeDecl before YYBEGIN INITIAL +); +^("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) + val _ = YYBEGIN INITIAL + val (decls, qed, stop, extra) = + case extra of + SOME (QED p) => (noDecls stop, SOME p, p + 3, NONE) + | SOME _ => (noDecls stop, NONE, stop, extra) + | NONE => parseDecls yyarg continue stop (fn QED p => SOME p | _ => NONE) + in + Decl (TheoremDecl { + head = (yypos, yytext), quote = q, proof_tok = proof_tok, + body = decls, qed = qed, stop = stop}, extra) + end); +^"QED" => (QED yypos); +^{Definitionpfx} => (let + val _ = YYBEGIN quote + val (q, tok, stop, extra) = parseQuoteBody yyarg continue (yypos, yypos + size yytext) (fn + TerminationTok p => TestOk (p, true) + | EndTok p => TestOk (p, false) + | _ => TestBad) + val _ = YYBEGIN INITIAL + val (termination, end_tok, stop, extra) = + case (tok, extra) of + (SOME (p, true), NONE) => let + val (decls, end_tok, stop, extra) = parseDecls yyarg continue stop + (fn EndTok p => SOME p | _ => NONE) + in (SOME {tok = p, decls = decls}, end_tok, stop, extra) end + | (SOME (p, false), NONE) => (NONE, SOME p, stop, NONE) + | _ => (NONE, NONE, stop, extra) + in + Decl (DefinitionDecl { + head = (yypos, yytext), quote = q, + termination = termination, end_tok = end_tok, stop = stop}, extra) + end); +^{Quote_pfx} => ( + YYBEGIN quote; + parseQuoteEndDef yyarg continue yypos yytext QuoteDecl before YYBEGIN INITIAL +); +^{Quote_eqnpfx} => ( + YYBEGIN quote; + parseQuoteEndDef yyarg continue yypos yytext QuoteEqnDecl before YYBEGIN INITIAL +); +{Theorempfx}({ws}|{newline})+"=" => ( + newlines yytext linecount yypos; + Decl (BeginSimpleThm (yypos, yytext), NONE) +); +^{Inductivepfx} => ( + YYBEGIN quote; + parseQuoteEndDef yyarg continue yypos yytext InductiveDecl before YYBEGIN INITIAL +); +{fullquotebegin} {ws}* ":" ({letter} | {ws} | [('] | {digit} | {lowergreek}) => ( + YYBEGIN quote; + yybufpos := !yybufpos - 1; (* unread last character *) + parseFullQuote yyarg continue yypos yytext (SOME (yyend - 2)) before YYBEGIN INITIAL +); +{fullquotebegin} {ws}* ":" {newline} => (let + val _ = YYBEGIN quote + val nllen = if String.sub(yytext, size yytext-2) = #":" then 1 else 2 + val _ = yybufpos := !yybufpos - nllen; (* unread newline *) + in parseFullQuote yyarg continue yypos yytext (SOME (yyend - nllen - 1)) before YYBEGIN INITIAL end); +{fullquotebegin} {ws}* ":^" => ( + YYBEGIN quote; + yybufpos := !yybufpos - 1; (* unread last character *) + parseFullQuote yyarg continue yypos yytext (SOME (yyend - 2)) before YYBEGIN INITIAL +); +{fullquotebegin} => ( + YYBEGIN quote; + parseFullQuote yyarg continue yypos yytext NONE before YYBEGIN INITIAL +); +{quotebegin} => ( + YYBEGIN quote; + parseQuote yyarg continue yypos yytext before YYBEGIN INITIAL +); +"\"" => ( + YYBEGIN string; + case continue() of + StringEnd p => (YYBEGIN INITIAL; Decl (String (yypos, p), NONE)) + | tk as EOF p => ( + parseError (yypos, yyend) "unterminated string"; + YYBEGIN INITIAL; Decl (String (yypos, p), SOME tk)) + | _ => raise Unreachable); +{declforms} => (if !pardepth = 0 then Decl (Chunk yypos, NONE) else continue()); +{MLid} => (continue()); +{newline}"End" => (newline linecount (yyend-3); EndTok (yyend-3)); + +"\\\\" => (continue()); +"\\\"" => (continue()); +"\\"{newline} => (newline linecount yyend; YYBEGIN stringlbrk; continue()); +"\\"{ws} => (YYBEGIN stringlbrk; continue()); +"\"" => (StringEnd yyend); +[^\\""\n\015]{1,10} => (continue()); + +"\\" => (YYBEGIN string; continue()); + +"(*" => (inc comdepth; continue()); +"*)" => (dec comdepth; if !comdepth < 1 then Comment else continue()); +[^\n()*]{1,10} => (continue()); + +{ProofLine} => (ProofLine (yypos, yytext)); +{HOLSTRLITstart} => (let + fun go () = + case continue() of + HolStrLitEnd (endpos, endq) => + if strlitMatch yytext endq then + (YYBEGIN quote; continue()) + else + (parseError (endpos, endpos + size endq) "unexpected end quote"; go ()) + | EOF p => (parseError (yypos, yyend) "unterminated string"; EOF p) + | _ => raise Unreachable + in YYBEGIN holstrlit; go () end); + +"^"({symbol}|"^"*{ws}|[`^]) => (continue()); +"^"+{newline}"End" => (newline linecount (yyend-3); EndTok (yyend-3)); +"^"+{newline} => (newline linecount yyend; 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); +"(*" => ( + 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" => (newline linecount (yyend-3); EndTok (yyend-3)); +{newline}"Termination" => (newline linecount (yyend-11); TerminationTok (yyend-11)); +{fullquoteend} => (FullQuoteEnd (yypos, yytext)); +"^" => ( + YYBEGIN ANTIQ; + case continue() of + Antiq (aq, extra) => (YYBEGIN quote; QDecl (QuoteAntiq (yypos, aq), extra)) + | EOF p => (parseError (p, p) "unexpected EOF"; EOF p) + | _ => raise Unreachable +); +{ws}+ => (continue()); + +"\\"{HOLSTRLITend} => (continue()); +{HOLSTRLITend} => (HolStrLitEnd (yypos, yytext)); +"\\\\" => (continue()); +"\\"{newline} => (newline linecount yyend; YYBEGIN holstrlitlbrk; continue()); +"\\"{ws} => (YYBEGIN holstrlitlbrk; continue()); +"\\" . => (continue()); + +"\\" => (YYBEGIN holstrlit; continue()); + +{MLid} => (Antiq (Ident (yypos, yytext), NONE)); +"(" => (let + val _ = YYBEGIN INITIAL + 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()); +. => ( + parseError (yypos, yyend) "expected identifier or parenthesized group"; + yybufpos := !yybufpos - 1; (* unread last character *) + Antiq (BadAntiq yypos, NONE) +); + +{newline} => (newline linecount yyend; continue()); +. => (continue()); diff --git a/tools/Holmake/HolParser.sig b/tools/Holmake/HolParser.sig new file mode 100644 index 0000000000..b776ec3e9a --- /dev/null +++ b/tools/Holmake/HolParser.sig @@ -0,0 +1,84 @@ +signature HolParser = +sig + +structure Simple: sig + + datatype decl = datatype HolLex.UserDeclarations.decl + datatype decls = datatype HolLex.UserDeclarations.decls + datatype antiq = datatype HolLex.UserDeclarations.antiq + datatype qdecl = datatype HolLex.UserDeclarations.qdecl + datatype qbody = datatype HolLex.UserDeclarations.qbody + + datatype topdecl + = TopDecl of decl + | EOF of int + + datatype type_kind = + OverloadKind of {by_nametype: bool, inferior: bool} + | TypeKind of {pp: bool} + + val destAttrs: substring -> (substring * substring list) list + val destMLThmBinding: substring -> + {attrs: substring, keyword: substring, name: substring, name_attrs: substring} + val destNameAttrs: substring -> substring * substring + val fromSS: int * substring -> int * int + val killEnvelopingSpace: substring -> substring + val kindToName: bool -> type_kind -> string + val parseBeginType: int * string -> (int * int -> string -> unit) -> + {attrs: unit, keyword: substring, kind: type_kind, local_: bool, tyname: substring} + val parseDefinitionPfx: string -> + {attrs: substring, keyword: substring, name: substring, name_attrs: substring} + val parseDefnLabel: string -> + {attrs: substring, name: (substring * bool) option, name_attrs: substring} + val parseInductivePfx: string -> {isCo: bool, keyword: substring, thmname: substring} + val parseQuoteEqnPfx: string -> {bind: substring, keyword: substring, name: substring} + val parseQuotePfx: string -> {keyword: substring, name: substring} + val parseTheoremPfx: string -> + {attrs: substring, isTriv: bool, keyword: substring, name_attrs: substring, thmname: substring} + + val mkParser: + {parseError: int * int -> string -> unit, pos: int, read: int -> string} -> + unit -> topdecl + +end + +structure ToSML: sig + + type double_reader = + {read: int -> string, readAt: int -> int -> (int * substring -> unit) -> unit} + val mkDoubleReader: (int -> string) -> int -> double_reader + + val mkPullTranslator: + {parseError: int * int -> string -> unit, read: int -> string} -> + unit -> string + + type strcode = { + aux: string -> unit, + regular: int * substring -> unit, + strcode: int * substring -> unit, + strstr: int * substring -> unit + } + val mkStrcode: (string -> unit) -> strcode + val mkPushTranslator: + {parseError: int * int -> string -> unit, read: int -> string} -> + strcode -> unit -> bool + +end + +type reader = {read : unit -> char option, eof : unit -> bool} + +val inputFile : string -> string +val fromString : bool -> string -> string + +val fileToReader : string -> reader +val stringToReader : bool -> string -> reader +val inputToReader : bool -> (int -> string) -> reader +val streamToReader : bool -> TextIO.instream -> reader +(* bool is true if the stream corresponds to an interactive session + (stdin) or a Script file. In both such situations, the magic >- and + Theorem-syntax transformations should be performed *) + +(* In inputFile and fileToReader, the determination is made on whether or + not the filename ends in "Script.sml" *) + +end diff --git a/tools/Holmake/HolParser.sml b/tools/Holmake/HolParser.sml new file mode 100644 index 0000000000..929c71b4b4 --- /dev/null +++ b/tools/Holmake/HolParser.sml @@ -0,0 +1,588 @@ +structure HolParser = +struct + +infix |> +fun x |> f = f x +fun mlquote s = String.concat ["\"", String.toString s, "\""] +fun K a _ = a +fun I a = a + +structure Simple = struct + +local + structure H = HolLex.UserDeclarations +in + datatype decl = datatype H.decl + datatype decls = datatype H.decls + datatype antiq = datatype H.antiq + datatype qdecl = datatype H.qdecl + datatype qbody = datatype H.qbody + + datatype topdecl + = TopDecl of decl + | EOF of int + + 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}) + val lookahead = ref NONE + fun go () = + case (case !lookahead of SOME tk => tk | NONE => lex ()) of + H.Decl (td, look) => (lookahead := look; TopDecl td) + | H.CloseParen p => (parseError (p, p + 1) ("unexpected ')'"); go ()) + | H.EndTok _ => go () + | H.QED _ => go () + | H.EOF p => EOF p + | _ => raise H.Unreachable + in go end +end + +fun killEnvelopingSpace s = + s |> Substring.dropl Char.isSpace + |> Substring.dropr Char.isSpace + +fun destNameAttrs ss = + if Substring.sub(ss, 0) = #"\"" then let + val ss' = Substring.slice(ss, 1, NONE) + val (nm, rest) = Substring.position "\"" ss' + in (nm, Substring.slice(rest, 1, NONE)) end + else + Substring.position "[" ss + +fun stringOfKey k = + case k of + "exclude_simps" => "simpLib.remove_simps" + | "exclude_frags" => "simpLib.remove_ssfrags" + | _ => k + +fun destAttrs attrs = + if Substring.isEmpty attrs then [] + else + Substring.slice(attrs, 1, SOME (Substring.size attrs - 2)) + |> Substring.fields (fn c => c = #",") + |> map (fn attr => + case Substring.fields (fn c => c = #"=") (killEnvelopingSpace attr) of + [] => raise Fail "String.fields can't return an empty list" + | [key] => (killEnvelopingSpace key, []) + | key::vals::_ => (killEnvelopingSpace key, Substring.tokens Char.isSpace vals)) + +fun destMLThmBinding s = + let + (* s matches {keyword}{ws}+{ident}[attrs] + ident is either a standard ML identifier, or something in double quotes + NB: If it's in double quotes, the thing in quotes might include square + brackets! + + returns the ident, the original string corresponding to the string + + attributes, and the attributes as a separate list of strings + *) + val (kwordss, restss) = + s |> Substring.splitl Char.isAlpha + val ss = restss |> Substring.dropl Char.isSpace + val (nms, attrs) = destNameAttrs ss + in + {keyword = kwordss, name_attrs = ss, name = nms, attrs = attrs} + end + +fun fromSS (base, ss) = let + val (_, lo, len) = Substring.base ss + in (base + lo, base + lo + len) end + +datatype type_kind + = OverloadKind of {inferior: bool, by_nametype: bool} + | TypeKind of {pp: bool} + +fun kindToName local_ kind = + (if local_ then "temp_" else "") ^ + (case kind of + OverloadKind {inferior, by_nametype} => + (if inferior then "inferior_" else "") ^ + "overload_on" ^ + (if by_nametype then "_by_nametype" else "") + | TypeKind {pp} => "type_abbrev" ^ (if pp then "_pp" else "")) + +(* ("Type"|"Overload"){ws}+({alphaMLid}|{quotedsymbolid})("["{alphaMLid_list}"]")?{ws}*"=" *) +fun parseBeginType (start, text) parseError = let + val s = (Substring.substring(text, 0, size text - 1)) (* drop = *) + |> Substring.dropr Char.isSpace (* drop wspace after name *) + val {keyword, name, attrs, ...} = destMLThmBinding s + val isOverload = Substring.size keyword = 8 + fun expectNoArgs [] = () + | expectNoArgs (v :: _) = parseError (fromSS (start, v)) "expected no arguments" + val inferior = ref false + val local_ = ref false + val pp = ref false + val by_nametype = ref false + fun parseAttr (k, vs) = + case (Substring.string k, isOverload) of + ("inferior", true) => (expectNoArgs vs; inferior := true) + | ("local", _) => (expectNoArgs vs; local_ := true) + | ("pp", false) => (expectNoArgs vs; pp := true) + | ("by_nametype", true) => (expectNoArgs vs; by_nametype := true) + | (sk, _) => parseError (fromSS (start, k)) ("unexpected attribute '"^sk^"'") + val kind = + if isOverload then OverloadKind {inferior = !inferior, by_nametype = !by_nametype} + else TypeKind {pp = !pp} + val _ = app parseAttr (destAttrs attrs) + in {local_ = !local_, kind = kind, keyword = keyword, tyname = name} end + +(* {Theorempfx}{ws}*":" or {Theorempfx}({ws}|{newline})+"=" +where Theorempfx = ("Theorem"|"Triviality"){ws}+{alphaMLid}({ws}*"["{alphaMLid_list}"]")?; *) +fun parseTheoremPfx text = let + val s = Substring.substring(text, 0, size text - 1) (* drop : or = *) + |> Substring.dropr Char.isSpace (* drop wspace between name and ] *) + val {keyword, name, attrs, name_attrs} = destMLThmBinding s + val isTriv = Substring.size keyword = 10 + in {isTriv = isTriv, keyword = keyword, + thmname = name, attrs = attrs, name_attrs = name_attrs} end + +(* Inductivepfx = ("Co")?"Inductive"{ws}+{alphaMLid}{ws}*":"; *) +fun parseInductivePfx text = let + val (keyword, s) = Substring.substring(text, 0, size text - 1) (* drop : *) + |> Substring.splitl (not o Char.isSpace) (* split keyword *) + val name = s + |> Substring.dropl Char.isSpace (* space before name *) + |> Substring.dropr Char.isSpace (* space after name *) + in {isCo = Substring.size keyword = 11, keyword = keyword, thmname = name} end + +(* Definitionpfx = +"Definition"{ws}+{alphaMLid}({ws}*"["{optallws}{defn_attribute_list}"]")?{ws}*":"; *) +fun parseDefinitionPfx text = let + val s = Substring.substring(text, 0, size text - 1) (* drop : *) + |> Substring.dropr Char.isSpace (* drop wspace after name *) + in destMLThmBinding s end + +(* Quote_pfx = "Quote"{ws}+{QUALalphaMLid}{ws}*":"; *) +fun parseQuotePfx text = let + val name = Substring.substring(text, 6, size text - 1) (* drop :, "Quote" + next ws char *) + |> Substring.dropl Char.isSpace (* space before name *) + |> Substring.dropr Char.isSpace (* space after name *) + in {keyword = Substring.substring(text, 0, 5), name = name} end + +(* Quote_eqnpfx = "Quote"{ws}+{alphaMLid}{ws}*"="{ws}*{QUALalphaMLid}{ws}*":"; *) +fun parseQuoteEqnPfx text = let + val (left, right) = Substring.substring(text, 6, size text - 1) (* drop :, Quote, next ws char *) + |> Substring.dropl Char.isSpace (* space before name *) + |> Substring.dropr Char.isSpace (* space after name *) + |> Substring.position "=" + val bind = left |> Substring.dropr Char.isSpace + val name = Substring.slice(right, 1, NONE) |> Substring.dropl Char.isSpace + in {keyword = Substring.substring(text, 0, 5), bind = bind, name = name} end + +(* DefinitionLabel = "["{ws}*{DefinitionLabelID}?("["{alphaMLid_list}"]")?{ws}*":"?{ws}*"]"; *) +fun parseDefnLabel text = let + val ss = Substring.full text + |> Substring.dropr Char.isSpace + |> (fn s => Substring.slice (s, 1, SOME (Substring.size s - 2))) + |> Substring.dropl Char.isSpace + |> Substring.dropr (fn c => Char.isSpace c orelse c = #":") + val (ss, tilde) = + case Substring.getc ss of + SOME (#"~", ss) => (ss, true) + | _ => (ss, false) + val (name, attrs) = destNameAttrs ss + val str = Substring.string name + val name = + if str = "/\092" orelse str = "\226\136\167" orelse str = "" then NONE + else SOME name + in {tilde = tilde, name = name, attrs = attrs, name_attrs = ss} end + +end + +structure ToSML = struct + + type double_reader = { + read: int -> string, + readAt: int -> int -> (int * substring -> unit) -> unit + } + + (* + This function takes an input stream `read: int -> string` and returns another stream with the + same type, along with a function `readAt (from: int) (to: int) (push: int * substring -> unit)` + which is another stream, yielding values that have already been yielded from the first stream. + Internally it maintains a buffer of results that `read` has yielded, indexed by byte positions + (starting at `pos`). + + `readAt from to push` is a request to skip forward to position `from`, then yield the bytes + `from .. to` to the callback `push`. This function can only be called once for these positions; + the next call to `readAt` must have a `from` larger than the previous `to` value and `to` must + be no larger than the total of all bytes provided by the main stream `read`. + + `push (bufstart, chunk)` is called repeatedly to output each chunk of the response, where + `bufstart + chunk.start` is the position of the start of `chunk` in the stream. + *) + fun mkDoubleReader read pos: double_reader = let + val inbox = ref (pos, []) + val outbox = ref (pos, []) + val pos = ref pos + fun read' n = let + val buf = read n + val _ = if buf = "" then () else let + val (ahead, backlog) = !inbox + in inbox := (ahead + size buf, buf :: backlog) end + in buf end + fun readAt from to push = let + fun checkInbox from = if from = to then () else let + fun moveToOutbox [] mid acc = raise Fail "unreachable" + | moveToOutbox (chunk :: rest) mid acc = let + val mid' = mid - size chunk + in + if mid' <= from then printOutbox mid' chunk mid acc from + else moveToOutbox rest mid' (chunk :: acc) + end + val (lead, bufs) = !inbox + val _ = if to <= lead then () else raise Fail "main reader has not yielded this much yet" + in inbox := (lead, []); moveToOutbox bufs lead [] end + and printOutbox trail chunk trail' rest from = + if to <= trail' then ( + push (trail, Substring.substring (chunk, from - trail, to - from)); + outbox := (trail, chunk :: rest) + ) else ( + push (trail, Substring.substring (chunk, from - trail, trail' - from)); + case rest of + [] => checkInbox trail' + | chunk' :: rest' => printOutbox trail' chunk' (trail' + size chunk') rest' trail' + ) + fun dropOutbox [] _ = checkInbox from + | dropOutbox (chunk :: rest) trail = let + val trail' = trail + size chunk + in + if trail' <= from then dropOutbox rest trail' + else printOutbox trail chunk trail' rest from + end + val _ = if from <= to then () else raise Fail "readAt: to < from" + val (back, bufs) = !outbox + val _ = if back <= from then () else raise Fail "segment has already been yielded" + in dropOutbox bufs back end + in {read = read', readAt = readAt} end + + type strcode = { + aux: string -> unit, + regular: int * substring -> unit, + strcode: int * substring -> unit, + strstr: int * substring -> unit + } + + fun mkStrcode push: strcode = let + fun encoder st f (_, s) = let + val (s, start, len) = Substring.base s + val stop = start + len + fun loop start p = + if p = stop then + if start = p then () else push (String.substring (s, start, p - start)) + else + case f (String.sub (s, p)) of + NONE => loop start (p+1) + | SOME r => ( + if start = p then () else push (String.substring (s, start, p - start)); + push r; + loop (p+1) (p+1)) + in loop start start end + in { + regular = fn s => push (Substring.string (#2 s)), + aux = push, + strstr = encoder "str" (fn ch => + if ch < #"\128" then NONE else SOME (AttributeSyntax.bslash_escape ch)), + strcode = encoder "code" (fn + #"\\" => SOME "\\\\" + | #"\"" => SOME "\\\"" + | #"\n" => SOME "\\n\\\n\\" + | ch => if Char.isPrint ch then NONE else SOME (AttributeSyntax.bslash_escape ch)) + } end + + fun mkPushTranslator {read, parseError} ({regular, aux, strstr, strcode = strcode0}:strcode) = let + open Simple + val ss = Substring.string + val full = Substring.full + val cat = Substring.concat + val {read, readAt} = mkDoubleReader read 0 + val feed = mkParser {read = read, pos = ~1 (* fix for mllex bug *), parseError = parseError} + val lookahead = ref NONE + fun feed' () = case !lookahead of SOME tk => tk | NONE => feed () + val inThmVal = ref false + fun finishThmVal () = if !inThmVal then (aux ");"; inThmVal := false) else () + val line = ref (0, 0) + fun countlines (p, s) = let + val lastline = Substring.dropr (fn c => c <> #"\n") s + in + if Substring.isEmpty lastline then () + else line := ( + Substring.foldr (fn (c, n) => if c = #"\n" then n+1 else n) (#1 (!line)) lastline, + let val (_, start, len) = Substring.base lastline in p + start + len end) + end + fun wrap f (start, stop) = if start = stop then () else + readAt start stop (fn s => (countlines s; f s)) + val regular = wrap regular + val strcode = wrap strcode0 + val strstr = wrap strstr + val regular' = regular o fromSS + val strcode' = strcode o fromSS + val strstr' = strstr o fromSS + fun locpragma pos = let + val (line, start) = !line + in + aux (concat [ + " (*#loc ", Int.toString (line + 1), " ", Int.toString (pos - start + 1), "*)"]) + (* NB: the initial space is critical, or else the comment might not be recognised + when prepended by a paren or symbol char. --KW + See cvs log comment at rev 1.2 of src/parse/base_tokens.lex *) + end + fun quote (start, stop) = (locpragma start; strcode (start, stop)) + fun magicBind name = + aux (" " ^ Systeml.bindstr (concat ["val ", name, " = DB.fetch \"-\" \"", name, + "\" handle Feedback.HOL_ERR _ => boolTheory.TRUTH;"]) ^ ";") + fun doThmAttrs false p attrs name_attrs = strcode' (p, name_attrs) + | doThmAttrs true p attrs name_attrs = + if Substring.isEmpty attrs then + (strcode' (p, name_attrs); aux "[local]") + else ( + strcode' (p, Substring.slice (name_attrs, 0, SOME (Substring.size name_attrs - 1))); + aux ",local]") + fun doQuoteCore start ds stop f = case ds of + [] => quote (start, stop) + | QuoteAntiq (_, BadAntiq _) :: rest => doQuoteCore start rest stop f + | QuoteAntiq (p, Ident (idstart, id)) :: rest => ( + quote (start, p); + aux "\", ANTIQUOTE "; regular (idstart, idstart + size id); aux ", QUOTE \""; + doQuoteCore (idstart + size id) rest stop f) + | QuoteAntiq (p, Paren {start_tok, decls, end_tok, stop = pstop}) :: rest => let + val Decls {start = dstart, decls, stop = dstop} = decls + in + quote (start, p); aux "\", ANTIQUOTE "; + case end_tok of + NONE => (doDecls start_tok decls dstop; aux ")") + | SOME _ => doDecls start_tok decls pstop; + aux ", QUOTE \""; + doQuoteCore pstop rest stop f + end + | DefinitionLabel (l as (p, t)) :: rest => + case f of + NONE => doQuoteCore start rest stop f + | 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 doDecl eager pos d = case d of + DefinitionDecl {head = (p, head), quote, termination, stop, ...} => let + val {keyword, name, attrs, name_attrs} = parseDefinitionPfx head + val attrs = destAttrs attrs + val indThm = + case List.find (fn (k,v) => Substring.compare (k, full "induction") = EQUAL) attrs of + SOME (_, s::_) => ss s + | _ => + if Substring.isSuffix "_def" name then + cat [Substring.slice (name, 0, SOME (Substring.size name - 4)), full "_ind"] + else if Substring.isSuffix "_DEF" name then + cat [Substring.slice (name, 0, SOME (Substring.size name - 4)), full "_IND"] + else cat [name, full "_ind"] + in + regular (pos, p); finishThmVal (); + aux "val "; aux (ss name); aux " = TotalDefn.qDefine \""; + strcode' (p, name_attrs); aux "\" "; doQuote quote; + case termination of + NONE => aux " NONE;" + | SOME {decls = Decls {start = dstart, decls = decls, stop = dstop}, ...} => + (aux " (SOME ("; doDecls dstart decls dstop; aux "));"); + magicBind indThm; + stop + end + | DatatypeDecl {head = (p, head), quote, stop, ...} => ( + regular (pos, p); finishThmVal (); + aux "val _ = bossLib.Datatype "; doQuote quote; aux ";"; + stop) + | QuoteDecl {head = (p, head), quote, stop, ...} => let + val {keyword, name} = parseQuotePfx head + in + regular (pos, p); finishThmVal (); + aux "val _ = "; regular' (p, name); aux " "; doQuote quote; aux ";"; + stop + end + | QuoteEqnDecl {head = (p, head), quote, stop, ...} => let + val {keyword, name, bind} = parseQuoteEqnPfx head + in + regular (pos, p); finishThmVal (); + aux "val "; regular' (p, bind); aux " = "; + regular' (p, name); aux " "; doQuote quote; aux ";"; + stop + end + | InductiveDecl {head = (p, head), quote, stop, ...} => let + val {isCo, keyword, thmname = stem} = parseInductivePfx head + val (entryPoint, indSuffix) = + if isCo then ("CoIndDefLib.xHol_coreln", "_coind") else ("IndDefLib.xHol_reln", "_ind") + val conjIdx = ref 1 + val conjs = ref [] + fun collect first (p, lab) = let + val n = !conjIdx + val _ = if first then () else aux ") /\\\\ (" + val _ = case parseDefnLabel lab of + {tilde, name = SOME name, name_attrs, ...} => + conjs := (n, tilde, name, name_attrs) :: !conjs + | _ => () + in conjIdx := n+1 end + in + regular (pos, p); finishThmVal (); + app aux ["val (", ss stem, "_rules,", ss stem, indSuffix, ",", + ss stem, "_cases) = ", entryPoint, " \"", ss stem, "\" "]; + doQuoteConj quote collect; aux ";"; + magicBind (cat [stem, full "_strongind"]); + app (fn (i, tilde, name, name_attrs) => let + val f = if tilde then fn s => app aux [ss stem, "_", s] else aux + in + aux " val "; f (ss name); aux " = boolLib.save_thm(\""; f (ss name_attrs); + app aux ["\", Drule.cj ", Int.toString i, " ", + ss stem, "_rules handle HOL_ERR _ => boolTheory.TRUTH);"] + end) (rev (!conjs)); + stop + end + | BeginType (p, head) => let + val {local_, kind, keyword, tyname} = parseBeginType (p, head) parseError + val fnm = kindToName local_ kind + in + regular (pos, p); finishThmVal (); + app aux ["val _ = Parse.", fnm, "(\""]; strstr' (p, tyname); aux "\","; + inThmVal := true; p + size head + end + | BeginSimpleThm (p, head) => let + val {isTriv, keyword, thmname, attrs, name_attrs} = parseTheoremPfx head + in + regular (pos, p); finishThmVal (); + app aux ["val ", ss thmname, " = boolLib.save_thm(\""]; + doThmAttrs isTriv p attrs name_attrs; aux "\","; inThmVal := true; + p + size head + end + | TheoremDecl {head = (p, head), quote, proof_tok, body, stop, ...} => let + val {isTriv, keyword, thmname, attrs, name_attrs} = parseTheoremPfx head + val goalabs = "(fn HOL__GOAL__foo => ("; + val Decls {start = dstart, decls, stop = dstop} = body + in + regular (pos, p); finishThmVal (); + app aux ["val ", ss thmname, " = Q.store_thm(\""]; + doThmAttrs isTriv p attrs name_attrs; aux "\", "; + doQuote quote; aux ", "; + case proof_tok of + SOME (p, tok) => let + fun ofKey "exclude_simps" = "simpLib.remove_simps" + | ofKey "exclude_frags" = "simpLib.remove_ssfrags" + | ofKey k = k + fun mktm1 (k,vals) = ofKey (ss k) ^ " [" ^ + String.concatWith "," (map (mlquote o ss) vals) ^ "]" + fun mktm kv [] = mktm1 kv + | mktm kv (kv2::xs) = mktm1 kv ^ " o " ^ mktm kv2 xs + val () = case destAttrs (#2 (destNameAttrs (full tok))) of + [] => () + | kv::attrs => aux ("BasicProvers.with_simpset_updates (" ^ mktm kv attrs ^ ") ") + val n = #1 (!line) + val _ = readAt p (p + size tok) countlines + in aux goalabs; aux (CharVector.tabulate (#1 (!line) - n, (fn _ => #"\n"))) end + | _ => aux goalabs; + doDecls dstart decls dstop; aux ") HOL__GOAL__foo));"; + stop + end + | Chunk p => + if !inThmVal then + (regular (pos, p); aux ");"; inThmVal := false; p) + else if eager then + (regular (pos, p); p) + else + pos + | FullQuote {head = (p, head), type_q, quote, stop, ...} => ( + regular (pos, p); + aux (case type_q of NONE => "(Parse.Term " | SOME _ => "(Parse.Type "); + doQuote quote; aux ")"; + stop) + | Quote {head = (p, _), quote, stop, ...} => (regular (pos, p); doQuote quote; stop) + | String (start, stop) => (regular (pos, start); strstr (start, stop); stop) + and doDecls start [] stop = regular (start, stop) + | doDecls start (d :: ds) stop = doDecls (doDecl false start d) ds stop + val pos = ref 0 + in fn () => + case feed' () of + TopDecl d => (pos := doDecl true (!pos) d; false) + | Simple.EOF p => (regular (!pos, p); finishThmVal (); pos := p; true) + end + +fun mkPullTranslator args = let + val queue = ref [] + val atEnd = ref false + val push = mkPushTranslator args (mkStrcode (fn s => queue := s :: !queue)) + fun loop () = + case !queue of + s :: rest => (queue := rest; s) + | [] => if !atEnd then "" else ( + atEnd := push (); + queue := rev (!queue); + loop ()) + in loop end + +end + +open HOLFileSys +type reader = {read : unit -> char option, eof : unit -> bool} + +fun exhaust_parser (read, close) = + let + fun recurse acc = + case read () of + "" => (close(); String.concat (List.rev acc)) + | s => recurse (s::acc) + in + recurse [] + end + +fun mkstate b = {inscriptp = b, quotefixp = false} + +fun file_to_parser fname = let + val instrm = openIn fname + (* val isscript = String.isSuffix "Script.sml" fname *) + val read = ToSML.mkPullTranslator {read = fn n => input instrm, parseError = K (K ())} + in (read, fn () => closeIn instrm) end + +fun string_to_parser isscriptp s = let + val sr = ref s + fun str_read _ = (!sr before sr := "") + val read = ToSML.mkPullTranslator {read = str_read, parseError = K (K ())} + in (read, I) end + +fun input_to_parser isscriptp inp = let + val read = ToSML.mkPullTranslator {read = inp, parseError = K (K ())} + in (read, I) end + +fun stream_to_parser isscriptp strm = + input_to_parser isscriptp (fn n => input strm) + +fun inputFile fname = exhaust_parser (file_to_parser fname) +fun fromString b s = exhaust_parser (string_to_parser b s) + +fun mkReaderEOF (read, close) = let + val i = ref 0 + val s = ref "" + val sz = ref 0 + val eofp = ref false + fun pull () = (s := read(); sz := size (!s); i := 0; + if !sz = 0 then (eofp := true; close()) else ()) + fun doit () = + if !eofp then NONE + else if !i < !sz then SOME (String.sub(!s,!i)) before i := !i + 1 + else (pull(); doit()) + fun eof () = !eofp + in {read = doit, eof = eof} end + +fun fileToReader fname = mkReaderEOF (file_to_parser fname) +fun stringToReader b s = mkReaderEOF (string_to_parser b s) +fun inputToReader b inp = mkReaderEOF (input_to_parser b inp) +fun streamToReader b strm = mkReaderEOF (stream_to_parser b strm) + +end diff --git a/tools/Holmake/Holdep.sml b/tools/Holmake/Holdep.sml index 41251375e6..6d8c8a86ec 100644 --- a/tools/Holmake/Holdep.sml +++ b/tools/Holmake/Holdep.sml @@ -124,7 +124,7 @@ fun encode_for_HOLMKfile {tgt, deps} = fun uqfname_holdep fname = let - val reader = QFRead.fileToReader fname + val reader = HolParser.fileToReader fname in Holdep_tokens.reader_deps (fname, #read reader) end diff --git a/tools/Holmake/hmcore.ML b/tools/Holmake/hmcore.ML index 3e1c83ce86..74f33c55dd 100644 --- a/tools/Holmake/hmcore.ML +++ b/tools/Holmake/hmcore.ML @@ -21,10 +21,10 @@ in myuse (OS.Path.concat(hmakedir, "poly")) "HFS_NameMunge.sml"; app appthis ["HOLFileSys", "regexpMatch", "parse_glob", "Holdep_tokens", "AttributeSyntax"] ; - app (myuse hmakedir) ["QuoteFilter.sml", "Holmake_tools_dtype.sml", + app (myuse hmakedir) ["HolLex.sml", "Holmake_tools_dtype.sml", "terminal_primitives.sig", "poly-terminal-prims.ML"]; - app appthis ["QFRead", "Holdep", "Holmake_tools", "internal_functions", + app appthis ["HolParser", "Holdep", "Holmake_tools", "internal_functions", "Holmake_types", "ReadHMF"] end; diff --git a/tools/Holmake/hmcore.mlb b/tools/Holmake/hmcore.mlb index fc0b5c8a1e..3103264113 100644 --- a/tools/Holmake/hmcore.mlb +++ b/tools/Holmake/hmcore.mlb @@ -15,9 +15,9 @@ Holdep_tokens.sig Holdep_tokens.sml AttributeSyntax.sig AttributeSyntax.sml -QuoteFilter.sml -QFRead.sig -QFRead.sml +HolLex.sml +HolParser.sig +HolParser.sml Holdep.sig Holdep.sml regexpMatch.sig diff --git a/tools/Holmake/holdeptool.sml b/tools/Holmake/holdeptool.sml index 9939e2505a..0ddbf6c6b8 100644 --- a/tools/Holmake/holdeptool.sml +++ b/tools/Holmake/holdeptool.sml @@ -23,7 +23,7 @@ fun main() = let handle LEX_ERROR s => diewith("Lexical error: " ^ s) | e => diewith ("Exception: "^General.exnMessage e)) | ["-h"] => usage ok - | [fname] => (reader_deps (fname, #read (QFRead.fileToReader fname)) + | [fname] => (reader_deps (fname, #read (HolParser.fileToReader fname)) handle LEX_ERROR s => diewith("Lexical error: " ^ s) | e => diewith ("Exception: "^General.exnMessage e)) | _ => usage die diff --git a/tools/Holmake/poly-holdeptool.ML b/tools/Holmake/poly-holdeptool.ML index a3f1cf3472..17c870e044 100644 --- a/tools/Holmake/poly-holdeptool.ML +++ b/tools/Holmake/poly-holdeptool.ML @@ -16,9 +16,9 @@ use "Systeml.sig"; use "../../tools-poly/Holmake/Systeml.sml"; use "AttributeSyntax.sig"; use "AttributeSyntax.sml"; -use "QuoteFilter.sml"; -use "QFRead.sig"; -use "QFRead.sml"; +use "HolLex.sml"; +use "HolParser.sig"; +use "HolParser.sml"; use "holdeptool.sml"; val main = holdeptool.main diff --git a/tools/configure.sml b/tools/configure.sml index b64977a386..4ec5f84cd2 100644 --- a/tools/configure.sml +++ b/tools/configure.sml @@ -304,6 +304,8 @@ val _ = systeml (pfx @ extras @ [srcobj]) end in + print "Calling mllex on HolLex\n"; + systeml [mllex, "HolLex"]; print "Calling mllex on QuoteFilter\n"; systeml [mllex, "QuoteFilter"]; compile [] "holpathdb.sig"; @@ -323,12 +325,12 @@ val _ = compile [] "Holdep_tokens.sml"; compile [] "AttributeSyntax.sig"; compile [] "AttributeSyntax.sml"; - compile [] "QuoteFilter.sml"; + compile [] "HolLex.sml"; compile [] "terminal_primitives.sig"; compile [] "terminal_primitives.sml"; compile [] "Holmake_tools_dtype.sml"; - compile [] "QFRead.sig"; - compile [] "QFRead.sml"; + compile [] "HolParser.sig"; + compile [] "HolParser.sml"; compile ["-I", "mosml"] "Holdep.sig"; compile ["-I", "mosml"] "Holdep.sml"; compile [] "Holmake_tools.sig"; diff --git a/tools/mllex/mllex.sml b/tools/mllex/mllex.sml index b9bad1b24a..fcdea9610a 100644 --- a/tools/mllex/mllex.sml +++ b/tools/mllex/mllex.sml @@ -253,6 +253,7 @@ structure LexGen: LEXGEN = | REPS of int * int | ID of string | ACTION of string | BOF | EOF | ASSIGN | SEMI | ARROW | LEXMARK | LEXSTATES | COUNT | REJECT | FULLCHARSET | STRUCT | HEADER | ARG | POSARG + | EOFPOS datatype exp = EPS | CLASS of bool array * int | CLOSURE of exp | ALT of exp * exp | CAT of exp * exp | TRAIL of int @@ -271,6 +272,7 @@ structure LexGen: LEXGEN = val CountNewLines = ref false; val PosArg = ref false; + val EofPos = ref false; val HaveReject = ref false; (* Can increase size of character set *) @@ -287,6 +289,7 @@ structure LexGen: LEXGEN = val ResetFlags = fn () => (CountNewLines := false; HaveReject := false; PosArg := false; + EofPos := false; UsesTrailingContext := false; CharSetSize := 129; StrName := "Mlex"; HeaderCode := ""; HeaderDecl:= false; @@ -516,6 +519,7 @@ fun AdvanceTok () : unit = let | "header" => HEADER | "arg" => ARG | "posarg" => POSARG + | "eofpos" => EOFPOS | _ => prErr "unknown % operator " end ) @@ -849,6 +853,7 @@ fun parse() : (string * (int list * exp) list * ((string,string) dictionary * st HeaderDecl := true; ParseDefs()) | _ => raise SyntaxError) | POSARG => (PosArg := true; ParseDefs()) + | EOFPOS => (EofPos := true; ParseDefs()) | ARG => (LexState := 2; AdvanceTok(); case GetTok() of ACTION s => @@ -1260,7 +1265,8 @@ fun lexGen infile = sayln "\t\tcase node of"; sayln "\t\t Internal.N yyk =>"; sayln "\t\t\t(let fun yymktext() = String.substring(!yyb,i0,i-i0)\n\ - \\t\t\t val yypos: int = i0+ !yygone"; + \\t\t\t val yypos: int = i0+ !yygone\n\ + \\t\t\t val yyend: int = yypos + (i-i0)"; if !CountNewLines then (sayln "\t\t\tval _ = yylineno := CharVectorSlice.foldli"; sayln "\t\t\t\t(fn (_,#\"\\n\", n) => n+1 | (_,_, n) => n) (!yylineno) (CharVectorSlice.slice(!yyb,i0,SOME(i-i0)))") @@ -1289,7 +1295,8 @@ fun lexGen infile = sayln "\t in if (String.size newchars)=0"; sayln "\t\t then (yydone := true;"; say "\t\t if (l=i0) then UserDeclarations.eof "; - sayln (case !ArgCode of NONE => "()" | SOME _ => "yyarg"); + say (case !ArgCode of NONE => "()" | SOME _ => "yyarg"); + sayln (if !EofPos then " (!yygone+i0)" else ""); say "\t\t else action(l,NewAcceptingLeaves"; if !UsesTrailingContext then sayln ",nil))" else sayln "))"; diff --git a/tools/quote-filter/poly-unquote.ML b/tools/quote-filter/poly-unquote.ML index 031abc6c26..f27d3a886c 100644 --- a/tools/quote-filter/poly-unquote.ML +++ b/tools/quote-filter/poly-unquote.ML @@ -6,7 +6,17 @@ use "../Holmake/Systeml.sig"; use "../../tools-poly/Holmake/Systeml.sml"; use "../Holmake/AttributeSyntax.sig"; use "../Holmake/AttributeSyntax.sml"; -use "../Holmake/QuoteFilter.sml"; +use "../Holmake/HolLex.sml"; +use "../Holmake/HM_SimpleBuffer.sig"; +use "../Holmake/HM_SimpleBuffer.sml"; +use "../Holmake/HOLFS_dtype.sml"; +use "../Holmake/HFS_NameMunge.sig"; +use "../Holmake/poly/HFS_NameMunge.sml"; +use "../Holmake/HOLFS_dtype.sml"; +use "../Holmake/HOLFileSys.sig"; +use "../Holmake/HOLFileSys.sml"; +use "../Holmake/HolParser.sig"; +use "../Holmake/HolParser.sml"; open OS.Process fun read_from_stream is n = TextIO.input is; @@ -19,25 +29,40 @@ fun main() = let linked executable as Interrupt exceptions *) val _ = Signal.signal(2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt())) - val (instream, outstream, intp, qfixp, cb) = - qfilter_util.processArgs(false,false,false) (CommandLine.arguments()) + val (instream, outstream, intp, qfixp, oldp, cb) = + qfilter_util.processArgs(false,false,false,false) (CommandLine.arguments()) (* with many thanks to Ken Friis Larsen, Peter Sestoft, Claudio Russo and Kenn Heinrich who helped me see the light with respect to this code *) - open QuoteFilter.UserDeclarations - val state as QFS args = newstate {inscriptp = intp, quotefixp = qfixp} - - fun loop() = - let - val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instream) state - fun coreloop () = - case lexer() of - "" => () - | s => (TextIO.output(outstream, s); coreloop()) - in - coreloop() handle Interrupt => (resetstate state; loop()) - end + val _ = PolyML.print_depth 100; + val loop = + if oldp orelse qfixp then let + open QuoteFilter.UserDeclarations + val state as QFS args = newstate {inscriptp = intp, quotefixp = qfixp} + + fun loop() = + let + val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instream) state + fun coreloop () = + case lexer() of + "" => () + | s => (TextIO.output(outstream, s); coreloop()) + in + coreloop() handle Interrupt => (resetstate state; loop()) + end + in loop end + else let + open HolParser.ToSML + val read = mkPushTranslator { + read = read_from_stream instream, + parseError = fn (start, stop) => fn s => + TextIO.output (TextIO.stdErr, + "parse error at " ^ Int.toString start ^ "-" ^ Int.toString stop ^ ": " ^ s ^ "\n") + } (mkStrcode (fn s => TextIO.output(outstream, s))) + + fun loop () = if read () then () else loop () + in loop end in loop(); TextIO.closeOut outstream; diff --git a/tools/quote-filter/qfilter_util.sig b/tools/quote-filter/qfilter_util.sig index 9361b5c43e..303bfacd82 100644 --- a/tools/quote-filter/qfilter_util.sig +++ b/tools/quote-filter/qfilter_util.sig @@ -1,8 +1,8 @@ signature qfilter_util = sig - val processArgs : bool * bool * bool -> string list -> - TextIO.instream * TextIO.outstream * bool * bool * + val processArgs : bool * bool * bool * bool -> string list -> + TextIO.instream * TextIO.outstream * bool * bool * bool * (unit -> unit) end diff --git a/tools/quote-filter/qfilter_util.sml b/tools/quote-filter/qfilter_util.sml index 242654e53f..e866ff912a 100644 --- a/tools/quote-filter/qfilter_util.sml +++ b/tools/quote-filter/qfilter_util.sml @@ -3,7 +3,7 @@ struct open OS.Process fun nothing() = () -fun open_files intp infn outfn = +fun open_files intp oldp infn outfn = let open TextIO val is = TextIO.openIn infn @@ -32,7 +32,7 @@ fun open_files intp infn outfn = (strm, cb) end in - (is, os, intp, false, cb) + (is, os, intp, false, oldp, cb) end fun usage strm status = @@ -45,28 +45,30 @@ fun usage strm status = \Other options occur as sole arguments:\n\ \ -h : show this message\n\ \ -n : don't use \"interactive\" mode\n\ + \ -q : use old \"QuoteFilter\" parser\n\ \ --quotefix : filter to replace ` with Unicode quotes\n"); exit status) fun badusage() = usage TextIO.stdErr failure -fun processArgs (nonp, intp, qfixp) args = +fun processArgs (nonp, intp, qfixp, oldp) args = case args of [] => if intp then badusage() else if qfixp then - (TextIO.stdIn, TextIO.stdOut, false, qfixp, nothing) - else (TextIO.stdIn, TextIO.stdOut, not intp, false, nothing) + (TextIO.stdIn, TextIO.stdOut, false, qfixp, oldp, nothing) + else (TextIO.stdIn, TextIO.stdOut, not intp, false, oldp, nothing) | ["-h"] => usage TextIO.stdOut success | "-h" :: _ => badusage() | "-i" :: rest => if nonp orelse qfixp then badusage() - else processArgs (false, true, false) rest + else processArgs (false, true, false, oldp) rest | "-n"::rest => if intp orelse qfixp then badusage() - else processArgs (true, false, false) rest + else processArgs (true, false, false, oldp) rest + | "-q"::rest => processArgs (nonp, intp, qfixp, false) rest | "--quotefix"::rest => if intp orelse nonp then badusage() - else processArgs (false, false, true) rest + else processArgs (false, false, true, oldp) rest | [ifile, ofile] => if qfixp orelse nonp then badusage() - else open_files intp ifile ofile + else open_files intp oldp ifile ofile | _ => badusage() end (* struct *) diff --git a/tools/quote-filter/quote-filter.sml b/tools/quote-filter/quote-filter.sml index 0d29c81845..d3e96c4497 100644 --- a/tools/quote-filter/quote-filter.sml +++ b/tools/quote-filter/quote-filter.sml @@ -7,26 +7,38 @@ val _ = catch_interrupt true; fun read_from_stream is n = TextIO.input is -val (instream, outstream, intp, qfixp, callback) = - processArgs (false,false,false) (CommandLine.arguments()) - -open QuoteFilter.UserDeclarations -val state as QFS args = newstate {inscriptp = intp, quotefixp = qfixp} - +val (instream, outstream, intp, qfixp, oldp, callback) = + processArgs (false,false,false,false) (CommandLine.arguments()) (* with many thanks to Ken Friis Larsen, Peter Sestoft, Claudio Russo and Kenn Heinrich who helped me see the light with respect to this code *) -fun loop() = - let - val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instream) state - fun coreloop () = - case lexer() of - "" => () - | s => (TextIO.output(outstream, s); TextIO.flushOut outstream; - coreloop()) - in - coreloop() handle Interrupt => (resetstate state; loop()) - end +val loop = + if oldp orelse qfixp then let + open QuoteFilter.UserDeclarations + val state as QFS args = newstate {inscriptp = intp, quotefixp = qfixp} + + fun loop() = + let + val lexer = #2 o QuoteFilter.makeLexer (read_from_stream instream) state + fun coreloop () = + case lexer() of + "" => () + | s => (TextIO.output(outstream, s); coreloop()) + in + coreloop() handle Interrupt => (resetstate state; loop()) + end + in loop end + else let + open HolParser.ToSML + val read = mkPushTranslator { + read = read_from_stream instream, + parseError = fn (start, stop) => fn s => + TextIO.output (TextIO.stdErr, + "parse error at " ^ Int.toString start ^ "-" ^ Int.toString stop ^ ": " ^ s ^ "\n") + } (mkStrcode (fn s => TextIO.output(outstream, s))) + + fun loop () = if read () then () else loop () + in loop end val _ = loop() val _ = callback()