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