export_theory
Theory.export_theory : unit -> unit
Write a theory segment to disk.
If the Globals.interactive flag is false, an invocation
export_theory() saves the current theory segment to disk. All parents,
definitions, axioms, and stored theorems of the segment are saved in
such a way that, when the theory is loaded from disk in a later session,
the full theory in place at the time export_theory was called is
re-instated.
If the Globals.interactive flag is true, the call export_theory()
does nothing, returning unit () instantly.
If the current theory segment is named thy, then export_theory()
will create ML files thyTheory.sig and thyTheory.sml, in the current
directory at the time export_theory is invoked. These files need to be
compiled before they become usable. In the standard way of doing things,
the Holmake facility will handle this task.
Once a theory segment has been exported and compiled, it is available for use. It can be brought into an interactive proof session via
load "thyTheory";
When the segment is loaded, its parents, axioms, theorems, and definitions are incorporated into the current theory (recall that this notion is different than the current theory segment).
Failure
A call to export_theory may fail if the disk file cannot be opened. A
call to export_theory will also fail if some bindings are such that
the name of the binding is not a valid ML identifier. In that case,
export_theory will report all such bad names. These can be changed
with set_MLname, and then export_theory may be attempted again.
Example
save_thm("foo", REFL “x:bool”);
Globals.interactive := false;
export_theory();
(These calls are not evaluated by polyscripter when this entry is
rendered: actually running export_theory() freezes the
polyscripter session's current theory segment and breaks every
subsequent Definition / Theorem example.)
Comments
Note that export_theory exports the state of the theory (which can
include other user-definable data in addition to the logical content
(theorems, definitions, etc.), but not the state of the SML session.
When theories are developed interactively, the interactive flag will
typically be set to true; preventing export_theory() from doing
anything in this situation reserves special behaviours for when theories
are built with Holmake.
See also
Theory.new_theory,
Theory.adjoin_to_theory,
Theory.set_MLname