railroad diagrams in LaTeX as document antiquotation;
authorwenzelm
Sat Apr 30 19:50:39 2011 +0200 (2011-04-30)
changeset 42504869c3f6f2d6e
parent 42503 27514b6fbe93
child 42505 fef9a94706c2
railroad diagrams in LaTeX as document antiquotation;
src/Pure/IsaMakefile
src/Pure/ROOT.ML
src/Pure/Thy/rail.ML
     1.1 --- a/src/Pure/IsaMakefile	Sat Apr 30 18:16:40 2011 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sat Apr 30 19:50:39 2011 +0200
     1.3 @@ -196,6 +196,7 @@
     1.4    Thy/html.ML						\
     1.5    Thy/latex.ML						\
     1.6    Thy/present.ML					\
     1.7 +  Thy/rail.ML						\
     1.8    Thy/term_style.ML					\
     1.9    Thy/thm_deps.ML					\
    1.10    Thy/thy_header.ML					\
     2.1 --- a/src/Pure/ROOT.ML	Sat Apr 30 18:16:40 2011 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sat Apr 30 19:50:39 2011 +0200
     2.3 @@ -255,6 +255,7 @@
     2.4  use "Isar/outer_syntax.ML";
     2.5  use "PIDE/document.ML";
     2.6  use "Thy/thy_info.ML";
     2.7 +use "Thy/rail.ML";
     2.8  
     2.9  (*theory and proof operations*)
    2.10  use "Isar/rule_insts.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Thy/rail.ML	Sat Apr 30 19:50:39 2011 +0200
     3.3 @@ -0,0 +1,250 @@
     3.4 +(*  Title:      Pure/Thy/rail.ML
     3.5 +    Author:     Michael Kerscher, TU M√ľnchen
     3.6 +    Author:     Makarius
     3.7 +
     3.8 +Railroad diagrams in LaTeX.
     3.9 +*)
    3.10 +
    3.11 +structure Rail: sig end =
    3.12 +struct
    3.13 +
    3.14 +(** lexical syntax **)
    3.15 +
    3.16 +(* datatype token *)
    3.17 +
    3.18 +datatype kind = Keyword | Ident | String | EOF;
    3.19 +
    3.20 +datatype token = Token of Position.range * (kind * string);
    3.21 +
    3.22 +fun pos_of (Token ((pos, _), _)) = pos;
    3.23 +fun end_pos_of (Token ((_, pos), _)) = pos;
    3.24 +
    3.25 +fun kind_of (Token (_, (k, _))) = k;
    3.26 +fun content_of (Token (_, (_, x))) = x;
    3.27 +
    3.28 +
    3.29 +(* diagnostics *)
    3.30 +
    3.31 +val print_kind =
    3.32 + fn Keyword => "rail keyword"
    3.33 +  | Ident => "identifier"
    3.34 +  | String => "single-quoted string"
    3.35 +  | EOF => "end-of-file";
    3.36 +
    3.37 +fun print (Token ((pos, _), (k, x))) =
    3.38 +  (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
    3.39 +  Position.str_of pos;
    3.40 +
    3.41 +fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
    3.42 +
    3.43 +
    3.44 +(* stopper *)
    3.45 +
    3.46 +fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
    3.47 +val eof = mk_eof Position.none;
    3.48 +
    3.49 +fun is_eof (Token (_, (EOF, _))) = true
    3.50 +  | is_eof _ = false;
    3.51 +
    3.52 +val stopper =
    3.53 +  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
    3.54 +
    3.55 +
    3.56 +(* tokenize *)
    3.57 +
    3.58 +local
    3.59 +
    3.60 +fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
    3.61 +
    3.62 +val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
    3.63 +
    3.64 +val scan_keyword =
    3.65 +  Scan.one (member (op =) ["|", "*", "+", "?", "(", ")", "\\", ";", ":"] o Symbol_Pos.symbol);
    3.66 +
    3.67 +val scan_token =
    3.68 +  scan_space >> K [] ||
    3.69 +  scan_keyword >> (token Keyword o single) ||
    3.70 +  Lexicon.scan_id >> token Ident ||
    3.71 +  Symbol_Pos.scan_string_q >> (token String o #1 o #2);
    3.72 +
    3.73 +in
    3.74 +
    3.75 +fun tokenize pos str =
    3.76 +  Source.of_string str
    3.77 +  |> Symbol.source
    3.78 +  |> Symbol_Pos.source pos
    3.79 +  |> Source.source Symbol_Pos.stopper
    3.80 +      (Scan.bulk (Symbol_Pos.!!! "Rail lexical error: bad input" scan_token) >> flat) NONE
    3.81 +  |> Source.exhaust;
    3.82 +
    3.83 +end;
    3.84 +
    3.85 +
    3.86 +
    3.87 +(** parsing **)
    3.88 +
    3.89 +fun !!! scan =
    3.90 +  let
    3.91 +    val prefix = "Rail syntax error";
    3.92 +
    3.93 +    fun get_pos [] = " (past end-of-file!)"
    3.94 +      | get_pos (tok :: _) = Position.str_of (pos_of tok);
    3.95 +
    3.96 +    fun err (toks, NONE) = prefix ^ get_pos toks
    3.97 +      | err (toks, SOME msg) =
    3.98 +          if String.isPrefix prefix msg then msg
    3.99 +          else prefix ^ get_pos toks ^ ": " ^ msg;
   3.100 +  in Scan.!! err scan end;
   3.101 +
   3.102 +fun $$$ x =
   3.103 +  Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   3.104 +  Scan.fail_with
   3.105 +    (fn [] => print_keyword x ^ " expected (past end-of-file!)"
   3.106 +      | tok :: _ => print_keyword x ^ "expected,\nbut " ^ print tok ^ " was found");
   3.107 +
   3.108 +fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
   3.109 +fun enum sep scan = enum1 sep scan || Scan.succeed [];
   3.110 +
   3.111 +fun parse_token kind =
   3.112 +  Scan.some (fn tok => if kind_of tok = kind then SOME (content_of tok) else NONE);
   3.113 +
   3.114 +val ident = parse_token Ident;
   3.115 +val string = parse_token String;
   3.116 +
   3.117 +
   3.118 +
   3.119 +(** rail expressions **)
   3.120 +
   3.121 +(* datatype *)
   3.122 +
   3.123 +datatype rails =
   3.124 +  Cat of int * rail list
   3.125 +and rail =
   3.126 +  Bar of rails list |
   3.127 +  Plus of rails * rails |
   3.128 +  Newline of int |
   3.129 +  Nonterminal of string |
   3.130 +  Terminal of string;
   3.131 +
   3.132 +fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
   3.133 +and reverse (Bar cats) = Bar (map reverse_cat cats)
   3.134 +  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   3.135 +  | reverse x = x;
   3.136 +
   3.137 +fun cat rails = Cat (0, rails);
   3.138 +
   3.139 +val empty = cat [];
   3.140 +fun is_empty (Cat (_, [])) = true | is_empty _ = false;
   3.141 +
   3.142 +fun is_newline (Newline _) = true | is_newline _ = false;
   3.143 +
   3.144 +fun bar [Cat (_, [rail])] = rail
   3.145 +  | bar cats = Bar cats;
   3.146 +
   3.147 +fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
   3.148 +
   3.149 +fun star cat1 cat2 =
   3.150 +  if is_empty cat2 then plus empty cat1
   3.151 +  else bar [empty, cat [plus cat1 cat2]];
   3.152 +
   3.153 +fun maybe rail = bar [empty, cat [rail]];
   3.154 +
   3.155 +
   3.156 +(* read *)
   3.157 +
   3.158 +local
   3.159 +
   3.160 +fun body x = (enum1 "|" body1 >> bar) x
   3.161 +and body0 x = (enum "|" body1 >> bar) x
   3.162 +and body1 x =
   3.163 + (body2 :|-- (fn a =>
   3.164 +   $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
   3.165 +   $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
   3.166 +   Scan.succeed a)) x
   3.167 +and body2 x = (Scan.repeat1 body3 >> cat) x
   3.168 +and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
   3.169 +and body4 x =
   3.170 + ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   3.171 +  $$$ "\\" >> K (Newline 0) ||
   3.172 +  ident >> Nonterminal ||
   3.173 +  string >> Terminal) x
   3.174 +and body4e x = (Scan.option body4 >> (cat o the_list)) x;
   3.175 +
   3.176 +val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair "";
   3.177 +val rules = enum1 ";" (Scan.option rule) >> map_filter I;
   3.178 +
   3.179 +in
   3.180 +
   3.181 +fun read pos str =
   3.182 +  (case Scan.error (Scan.finite stopper rules) (tokenize pos str) of
   3.183 +    (res, []) => res
   3.184 +  | (_, tok :: _) => error ("Malformed rail input: " ^ print tok));
   3.185 +
   3.186 +end;
   3.187 +
   3.188 +
   3.189 +(* latex output *)
   3.190 +
   3.191 +local
   3.192 +
   3.193 +fun vertical_range_cat (Cat (_, rails)) y =
   3.194 +  let val (rails', (_, y')) =
   3.195 +    fold_map (fn rail => fn (y0, y') =>
   3.196 +      if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
   3.197 +      else
   3.198 +        let val (rail', y0') = vertical_range rail y0;
   3.199 +        in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
   3.200 +  in (Cat (y, rails'), y') end
   3.201 +
   3.202 +and vertical_range (Bar cats) y =
   3.203 +      let val (cats', y') = fold_map vertical_range_cat cats y
   3.204 +      in (Bar cats', Int.max (y + 1, y')) end
   3.205 +  | vertical_range (Plus (cat1, cat2)) y =
   3.206 +      let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
   3.207 +      in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
   3.208 +  | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   3.209 +  | vertical_range atom y = (atom, y + 1);
   3.210 +
   3.211 +
   3.212 +fun output_text s = "\\isa{" ^ Output.output s ^ "}";
   3.213 +
   3.214 +fun output_cat c (Cat (_, rails)) = outputs c rails
   3.215 +and outputs c [rail] = output c rail
   3.216 +  | outputs _ rails = implode (map (output "") rails)
   3.217 +and output _ (Bar []) = ""
   3.218 +  | output c (Bar [cat]) = output_cat c cat
   3.219 +  | output _ (Bar (cat :: cats)) =
   3.220 +      "\\rail@bar\n" ^ output_cat "" cat ^
   3.221 +      implode (map (fn Cat (y, rails) =>
   3.222 +          "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
   3.223 +      "\\rail@endbar\n"
   3.224 +  | output c (Plus (cat, Cat (y, rails))) =
   3.225 +      "\\rail@plus\n" ^ output_cat c cat ^
   3.226 +      "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
   3.227 +      "\\rail@endplus\n"
   3.228 +  | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
   3.229 +  | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text s ^ "}[]\n"
   3.230 +  | output c (Terminal s) = "\\rail@" ^ c ^ "term{" ^ output_text s ^ "}[]\n";
   3.231 +
   3.232 +fun output_rule (name, rail) =
   3.233 +  let val (rail', y') = vertical_range rail 0 in
   3.234 +    "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ output_text name ^ "}\n" ^
   3.235 +    output "" rail' ^
   3.236 +    "\\rail@end\n"
   3.237 +  end;
   3.238 +
   3.239 +fun output_rules rules =
   3.240 +  "\\begin{railoutput}\n" ^
   3.241 +  implode (map output_rule rules) ^
   3.242 +  "\\end{railoutput}\n";
   3.243 +
   3.244 +in
   3.245 +
   3.246 +val _ =
   3.247 +  Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
   3.248 +    (fn _ => fn (str, pos) => output_rules (read pos str));
   3.249 +
   3.250 +end;
   3.251 +
   3.252 +end;
   3.253 +