src/Pure/Isar/isar_cmd.ML
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 12382 8896d7f49422
child 12758 f6aceb9d4b8e
permissions -rw-r--r--
removed unused functionality (weight etc.);
     1 (*  Title:      Pure/Isar/isar_cmd.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Non-logical toplevel commands.
     7 *)
     8 
     9 signature ISAR_CMD =
    10 sig
    11   val welcome: Toplevel.transition -> Toplevel.transition
    12   val init_toplevel: Toplevel.transition -> Toplevel.transition
    13   val exit: Toplevel.transition -> Toplevel.transition
    14   val quit: Toplevel.transition -> Toplevel.transition
    15   val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
    16   val touch_all_thys: Toplevel.transition -> Toplevel.transition
    17   val touch_thy: string -> Toplevel.transition -> Toplevel.transition
    18   val remove_thy: string -> Toplevel.transition -> Toplevel.transition
    19   val kill_thy: string -> Toplevel.transition -> Toplevel.transition
    20   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
    21   val disable_pr: Toplevel.transition -> Toplevel.transition
    22   val enable_pr: Toplevel.transition -> Toplevel.transition
    23   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    24   val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
    25   val redo: Toplevel.transition -> Toplevel.transition
    26   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    27   val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition
    28   val kill_proof: Toplevel.transition -> Toplevel.transition
    29   val undo_theory: Toplevel.transition -> Toplevel.transition
    30   val undo: Toplevel.transition -> Toplevel.transition
    31   val kill: Toplevel.transition -> Toplevel.transition
    32   val back: bool * Comment.text -> Toplevel.transition -> Toplevel.transition
    33   val use: string * Comment.text -> Toplevel.transition -> Toplevel.transition
    34   val use_mltext_theory: string * Comment.text -> Toplevel.transition -> Toplevel.transition
    35   val use_mltext: bool -> string * Comment.text -> Toplevel.transition -> Toplevel.transition
    36   val use_setup: string * Comment.text -> theory -> theory
    37   val use_commit: Toplevel.transition -> Toplevel.transition
    38   val cd: string -> Toplevel.transition -> Toplevel.transition
    39   val pwd: Toplevel.transition -> Toplevel.transition
    40   val use_thy: string -> Toplevel.transition -> Toplevel.transition
    41   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    42   val update_thy: string -> Toplevel.transition -> Toplevel.transition
    43   val update_thy_only: string -> 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 -> Toplevel.transition -> Toplevel.transition
    51   val print_attributes: Toplevel.transition -> Toplevel.transition
    52   val print_rules: Toplevel.transition -> Toplevel.transition
    53   val print_induct_rules: Toplevel.transition -> Toplevel.transition
    54   val print_trans_rules: Toplevel.transition -> Toplevel.transition
    55   val print_methods: Toplevel.transition -> Toplevel.transition
    56   val print_antiquotations: Toplevel.transition -> Toplevel.transition
    57   val print_thms_containing: string list -> Toplevel.transition -> Toplevel.transition
    58   val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
    59   val print_binds: Toplevel.transition -> Toplevel.transition
    60   val print_lthms: Toplevel.transition -> Toplevel.transition
    61   val print_cases: Toplevel.transition -> Toplevel.transition
    62   val print_thms: (string list * (string * Args.src list) list) * Comment.text
    63     -> Toplevel.transition -> Toplevel.transition
    64   val print_prfs: bool -> (string list * (string * Args.src list) list option) * Comment.text
    65     -> Toplevel.transition -> Toplevel.transition
    66   val print_prop: (string list * string) * Comment.text
    67     -> Toplevel.transition -> Toplevel.transition
    68   val print_term: (string list * string) * Comment.text
    69     -> Toplevel.transition -> Toplevel.transition
    70   val print_type: (string list * string) * Comment.text
    71     -> Toplevel.transition -> Toplevel.transition
    72 end;
    73 
    74 structure IsarCmd: ISAR_CMD =
    75 struct
    76 
    77 
    78 (* variations on init / exit *)
    79 
    80 val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    81 val welcome = Toplevel.imperative (writeln o Session.welcome);
    82 
    83 val exit = Toplevel.keep (fn state =>
    84   (Context.set_context (try Toplevel.theory_of state);
    85     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
    86     raise Toplevel.TERMINATE));
    87 
    88 val quit = Toplevel.imperative quit;
    89 
    90 
    91 (* touch theories *)
    92 
    93 fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
    94 val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    95 fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    96 fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
    97 fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
    98 
    99 
   100 (* print state *)
   101 
   102 fun with_modes modes e =
   103   Library.setmp print_mode (modes @ ! print_mode) e ();
   104 
   105 fun set_limit _ None = ()
   106   | set_limit r (Some n) = r := n;
   107 
   108 fun pr (ms, (lim1, lim2)) = Toplevel.keep (fn state =>
   109   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
   110     with_modes ms (fn () => Toplevel.print_state true state)));
   111 
   112 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
   113 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   114 
   115 
   116 (* history commands *)
   117 
   118 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
   119 val clear_undos_theory = Toplevel.history o History.clear;
   120 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
   121 
   122 fun undos_proof n = Toplevel.proof (fn prf =>
   123   if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
   124 
   125 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist =>
   126   (case History.current hist of
   127     Toplevel.Theory _ => raise Toplevel.UNDEF
   128   | Toplevel.Proof _ => (f (); History.undo hist)));
   129 
   130 val kill_proof = kill_proof_notify (K ());
   131 
   132 val undo_theory = Toplevel.history (fn hist =>
   133   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
   134 
   135 val undo = Toplevel.kill o undo_theory o undos_proof 1;
   136 val kill = Toplevel.kill o kill_proof;
   137 
   138 val back = Toplevel.proof o ProofHistory.back o Comment.ignore;
   139 
   140 
   141 (* use ML text *)
   142 
   143 fun use (name, comment_ignore) = Toplevel.keep (fn state =>
   144   Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
   145 
   146 (*passes changes of theory context*)
   147 val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore;
   148 
   149 (*ignore result theory context*)
   150 fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state =>
   151   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
   152 
   153 val use_setup = Context.use_setup o Comment.ignore;
   154 
   155 (*Note: commit is dynamically bound*)
   156 val use_commit = use_mltext false ("commit();", Comment.none);
   157 
   158 
   159 (* current working directory *)
   160 
   161 fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir)));
   162 val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ())));
   163 
   164 
   165 (* load theory files *)
   166 
   167 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
   168 fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
   169 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
   170 fun update_thy_only name =
   171   Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
   172 
   173 
   174 (* pretty_setmargin *)
   175 
   176 fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
   177 
   178 
   179 (* print parts of theory and proof context *)
   180 
   181 val print_context = Toplevel.keep Toplevel.print_state_context;
   182 
   183 val print_theory = Toplevel.unknown_theory o
   184   Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
   185 
   186 val print_syntax = Toplevel.unknown_theory o
   187   Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
   188   Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of);
   189 
   190 val print_theorems = Toplevel.unknown_theory o
   191   Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
   192 
   193 val print_locales = Toplevel.unknown_theory o
   194   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
   195 
   196 fun print_locale name = Toplevel.unknown_theory o
   197   Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) name);
   198 
   199 val print_attributes = Toplevel.unknown_theory o
   200   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);
   201 
   202 val print_rules = Toplevel.unknown_context o
   203   Toplevel.keep (Toplevel.node_case ContextRules.print_global_rules
   204     (ContextRules.print_local_rules o Proof.context_of));
   205 
   206 val print_induct_rules = Toplevel.unknown_context o
   207   Toplevel.keep (Toplevel.node_case InductAttrib.print_global_rules
   208     (InductAttrib.print_local_rules o Proof.context_of));
   209 
   210 val print_trans_rules = Toplevel.unknown_context o
   211   Toplevel.keep (Toplevel.node_case Calculation.print_global_rules
   212     (Calculation.print_local_rules o Proof.context_of));
   213 
   214 val print_methods = Toplevel.unknown_theory o
   215   Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   216 
   217 val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
   218 
   219 fun print_thms_containing ss = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   220   ThmDatabase.print_thms_containing (Toplevel.theory_of state)
   221     (map (ProofContext.read_term (Toplevel.context_of state)) ss));
   222 
   223 fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   224   ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
   225 
   226 
   227 (* print proof context contents *)
   228 
   229 val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   230   ProofContext.setmp_verbose
   231     ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
   232 
   233 val print_lthms = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   234   ProofContext.setmp_verbose
   235     ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state)));
   236 
   237 val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   238   ProofContext.setmp_verbose
   239     ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
   240 
   241 
   242 (* print theorems / types / terms / props *)
   243 
   244 fun string_of_thms state ms args = with_modes ms (fn () =>
   245   Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
   246     (IsarThy.get_thmss args state)));
   247 
   248 fun string_of_prfs full state ms arg = with_modes ms (fn () =>
   249   Pretty.string_of (case arg of    (* FIXME context syntax!? *)
   250       None =>
   251         let
   252           val (_, (_, thm)) = Proof.get_goal state;
   253           val {sign, prop, der = (_, prf), ...} = rep_thm thm;
   254           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
   255         in
   256           ProofSyntax.pretty_proof sign
   257             (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   258         end
   259     | Some args => Pretty.chunks
   260         (map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state))));
   261 
   262 fun string_of_prop state ms s =
   263   let
   264     val ctxt = Proof.context_of state;
   265     val prop = ProofContext.read_prop ctxt s;
   266   in
   267     with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)))
   268   end;
   269 
   270 fun string_of_term state ms s =
   271   let
   272     val ctxt = Proof.context_of state;
   273     val t = ProofContext.read_term ctxt s;
   274     val T = Term.type_of t;
   275   in
   276     with_modes ms (fn () => Pretty.string_of
   277       (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
   278         Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
   279   end;
   280 
   281 fun string_of_type state ms s =
   282   let
   283     val ctxt = Proof.context_of state;
   284     val T = ProofContext.read_typ ctxt s;
   285   in with_modes ms (fn () => Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T))) end;
   286 
   287 fun print_item string_of (x, y) = Toplevel.keep (fn state =>
   288   writeln (string_of (Toplevel.enter_forward_proof state) x y));
   289 
   290 val print_thms = print_item string_of_thms o Comment.ignore;
   291 fun print_prfs full = print_item (string_of_prfs full) o Comment.ignore;
   292 val print_prop = print_item string_of_prop o Comment.ignore;
   293 val print_term = print_item string_of_term o Comment.ignore;
   294 val print_type = print_item string_of_type o Comment.ignore;
   295 
   296 
   297 end;