src/Pure/Thy/rail.ML
author wenzelm
Sat Apr 30 20:48:29 2011 +0200 (2011-04-30)
changeset 42506 876887b07e8d
parent 42504 869c3f6f2d6e
child 42507 651aef3cc854
permissions -rw-r--r--
more robust error handling (NB: Source.source requires total scanner or recover);
tuned;
wenzelm@42504
     1
(*  Title:      Pure/Thy/rail.ML
wenzelm@42504
     2
    Author:     Michael Kerscher, TU M√ľnchen
wenzelm@42504
     3
    Author:     Makarius
wenzelm@42504
     4
wenzelm@42504
     5
Railroad diagrams in LaTeX.
wenzelm@42504
     6
*)
wenzelm@42504
     7
wenzelm@42504
     8
structure Rail: sig end =
wenzelm@42504
     9
struct
wenzelm@42504
    10
wenzelm@42504
    11
(** lexical syntax **)
wenzelm@42504
    12
wenzelm@42504
    13
(* datatype token *)
wenzelm@42504
    14
wenzelm@42504
    15
datatype kind = Keyword | Ident | String | EOF;
wenzelm@42504
    16
wenzelm@42504
    17
datatype token = Token of Position.range * (kind * string);
wenzelm@42504
    18
wenzelm@42504
    19
fun pos_of (Token ((pos, _), _)) = pos;
wenzelm@42504
    20
fun end_pos_of (Token ((_, pos), _)) = pos;
wenzelm@42504
    21
wenzelm@42504
    22
fun kind_of (Token (_, (k, _))) = k;
wenzelm@42504
    23
fun content_of (Token (_, (_, x))) = x;
wenzelm@42504
    24
wenzelm@42504
    25
wenzelm@42504
    26
(* diagnostics *)
wenzelm@42504
    27
wenzelm@42504
    28
val print_kind =
wenzelm@42504
    29
 fn Keyword => "rail keyword"
wenzelm@42504
    30
  | Ident => "identifier"
wenzelm@42504
    31
  | String => "single-quoted string"
wenzelm@42504
    32
  | EOF => "end-of-file";
wenzelm@42504
    33
wenzelm@42504
    34
fun print (Token ((pos, _), (k, x))) =
wenzelm@42504
    35
  (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
wenzelm@42504
    36
  Position.str_of pos;
wenzelm@42504
    37
wenzelm@42504
    38
fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
wenzelm@42504
    39
wenzelm@42504
    40
wenzelm@42504
    41
(* stopper *)
wenzelm@42504
    42
wenzelm@42504
    43
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
wenzelm@42504
    44
val eof = mk_eof Position.none;
wenzelm@42504
    45
wenzelm@42504
    46
fun is_eof (Token (_, (EOF, _))) = true
wenzelm@42504
    47
  | is_eof _ = false;
wenzelm@42504
    48
wenzelm@42504
    49
val stopper =
wenzelm@42504
    50
  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
wenzelm@42504
    51
wenzelm@42504
    52
wenzelm@42504
    53
(* tokenize *)
wenzelm@42504
    54
wenzelm@42504
    55
local
wenzelm@42504
    56
wenzelm@42504
    57
fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
wenzelm@42504
    58
wenzelm@42504
    59
val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
wenzelm@42504
    60
wenzelm@42504
    61
val scan_keyword =
wenzelm@42504
    62
  Scan.one (member (op =) ["|", "*", "+", "?", "(", ")", "\\", ";", ":"] o Symbol_Pos.symbol);
wenzelm@42504
    63
wenzelm@42504
    64
val scan_token =
wenzelm@42504
    65
  scan_space >> K [] ||
wenzelm@42504
    66
  scan_keyword >> (token Keyword o single) ||
wenzelm@42504
    67
  Lexicon.scan_id >> token Ident ||
wenzelm@42504
    68
  Symbol_Pos.scan_string_q >> (token String o #1 o #2);
wenzelm@42504
    69
wenzelm@42506
    70
val scan =
wenzelm@42506
    71
  (Scan.repeat scan_token >> flat) --|
wenzelm@42506
    72
    Symbol_Pos.!!! "Rail lexical error: bad input"
wenzelm@42506
    73
      (Scan.ahead (Scan.one Symbol_Pos.is_eof));
wenzelm@42506
    74
wenzelm@42504
    75
in
wenzelm@42504
    76
wenzelm@42506
    77
fun tokenize text =
wenzelm@42506
    78
  #1 (Scan.error (Scan.finite Symbol_Pos.stopper scan) (Symbol_Pos.explode text));
wenzelm@42504
    79
wenzelm@42504
    80
end;
wenzelm@42504
    81
wenzelm@42504
    82
wenzelm@42504
    83
wenzelm@42504
    84
(** parsing **)
wenzelm@42504
    85
wenzelm@42504
    86
fun !!! scan =
wenzelm@42504
    87
  let
wenzelm@42504
    88
    val prefix = "Rail syntax error";
wenzelm@42504
    89
wenzelm@42504
    90
    fun get_pos [] = " (past end-of-file!)"
wenzelm@42504
    91
      | get_pos (tok :: _) = Position.str_of (pos_of tok);
wenzelm@42504
    92
wenzelm@42504
    93
    fun err (toks, NONE) = prefix ^ get_pos toks
wenzelm@42504
    94
      | err (toks, SOME msg) =
wenzelm@42504
    95
          if String.isPrefix prefix msg then msg
wenzelm@42504
    96
          else prefix ^ get_pos toks ^ ": " ^ msg;
wenzelm@42504
    97
  in Scan.!! err scan end;
wenzelm@42504
    98
wenzelm@42504
    99
fun $$$ x =
wenzelm@42504
   100
  Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
wenzelm@42504
   101
  Scan.fail_with
wenzelm@42504
   102
    (fn [] => print_keyword x ^ " expected (past end-of-file!)"
wenzelm@42506
   103
      | tok :: _ => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found");
wenzelm@42504
   104
wenzelm@42504
   105
fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
wenzelm@42504
   106
fun enum sep scan = enum1 sep scan || Scan.succeed [];
wenzelm@42504
   107
wenzelm@42504
   108
fun parse_token kind =
wenzelm@42504
   109
  Scan.some (fn tok => if kind_of tok = kind then SOME (content_of tok) else NONE);
wenzelm@42504
   110
wenzelm@42504
   111
val ident = parse_token Ident;
wenzelm@42504
   112
val string = parse_token String;
wenzelm@42504
   113
wenzelm@42504
   114
wenzelm@42504
   115
wenzelm@42504
   116
(** rail expressions **)
wenzelm@42504
   117
wenzelm@42504
   118
(* datatype *)
wenzelm@42504
   119
wenzelm@42504
   120
datatype rails =
wenzelm@42504
   121
  Cat of int * rail list
wenzelm@42504
   122
and rail =
wenzelm@42504
   123
  Bar of rails list |
wenzelm@42504
   124
  Plus of rails * rails |
wenzelm@42504
   125
  Newline of int |
wenzelm@42504
   126
  Nonterminal of string |
wenzelm@42504
   127
  Terminal of string;
wenzelm@42504
   128
wenzelm@42504
   129
fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
wenzelm@42504
   130
and reverse (Bar cats) = Bar (map reverse_cat cats)
wenzelm@42504
   131
  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
wenzelm@42504
   132
  | reverse x = x;
wenzelm@42504
   133
wenzelm@42504
   134
fun cat rails = Cat (0, rails);
wenzelm@42504
   135
wenzelm@42504
   136
val empty = cat [];
wenzelm@42504
   137
fun is_empty (Cat (_, [])) = true | is_empty _ = false;
wenzelm@42504
   138
wenzelm@42504
   139
fun is_newline (Newline _) = true | is_newline _ = false;
wenzelm@42504
   140
wenzelm@42504
   141
fun bar [Cat (_, [rail])] = rail
wenzelm@42504
   142
  | bar cats = Bar cats;
wenzelm@42504
   143
wenzelm@42504
   144
fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
wenzelm@42504
   145
wenzelm@42504
   146
fun star cat1 cat2 =
wenzelm@42504
   147
  if is_empty cat2 then plus empty cat1
wenzelm@42504
   148
  else bar [empty, cat [plus cat1 cat2]];
wenzelm@42504
   149
wenzelm@42504
   150
fun maybe rail = bar [empty, cat [rail]];
wenzelm@42504
   151
wenzelm@42504
   152
wenzelm@42504
   153
(* read *)
wenzelm@42504
   154
wenzelm@42504
   155
local
wenzelm@42504
   156
wenzelm@42504
   157
fun body x = (enum1 "|" body1 >> bar) x
wenzelm@42504
   158
and body0 x = (enum "|" body1 >> bar) x
wenzelm@42504
   159
and body1 x =
wenzelm@42504
   160
 (body2 :|-- (fn a =>
wenzelm@42504
   161
   $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
wenzelm@42504
   162
   $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
wenzelm@42504
   163
   Scan.succeed a)) x
wenzelm@42504
   164
and body2 x = (Scan.repeat1 body3 >> cat) x
wenzelm@42504
   165
and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
wenzelm@42504
   166
and body4 x =
wenzelm@42504
   167
 ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
wenzelm@42504
   168
  $$$ "\\" >> K (Newline 0) ||
wenzelm@42504
   169
  ident >> Nonterminal ||
wenzelm@42504
   170
  string >> Terminal) x
wenzelm@42504
   171
and body4e x = (Scan.option body4 >> (cat o the_list)) x;
wenzelm@42504
   172
wenzelm@42504
   173
val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair "";
wenzelm@42504
   174
val rules = enum1 ";" (Scan.option rule) >> map_filter I;
wenzelm@42504
   175
wenzelm@42504
   176
in
wenzelm@42504
   177
wenzelm@42506
   178
fun read text =
wenzelm@42506
   179
  (case Scan.error (Scan.finite stopper rules) (tokenize text) of
wenzelm@42504
   180
    (res, []) => res
wenzelm@42504
   181
  | (_, tok :: _) => error ("Malformed rail input: " ^ print tok));
wenzelm@42504
   182
wenzelm@42504
   183
end;
wenzelm@42504
   184
wenzelm@42504
   185
wenzelm@42504
   186
(* latex output *)
wenzelm@42504
   187
wenzelm@42504
   188
local
wenzelm@42504
   189
wenzelm@42504
   190
fun vertical_range_cat (Cat (_, rails)) y =
wenzelm@42504
   191
  let val (rails', (_, y')) =
wenzelm@42504
   192
    fold_map (fn rail => fn (y0, y') =>
wenzelm@42504
   193
      if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
wenzelm@42504
   194
      else
wenzelm@42504
   195
        let val (rail', y0') = vertical_range rail y0;
wenzelm@42504
   196
        in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
wenzelm@42504
   197
  in (Cat (y, rails'), y') end
wenzelm@42504
   198
wenzelm@42504
   199
and vertical_range (Bar cats) y =
wenzelm@42504
   200
      let val (cats', y') = fold_map vertical_range_cat cats y
wenzelm@42504
   201
      in (Bar cats', Int.max (y + 1, y')) end
wenzelm@42504
   202
  | vertical_range (Plus (cat1, cat2)) y =
wenzelm@42504
   203
      let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
wenzelm@42504
   204
      in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
wenzelm@42504
   205
  | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
wenzelm@42504
   206
  | vertical_range atom y = (atom, y + 1);
wenzelm@42504
   207
wenzelm@42504
   208
wenzelm@42504
   209
fun output_text s = "\\isa{" ^ Output.output s ^ "}";
wenzelm@42504
   210
wenzelm@42504
   211
fun output_cat c (Cat (_, rails)) = outputs c rails
wenzelm@42504
   212
and outputs c [rail] = output c rail
wenzelm@42504
   213
  | outputs _ rails = implode (map (output "") rails)
wenzelm@42504
   214
and output _ (Bar []) = ""
wenzelm@42504
   215
  | output c (Bar [cat]) = output_cat c cat
wenzelm@42504
   216
  | output _ (Bar (cat :: cats)) =
wenzelm@42504
   217
      "\\rail@bar\n" ^ output_cat "" cat ^
wenzelm@42504
   218
      implode (map (fn Cat (y, rails) =>
wenzelm@42504
   219
          "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
wenzelm@42504
   220
      "\\rail@endbar\n"
wenzelm@42504
   221
  | output c (Plus (cat, Cat (y, rails))) =
wenzelm@42504
   222
      "\\rail@plus\n" ^ output_cat c cat ^
wenzelm@42504
   223
      "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
wenzelm@42504
   224
      "\\rail@endplus\n"
wenzelm@42504
   225
  | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
wenzelm@42504
   226
  | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
wenzelm@42504
   227
  | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n";
wenzelm@42504
   228
wenzelm@42504
   229
fun output_rule (name, rail) =
wenzelm@42504
   230
  let val (rail', y') = vertical_range rail 0 in
wenzelm@42504
   231
    "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ output_text name ^ "}\n" ^
wenzelm@42504
   232
    output "" rail' ^
wenzelm@42504
   233
    "\\rail@end\n"
wenzelm@42504
   234
  end;
wenzelm@42504
   235
wenzelm@42504
   236
fun output_rules rules =
wenzelm@42504
   237
  "\\begin{railoutput}\n" ^
wenzelm@42504
   238
  implode (map output_rule rules) ^
wenzelm@42504
   239
  "\\end{railoutput}\n";
wenzelm@42504
   240
wenzelm@42504
   241
in
wenzelm@42504
   242
wenzelm@42504
   243
val _ =
wenzelm@42504
   244
  Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
wenzelm@42506
   245
    (fn _ => output_rules o read);
wenzelm@42504
   246
wenzelm@42504
   247
end;
wenzelm@42504
   248
wenzelm@42504
   249
end;
wenzelm@42504
   250