--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/rail.ML Sat Apr 30 19:50:39 2011 +0200
@@ -0,0 +1,250 @@
+(* Title: Pure/Thy/rail.ML
+ Author: Michael Kerscher, TU München
+ Author: Makarius
+
+Railroad diagrams in LaTeX.
+*)
+
+structure Rail: sig end =
+struct
+
+(** lexical syntax **)
+
+(* datatype token *)
+
+datatype kind = Keyword | Ident | String | EOF;
+
+datatype token = Token of Position.range * (kind * string);
+
+fun pos_of (Token ((pos, _), _)) = pos;
+fun end_pos_of (Token ((_, pos), _)) = pos;
+
+fun kind_of (Token (_, (k, _))) = k;
+fun content_of (Token (_, (_, x))) = x;
+
+
+(* diagnostics *)
+
+val print_kind =
+ fn Keyword => "rail keyword"
+ | Ident => "identifier"
+ | String => "single-quoted string"
+ | EOF => "end-of-file";
+
+fun print (Token ((pos, _), (k, x))) =
+ (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
+ Position.str_of pos;
+
+fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
+
+
+(* stopper *)
+
+fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
+val eof = mk_eof Position.none;
+
+fun is_eof (Token (_, (EOF, _))) = true
+ | is_eof _ = false;
+
+val stopper =
+ Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
+
+
+(* tokenize *)
+
+local
+
+fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
+
+val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
+
+val scan_keyword =
+ Scan.one (member (op =) ["|", "*", "+", "?", "(", ")", "\\", ";", ":"] o Symbol_Pos.symbol);
+
+val scan_token =
+ scan_space >> K [] ||
+ scan_keyword >> (token Keyword o single) ||
+ Lexicon.scan_id >> token Ident ||
+ Symbol_Pos.scan_string_q >> (token String o #1 o #2);
+
+in
+
+fun tokenize pos str =
+ Source.of_string str
+ |> Symbol.source
+ |> Symbol_Pos.source pos
+ |> Source.source Symbol_Pos.stopper
+ (Scan.bulk (Symbol_Pos.!!! "Rail lexical error: bad input" scan_token) >> flat) NONE
+ |> Source.exhaust;
+
+end;
+
+
+
+(** parsing **)
+
+fun !!! scan =
+ let
+ val prefix = "Rail syntax error";
+
+ fun get_pos [] = " (past end-of-file!)"
+ | get_pos (tok :: _) = Position.str_of (pos_of tok);
+
+ fun err (toks, NONE) = prefix ^ get_pos toks
+ | err (toks, SOME msg) =
+ if String.isPrefix prefix msg then msg
+ else prefix ^ get_pos toks ^ ": " ^ msg;
+ in Scan.!! err scan end;
+
+fun $$$ x =
+ Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
+ Scan.fail_with
+ (fn [] => print_keyword x ^ " expected (past end-of-file!)"
+ | tok :: _ => print_keyword x ^ "expected,\nbut " ^ print tok ^ " was found");
+
+fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
+fun enum sep scan = enum1 sep scan || Scan.succeed [];
+
+fun parse_token kind =
+ Scan.some (fn tok => if kind_of tok = kind then SOME (content_of tok) else NONE);
+
+val ident = parse_token Ident;
+val string = parse_token String;
+
+
+
+(** rail expressions **)
+
+(* datatype *)
+
+datatype rails =
+ Cat of int * rail list
+and rail =
+ Bar of rails list |
+ Plus of rails * rails |
+ Newline of int |
+ Nonterminal of string |
+ Terminal of string;
+
+fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
+and reverse (Bar cats) = Bar (map reverse_cat cats)
+ | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
+ | reverse x = x;
+
+fun cat rails = Cat (0, rails);
+
+val empty = cat [];
+fun is_empty (Cat (_, [])) = true | is_empty _ = false;
+
+fun is_newline (Newline _) = true | is_newline _ = false;
+
+fun bar [Cat (_, [rail])] = rail
+ | bar cats = Bar cats;
+
+fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
+
+fun star cat1 cat2 =
+ if is_empty cat2 then plus empty cat1
+ else bar [empty, cat [plus cat1 cat2]];
+
+fun maybe rail = bar [empty, cat [rail]];
+
+
+(* read *)
+
+local
+
+fun body x = (enum1 "|" body1 >> bar) x
+and body0 x = (enum "|" body1 >> bar) x
+and body1 x =
+ (body2 :|-- (fn a =>
+ $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
+ $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
+ Scan.succeed a)) x
+and body2 x = (Scan.repeat1 body3 >> cat) x
+and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
+and body4 x =
+ ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
+ $$$ "\\" >> K (Newline 0) ||
+ ident >> Nonterminal ||
+ string >> Terminal) x
+and body4e x = (Scan.option body4 >> (cat o the_list)) x;
+
+val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair "";
+val rules = enum1 ";" (Scan.option rule) >> map_filter I;
+
+in
+
+fun read pos str =
+ (case Scan.error (Scan.finite stopper rules) (tokenize pos str) of
+ (res, []) => res
+ | (_, tok :: _) => error ("Malformed rail input: " ^ print tok));
+
+end;
+
+
+(* latex output *)
+
+local
+
+fun vertical_range_cat (Cat (_, rails)) y =
+ let val (rails', (_, y')) =
+ fold_map (fn rail => fn (y0, y') =>
+ if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
+ else
+ let val (rail', y0') = vertical_range rail y0;
+ in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
+ in (Cat (y, rails'), y') end
+
+and vertical_range (Bar cats) y =
+ let val (cats', y') = fold_map vertical_range_cat cats y
+ in (Bar cats', Int.max (y + 1, y')) end
+ | vertical_range (Plus (cat1, cat2)) y =
+ let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
+ in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
+ | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
+ | vertical_range atom y = (atom, y + 1);
+
+
+fun output_text s = "\\isa{" ^ Output.output s ^ "}";
+
+fun output_cat c (Cat (_, rails)) = outputs c rails
+and outputs c [rail] = output c rail
+ | outputs _ rails = implode (map (output "") rails)
+and output _ (Bar []) = ""
+ | output c (Bar [cat]) = output_cat c cat
+ | output _ (Bar (cat :: cats)) =
+ "\\rail@bar\n" ^ output_cat "" cat ^
+ implode (map (fn Cat (y, rails) =>
+ "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
+ "\\rail@endbar\n"
+ | output c (Plus (cat, Cat (y, rails))) =
+ "\\rail@plus\n" ^ output_cat c cat ^
+ "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
+ "\\rail@endplus\n"
+ | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
+ | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
+ | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n";
+
+fun output_rule (name, rail) =
+ let val (rail', y') = vertical_range rail 0 in
+ "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ output_text name ^ "}\n" ^
+ output "" rail' ^
+ "\\rail@end\n"
+ end;
+
+fun output_rules rules =
+ "\\begin{railoutput}\n" ^
+ implode (map output_rule rules) ^
+ "\\end{railoutput}\n";
+
+in
+
+val _ =
+ Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
+ (fn _ => fn (str, pos) => output_rules (read pos str));
+
+end;
+
+end;
+