(* 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 | Antiq of Symbol_Pos.T list * Position.range | 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"
| Antiq _ => "antiquotation"
| 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 [] ||
Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
scan_keyword >> (token Keyword o single) ||
Lexicon.scan_id >> token Ident ||
Symbol_Pos.scan_string_q >> (token String o #1 o #2);
val scan =
(Scan.repeat scan_token >> flat) --|
Symbol_Pos.!!! "Rail lexical error: bad input"
(Scan.ahead (Scan.one Symbol_Pos.is_eof));
in
val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
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 [];
val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
(** 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 bool * string |
Antiquote of bool * (Symbol_Pos.T list * Position.range);
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
val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
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 ||
at_mode -- string >> Terminal ||
at_mode -- antiq >> Antiquote) x
and body4e x = (Scan.option body4 >> (cat o the_list)) x;
val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
val rules = enum1 ";" (Scan.option rule) >> map_filter I;
in
val read =
#1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
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_rules state rules =
let
val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
fun output_text b s =
Output.output s
|> b ? enclose "\\isakeyword{" "}"
|> enclose "\\isa{" "}";
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 false s ^ "}[]\n"
| output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
| output c (Antiquote (b, a)) =
"\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
fun output_rule (name, rail) =
let
val (rail', y') = vertical_range rail 0;
val out_name =
(case name of
Antiquote.Text "" => ""
| Antiquote.Text s => output_text false s
| Antiquote.Antiq a => output_antiq a);
in
"\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
output "" rail' ^
"\\rail@end\n"
end;
in
"\\begin{railoutput}\n" ^
implode (map output_rule rules) ^
"\\end{railoutput}\n"
end;
in
val _ =
Thy_Output.antiquotation "rail" (Scan.lift (Parse.source_position Parse.string))
(fn {state, ...} => output_rules state o read);
end;
end;