doc-src/rail.ML
author wenzelm
Wed Jul 22 11:48:04 2009 +0200 (2009-07-22)
changeset 32132 29aed5725acb
child 32233 2b175fc6668a
permissions -rw-r--r--
original rail implementation by Michael Kerscher;
     1 datatype token =
     2   Identifier of string |
     3   Special_Identifier of string |
     4   Text of string |
     5   Anot of string |
     6   Symbol of string |
     7   EOF;
     8 
     9 fun is_identifier (Identifier _) = true
    10   | is_identifier (Special_Identifier _ ) = true
    11   | is_identifier _ = false;
    12   
    13 fun is_text (Text _) = true
    14   | is_text _ = false;
    15 
    16 fun is_anot (Anot _) = true
    17   | is_anot _ = false;
    18 
    19 fun is_symbol (Symbol _) = true
    20   | is_symbol _ = false;
    21 
    22 fun is_ str = (fn s => s = Symbol str);
    23 
    24 
    25 local (* copied from antiquote-setup... *)
    26 fun translate f = Symbol.explode #> map f #> implode;
    27 
    28 fun clean_name "\<dots>" = "dots"
    29   | clean_name ".." = "ddot"
    30   | clean_name "." = "dot"
    31   | clean_name "_" = "underscore"
    32   | clean_name "{" = "braceleft"
    33   | clean_name "}" = "braceright"
    34   | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
    35 
    36 fun no_check _ _ = true;
    37 
    38 fun false_check _ _ = false;
    39 
    40 fun thy_check intern defined ctxt =
    41   let val thy = ProofContext.theory_of ctxt
    42   in defined thy o intern thy end;
    43 
    44 fun check_tool name =
    45   File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
    46 
    47 val arg = enclose "{" "}";
    48 
    49 val markup_table =
    50 (*  [(kind, (markup, check, style))*)
    51   Symtab.make [
    52   ("syntax", ("", no_check, true)),
    53   ("command", ("isacommand", K (is_some o OuterKeyword.command_keyword), true)),
    54   ("keyword", ("isakeyword", K OuterKeyword.is_keyword, true)),
    55   ("element", ("isakeyword", K OuterKeyword.is_keyword, true)),
    56   ("method", ("", thy_check Method.intern Method.defined, true)),
    57   ("attribute", ("", thy_check Attrib.intern Attrib.defined, true)),
    58   ("fact", ("", no_check, true)),
    59   ("variable", ("", no_check, true)),
    60   ("case", ("", no_check, true)),
    61   ("antiquotation", ("", K ThyOutput.defined_command, true)),
    62   ("antiquotation option", ("", K ThyOutput.defined_option, true)), (* kann mein scanner nicht erkennen *)
    63   ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
    64   ("inference", ("", no_check, true)),
    65   ("executable", ("isatt", no_check, true)),
    66   ("tool", ("isatt", K check_tool, true)),
    67   ("file", ("isatt", K (File.exists o Path.explode), true)),
    68   ("theory", ("", K ThyInfo.known_thy, true)) 
    69   ];
    70 
    71 in
    72 
    73 fun decode_link ctxt (kind,index,logic,name) =
    74   let
    75   val (markup, check, style) = case Symtab.lookup markup_table kind of
    76     SOME x => x
    77   | NONE => ("", false_check, false);
    78   val hyper_name =
    79     "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
    80   val hyper =
    81     enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
    82     index = "def" ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
    83   val idx =
    84     if index = "" then ""
    85     else "\\index" ^ index ^ arg logic ^ arg kind ^ arg name;
    86   in
    87   if check ctxt name then
    88     (idx ^
    89     (Output.output name
    90       |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    91       |> (if ! ThyOutput.quotes then quote else I)
    92       |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    93 	  else hyper o enclose "\\mbox{\\isa{" "}}")), style)
    94   else ("Bad " ^ kind ^ " " ^ name, false)
    95   end;
    96 end;
    97 
    98 val blanks =
    99   Scan.many Symbol.is_blank >> implode;
   100 
   101 val scan_symbol =
   102   $$ ";" || $$ ":"|| $$ "("|| $$ ")"|| $$ "+"|| $$ "|"|| $$ "*"|| $$ "?"|| $$ "\\";
   103 
   104 (* escaped version *)
   105 val scan_link = (* @{kind{_def|_ref (logic) name} *)
   106   let
   107     fun pseudo_antiquote inner_scan = ($$ "@" ^^ $$ "{") |-- inner_scan --| (blanks -- $$ "}");
   108     fun parens scan = $$ "(" |-- scan --| $$ ")";
   109     fun opt_quotes scan = $$ "'" |-- scan --| $$ "'" || scan;
   110     val letters = Scan.many Symbol.is_letter >> implode;
   111     val kind_name = letters;
   112     val opt_kind_type = Scan.optional (
   113       $$ "_" |-- (Scan.this_string "def" || Scan.this_string "ref")) "";
   114     val logic_name = letters;
   115     val escaped_singlequote = $$ "\\" |-- $$ "'";
   116     val text = Scan.repeat (Scan.one Symbol.is_letter || escaped_singlequote) >> implode;
   117   in
   118    pseudo_antiquote (
   119     kind_name -- opt_kind_type --
   120     (blanks |-- Scan.optional ( parens logic_name ) "") --
   121     (blanks |-- opt_quotes text) )
   122     >> (fn (((kind,index),logic),name) => (kind, index, logic, name))
   123 end;
   124 
   125 (* escaped version *)
   126 fun scan_identifier ctxt = 
   127   let fun is_identifier_start s =
   128     Symbol.is_letter s orelse
   129     s = "_"
   130   fun is_identifier_rest s =
   131     Symbol.is_letter s orelse
   132     Symbol.is_digit s orelse
   133     s = "_" orelse
   134     s = "."
   135   in
   136   (Scan.one is_identifier_start :::
   137     Scan.repeat (Scan.one is_identifier_rest || ($$ "\\" |-- $$ "'"))
   138   ) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||
   139   scan_link >> (decode_link ctxt) >>
   140     (fn (txt, style) =>
   141 	if style then Special_Identifier(txt)
   142 	else Identifier(txt))
   143 end;
   144 
   145 fun scan_anot ctxt =
   146   let val scan_anot =
   147     Scan.many (fn s =>
   148       s <> "\n" andalso
   149       s <> "\t" andalso
   150       s <> "]" andalso
   151       Symbol.is_regular s) >> implode
   152   in
   153   $$ "[" |-- scan_link --| $$ "]" >> (fst o (decode_link ctxt)) ||
   154   $$ "[" |-- scan_anot --| $$ "]" >> Output.output
   155 end;
   156 
   157 (* escaped version *)
   158 fun scan_text ctxt =
   159   let
   160     val text_sq =
   161       Scan.repeat (
   162         Scan.one (fn s =>
   163 	  s <> "\n" andalso
   164 	  s <> "\t" andalso
   165 	  s <> "'" andalso
   166 	  s <> "\\" andalso
   167 	  Symbol.is_regular s) ||
   168 	($$ "\\" |-- $$ "'")
   169       ) >> implode
   170   fun quoted scan = $$ "'" |-- scan --| $$ "'";
   171   in
   172   quoted scan_link >> (fst o (decode_link ctxt)) ||
   173   quoted text_sq >> (enclose "\\isa{" "}" o Output.output)
   174 end;
   175 
   176 fun scan_rail ctxt =
   177   Scan.repeat ( blanks |-- (
   178     scan_identifier ctxt ||
   179     scan_anot ctxt >> Anot ||
   180     scan_text ctxt >> Text ||
   181     scan_symbol >> Symbol)
   182   ) --| blanks;
   183 
   184 fun lex_rail txt ctxt = (* Symbol_Pos fuer spaeter durchgereicht *)
   185   Symbol.scanner "Malformed rail-declaration" (scan_rail ctxt) (map fst (Symbol_Pos.explode txt));
   186 
   187 val lex = lex_rail;
   188 
   189 datatype id_kind = UNKNOWN | TOKEN | TERM | NTERM;
   190 
   191 datatype id_type =
   192   Id of string * id_kind |
   193   Null_Id;
   194 
   195 datatype body_kind =
   196   CAT | BAR | PLUS |
   197   CR | EMPTY | ANNOTE | IDENT | STRING |
   198   Null_Kind;
   199 
   200 datatype body_type =	
   201   Body of body_kind * string * string * id_type * body_type list |
   202   Body_Pos of body_kind * string * string * id_type * body_type list * int * int |
   203   Empty_Body |
   204   Null_Body;
   205 
   206 datatype rule = 
   207   Rule of id_type * body_type;
   208 
   209 fun new_id id kind = Id (id, kind);
   210 
   211 fun is_empty (Body(kind,_,_,_,_)) = kind = EMPTY;
   212 
   213 fun new_body (kind, Null_Body, Null_Body) = Body (kind, "", "", Null_Id, [])
   214   | new_body (kind, body1, body2) = Body (kind, "", "", Null_Id, body1 :: [body2]);
   215 
   216 fun is_kind_of kind (Body(bodyKind,_,_,_,_)) = kind = bodyKind
   217   | is_kind_of _ _ = false;
   218 
   219 fun add_list (Body(kind, text, annot, id, bodies), body) =
   220   Body(kind, text, annot, id, bodies @ [body]);
   221 
   222 fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) = 
   223       Body(kind, text, annot, id, bodies1 @ bodies2);
   224 
   225 fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) =
   226   if kind = kind1 andalso kind <> BAR then
   227     if kind = kind2 then
   228       cat_body_lists(body1, body2)
   229     else (* kind <> kind2 *)
   230       add_list(body1, body2)
   231   else (* kind <> kind1 orelse kind = BAR *)
   232     if kind = kind2 then
   233       cat_body_lists(add_list(new_body(kind,Null_Body,Null_Body), body1), body2)
   234     else (* kind <> kind2 *)
   235       add_list(add_list(new_body(kind,Null_Body,Null_Body), body1), body2);
   236 
   237 fun rev_body (body as Body (kind, text, annot, id, [])) = body
   238   | rev_body (Body (CAT, text, annot, id, bodies)) =
   239       Body(CAT, text, annot, id, map rev_body (rev bodies))
   240   | rev_body (Body (kind, text, annot, id, bodies)) =
   241       Body(kind, text, annot, id, map rev_body bodies)
   242   | rev_body body = body;
   243 
   244 fun set_body_text text (Body(k,_,a,i,b)) = Body(k,text,a,i,b);
   245 fun set_body_anot anot (Body(k,t,_,i,b)) = Body(k,t,anot,i,b);
   246 fun set_body_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TOKEN,b);
   247 fun set_body_special_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TERM,b);
   248 
   249 
   250 fun mk_eof _ = EOF;
   251 fun is_eof s = s = EOF;
   252 val stopper = Scan.stopper mk_eof is_eof;
   253 
   254 (* TODO: change this, so the next or next two tokens are printed *)
   255 fun lex_err msg (cs, _) = "rail grammar error: " ^ msg cs;
   256 fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
   257 fun $$$ tok = Scan.one (is_ tok);
   258 
   259 
   260 local
   261 fun new_bar_body([], body2) = body2
   262   | new_bar_body(body1::bodies, body2) =
   263       add_body(BAR, body1, new_bar_body(bodies, body2));
   264 
   265 fun new_cat_body(body::[]) = body
   266   | new_cat_body(body1::bodies) = add_body(CAT, body1, new_cat_body(bodies));
   267 
   268 fun new_annote_body (Anot anot) =
   269   set_body_text anot (new_body(ANNOTE, Empty_Body, Empty_Body));
   270 
   271 fun new_text_annote_body (Text text, Anot anot) =
   272   set_body_anot anot (set_body_text text (new_body(STRING, Empty_Body, Empty_Body)));
   273 
   274 fun new_ident_body (Identifier ident, Anot anot) =
   275       set_body_anot anot (set_body_ident ident (new_body(IDENT, Empty_Body, Empty_Body)))
   276   | new_ident_body (Special_Identifier ident, Anot anot) =
   277       set_body_anot anot (set_body_special_ident ident (new_body(IDENT, Empty_Body, Empty_Body)));
   278 
   279 val new_empty_body = new_body(EMPTY, Null_Body, Null_Body);
   280 in
   281 
   282 fun parse_body x =
   283   (
   284   Scan.repeat1 (parse_body0 --| $$$ "|") -- !!! "body0 expected" (parse_body0) >>
   285     new_bar_body ||
   286   parse_body0
   287   ) x
   288 and parse_body0 x =
   289   (
   290   Scan.one is_anot -- !!! "body1 expected" (parse_body1) >>
   291     (fn (anot, body) => add_body(CAT, new_annote_body(anot), body))  ||
   292   parse_body1
   293   ) x
   294 and parse_body1 x =
   295   (
   296   parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>
   297     (fn (body1, body2) =>
   298       if is_empty body2 then
   299 	add_body(PLUS, new_empty_body, rev_body body1)
   300       else
   301 	add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
   302   parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >> 
   303     (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
   304   parse_body2e
   305   ) x
   306 and parse_body2e x =
   307   (
   308   parse_body2 ||
   309   (fn toks => (new_empty_body, toks))
   310   ) x
   311 and parse_body2 x =
   312   (
   313   Scan.repeat1 (parse_body3) >> new_cat_body
   314   ) x
   315 and parse_body3 x =
   316   (
   317   parse_body4 --| $$$ "?" >> (fn body => new_body (BAR, new_empty_body, body) ) ||
   318   parse_body4
   319   ) x
   320 and parse_body4e x =
   321   (
   322   parse_body4 ||
   323   (fn toks => (new_empty_body, toks))
   324   ) x
   325 and parse_body4 x =
   326   (
   327   $$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") ||
   328   Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
   329     (fn (text, anot) => new_text_annote_body (text,anot)) ||    
   330   Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
   331     (fn (id, anot) => new_ident_body (id,anot)) ||
   332   $$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body))
   333   ) x;
   334 end;
   335 
   336 fun new_named_rule (Identifier name, body) = Rule(Id(name, UNKNOWN), body)
   337   | new_named_rule (Special_Identifier name, body) = Rule(Id(name, UNKNOWN), body);
   338 fun new_anonym_rule body = Rule(Null_Id, body);
   339 
   340 val parse_rule =
   341   (Scan.one (is_identifier) -- ($$$ ":" |-- !!! "body expected" (parse_body)) ) >>
   342     new_named_rule ||
   343   parse_body >> new_anonym_rule;
   344 
   345 val parse_rules =
   346   Scan.repeat ( parse_rule --| $$$ ";") @@@ Scan.single parse_rule;
   347 
   348 fun parse_rail s =
   349   Scan.read stopper parse_rules s;
   350 
   351 val parse = parse_rail;
   352 
   353 fun getystart (Body_Pos(_,_,_,_,_,ystart,_)) = ystart;
   354 fun getynext (Body_Pos(_,_,_,_,_,_,ynext)) = ynext;
   355 
   356 fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =
   357   let fun max (x,y) = if x > y then x else y
   358     fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =
   359 	  Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
   360     fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)
   361       | pos_bodies_cat (x::xs, ystart, ynext, liste) =
   362 	  if is_kind_of CR x then
   363 	      (case set_body_position(x, ystart, ynext+1) of
   364 		body as Body_Pos(_,_,_,_,_,_,ynext1) =>
   365 		  pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
   366 	      )
   367 	  else
   368 	      (case position_body(x, ystart) of
   369 		body as Body_Pos(_,_,_,_,_,_,ynext1) =>
   370 		  pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
   371 	      )
   372     fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)
   373       | pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =
   374 	  (case position_body(x, ystart) of
   375 	    body as Body_Pos(_,_,_,_,_,_,ynext1) =>
   376 	      pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
   377 	  )
   378   in
   379   (case kind of
   380     CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of
   381 	      (bodiesPos, ynext) =>
   382 		Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   383   | BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
   384 	      (bodiesPos, ynext) =>
   385 		Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   386   | PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
   387 	      (bodiesPos, ynext) =>
   388 		Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
   389   | CR => set_body_position(body, ystart, ystart+3)
   390   | EMPTY => set_body_position(body, ystart, ystart+1)
   391   | ANNOTE => set_body_position(body, ystart, ystart+1)
   392   | IDENT => set_body_position(body, ystart, ystart+1)
   393   | STRING => set_body_position(body, ystart, ystart+1)
   394   )
   395   end;
   396 
   397 fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""
   398   | format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =
   399     let fun format_bodies([]) = ""
   400 	  | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
   401     in
   402       format_bodies(bodies)
   403     end
   404   | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) = 
   405     let fun format_bodies([]) = "\\rail@endbar\n"
   406 	  | format_bodies(x::xs) =
   407 	      "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
   408 	      format_body(x, "") ^ format_bodies(xs)
   409     in
   410       "\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))
   411     end
   412   | format_body (Body_Pos(PLUS,_,_,_,x::y::xs,_,_),cent) =
   413       "\\rail@plus\n" ^ format_body(x, cent) ^
   414       "\\rail@nextplus{" ^ string_of_int(getystart(y)) ^ "}\n" ^
   415       format_body(y, "c") ^
   416       "\\rail@endplus\n"
   417   | format_body (Body_Pos(ANNOTE,text,_,_,_,_,_),cent) =
   418       "\\rail@annote[" ^ text ^ "]\n"
   419   | format_body (Body_Pos(IDENT,_,annot,Id(name,TERM),_,_,_),cent) =
   420       "\\rail@" ^ cent ^ "token{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"
   421   | format_body (Body_Pos(IDENT,_,annot,Id(name,_),_,_,_),cent) =
   422       "\\rail@" ^ cent ^ "nont{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"
   423   | format_body (Body_Pos(CR,_,_,_,_,_,ynext),cent) =
   424       "\\rail@cr{" ^ string_of_int(ynext) ^ "}\n"
   425   | format_body (Body_Pos(STRING,text,annot,_,_,_,_),cent) =
   426       "\\rail@" ^ cent ^ "term{" ^ text ^ "}[" ^ annot ^ "]\n"
   427   | format_body _ =
   428       "\\rail@unknown\n";
   429 
   430 fun out_body (Id(name,_), body) =
   431   let val bodyPos as Body_Pos(_,_,_,_,_,_,ynext) = position_body(body,0)
   432   in
   433     "\\rail@begin{" ^ string_of_int(ynext) ^ "}{" ^ name ^ "}\n" ^
   434     format_body(bodyPos,"") ^
   435     "\\rail@end\n"
   436   end
   437   | out_body (Null_Id, body) = out_body (Id("", UNKNOWN), body);
   438 
   439 fun out_rule (Rule(id, body)) =
   440   if is_empty body then ""
   441   else out_body (id, body);
   442 
   443 fun out_rules ([]) = ""
   444   | out_rules (rule::rules) = out_rule rule ^ out_rules rules;
   445 
   446 val output_no_rules =
   447   "\\rail@begin{1}{}\n" ^
   448   "\\rail@setbox{\\bfseries ???}\n" ^
   449   "\\rail@oval\n" ^
   450   "\\rail@end\n";
   451 
   452 
   453 fun print (SOME rules) =
   454     "\\begin{railoutput}\n" ^
   455     out_rules rules ^
   456     "\\end{railoutput}\n"
   457   | print (NONE) =
   458     "\\begin{railoutput}\n" ^
   459     output_no_rules ^
   460     "\\end{railoutput}\n";
   461 
   462 fun process txt ctxt =
   463   lex txt ctxt
   464   |> parse
   465   |> print;
   466 
   467 val _ = ThyOutput.antiquotation "rail" (Scan.lift ( OuterParse.position Args.name ))
   468   (fn {context = ctxt,...} => fn txt => process txt ctxt);