src/Pure/Isar/isar_cmd.ML
author wenzelm
Sun Jun 05 11:31:21 2005 +0200 (2005-06-05)
changeset 16258 f3d913abf7e5
parent 16193 05413e43d2f3
child 16499 2076b2e6ac58
permissions -rw-r--r--
File.shell_path;
     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: bool -> 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: Toplevel.transition -> Toplevel.transition
    47   val print_syntax: Toplevel.transition -> Toplevel.transition
    48   val print_theorems: Toplevel.transition -> Toplevel.transition
    49   val print_locales: Toplevel.transition -> Toplevel.transition
    50   val print_locale: Locale.expr * Locale.element list
    51     -> Toplevel.transition -> Toplevel.transition
    52   val print_registrations: string -> Toplevel.transition -> Toplevel.transition
    53   val print_attributes: Toplevel.transition -> Toplevel.transition
    54   val print_simpset: Toplevel.transition -> Toplevel.transition
    55   val print_rules: Toplevel.transition -> Toplevel.transition
    56   val print_induct_rules: Toplevel.transition -> Toplevel.transition
    57   val print_trans_rules: Toplevel.transition -> Toplevel.transition
    58   val print_methods: Toplevel.transition -> Toplevel.transition
    59   val print_antiquotations: Toplevel.transition -> Toplevel.transition
    60   val thm_deps: (thmref * Attrib.src list) list ->
    61     Toplevel.transition -> Toplevel.transition
    62   val find_theorems: int option * (bool * string FindTheorems.criterion) list
    63     -> Toplevel.transition -> Toplevel.transition
    64   val print_binds: Toplevel.transition -> Toplevel.transition
    65   val print_lthms: Toplevel.transition -> Toplevel.transition
    66   val print_cases: Toplevel.transition -> Toplevel.transition
    67   val print_thms: string list * (thmref * Attrib.src list) list
    68     -> Toplevel.transition -> Toplevel.transition
    69   val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
    70     -> Toplevel.transition -> Toplevel.transition
    71   val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition
    72   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    73   val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition
    74   val add_header: string * Position.T -> Toplevel.transition -> Toplevel.transition
    75   val add_chapter: string * Position.T -> Toplevel.transition -> Toplevel.transition
    76   val add_section: string * Position.T -> Toplevel.transition -> Toplevel.transition
    77   val add_subsection: string * Position.T -> Toplevel.transition -> Toplevel.transition
    78   val add_subsubsection: string * Position.T -> Toplevel.transition -> Toplevel.transition
    79   val add_text: string * Position.T -> Toplevel.transition -> Toplevel.transition
    80   val add_text_raw: string * Position.T -> Toplevel.transition -> Toplevel.transition
    81   val add_sect: string * Position.T -> Toplevel.transition -> Toplevel.transition
    82   val add_subsect: string * Position.T -> Toplevel.transition -> Toplevel.transition
    83   val add_subsubsect: string * Position.T -> Toplevel.transition -> Toplevel.transition
    84   val add_txt: string * Position.T -> Toplevel.transition -> Toplevel.transition
    85   val add_txt_raw: string * Position.T -> Toplevel.transition -> Toplevel.transition
    86 end;
    87 
    88 structure IsarCmd: ISAR_CMD =
    89 struct
    90 
    91 
    92 (* variations on init / exit *)
    93 
    94 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    95 val welcome = Toplevel.imperative (writeln o Session.welcome);
    96 
    97 val exit = Toplevel.keep (fn state =>
    98   (Context.set_context (try Toplevel.theory_of state);
    99     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
   100     raise Toplevel.TERMINATE));
   101 
   102 val quit = Toplevel.imperative quit;
   103 
   104 
   105 (* touch theories *)
   106 
   107 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
   108 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
   109 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
   110 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
   111 fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
   112 
   113 
   114 (* print state *)
   115 
   116 fun with_modes modes e =
   117   Library.setmp print_mode (modes @ ! print_mode) e ();
   118 
   119 fun set_limit _ NONE = ()
   120   | set_limit r (SOME n) = r := n;
   121 
   122 fun pr (ms, (lim1, lim2)) = Toplevel.keep (fn state =>
   123   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
   124     with_modes ms (fn () => Toplevel.print_state true state)));
   125 
   126 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
   127 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   128 
   129 
   130 (* history commands *)
   131 
   132 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
   133 val clear_undos_theory = Toplevel.history o History.clear;
   134 val redo = Toplevel.history History.redo o Toplevel.proof'' ProofHistory.redo o
   135   Toplevel.skip_proof History.redo;
   136 
   137 fun undos_proof n = Toplevel.proof'' (fn prf =>
   138     if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o
   139   Toplevel.skip_proof (fn h =>
   140     if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h);
   141 
   142 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
   143   (case History.current hist of
   144     Toplevel.Theory _ => raise Toplevel.UNDEF
   145   | _ => (f (); History.undo hist)));
   146 
   147 val kill_proof = kill_proof_notify (K ());
   148 
   149 val undo_theory = Toplevel.history (fn hist =>
   150   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
   151 
   152 val undo = Toplevel.kill o undo_theory o undos_proof 1;
   153 val kill = Toplevel.kill o kill_proof;
   154 val back = Toplevel.proof o ProofHistory.back;
   155 
   156 
   157 (* use ML text *)
   158 
   159 fun use path = Toplevel.keep (fn state =>
   160   Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
   161 
   162 (*passes changes of theory context*)
   163 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
   164 
   165 (*ignore result theory context*)
   166 fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
   167   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   168 
   169 (*commit is dynamically bound!*)
   170 val use_commit = use_mltext false "commit();";
   171 
   172 
   173 (* current working directory *)
   174 
   175 fun cd path = Toplevel.imperative (fn () => (File.cd path));
   176 val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
   177 
   178 
   179 (* load theory files *)
   180 
   181 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
   182 fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
   183 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
   184 fun update_thy_only name =
   185   Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
   186 
   187 
   188 (* present draft files *)
   189 
   190 fun display_drafts files = Toplevel.imperative (fn () =>
   191   let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
   192   in File.isatool ("display -c " ^ outfile ^ " &"); () end);
   193 
   194 fun print_drafts files = Toplevel.imperative (fn () =>
   195   let val outfile = File.shell_path (Present.drafts "ps" files)
   196   in File.isatool ("print -c " ^ outfile); () end);
   197 
   198 
   199 (* pretty_setmargin *)
   200 
   201 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
   202 
   203 
   204 (* print parts of theory and proof context *)
   205 
   206 val print_context = Toplevel.keep Toplevel.print_state_context;
   207 
   208 val print_theory = Toplevel.unknown_theory o
   209   Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
   210 
   211 val print_syntax = Toplevel.unknown_theory o
   212   Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
   213   Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of);
   214 
   215 val print_theorems = Toplevel.unknown_theory o
   216   Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
   217 
   218 val print_locales = Toplevel.unknown_theory o
   219   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
   220 
   221 fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   222   Locale.print_locale (Toplevel.theory_of state) import body);
   223 
   224 fun print_registrations name = Toplevel.unknown_context o
   225   Toplevel.keep (Toplevel.node_case (Locale.print_global_registrations name)
   226     (Locale.print_local_registrations name o Proof.context_of));
   227 
   228 val print_attributes = Toplevel.unknown_theory o
   229   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   230 
   231 val print_simpset = Toplevel.unknown_context o
   232   Toplevel.keep (Toplevel.node_case Simplifier.print_simpset
   233     (Simplifier.print_local_simpset o Proof.context_of));
   234 
   235 val print_rules = Toplevel.unknown_context o
   236   Toplevel.keep (Toplevel.node_case ContextRules.print_global_rules
   237     (ContextRules.print_local_rules o Proof.context_of));
   238 
   239 val print_induct_rules = Toplevel.unknown_context o
   240   Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules
   241     (InductAttrib.print_local_rules o Proof.context_of));
   242 
   243 val print_trans_rules = Toplevel.unknown_context o
   244   Toplevel.keep (Toplevel.node_case Calculation.print_global_rules
   245     (Calculation.print_local_rules o Proof.context_of));
   246 
   247 val print_methods = Toplevel.unknown_theory o
   248   Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   249 
   250 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
   251 
   252 
   253 (* retrieve theorems *)
   254 
   255 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   256   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
   257 
   258 fun find_theorems (opt_lim, spec) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   259   let
   260     val proof_state = Toplevel.enter_forward_proof state;
   261     val ctxt = Proof.context_of proof_state;
   262     val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2);
   263   in FindTheorems.print_theorems ctxt opt_goal opt_lim spec end);
   264 
   265 
   266 (* print proof context contents *)
   267 
   268 val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   269   ProofContext.setmp_verbose
   270     ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
   271 
   272 val print_lthms = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   273   ProofContext.setmp_verbose
   274     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
   275 
   276 val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   277   ProofContext.setmp_verbose
   278     ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
   279 
   280 
   281 (* print theorems / types / terms / props *)
   282 
   283 fun string_of_thms state ms args = with_modes ms (fn () =>
   284   Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
   285     (IsarThy.get_thmss args state)));
   286 
   287 fun string_of_prfs full state ms arg = with_modes ms (fn () =>
   288   Pretty.string_of (case arg of    (* FIXME context syntax!? *)
   289       NONE =>
   290         let
   291           val (_, (_, thm)) = Proof.get_goal state;
   292           val {sign, prop, der = (_, prf), ...} = rep_thm thm;
   293           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
   294         in
   295           ProofSyntax.pretty_proof sign
   296             (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   297         end
   298     | SOME args => Pretty.chunks
   299         (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
   300 
   301 fun string_of_prop state ms s =
   302   let
   303     val ctxt = Proof.context_of state;
   304     val prop = ProofContext.read_prop ctxt s;
   305   in
   306     with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)))
   307   end;
   308 
   309 fun string_of_term state ms s =
   310   let
   311     val ctxt = Proof.context_of state;
   312     val t = ProofContext.read_term ctxt s;
   313     val T = Term.type_of t;
   314   in
   315     with_modes ms (fn () => Pretty.string_of
   316       (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
   317         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
   318   end;
   319 
   320 fun string_of_type state ms s =
   321   let
   322     val ctxt = Proof.context_of state;
   323     val T = ProofContext.read_typ ctxt s;
   324   in with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T))) end;
   325 
   326 fun print_item string_of (x, y) = Toplevel.keep (fn state =>
   327   writeln (string_of (Toplevel.enter_forward_proof state) x y));
   328 
   329 val print_thms = print_item string_of_thms;
   330 fun print_prfs full = print_item (string_of_prfs full);
   331 val print_prop = print_item string_of_prop;
   332 val print_term = print_item string_of_term;
   333 val print_type = print_item string_of_type;
   334 
   335 
   336 (* markup commands *)
   337 
   338 fun add_header s = Toplevel.keep' (fn int => fn state =>
   339   (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
   340     OuterSyntax.check_text s int state));
   341 
   342 local
   343 
   344 fun present_text assert_proof present (s, pos) = Toplevel.keep' (fn int => fn state =>
   345   (if can Toplevel.proof_of state = assert_proof then () else raise Toplevel.UNDEF;
   346     Context.setmp (SOME (Toplevel.theory_of state)) present s;
   347     OuterSyntax.check_text (s, pos) int state;
   348     raise Toplevel.UNDEF));
   349 
   350 fun theory f x = Toplevel.theory I o present_text false f x;
   351 fun proof f x = Toplevel.print o Toplevel.proof (ProofHistory.apply I) o present_text true f x;
   352 
   353 in
   354 
   355 val add_chapter = theory Present.section;
   356 val add_section = theory Present.section;
   357 val add_subsection = theory Present.subsection;
   358 val add_subsubsection = theory Present.subsubsection;
   359 val add_text = theory (K ());
   360 val add_text_raw = add_text;
   361 val add_txt = proof (K ());
   362 val add_txt_raw = add_txt;
   363 val add_sect = add_txt;
   364 val add_subsect = add_txt;
   365 val add_subsubsect = add_txt;
   366 
   367 end;
   368 
   369 end;