Rob,
The current saveState/loadState saves and restores the whole "state".
It works at the level of the memory and has no knowledge of what the
values represent. When you load "test2.polydb" this simply restores all
global references to the values they had when you saved the state. In
particular the global name space is restored so any declarations made
after the save will be lost. Using a hierarchy doesn't change this
behaviour; using child saved states merely reduces the amount of data
that may need to be written out.
To change this behaviour the process of saving and restoring would need
to be more closely integrated with ML itself. I think it would be
possible to adapt the existing scheme so that instead of treating the
global mutable values as roots the "save" operation would take a list of
pointers and write out the data structure reachable from this, apart
from any data in the parents. The corresponding "load" function would
be passed these pointers once the data structures had been brought into
memory. Using these operations as primitives it ought to be possible to
write a "saveStructure" function that would look up an ML structure in
the global state and write it out.
E.g.
structure S = struct val x = 1 end
PolyML.SaveState.saveStructure("S", "saveS.polydb", 1 (*Child level*));
The subsequently
PolyML.SaveState.loadStructure "saveS.polydb";
S.x;
Here "loadStructure" adds the structure declared within the saved state
to the global name space. Unlike the existing "loadState" function it
would know about the global name space.
There could be similar functions to save functors and signatures and, if
necessary, types, values and fixity.
Since these saved modules would be relative to an existing executable
and, possibly saved states, references to global types would match when
the module was read in and there would be no need to package up type
information explicitly. If a module referred to a type in a different
module, though, the types would be different when the modules were read in.
I haven't thought this through in detail or made any experiments to
check that it would all work but it seems feasible.
David
Rob Arthan wrote:
This may be obvious, but you don't need threads to exhibit this issue. E.g.,
val c1 = ref 1;
PolyML.SaveState.saveState "test1.polydb"; (* save state with c1 = ref 1 *)
val c2 = c1;
(c1 := 2; c2); (* val it = ref 2 *)
PolyML.SaveState.saveChild ("test2.polydb", 1); (* save state with c2 = c1 &
c1 = ref 1 *)
val c3 = c1;
(c1 := 3; c3); (* val it = ref 2 *)
(* load the child test2.polydb *)
val c4 = (PolyML.SaveState.loadState "test2.polydb"; c3);
c1; (* val it = ref 2 *)
c4; (* val it = ref 3 *)
c3; (* Error-Value or constructor (c3) has not been declared *)
(c4 := 9; (c1, c4));(* val it = (ref 2, ref 9) *)
(c1 := 5; (c1, c4));(* val it = (ref 5, ref 9) *)
I would expect it to restore only that part of the state that is referred to
by the child and that does not exist, if that makes sense. I would not have
expected it to undeclare c3 above and would have expected it to leave c1, c2,
c3 and c4 all referencing the same cell.
What would be very useful would be if you could save immediate children of
some state (say each containing some data and some code to operate on that
data) and load them in independently with any pointers into the common
ancestry being resolved in the obvious way.
In ProofPower, for example, we currently have to save and reload the entire
state of the theory hierarchy. It would be nice if theories and associated
proof procedures could be saved separately and only loaded when needed. HOL
IV has some kind of home-rolled way of achieving something that looks like
this under Moscow ML (which effectively doesn't allow data to be saved at
all, but does allow modules of code to be saved separately).
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
