(*  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;