src/Pure/Isar/isar_output.ML
author wenzelm
Thu Apr 07 09:26:48 2005 +0200 (2005-04-07 ago)
changeset 15666 5c5925dc4921
parent 15570 8d8c70b41bab
child 15880 d6aa6c707acf
permissions -rw-r--r--
Scan.peek;
     1 (*  Title:      Pure/Isar/isar_output.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar theory output.
     6 *)
     7 
     8 signature ISAR_OUTPUT =
     9 sig
    10   val display: bool ref
    11   val quotes: bool ref
    12   val indent: int ref
    13   val source: bool ref
    14   val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
    15   val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
    16   val print_antiquotations: unit -> unit
    17   val boolean: string -> bool
    18   val integer: string -> int
    19   val args: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    20     (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
    21   datatype markup = Markup | MarkupEnv | Verbatim
    22   val interest_level: int ref
    23   val hide_commands: bool ref
    24   val add_hidden_commands: string list -> unit
    25   val modes: string list ref
    26   val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string
    27   val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
    28     Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
    29       (Toplevel.transition * (Toplevel.state -> Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
    30   val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    31     Proof.context -> 'a -> string
    32 end;
    33 
    34 structure IsarOutput: ISAR_OUTPUT =
    35 struct
    36 
    37 structure T = OuterLex;
    38 structure P = OuterParse;
    39 
    40 
    41 
    42 (** global references -- defaults for options **)
    43 
    44 val locale = ref "";
    45 val display = ref false;
    46 val quotes = ref false;
    47 val indent = ref 0;
    48 val source = ref false;
    49 val break = ref false;
    50 
    51 
    52 
    53 (** maintain global commands **)
    54 
    55 local
    56 
    57 val global_commands =
    58   ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
    59 
    60 val global_options =
    61   ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
    62 
    63 
    64 fun add_item kind (tab, (name, x)) =
    65  (if is_none (Symtab.lookup (tab, name)) then ()
    66   else warning ("Redefined antiquotation output " ^ kind ^ ": " ^ quote name);
    67   Symtab.update ((name, x), tab));
    68 
    69 fun add_items kind xs tab = Library.foldl (add_item kind) (tab, xs);
    70 
    71 in
    72 
    73 val add_commands = Library.change global_commands o (add_items "command");
    74 val add_options = Library.change global_options o (add_items "option");
    75 
    76 fun command src =
    77   let val ((name, _), pos) = Args.dest_src src in
    78     (case Symtab.lookup (! global_commands, name) of
    79       NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
    80     | SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
    81   end;
    82 
    83 fun option (name, s) f () =
    84   (case Symtab.lookup (! global_options, name) of
    85     NONE => error ("Unknown antiquotation option: " ^ quote name)
    86   | SOME opt => opt s f ());
    87 
    88 fun options [] f = f
    89   | options (opt :: opts) f = option opt (options opts f);
    90 
    91 
    92 fun print_antiquotations () =
    93  [Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))),
    94   Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
    95  |> Pretty.chunks |> Pretty.writeln;
    96 
    97 end;
    98 
    99 
   100 
   101 (** syntax of antiquotations **)
   102 
   103 (* option values *)
   104 
   105 fun boolean "" = true
   106   | boolean "true" = true
   107   | boolean "false" = false
   108   | boolean s = error ("Bad boolean value: " ^ quote s);
   109 
   110 fun integer s =
   111   let
   112     fun int ss =
   113       (case Library.read_int ss of (i, []) => i
   114       | _ => error ("Bad integer value: " ^ quote s));
   115   in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
   116 
   117 
   118 (* args syntax *)
   119 
   120 fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
   121   Args.syntax "antiquotation" scan;
   122 
   123 fun args scan f src state : string =
   124   let
   125     val ctxt0 =
   126       if ! locale = "" then Toplevel.context_of state
   127       else #3 (Locale.read_context_statement (SOME (! locale)) [] []
   128         (ProofContext.init (Toplevel.theory_of state)));
   129     val (ctxt, x) = syntax scan src ctxt0;
   130   in f src ctxt x end;
   131 
   132 
   133 (* outer syntax *)
   134 
   135 local
   136 
   137 val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
   138 val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
   139 
   140 val antiq = P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof
   141   >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
   142 
   143 fun antiq_args_aux keyword_lexicon (str, pos) =
   144   Source.of_string str
   145   |> Symbol.source false
   146   |> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos
   147   |> T.source_proper
   148   |> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) NONE
   149   |> Source.exhaust;
   150 
   151 in
   152 
   153 fun antiq_args lex (s, pos) =
   154   (case antiq_args_aux lex (s, pos) of [x] => x | _ => raise ERROR) handle ERROR =>
   155     error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos);
   156 
   157 end;
   158 
   159 
   160 (* eval_antiquote *)
   161 
   162 val modes = ref ([]: string list);
   163 
   164 fun eval_antiquote lex state (str, pos) =
   165   let
   166     fun expand (Antiquote.Text s) = s
   167       | expand (Antiquote.Antiq x) =
   168           let val (opts, src) = antiq_args lex x in
   169             options opts (fn () => command src state) ();  (*preview errors!*)
   170             Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode)
   171               (options opts (fn () => command src state)) ()
   172           end;
   173     val ants = Antiquote.antiquotes_of (str, pos);
   174   in
   175     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
   176       error ("Cannot expand antiquotations at top-level" ^ Position.str_of pos)
   177     else implode (map expand ants)
   178   end;
   179 
   180 
   181 
   182 (** present theory source **)
   183 
   184 (* present_tokens *)
   185 
   186 val interest_level = ref 0;
   187 
   188 val hide_commands = ref true;
   189 val hidden_commands = ref ([] : string list);
   190 
   191 fun add_hidden_commands cmds = (hidden_commands := !hidden_commands @ cmds);
   192 
   193 fun is_proof state = (case Toplevel.node_of state of
   194   Toplevel.Theory _ => false | _ => true) handle Toplevel.UNDEF => false;
   195 
   196 fun is_newline (Latex.Basic tk, _) = T.is_newline tk
   197   | is_newline _ = false;
   198 
   199 fun is_hidden (Latex.Basic tk, _) =
   200       T.is_kind T.Command tk andalso T.val_of tk mem !hidden_commands
   201   | is_hidden _ = false;
   202 
   203 fun filter_newlines toks = (case List.mapPartial
   204     (fn (tk, i) => if is_newline tk then SOME tk else NONE) toks of
   205   [] => [] | [tk] => [tk] | _ :: toks' => toks');
   206 
   207 fun present_tokens lex (flag, toks) state state' =
   208   Buffer.add (case flag of NONE => "" | SOME b => Latex.flag_markup b) o
   209    ((if !hide_commands andalso exists (is_hidden o fst) toks then []
   210      else if !hide_commands andalso is_proof state then
   211        if is_proof state' then [] else filter_newlines toks
   212      else List.mapPartial (fn (tk, i) =>
   213        if i > ! interest_level then NONE else SOME tk) toks)
   214     |> map (apsnd (eval_antiquote lex state'))
   215     |> Latex.output_tokens
   216     |> Buffer.add);
   217 
   218 
   219 (* parse_thy *)
   220 
   221 datatype markup = Markup | MarkupEnv | Verbatim;
   222 
   223 local
   224 
   225 val opt_newline = Scan.option (Scan.one T.is_newline);
   226 
   227 fun check_level i =
   228   if i > 0 then Scan.succeed ()
   229   else Scan.fail_with (K "Bad nesting of meta-comments");
   230 
   231 val ignore =
   232   Scan.depend (fn i => opt_newline |-- P.position (Scan.one T.is_begin_ignore) >> pair (i + 1)) ||
   233   Scan.depend (fn i => P.position (Scan.one T.is_end_ignore) --|
   234     (opt_newline -- check_level i) >> pair (i - 1));
   235 
   236 val ignore_cmd = Scan.state -- ignore
   237   >> (fn (i, (x, pos)) => (false, (NONE, ((Latex.Basic x, ("", pos)), i))));
   238 
   239 
   240 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
   241 val improper = Scan.any is_improper;
   242 
   243 val improper_keep_indent = Scan.repeat
   244   (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
   245 
   246 val improper_end =
   247   (improper -- P.semicolon) |-- improper_keep_indent ||
   248   improper_keep_indent;
   249 
   250 
   251 val stopper =
   252   ((false, (NONE, ((Latex.Basic (#1 T.stopper), ("", Position.none)), 0))),
   253     fn (_, (_, ((Latex.Basic x, _), _))) => (#2 T.stopper x) | _ => false);
   254 
   255 in
   256 
   257 fun parse_thy markup lex trs src =
   258   let
   259     val text = P.position P.text;
   260     val token = Scan.peek (fn i =>
   261      (improper |-- markup Markup -- P.!!!! (improper |-- text --| improper_end)
   262         >> (fn (x, y) => (true, (SOME true, ((Latex.Markup (T.val_of x), y), i)))) ||
   263       improper |-- markup MarkupEnv -- P.!!!! (improper |-- text --| improper_end)
   264         >> (fn (x, y) => (true, (SOME true, ((Latex.MarkupEnv (T.val_of x), y), i)))) ||
   265       (P.$$$ "--" |-- P.!!!! (improper |-- text))
   266         >> (fn y => (false, (NONE, ((Latex.Markup "cmt", y), i)))) ||
   267       (improper -- markup Verbatim) |-- P.!!!! (improper |-- text --| improper_end)
   268         >> (fn y => (true, (NONE, ((Latex.Verbatim, y), i)))) ||
   269       P.position (Scan.one T.not_eof)
   270         >> (fn (x, pos) => (T.is_kind T.Command x, (SOME false, ((Latex.Basic x, ("", pos)), i))))));
   271 
   272     val body = Scan.any (not o fst andf not o #2 stopper);
   273     val section = body -- Scan.one fst -- body
   274       >> (fn ((b1, c), b2) => (#1 (#2 c), map (snd o snd) (b1 @ (c :: b2))));
   275 
   276     val cmds =
   277       src
   278       |> Source.filter (not o T.is_semicolon)
   279       |> Source.source' 0 T.stopper (Scan.error (Scan.bulk (ignore_cmd || token))) NONE
   280       |> Source.source stopper (Scan.error (Scan.bulk section)) NONE
   281       |> Source.exhaust;
   282   in
   283     if length cmds = length trs then
   284       (trs ~~ map (present_tokens lex) cmds, Buffer.empty)
   285     else error "Messed-up outer syntax for presentation"
   286   end;
   287 
   288 end;
   289 
   290 
   291 
   292 (** setup default output **)
   293 
   294 (* options *)
   295 
   296 val _ = add_options
   297  [("show_types", Library.setmp Syntax.show_types o boolean),
   298   ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
   299   ("show_structs", Library.setmp show_structs o boolean),
   300   ("show_var_qmarks", Library.setmp show_var_qmarks o boolean),
   301   ("long_names", Library.setmp NameSpace.long_names o boolean),
   302   ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
   303   ("locale", Library.setmp locale),
   304   ("display", Library.setmp display o boolean),
   305   ("break", Library.setmp break o boolean),
   306   ("quotes", Library.setmp quotes o boolean),
   307   ("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()),
   308   ("margin", Pretty.setmp_margin o integer),
   309   ("indent", Library.setmp indent o integer),
   310   ("source", Library.setmp source o boolean),
   311   ("goals_limit", Library.setmp goals_limit o integer)];
   312 
   313 
   314 (* commands *)
   315 
   316 fun cond_quote prt =
   317   if ! quotes then Pretty.quote prt else prt;
   318 
   319 fun cond_display prt =
   320   if ! display then
   321     Output.output (Pretty.string_of (Pretty.indent (! indent) prt))
   322     |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   323   else
   324     Output.output ((if ! break then Pretty.string_of else Pretty.str_of) prt)
   325     |> enclose "\\isa{" "}";
   326 
   327 fun cond_seq_display prts =
   328   if ! display then
   329     map (Output.output o Pretty.string_of o Pretty.indent (! indent)) prts
   330     |> separate "\\isasep\\isanewline%\n"
   331     |> implode
   332     |> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   333   else
   334     map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) prts
   335     |> separate "\\isasep\\isanewline%\n"
   336     |> implode
   337     |> enclose "\\isa{" "}";
   338 
   339 fun tweak_line s =
   340   if ! display then s else Symbol.strip_blanks s;
   341 
   342 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
   343 
   344 val pretty_source =
   345   pretty_text o space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
   346 
   347 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
   348 
   349 fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
   350 
   351 fun lhs_of (Const ("==",_) $ t $ _) = t
   352   | lhs_of (Const ("Trueprop",_) $ t) = lhs_of t
   353   | lhs_of (Const ("==>",_) $ _ $ t) = lhs_of t
   354   | lhs_of (_ $ t $ _) = t
   355   | lhs_of _ = error ("Binary operator expected")
   356 
   357 fun pretty_lhs ctxt = pretty_term ctxt o lhs_of o Thm.prop_of;
   358 
   359 fun rhs_of (Const ("==",_) $ _ $ t) = t
   360   | rhs_of (Const ("Trueprop",_) $ t) = rhs_of t
   361   | rhs_of (Const ("==>",_) $ _ $ t) = rhs_of t
   362   | rhs_of (_ $ _ $ t) = t
   363   | rhs_of _ = error ("Binary operator expected")
   364 
   365 fun pretty_rhs ctxt = pretty_term ctxt o rhs_of o Thm.prop_of;
   366 
   367 fun pretty_prf full ctxt thms =    (* FIXME context syntax!? *)
   368   Pretty.chunks (map (ProofSyntax.pretty_proof_of full) thms);
   369 
   370 fun output_with pretty src ctxt x =
   371   let
   372     val prt = pretty ctxt x;      (*always pretty in order to catch errors!*)
   373     val prt' = if ! source then pretty_source src else prt;
   374   in cond_display (cond_quote prt') end;
   375 
   376 fun output_seq_with pretty src ctxt xs =
   377   let
   378     val prts = map (pretty ctxt) xs;   (*always pretty in order to catch errors!*)
   379     val prts' = if ! source then [pretty_source src] else prts;
   380   in cond_seq_display (map cond_quote prts') end;
   381 
   382 fun output_goals main_goal src state = args (Scan.succeed ()) (output_with (fn _ => fn _ =>
   383   Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state
   384       handle Toplevel.UNDEF => error "No proof state")))) src state;
   385 
   386 val _ = add_commands
   387  [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
   388   ("lhs", args Attrib.local_thmss (output_seq_with pretty_lhs)),
   389   ("rhs", args Attrib.local_thmss (output_seq_with pretty_rhs)),
   390   ("prop", args Args.local_prop (output_with pretty_term)),
   391   ("term", args Args.local_term (output_with pretty_term)),
   392   ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
   393   ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
   394   ("goals", output_goals true),
   395   ("subgoals", output_goals false),
   396   ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
   397   ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
   398 
   399 end;