(*  Title:      doc-src/rail.ML

     Author:     Michael Kerscher, TUM

 Railroad diagrams for LaTeX.

 *)

 structure Rail =

 struct

 datatype token =

   Identifier of string |

   Special_Identifier of string |

   Text of string |

   Anot of string |

   Symbol of string |

   EOF;

 fun is_identifier (Identifier _) = true

   | is_identifier (Special_Identifier _ ) = true

   | is_identifier _ = false;

 fun is_text (Text _) = true

   | is_text _ = false;

 fun is_anot (Anot _) = true

   | is_anot _ = false;

 fun is_symbol (Symbol _) = true

   | is_symbol _ = false;

 fun is_ str = (fn s => s = Symbol str);

 local (* copied from antiquote-setup... *)

 fun translate f = Symbol.explode #> map f #> implode;

 fun clean_name "\<dots>" = "dots"

   | clean_name ".." = "ddot"

   | clean_name "." = "dot"

   | clean_name "_" = "underscore"

   | clean_name "{" = "braceleft"

   | clean_name "}" = "braceright"

   | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);

 fun no_check _ _ = true;

 fun false_check _ _ = false;

 fun thy_check intern defined ctxt =

   let val thy = ProofContext.theory_of ctxt

   in defined thy o intern thy end;

 fun check_tool name =

   File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));

 val arg = enclose "{" "}";

 val markup_table =

 (*  [(kind, (markup, check, style))*)

   Symtab.make [

   ("syntax", ("", no_check, true)),

   ("command", ("isacommand", K (is_some o Keyword.command_keyword), true)),

   ("keyword", ("isakeyword", K Keyword.is_keyword, true)),

   ("element", ("isakeyword", K Keyword.is_keyword, true)),

   ("method", ("", thy_check Method.intern Method.defined, true)),

   ("attribute", ("", thy_check Attrib.intern Attrib.defined, true)),

   ("fact", ("", no_check, true)),

   ("variable", ("", no_check, true)),

   ("case", ("", no_check, true)),

   ("antiquotation", ("", K Thy_Output.defined_command, true)),

   ("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *)

   ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),

   ("inference", ("", no_check, true)),

   ("executable", ("isatt", no_check, true)),

   ("tool", ("isatt", K check_tool, true)),

   ("file", ("isatt", K (File.exists o Path.explode), true)),

   ("theory", ("", K Thy_Info.known_thy, true))

   ];

 in

 fun decode_link ctxt (kind,index,logic,name) =

   let

   val (markup, check, style) = case Symtab.lookup markup_table kind of

     SOME x => x

   | NONE => ("", false_check, false);

   val hyper_name =

     "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";

   val hyper =

     enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>

     index = "def" ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";

   val idx =

     if index = "" then ""

     else "\\index" ^ index ^ arg logic ^ arg kind ^ arg name;

   in

   if check ctxt name then

     (idx ^

     (Output.output name

       |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")

       |> (if ! Thy_Output.quotes then quote else I)

       |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"

           else hyper o enclose "\\mbox{\\isa{" "}}")), style)

   else ("Bad " ^ kind ^ " " ^ name, false)

   end;

 end;

 val blanks =

   Scan.many Symbol.is_blank >> implode;

 val scan_symbol =

   $$ ";" || $$ ":"|| $$ "("|| $$ ")"|| $$ "+"|| $$ "|"|| $$ "*"|| $$ "?"|| $$ "\\";

 (* escaped version *)

 val scan_link = (* @{kind{_def|_ref (logic) name} *)

   let

     fun pseudo_antiquote inner_scan = ($$ "@" ^^ $$ "{") |-- inner_scan --| (blanks -- $$ "}");

     fun parens scan = $$ "(" |-- scan --| $$ ")";

     fun opt_quotes scan = $$ "'" |-- scan --| $$ "'" || scan;

     val letters = Scan.many Symbol.is_letter >> implode;

     val kind_name = letters;

     val opt_kind_type = Scan.optional (

       $$ "_" |-- (Scan.this_string "def" || Scan.this_string "ref")) "";

     val logic_name = letters;

     val escaped_singlequote = $$ "\\" |-- $$ "'";

     val text = Scan.repeat (Scan.one Symbol.is_letter || escaped_singlequote) >> implode;

   in

    pseudo_antiquote (

     kind_name -- opt_kind_type --

     (blanks |-- Scan.optional ( parens logic_name ) "") --

     (blanks |-- opt_quotes text) )

     >> (fn (((kind,index),logic),name) => (kind, index, logic, name))

 end;

 (* escaped version *)

 fun scan_identifier ctxt =

   let fun is_identifier_start s =

     Symbol.is_letter s orelse

     s = "_"

   fun is_identifier_rest s =

     Symbol.is_letter s orelse

     Symbol.is_digit s orelse

     s = "_" orelse

     s = "."

   in

   (Scan.one is_identifier_start :::

     Scan.repeat (Scan.one is_identifier_rest || ($$ "\\" |-- $$ "'"))

   ) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||

   scan_link >> (decode_link ctxt) >>

     (fn (txt, style) =>

         if style then Special_Identifier(txt)

         else Identifier(txt))

 end;

 fun scan_anot ctxt =

   let val scan_anot =

     Scan.many (fn s =>

       s <> "\n" andalso

       s <> "\t" andalso

       s <> "]" andalso

       Symbol.is_regular s) >> implode

   in

   $$ "[" |-- scan_link --| $$ "]" >> (fst o (decode_link ctxt)) ||

   $$ "[" |-- scan_anot --| $$ "]" >> Output.output

 end;

 (* escaped version *)

 fun scan_text ctxt =

   let

     val text_sq =

       Scan.repeat (

         Scan.one (fn s =>

           s <> "\n" andalso

           s <> "\t" andalso

           s <> "'" andalso

           s <> "\\" andalso

           Symbol.is_regular s) ||

         ($$ "\\" |-- $$ "'")

       ) >> implode

   fun quoted scan = $$ "'" |-- scan --| $$ "'";

   in

   quoted scan_link >> (fst o (decode_link ctxt)) ||

   quoted text_sq >> (enclose "\\isa{" "}" o Output.output)

 end;

 fun scan_rail ctxt =

   Scan.repeat ( blanks |-- (

     scan_identifier ctxt ||

     scan_anot ctxt >> Anot ||

     scan_text ctxt >> Text ||

     scan_symbol >> Symbol)

   ) --| blanks;

 fun lex_rail txt ctxt = (* Symbol_Pos fuer spaeter durchgereicht *)

   Symbol.scanner "Malformed rail-declaration" (scan_rail ctxt) (map fst (Symbol_Pos.explode txt));

 val lex = lex_rail;

 datatype id_kind = UNKNOWN | TOKEN | TERM | NTERM;

 datatype id_type =

   Id of string * id_kind |

   Null_Id;

 datatype body_kind =

   CAT | BAR | PLUS |

   CR | EMPTY | ANNOTE | IDENT | STRING |

   Null_Kind;

 datatype body_type =

   Body of body_kind * string * string * id_type * body_type list |

   Body_Pos of body_kind * string * string * id_type * body_type list * int * int |

   Empty_Body |

   Null_Body;

 datatype rule =

   Rule of id_type * body_type;

 fun new_id id kind = Id (id, kind);

 fun is_empty (Body(kind,_,_,_,_)) = kind = EMPTY;

 fun new_body (kind, Null_Body, Null_Body) = Body (kind, "", "", Null_Id, [])

   | new_body (kind, body1, body2) = Body (kind, "", "", Null_Id, body1 :: [body2]);

 fun is_kind_of kind (Body(bodyKind,_,_,_,_)) = kind = bodyKind

   | is_kind_of _ _ = false;

 fun add_list (Body(kind, text, annot, id, bodies), body) =

   Body(kind, text, annot, id, bodies @ [body]);

 fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) =

       Body(kind, text, annot, id, bodies1 @ bodies2);

 fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) =

   if kind = kind1 andalso kind <> BAR then

     if kind = kind2 then

       cat_body_lists(body1, body2)

     else (* kind <> kind2 *)

       add_list(body1, body2)

   else (* kind <> kind1 orelse kind = BAR *)

     if kind = kind2 then

       cat_body_lists(add_list(new_body(kind,Null_Body,Null_Body), body1), body2)

     else (* kind <> kind2 *)

       add_list(add_list(new_body(kind,Null_Body,Null_Body), body1), body2);

 fun rev_body (body as Body (kind, text, annot, id, [])) = body

   | rev_body (Body (CAT, text, annot, id, bodies)) =

       Body(CAT, text, annot, id, map rev_body (rev bodies))

   | rev_body (Body (kind, text, annot, id, bodies)) =

       Body(kind, text, annot, id, map rev_body bodies)

   | rev_body body = body;

 fun set_body_text text (Body(k,_,a,i,b)) = Body(k,text,a,i,b);

 fun set_body_anot anot (Body(k,t,_,i,b)) = Body(k,t,anot,i,b);

 fun set_body_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TOKEN,b);

 fun set_body_special_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TERM,b);

 fun mk_eof _ = EOF;

 fun is_eof s = s = EOF;

 val stopper = Scan.stopper mk_eof is_eof;

 (* TODO: change this, so the next or next two tokens are printed *)

 fun lex_err msg (cs, _) = "rail grammar error: " ^ msg cs;

 fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;

 fun $$$ tok = Scan.one (is_ tok);

 local

 fun new_bar_body([], body2) = body2

   | new_bar_body(body1::bodies, body2) =

       add_body(BAR, body1, new_bar_body(bodies, body2));

 fun new_cat_body(body::[]) = body

   | new_cat_body(body1::bodies) = add_body(CAT, body1, new_cat_body(bodies));

 fun new_annote_body (Anot anot) =

   set_body_text anot (new_body(ANNOTE, Empty_Body, Empty_Body));

 fun new_text_annote_body (Text text, Anot anot) =

   set_body_anot anot (set_body_text text (new_body(STRING, Empty_Body, Empty_Body)));

 fun new_ident_body (Identifier ident, Anot anot) =

       set_body_anot anot (set_body_ident ident (new_body(IDENT, Empty_Body, Empty_Body)))

   | new_ident_body (Special_Identifier ident, Anot anot) =

       set_body_anot anot (set_body_special_ident ident (new_body(IDENT, Empty_Body, Empty_Body)));

 val new_empty_body = new_body(EMPTY, Null_Body, Null_Body);

 in

 fun parse_body x =

   (

   Scan.repeat1 (parse_body0 --| $$$ "|") -- !!! "body0 expected" (parse_body0) >>

     new_bar_body ||

   parse_body0

   ) x

 and parse_body0 x =

   (

   Scan.one is_anot -- !!! "body1 expected" (parse_body1) >>

     (fn (anot, body) => add_body(CAT, new_annote_body(anot), body))  ||

   parse_body1

   ) x

 and parse_body1 x =

   (

   parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>

     (fn (body1, body2) =>

       if is_empty body2 then

         add_body(PLUS, new_empty_body, rev_body body1)

       else

         add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||

   parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>

     (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||

   parse_body2e

   ) x

 and parse_body2e x =

   (

   parse_body2 ||

   (fn toks => (new_empty_body, toks))

   ) x

 and parse_body2 x =

   (

   Scan.repeat1 (parse_body3) >> new_cat_body

   ) x

 and parse_body3 x =

   (

   parse_body4 --| $$$ "?" >> (fn body => new_body (BAR, new_empty_body, body) ) ||

   parse_body4

   ) x

 and parse_body4e x =

   (

   parse_body4 ||

   (fn toks => (new_empty_body, toks))

   ) x

 and parse_body4 x =

   (

   $$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") ||

   Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>

     (fn (text, anot) => new_text_annote_body (text,anot)) ||

   Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>

     (fn (id, anot) => new_ident_body (id,anot)) ||

   $$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body))

   ) x;

 end;

 fun new_named_rule (Identifier name, body) = Rule(Id(name, UNKNOWN), body)

   | new_named_rule (Special_Identifier name, body) = Rule(Id(name, UNKNOWN), body);

 fun new_anonym_rule body = Rule(Null_Id, body);

 val parse_rule =

   (Scan.one (is_identifier) -- ($$$ ":" |-- !!! "body expected" (parse_body)) ) >>

     new_named_rule ||

   parse_body >> new_anonym_rule;

 val parse_rules =

   Scan.repeat ( parse_rule --| $$$ ";") @@@ Scan.single parse_rule;

 fun parse_rail s =

   Scan.read stopper parse_rules s;

 val parse = parse_rail;

 fun getystart (Body_Pos(_,_,_,_,_,ystart,_)) = ystart;

 fun getynext (Body_Pos(_,_,_,_,_,_,ynext)) = ynext;

 fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =

   let fun max (x,y) = if x > y then x else y

     fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =

           Body_Pos(kind, text, annot, id, bodies, ystart, ynext)

     fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)

       | pos_bodies_cat (x::xs, ystart, ynext, liste) =

           if is_kind_of CR x then

               (case set_body_position(x, ystart, ynext+1) of

                 body as Body_Pos(_,_,_,_,_,_,ynext1) =>

                   pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])

               )

           else

               (case position_body(x, ystart) of

                 body as Body_Pos(_,_,_,_,_,_,ynext1) =>

                   pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])

               )

     fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)

       | pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =

           (case position_body(x, ystart) of

             body as Body_Pos(_,_,_,_,_,_,ynext1) =>

               pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])

           )

   in

   (case kind of

     CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of

               (bodiesPos, ynext) =>

                 Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))

   | BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of

               (bodiesPos, ynext) =>

                 Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))

   | PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of

               (bodiesPos, ynext) =>

                 Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))

   | CR => set_body_position(body, ystart, ystart+3)

   | EMPTY => set_body_position(body, ystart, ystart+1)

   | ANNOTE => set_body_position(body, ystart, ystart+1)

   | IDENT => set_body_position(body, ystart, ystart+1)

   | STRING => set_body_position(body, ystart, ystart+1)

   )

   end;

 fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""

   | format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =

     let fun format_bodies([]) = ""

           | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)

     in

       format_bodies(bodies)

     end

   | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =

     let fun format_bodies([]) = "\\rail@endbar\n"

           | format_bodies(x::xs) =

               "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^

               format_body(x, "") ^ format_bodies(xs)

     in

       "\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))

     end

   | format_body (Body_Pos(PLUS,_,_,_,x::y::xs,_,_),cent) =

       "\\rail@plus\n" ^ format_body(x, cent) ^

       "\\rail@nextplus{" ^ string_of_int(getystart(y)) ^ "}\n" ^

       format_body(y, "c") ^

       "\\rail@endplus\n"

   | format_body (Body_Pos(ANNOTE,text,_,_,_,_,_),cent) =

       "\\rail@annote[" ^ text ^ "]\n"

   | format_body (Body_Pos(IDENT,_,annot,Id(name,TERM),_,_,_),cent) =

       "\\rail@" ^ cent ^ "token{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"

   | format_body (Body_Pos(IDENT,_,annot,Id(name,_),_,_,_),cent) =

       "\\rail@" ^ cent ^ "nont{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"

   | format_body (Body_Pos(CR,_,_,_,_,_,ynext),cent) =

       "\\rail@cr{" ^ string_of_int(ynext) ^ "}\n"

   | format_body (Body_Pos(STRING,text,annot,_,_,_,_),cent) =

       "\\rail@" ^ cent ^ "term{" ^ text ^ "}[" ^ annot ^ "]\n"

   | format_body _ =

       "\\rail@unknown\n";

 fun out_body (Id(name,_), body) =

   let val bodyPos as Body_Pos(_,_,_,_,_,_,ynext) = position_body(body,0)

   in

     "\\rail@begin{" ^ string_of_int(ynext) ^ "}{" ^ name ^ "}\n" ^

     format_body(bodyPos,"") ^

     "\\rail@end\n"

   end

   | out_body (Null_Id, body) = out_body (Id("", UNKNOWN), body);

 fun out_rule (Rule(id, body)) =

   if is_empty body then ""

   else out_body (id, body);

 fun out_rules ([]) = ""

   | out_rules (rule::rules) = out_rule rule ^ out_rules rules;

 val output_no_rules =

   "\\rail@begin{1}{}\n" ^

   "\\rail@setbox{\\bfseries ???}\n" ^

   "\\rail@oval\n" ^

   "\\rail@end\n";

 fun print (SOME rules) =

     "\\begin{railoutput}\n" ^

     out_rules rules ^

     "\\end{railoutput}\n"

   | print (NONE) =

     "\\begin{railoutput}\n" ^

     output_no_rules ^

     "\\end{railoutput}\n";

 fun process txt ctxt =

   lex txt ctxt

   |> parse

   |> print;

 val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))

   (fn {context = ctxt,...} => fn txt => process txt ctxt);

 end;