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