src/Pure/Isar/isar_cmd.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 21003 37492b0062c6
child 21350 6e58289b6685
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
     1 (*  Title:      Pure/Isar/isar_cmd.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Non-logical toplevel commands.
     6 *)
     7 
     8 signature ISAR_CMD =
     9 sig
    10   val welcome: Toplevel.transition -> Toplevel.transition
    11   val init_toplevel: Toplevel.transition -> Toplevel.transition
    12   val exit: Toplevel.transition -> Toplevel.transition
    13   val quit: Toplevel.transition -> Toplevel.transition
    14   val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
    15   val touch_all_thys: Toplevel.transition -> Toplevel.transition
    16   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
    17   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
    18   val kill_thy: string -> Toplevel.transition -> Toplevel.transition
    19   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
    20   val disable_pr: Toplevel.transition -> Toplevel.transition
    21   val enable_pr: Toplevel.transition -> Toplevel.transition
    22   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    23   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
    24   val redo: Toplevel.transition -> Toplevel.transition
    25   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    26   val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition
    27   val kill_proof: Toplevel.transition -> Toplevel.transition
    28   val undo_theory: Toplevel.transition -> Toplevel.transition
    29   val undo: Toplevel.transition -> Toplevel.transition
    30   val kill: Toplevel.transition -> Toplevel.transition
    31   val back: Toplevel.transition -> Toplevel.transition
    32   val use: Path.T -> Toplevel.transition -> Toplevel.transition
    33   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    34   val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
    35   val use_commit: Toplevel.transition -> Toplevel.transition
    36   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
    37   val pwd: Toplevel.transition -> Toplevel.transition
    38   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    39   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    40   val update_thy: string -> Toplevel.transition -> Toplevel.transition
    41   val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
    42   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    43   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    44   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
    45   val print_context: Toplevel.transition -> Toplevel.transition
    46   val print_theory: bool -> Toplevel.transition -> Toplevel.transition
    47   val print_syntax: Toplevel.transition -> Toplevel.transition
    48   val print_facts: Toplevel.transition -> Toplevel.transition
    49   val print_theorems: Toplevel.transition -> Toplevel.transition
    50   val print_locales: Toplevel.transition -> Toplevel.transition
    51   val print_locale: bool * (Locale.expr * Element.context list)
    52     -> Toplevel.transition -> Toplevel.transition
    53   val print_registrations: bool -> string -> Toplevel.transition -> Toplevel.transition
    54   val print_attributes: Toplevel.transition -> Toplevel.transition
    55   val print_simpset: Toplevel.transition -> Toplevel.transition
    56   val print_rules: Toplevel.transition -> Toplevel.transition
    57   val print_induct_rules: Toplevel.transition -> Toplevel.transition
    58   val print_trans_rules: Toplevel.transition -> Toplevel.transition
    59   val print_methods: Toplevel.transition -> Toplevel.transition
    60   val print_antiquotations: Toplevel.transition -> Toplevel.transition
    61   val class_deps: Toplevel.transition -> Toplevel.transition
    62   val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    63   val find_theorems: int option * (bool * string FindTheorems.criterion) list
    64     -> Toplevel.transition -> Toplevel.transition
    65   val print_binds: Toplevel.transition -> Toplevel.transition
    66   val print_cases: Toplevel.transition -> Toplevel.transition
    67   val print_stmts: string list * (thmref * Attrib.src list) list
    68     -> Toplevel.transition -> Toplevel.transition
    69   val print_thms: string list * (thmref * Attrib.src list) list
    70     -> Toplevel.transition -> Toplevel.transition
    71   val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
    72     -> Toplevel.transition -> Toplevel.transition
    73   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
    74   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    75   val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
    76   val add_header: string * Position.T -> Toplevel.transition -> Toplevel.transition
    77   val add_chapter: xstring option * (string * Position.T) ->
    78     Toplevel.transition -> Toplevel.transition
    79   val add_section: xstring option * (string * Position.T) ->
    80     Toplevel.transition -> Toplevel.transition
    81   val add_subsection: xstring option * (string * Position.T) ->
    82     Toplevel.transition -> Toplevel.transition
    83   val add_subsubsection: xstring option * (string * Position.T) ->
    84     Toplevel.transition -> Toplevel.transition
    85   val add_text: xstring option * (string * Position.T) ->
    86     Toplevel.transition -> Toplevel.transition
    87   val add_text_raw: string * Position.T -> Toplevel.transition -> Toplevel.transition
    88   val add_sect: string * Position.T -> Toplevel.transition -> Toplevel.transition
    89   val add_subsect: string * Position.T -> Toplevel.transition -> Toplevel.transition
    90   val add_subsubsect: string * Position.T -> Toplevel.transition -> Toplevel.transition
    91   val add_txt: string * Position.T -> Toplevel.transition -> Toplevel.transition
    92   val add_txt_raw: string * Position.T -> Toplevel.transition -> Toplevel.transition
    93 end;
    94 
    95 structure IsarCmd: ISAR_CMD =
    96 struct
    97 
    98 
    99 (* variations on init / exit *)
   100 
   101 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
   102 val welcome = Toplevel.imperative (writeln o Session.welcome);
   103 
   104 val exit = Toplevel.keep (fn state =>
   105   (Context.set_context (try Toplevel.theory_of state);
   106     writeln "Leaving the Isar loop.  Invoke 'Isar.loop();' to continue.";
   107     raise Toplevel.TERMINATE));
   108 
   109 val quit = Toplevel.imperative quit;
   110 
   111 
   112 (* touch theories *)
   113 
   114 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
   115 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
   116 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
   117 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
   118 fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
   119 
   120 
   121 (* print state *)
   122 
   123 fun with_modes modes e =
   124   Library.setmp print_mode (modes @ ! print_mode) e ();
   125 
   126 fun set_limit _ NONE = ()
   127   | set_limit r (SOME n) = r := n;
   128 
   129 fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
   130   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
   131     with_modes modes (fn () => Toplevel.print_state true state)));
   132 
   133 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
   134 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   135 
   136 
   137 (* history commands *)
   138 
   139 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
   140 
   141 val clear_undos_theory = Toplevel.history o History.clear;
   142 
   143 val redo =
   144   Toplevel.history History.redo o
   145   Toplevel.actual_proof ProofHistory.redo o
   146   Toplevel.skip_proof History.redo;
   147 
   148 fun undos_proof n =
   149   Toplevel.actual_proof (fn prf =>
   150     if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
   151   Toplevel.skip_proof (fn h =>
   152     if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);
   153 
   154 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
   155   if is_some (Toplevel.theory_node (History.current hist)) then raise Toplevel.UNDEF
   156   else (f (); History.undo hist));
   157 
   158 val kill_proof = kill_proof_notify (K ());
   159 
   160 val undo_theory = Toplevel.history (fn hist =>
   161   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
   162 
   163 val undo = Toplevel.kill o undo_theory o undos_proof 1;
   164 val kill = Toplevel.kill o kill_proof;
   165 
   166 val back =
   167   Toplevel.actual_proof ProofHistory.back o
   168   Toplevel.skip_proof (History.apply I);
   169 
   170 
   171 (* use ML text *)
   172 
   173 fun use path = Toplevel.keep (fn state =>
   174   Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
   175 
   176 (*passes changes of theory context*)
   177 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
   178 
   179 (*ignore result theory context*)
   180 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   181   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   182 
   183 val use_commit = Toplevel.imperative Secure.commit;
   184 
   185 
   186 (* current working directory *)
   187 
   188 fun cd path = Toplevel.imperative (fn () => (File.cd path));
   189 val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
   190 
   191 
   192 (* load theory files *)
   193 
   194 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
   195 fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
   196 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
   197 fun update_thy_only name =
   198   Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
   199 
   200 
   201 (* present draft files *)
   202 
   203 fun display_drafts files = Toplevel.imperative (fn () =>
   204   let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
   205   in File.isatool ("display -c " ^ outfile ^ " &"); () end);
   206 
   207 fun print_drafts files = Toplevel.imperative (fn () =>
   208   let val outfile = File.shell_path (Present.drafts "ps" files)
   209   in File.isatool ("print -c " ^ outfile); () end);
   210 
   211 
   212 (* pretty_setmargin *)
   213 
   214 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
   215 
   216 
   217 (* print parts of theory and proof context *)
   218 
   219 val print_context = Toplevel.keep Toplevel.print_state_context;
   220 
   221 fun print_theory verbose = Toplevel.unknown_theory o
   222   Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
   223 
   224 val print_syntax = Toplevel.unknown_theory o
   225   Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
   226   Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of);
   227 
   228 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
   229   ProofContext.setmp_verbose
   230     ProofContext.print_lthms (Context.proof_of (Toplevel.context_of state)));
   231 
   232 val print_theorems_proof = Toplevel.keep (fn state =>
   233   ProofContext.setmp_verbose
   234     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
   235 
   236 val print_theorems_theory = Toplevel.keep (fn state =>
   237   Toplevel.theory_of state |>
   238   (case Option.map Toplevel.theory_node (History.previous (Toplevel.node_history_of state)) of
   239     SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy)
   240   | _ => ProofDisplay.print_theorems));
   241 
   242 val print_theorems = Toplevel.unknown_theory o print_theorems_theory o print_theorems_proof;
   243 
   244 val print_locales = Toplevel.unknown_theory o
   245   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
   246 
   247 fun print_locale (show_facts, (import, body)) = Toplevel.unknown_theory o
   248   Toplevel.keep (fn state =>
   249     Locale.print_locale (Toplevel.theory_of state) show_facts import body);
   250 
   251 fun print_registrations show_wits name = Toplevel.unknown_context o
   252   Toplevel.keep (Toplevel.node_case
   253       (Context.cases (Locale.print_global_registrations show_wits name)
   254         (Locale.print_local_registrations show_wits name))
   255     (Locale.print_local_registrations show_wits name o Proof.context_of));
   256 
   257 val print_attributes = Toplevel.unknown_theory o
   258   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   259 
   260 val print_simpset = Toplevel.unknown_context o
   261   Toplevel.keep (Toplevel.node_case
   262     (Context.cases Simplifier.print_simpset Simplifier.print_local_simpset)
   263     (Simplifier.print_local_simpset o Proof.context_of));
   264 
   265 val print_rules = Toplevel.unknown_context o
   266   Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
   267 
   268 val print_induct_rules = Toplevel.unknown_context o
   269   Toplevel.keep (InductAttrib.print_rules o Toplevel.context_of);
   270 
   271 val print_trans_rules = Toplevel.unknown_context o
   272   Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
   273 
   274 val print_methods = Toplevel.unknown_theory o
   275   Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   276 
   277 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
   278 
   279 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   280   let
   281     val thy = Toplevel.theory_of state;
   282     val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
   283     val {classes, ...} = Sorts.rep_algebra algebra;
   284     fun entry (c, (i, (_, cs))) =
   285       (i, {name = NameSpace.extern space c, ID = c, parents = cs,
   286             dir = "", unfold = true, path = ""});
   287     val gr =
   288       Graph.fold (cons o entry) classes []
   289       |> sort (int_ord o pairself #1) |> map #2;
   290   in Present.display_graph gr end);
   291 
   292 
   293 (* retrieve theorems *)
   294 
   295 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   296   ThmDeps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body state) args));
   297 
   298 fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   299   let
   300     val proof_state = Toplevel.enter_proof_body state;
   301     val ctxt = Proof.context_of proof_state;
   302     val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
   303   in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
   304 
   305 
   306 (* print proof context contents *)
   307 
   308 val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   309   ProofContext.setmp_verbose
   310     ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
   311 
   312 val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   313   ProofContext.setmp_verbose
   314     ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
   315 
   316 
   317 (* print theorems, terms, types etc. *)
   318 
   319 local
   320 
   321 fun string_of_stmts state args =
   322   Proof.get_thmss state args
   323   |> map (Element.pretty_statement (Proof.context_of state) PureThy.lemmaK)
   324   |> Pretty.chunks2 |> Pretty.string_of;
   325 
   326 fun string_of_thms state args =
   327   Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
   328     (Proof.get_thmss state args));
   329 
   330 fun string_of_prfs full state arg =
   331   Pretty.string_of (case arg of
   332       NONE =>
   333         let
   334           val (ctxt, (_, thm)) = Proof.get_goal state;
   335           val {thy, der = (_, prf), ...} = Thm.rep_thm thm;
   336           val prop = Thm.full_prop_of thm;
   337           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
   338         in
   339           ProofContext.pretty_proof ctxt
   340             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
   341         end
   342     | SOME args => Pretty.chunks
   343         (map (ProofContext.pretty_proof_of (Proof.context_of state) full)
   344           (Proof.get_thmss state args)));
   345 
   346 fun string_of_prop state s =
   347   let
   348     val ctxt = Proof.context_of state;
   349     val prop = ProofContext.read_prop ctxt s;
   350   in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
   351 
   352 fun string_of_term state s =
   353   let
   354     val ctxt = Proof.context_of state;
   355     val t = ProofContext.read_term ctxt s;
   356     val T = Term.type_of t;
   357   in
   358     Pretty.string_of
   359       (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
   360         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
   361   end;
   362 
   363 fun string_of_type state s =
   364   let
   365     val ctxt = Proof.context_of state;
   366     val T = ProofContext.read_typ ctxt s;
   367   in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
   368 
   369 fun print_item string_of (modes, arg) = Toplevel.keep (fn state => with_modes modes (fn () =>
   370   writeln (string_of (Toplevel.enter_proof_body state) arg)));
   371 
   372 in
   373 
   374 val print_stmts = print_item string_of_stmts;
   375 val print_thms = print_item string_of_thms;
   376 val print_prfs = print_item o string_of_prfs;
   377 val print_prop = print_item string_of_prop;
   378 val print_term = print_item string_of_term;
   379 val print_type = print_item string_of_type;
   380 
   381 end;
   382 
   383 
   384 (* markup commands *)
   385 
   386 fun add_header s = Toplevel.keep' (fn int => fn state =>
   387   (Toplevel.assert (Toplevel.is_toplevel state);
   388    if int then OuterSyntax.check_text s NONE else ()));
   389 
   390 local
   391 
   392 fun present _ txt true node = OuterSyntax.check_text txt (SOME node)
   393   | present f (s, _) false node =
   394       Context.setmp (try (Toplevel.cases_node Context.theory_of Proof.theory_of) node) f s;
   395 
   396 fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt);
   397 fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt);
   398 
   399 in
   400 
   401 val add_chapter       = present_local_theory Present.section;
   402 val add_section       = present_local_theory Present.section;
   403 val add_subsection    = present_local_theory Present.subsection;
   404 val add_subsubsection = present_local_theory Present.subsubsection;
   405 val add_text          = present_local_theory (K ());
   406 fun add_text_raw txt  = present_local_theory (K ()) (NONE, txt);
   407 val add_txt           = present_proof (K ());
   408 val add_txt_raw       = add_txt;
   409 val add_sect          = add_txt;
   410 val add_subsect       = add_txt;
   411 val add_subsubsect    = add_txt;
   412 
   413 end;
   414 
   415 end;