]> matita.cs.unibo.it Git - helm.git/commit
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 17:37:05 +0000 (17:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 17:37:05 +0000 (17:37 +0000)
commitf6c887944d48d718f372a57f1609f3d059908aa8
tree4058ae773cbb7538b07790401751dfe43b41cebf
parent13c3708fc59d999727ee214e8ece1f03661a9737
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

Instead of serializing closures (of type status -> status), we now
serialize data. This is achieved by implementing an existential type

       NCicLibrary.Serializer(struct type status end).obj

whose semantics is "\exists 'a. 'a -> status -> status"
and by putting in the dump a list of these existential types.

The current implementation is the type-unsafe one based internally on Obj.magic.
However, the interface is (should be?) type-safe.
Other type-safe implementations could be derived by the ocaml m.l. thread on
existential types. In particular, I remember implementations via:
  - references
  - functors
  - exceptions
  - impredicative encoding via polymorphic methods

This fix allow to change the Matita code without invalidating the library.

(Critical) things still to be done:
 - decompilation
 - refreshment of URIs
16 files changed:
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/nEstatus.ml
helm/software/components/grafite_parser/nEstatus.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_refiner/check.ml
helm/software/components/ng_refiner/nRstatus.ml
helm/software/components/ng_refiner/nRstatus.mli
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/matita/matitaGui.ml
helm/software/matita/matitaWiki.ml
helm/software/matita/matitacLib.ml