author  wenzelm 
Wed, 05 Dec 2001 03:15:50 +0100  
changeset 12382  8896d7f49422 
parent 12288  c8214e408f35 
child 12758  f6aceb9d4b8e 
permissions  rwrr 
5831  1 
(* Title: Pure/Isar/isar_cmd.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

8807  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5831  5 

6 
Nonlogical toplevel commands. 

7 
*) 

8 

9 
signature ISAR_CMD = 

10 
sig 

7462  11 
val welcome: Toplevel.transition > Toplevel.transition 
12 
val init_toplevel: Toplevel.transition > Toplevel.transition 

5831  13 
val exit: Toplevel.transition > Toplevel.transition 
14 
val quit: Toplevel.transition > Toplevel.transition 

7908  15 
val touch_child_thys: string > Toplevel.transition > Toplevel.transition 
7101  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 

7931  19 
val kill_thy: string > Toplevel.transition > Toplevel.transition 
9731  20 
val pr: string list * (int option * int option) > Toplevel.transition > Toplevel.transition 
8453  21 
val disable_pr: Toplevel.transition > Toplevel.transition 
22 
val enable_pr: Toplevel.transition > Toplevel.transition 

6734  23 
val cannot_undo: string > Toplevel.transition > Toplevel.transition 
7729  24 
val clear_undos_theory: int > Toplevel.transition > Toplevel.transition 
6742  25 
val redo: Toplevel.transition > Toplevel.transition 
26 
val undos_proof: int > Toplevel.transition > Toplevel.transition 

7936  27 
val kill_proof_notify: (unit > unit) > Toplevel.transition > Toplevel.transition 
6742  28 
val kill_proof: Toplevel.transition > Toplevel.transition 
29 
val undo_theory: Toplevel.transition > Toplevel.transition 

6686  30 
val undo: Toplevel.transition > Toplevel.transition 
8498  31 
val kill: Toplevel.transition > Toplevel.transition 
9273  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 

5831  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 

6694  41 
val use_thy_only: string > Toplevel.transition > Toplevel.transition 
6195  42 
val update_thy: string > Toplevel.transition > Toplevel.transition 
7101  43 
val update_thy_only: string > Toplevel.transition > Toplevel.transition 
7124  44 
val pretty_setmargin: int > Toplevel.transition > Toplevel.transition 
7308  45 
val print_context: Toplevel.transition > Toplevel.transition 
5831  46 
val print_theory: Toplevel.transition > Toplevel.transition 
47 
val print_syntax: Toplevel.transition > Toplevel.transition 

5880  48 
val print_theorems: Toplevel.transition > Toplevel.transition 
12060  49 
val print_locales: Toplevel.transition > Toplevel.transition 
12288  50 
val print_locale: Locale.expr > Toplevel.transition > Toplevel.transition 
5831  51 
val print_attributes: Toplevel.transition > Toplevel.transition 
12382  52 
val print_rules: Toplevel.transition > Toplevel.transition 
11666  53 
val print_induct_rules: Toplevel.transition > Toplevel.transition 
9219  54 
val print_trans_rules: Toplevel.transition > Toplevel.transition 
5831  55 
val print_methods: Toplevel.transition > Toplevel.transition 
9219  56 
val print_antiquotations: Toplevel.transition > Toplevel.transition 
11017  57 
val print_thms_containing: string list > Toplevel.transition > Toplevel.transition 
9454  58 
val thm_deps: (string * Args.src list) list > Toplevel.transition > Toplevel.transition 
5831  59 
val print_binds: Toplevel.transition > Toplevel.transition 
60 
val print_lthms: Toplevel.transition > Toplevel.transition 

8369  61 
val print_cases: Toplevel.transition > Toplevel.transition 
10581  62 
val print_thms: (string list * (string * Args.src list) list) * Comment.text 
63 
> Toplevel.transition > Toplevel.transition 

12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

64 
val print_prfs: bool > (string list * (string * Args.src list) list option) * Comment.text 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

65 
> Toplevel.transition > Toplevel.transition 
10581  66 
val print_prop: (string list * string) * Comment.text 
8463  67 
> Toplevel.transition > Toplevel.transition 
10581  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 

5831  72 
end; 
73 

74 
structure IsarCmd: ISAR_CMD = 

75 
struct 

76 

77 

7462  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); 

5831  82 

83 
val exit = Toplevel.keep (fn state => 

84 
(Context.set_context (try Toplevel.theory_of state); 

6635  85 
writeln "Leaving the Isar loop. Invoke 'loop();' to restart."; 
5831  86 
raise Toplevel.TERMINATE)); 
87 

88 
val quit = Toplevel.imperative quit; 

89 

7101  90 

91 
(* touch theories *) 

92 

7908  93 
fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name); 
7101  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); 

7931  97 
fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name); 
7101  98 

5831  99 

8453  100 
(* print state *) 
101 

8463  102 
fun with_modes modes e = 
103 
Library.setmp print_mode (modes @ ! print_mode) e (); 

104 

9731  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; 

8886  110 
with_modes ms (fn () => Toplevel.print_state true state))); 
8453  111 

112 
val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true); 

113 
val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false); 

114 

115 

6686  116 
(* history commands *) 
117 

6734  118 
fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); 
7729  119 
val clear_undos_theory = Toplevel.history o History.clear; 
6686  120 
val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo; 
121 

6742  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); 

6686  124 

7936  125 
fun kill_proof_notify (f: unit > unit) = Toplevel.history (fn hist => 
6742  126 
(case History.current hist of 
127 
Toplevel.Theory _ => raise Toplevel.UNDEF 

7936  128 
 Toplevel.Proof _ => (f (); History.undo hist))); 
129 

130 
val kill_proof = kill_proof_notify (K ()); 

6686  131 

6742  132 
val undo_theory = Toplevel.history (fn hist => 
133 
if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist); 

6686  134 

7413  135 
val undo = Toplevel.kill o undo_theory o undos_proof 1; 
8498  136 
val kill = Toplevel.kill o kill_proof; 
6686  137 

9273  138 
val back = Toplevel.proof o ProofHistory.back o Comment.ignore; 
139 

6686  140 

5831  141 
(* use ML text *) 
142 

9273  143 
fun use (name, comment_ignore) = Toplevel.keep (fn state => 
6264  144 
Context.setmp (try Toplevel.theory_of state) ThyInfo.use name); 
5831  145 

146 
(*passes changes of theory context*) 

9273  147 
val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore; 
5831  148 

149 
(*ignore result theory context*) 

9273  150 
fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state => 
8349
611342539639
moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
wenzelm
parents:
7936
diff
changeset

151 
(Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); 
5831  152 

9273  153 
val use_setup = Context.use_setup o Comment.ignore; 
154 

5831  155 
(*Note: commit is dynamically bound*) 
9273  156 
val use_commit = use_mltext false ("commit();", Comment.none); 
5831  157 

158 

159 
(* current working directory *) 

160 

7790  161 
fun cd dir = Toplevel.imperative (fn () => (File.cd (Path.unpack dir))); 
162 
val pwd = Toplevel.imperative (fn () => writeln (Path.pack (File.pwd ()))); 

5831  163 

164 

165 
(* load theory files *) 

166 

6243  167 
fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name); 
6694  168 
fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name); 
6243  169 
fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name); 
7124  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); 

5831  177 

178 

9513  179 
(* print parts of theory and proof context *) 
5831  180 

7308  181 
val print_context = Toplevel.keep Toplevel.print_state_context; 
9513  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 

12069  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); 

9513  189 

190 
val print_theorems = Toplevel.unknown_theory o 

191 
Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of); 

192 

12060  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 

9513  199 
val print_attributes = Toplevel.unknown_theory o 
200 
Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); 

201 

12382  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 

11666  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 

9513  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 

9219  217 
val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; 
5831  218 

11017  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)); 

7615  222 

9513  223 
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state => 
9454  224 
ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state))); 
225 

5831  226 

227 
(* print proof context contents *) 

228 

9513  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 

12055  235 
ProofContext.print_lthms (Proof.context_of (Toplevel.proof_of state))); 
9513  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))); 

5831  240 

241 

7012  242 
(* print theorems / types / terms / props *) 
5880  243 

9128  244 
fun string_of_thms state ms args = with_modes ms (fn () => 
12055  245 
Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state) 
246 
(IsarThy.get_thmss args state))); 

5895  247 

12125
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

248 
fun string_of_prfs full state ms arg = with_modes ms (fn () => 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

249 
Pretty.string_of (case arg of (* FIXME context syntax!? *) 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

250 
None => 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

251 
let 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

252 
val (_, (_, thm)) = Proof.get_goal state; 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

253 
val {sign, prop, der = (_, prf), ...} = rep_thm thm; 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

254 
val prf' = Proofterm.rewrite_proof_notypes ([], []) prf 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

255 
in 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

256 
ProofSyntax.pretty_proof sign 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

257 
(if full then Reconstruct.reconstruct_proof sign prop prf' else prf') 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

258 
end 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

259 
 Some args => Pretty.chunks 
316d11f760f7
Commands prf and full_prf can now also be used to display proof term
berghofe
parents:
12069
diff
changeset

260 
(map (ProofSyntax.pretty_proof_of full) (IsarThy.get_thmss args state)))); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

261 

9128  262 
fun string_of_prop state ms s = 
5831  263 
let 
12055  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; 

5831  269 

9128  270 
fun string_of_term state ms s = 
5831  271 
let 
12055  272 
val ctxt = Proof.context_of state; 
273 
val t = ProofContext.read_term ctxt s; 

5831  274 
val T = Term.type_of t; 
275 
in 

9128  276 
with_modes ms (fn () => Pretty.string_of 
12055  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)])) 

9128  279 
end; 
5831  280 

9128  281 
fun string_of_type state ms s = 
5831  282 
let 
12055  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; 

9128  286 

287 
fun print_item string_of (x, y) = Toplevel.keep (fn state => 

9454  288 
writeln (string_of (Toplevel.enter_forward_proof state) x y)); 
9128  289 

10581  290 
val print_thms = print_item string_of_thms o Comment.ignore; 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11017
diff
changeset

291 
fun print_prfs full = print_item (string_of_prfs full) o Comment.ignore; 
10581  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; 

5831  295 

296 

297 
end; 