From a18562238677261e3d0b590e046290a14fe62e74 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Oct 2009 11:28:05 +0000 Subject: [PATCH] new ng_library module --- .../METAS/meta.helm-grafite_engine.src | 2 +- .../components/METAS/meta.helm-lexicon.src | 2 +- .../components/METAS/meta.helm-ng_library.src | 5 ++ helm/software/components/Makefile | 2 + .../grafite_engine/grafiteEngine.ml | 7 ++- .../grafite_engine/nCicCoercDeclaration.ml | 2 +- .../components/grafite_parser/nEstatus.ml | 4 +- .../components/grafite_parser/nEstatus.mli | 4 +- helm/software/components/ng_kernel/.depend | 7 --- .../software/components/ng_kernel/.depend.opt | 7 --- helm/software/components/ng_kernel/Makefile | 10 +--- helm/software/components/ng_library/.depend | 2 + .../components/ng_library/.depend.opt | 2 + helm/software/components/ng_library/Makefile | 24 ++++++++ .../{ng_kernel => ng_library}/check.ml | 0 .../{ng_kernel => ng_library}/nCicLibrary.ml | 60 +++++++++++++++---- .../{ng_kernel => ng_library}/nCicLibrary.mli | 25 +++++++- .../{ng_kernel => ng_library}/rt.ml | 0 helm/software/components/ng_refiner/Makefile | 27 --------- .../components/ng_refiner/nRstatus.ml | 43 +------------ .../components/ng_refiner/nRstatus.mli | 33 +--------- helm/software/matita/matitaGui.ml | 2 +- helm/software/matita/matitaWiki.ml | 2 +- helm/software/matita/matitacLib.ml | 2 +- 24 files changed, 123 insertions(+), 151 deletions(-) create mode 100644 helm/software/components/METAS/meta.helm-ng_library.src create mode 100644 helm/software/components/ng_library/.depend create mode 100644 helm/software/components/ng_library/.depend.opt create mode 100644 helm/software/components/ng_library/Makefile rename helm/software/components/{ng_kernel => ng_library}/check.ml (100%) rename helm/software/components/{ng_kernel => ng_library}/nCicLibrary.ml (92%) rename helm/software/components/{ng_kernel => ng_library}/nCicLibrary.mli (80%) rename helm/software/components/{ng_kernel => ng_library}/rt.ml (100%) diff --git a/helm/software/components/METAS/meta.helm-grafite_engine.src b/helm/software/components/METAS/meta.helm-grafite_engine.src index 45a02a30b..e23e0d0a7 100644 --- a/helm/software/components/METAS/meta.helm-grafite_engine.src +++ b/helm/software/components/METAS/meta.helm-grafite_engine.src @@ -1,4 +1,4 @@ -requires="helm-library helm-grafite helm-tactics helm-ng_tactics helm-ng_refiner" +requires="helm-library helm-grafite helm-tactics helm-ng_tactics helm-ng_library" version="0.0.1" archive(byte)="grafite_engine.cma" archive(native)="grafite_engine.cmxa" diff --git a/helm/software/components/METAS/meta.helm-lexicon.src b/helm/software/components/METAS/meta.helm-lexicon.src index 741fd603e..a98593133 100644 --- a/helm/software/components/METAS/meta.helm-lexicon.src +++ b/helm/software/components/METAS/meta.helm-lexicon.src @@ -1,4 +1,4 @@ -requires="helm-content_pres helm-cic_disambiguation camlp5.gramlib" +requires="helm-content_pres helm-ng_library helm-cic_disambiguation camlp5.gramlib" version="0.0.1" archive(byte)="lexicon.cma" archive(native)="lexicon.cmxa" diff --git a/helm/software/components/METAS/meta.helm-ng_library.src b/helm/software/components/METAS/meta.helm-ng_library.src new file mode 100644 index 000000000..94402278d --- /dev/null +++ b/helm/software/components/METAS/meta.helm-ng_library.src @@ -0,0 +1,5 @@ +requires="helm-ng_refiner" +version="0.0.1" +archive(byte)="ng_library.cma" +archive(native)="ng_library.cmxa" +linkopts="" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index 7035411f3..25169744f 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -27,6 +27,7 @@ MODULES = \ acic_content \ grafite \ ng_refiner \ + ng_library \ ng_cic_content \ content_pres \ cic_unification \ @@ -44,6 +45,7 @@ MODULES = \ tptp_grafite \ ng_kernel \ ng_refiner \ + ng_library \ $(NULL) METAS = $(MODULES:%=METAS/META.helm-%) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ea5afab4c..5ae6e92ed 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -487,7 +487,8 @@ let inject_unification_hint = = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in - NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint + NCicLibrary.Serializer.register + "unification_hints" basic_eval_unification_hint ;; let eval_unification_hint status t n = @@ -514,7 +515,7 @@ let inject_constraint = let u2 = refresh_uri_in_universe u2 in basic_eval_add_constraint (u1,u2) in - NRstatus.Serializer.register "constraints" basic_eval_add_constraint + NCicLibrary.Serializer.register "constraints" basic_eval_add_constraint ;; let eval_add_constraint status u1 u2 = @@ -980,7 +981,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status in let status = - NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + NCicLibrary.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in let status = GrafiteTypes.add_moo_content diff --git a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml index 550cb93c4..2f103cf83 100644 --- a/helm/software/components/grafite_engine/nCicCoercDeclaration.ml +++ b/helm/software/components/grafite_engine/nCicCoercDeclaration.ml @@ -294,7 +294,7 @@ let record_ncoercion = let aux_l l ~refresh_uri_in_universe ~refresh_uri_in_term = List.fold_right (aux ~refresh_uri_in_universe ~refresh_uri_in_term) l in - NRstatus.Serializer.register "ncoercion" aux_l + NCicLibrary.Serializer.register "ncoercion" aux_l ;; let basic_eval_and_record_ncoercion infos status = diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index 306eca9d6..ebfd686cd 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -14,13 +14,13 @@ class type g_status = object inherit LexiconEngine.g_status - inherit NRstatus.g_dumpable_status + inherit NCicLibrary.g_dumpable_status end class status = object (self) inherit LexiconEngine.status - inherit NRstatus.dumpable_status + inherit NCicLibrary.dumpable_status method set_estatus : 'status. #g_status as 'status -> 'self = fun o -> (self#set_lexicon_engine_status o)#set_dumpable_status o end diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli index 8e361407f..cc356aa46 100644 --- a/helm/software/components/grafite_parser/nEstatus.mli +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -14,13 +14,13 @@ class type g_status = object inherit LexiconEngine.g_status - inherit NRstatus.g_dumpable_status + inherit NCicLibrary.g_dumpable_status end class status : object ('self) inherit LexiconEngine.status - inherit NRstatus.dumpable_status + inherit NCicLibrary.dumpable_status inherit g_status method set_estatus: #g_status -> 'self end diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 159cee382..fa6e42064 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -8,7 +8,6 @@ nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -47,9 +46,3 @@ nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCicEnvironment.cmi nCic.cmo nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicUntrusted.cmi nCicPp.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmo \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicUntrusted.cmx nCicPp.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 01056b468..7720472e8 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -8,7 +8,6 @@ nCicPp.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx nCicUntrusted.cmi: nCic.cmx -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -47,9 +46,3 @@ nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ - nCicUntrusted.cmi nCicPp.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmx \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ - nCicUntrusted.cmx nCicPp.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index d533c8f73..50ecd2b47 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -12,8 +12,7 @@ INTERFACE_FILES = \ nCicPp.mli \ nCicReduction.mli \ nCicTypeChecker.mli \ - nCicUntrusted.mli \ - nCicLibrary.mli + nCicUntrusted.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) @@ -23,13 +22,6 @@ EXTRA_OBJECTS_TO_CLEAN = %.cmi: OCAMLOPTIONS += -w Ae %.cmx: OCAMLOPTIONS += -w Ae -all: rt check -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: rt.opt check.opt -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend new file mode 100644 index 000000000..c76001c01 --- /dev/null +++ b/helm/software/components/ng_library/.depend @@ -0,0 +1,2 @@ +nCicLibrary.cmo: nCicLibrary.cmi +nCicLibrary.cmx: nCicLibrary.cmi diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt new file mode 100644 index 000000000..c76001c01 --- /dev/null +++ b/helm/software/components/ng_library/.depend.opt @@ -0,0 +1,2 @@ +nCicLibrary.cmo: nCicLibrary.cmi +nCicLibrary.cmx: nCicLibrary.cmi diff --git a/helm/software/components/ng_library/Makefile b/helm/software/components/ng_library/Makefile new file mode 100644 index 000000000..ee8fbad13 --- /dev/null +++ b/helm/software/components/ng_library/Makefile @@ -0,0 +1,24 @@ +PACKAGE = ng_library +PREDICATES = + +INTERFACE_FILES = \ + nCicLibrary.mli + +IMPLEMENTATION_FILES = \ + $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = +%.cmo: OCAMLOPTIONS += -w Ae +%.cmi: OCAMLOPTIONS += -w Ae +%.cmx: OCAMLOPTIONS += -w Ae + +all: rt check +%: %.ml $(PACKAGE).cma + $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< +all.opt opt: rt.opt check.opt +%.opt: %.ml $(PACKAGE).cmxa + $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< + +include ../../Makefile.defs +include ../Makefile.common + diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_library/check.ml similarity index 100% rename from helm/software/components/ng_kernel/check.ml rename to helm/software/components/ng_library/check.ml diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml similarity index 92% rename from helm/software/components/ng_kernel/nCicLibrary.ml rename to helm/software/components/ng_library/nCicLibrary.ml index e7d7c3b11..6987ec1aa 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_library/nCicLibrary.ml @@ -145,11 +145,13 @@ let init = load_db;; class type g_status = object + inherit NRstatus.g_status method timestamp: timestamp end class status = object + inherit NRstatus.status val timestamp = (time0 : timestamp) method timestamp = timestamp method set_timestamp v = {< timestamp = v >} @@ -158,6 +160,19 @@ class status = = fun o -> {< timestamp = o#timestamp >} end + +module type SerializerT = + sig + type status + type obj + val register: + string -> + ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> obj) + val serialize: baseuri:NUri.uri -> obj list -> unit + val require: baseuri:NUri.uri -> status -> status + end + let time_travel status = let sto,ali,cac,inc = status#timestamp in let diff_len = List.length !storage - List.length sto in @@ -184,19 +199,7 @@ let serialize ~baseuri dump = time_travel (new status) ;; -module type Serializer = - sig - type status - type obj - val register: - string -> - ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> - ('a -> obj) - val serialize: baseuri:NUri.uri -> obj list -> unit - val require: baseuri:NUri.uri -> status -> status - end - -module Serializer(S: sig type status end) = +module SerializerF(S: sig type status end) = struct type status = S.status type obj = string * Obj.t @@ -224,6 +227,37 @@ module Serializer(S: sig type status end) = List.fold_right !require1 dump status end +type sstatus = status + +module Serializer = + struct + include SerializerF(struct type status = sstatus end) + + let require ~baseuri status = + let rstatus = require ~baseuri (status : #status :> status) in + let status = status#set_coerc_db (rstatus#coerc_db) in + let status = status#set_uhint_db (rstatus#uhint_db) in + let status = status#set_timestamp (rstatus#timestamp) in + status + end + +class type g_dumpable_status = + object + inherit g_status + method dump: Serializer.obj list + end + +class dumpable_status = + object(self) + inherit status + val dump = ([] : Serializer.obj list) + method dump = dump + method set_dump v = {< dump = v >} + method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self + = fun o -> (self#set_dump o#dump)#set_coercion_status o + end + + let decompile ~baseuri = let baseuris = get_deps baseuri in List.iter (fun baseuri -> diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_library/nCicLibrary.mli similarity index 80% rename from helm/software/components/ng_kernel/nCicLibrary.mli rename to helm/software/components/ng_library/nCicLibrary.mli index 6dc7dde43..e155aaf4a 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_library/nCicLibrary.mli @@ -18,6 +18,7 @@ type timestamp class type g_status = object method timestamp: timestamp + inherit NRstatus.g_status end class status : @@ -41,7 +42,7 @@ val clear_cache : unit -> unit val time_travel: #status -> unit val decompile: baseuri:NUri.uri -> unit -module type Serializer = +module type SerializerT = sig type status type obj @@ -53,10 +54,28 @@ module type Serializer = val require: baseuri:NUri.uri -> status -> status end -module Serializer(S: sig type status end): Serializer with type status= S.status - val init: unit -> unit +module Serializer: + sig + include SerializerT with type status = status + val require: baseuri:NUri.uri -> (#status as 'status) -> 'status + end + +class type g_dumpable_status = + object + inherit g_status + method dump: Serializer.obj list + end + +class dumpable_status : + object ('self) + inherit status + inherit g_dumpable_status + method set_dump: Serializer.obj list -> 'self + method set_dumpable_status: #g_dumpable_status -> 'self + end + (* CSC: only required during old-to-NG phase, to be deleted *) val refresh_uri: NUri.uri -> NUri.uri diff --git a/helm/software/components/ng_kernel/rt.ml b/helm/software/components/ng_library/rt.ml similarity index 100% rename from helm/software/components/ng_kernel/rt.ml rename to helm/software/components/ng_library/rt.ml diff --git a/helm/software/components/ng_refiner/Makefile b/helm/software/components/ng_refiner/Makefile index 9e0959c0d..7ff8f5fd0 100644 --- a/helm/software/components/ng_refiner/Makefile +++ b/helm/software/components/ng_refiner/Makefile @@ -18,33 +18,6 @@ EXTRA_OBJECTS_TO_CLEAN = %.cmi: OCAMLOPTIONS += -w Ae %.cmx: OCAMLOPTIONS += -w Ae -all: rt check -%: %.ml $(PACKAGE).cma - $(OCAMLC) -package helm-$(PACKAGE) -linkpkg -o $@ $< -all.opt opt: rt.opt check.opt -%.opt: %.ml $(PACKAGE).cmxa - $(OCAMLOPT) -package helm-$(PACKAGE) -linkpkg -o $@ $< - -depend.dot: $(IMPLEMENTATION_FILES) $(INTERFACE_FILES) - ocamldoc -o depend.dot -rectypes -I ../extlib/ -I ../cic -I ../cic_proof_checking/ -I ../urimanager/ -I ../logger/ -I ../registry/ -I ../getter/ -I ../hmysql/ -I ../library/ -I ../metadata/ -dot nUri.ml nReference.ml nCic.ml nCicPp.ml nCicEnvironment.ml nCicSubstitution.ml nCicReduction.ml nCicTypeChecker.ml nCicUtils.ml nCicLibrary.ml - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - for i in `cat depend.dot | grep darkturquoise | cut -d '"' -f 2`; do j=`echo $$i | sed s/^N/n/g`; size=`cat $$j.ml | wc -l`; funs=`cat $$j.mli | grep "^val " | wc -l`; size=`expr $$size - 13`; echo "\"$$i\" [ label=\"$$i\\n$$size lines,\\n$$funs functions\"];"; done >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "darkturquoise" > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot - tred < depend.dot > /tmp/depend.dot && mv /tmp/depend.dot . - cat depend.dot | grep -v "^}$$" > /tmp/depend.dot && mv /tmp/depend.dot . - echo " NCicEnvironment -> NCicTypeChecker;" >> depend.dot - cat depend.dot | grep -v "NCicEnvironment -> NCic;" > /tmp/depend.dot && mv /tmp/depend.dot . - echo "NCicLibrary [ style=dashed ];" >> depend.dot - echo "NCicPp [ style=dashed ];" >> depend.dot - echo "}" >> depend.dot - cat depend.dot | grep -v "rotate" > /tmp/depend.dot && mv /tmp/depend.dot . - -depend.png depend.eps: depend.dot - dot -Tpng > depend.png < depend.dot - dot -Tps > depend.eps < depend.dot - include ../../Makefile.defs include ../Makefile.common diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 68fdf4f50..9a6fd4ef2 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -11,46 +11,7 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -class type g_status = - object - inherit NCicCoercion.g_status - inherit NCicLibrary.g_status - end +class type g_status = NCicCoercion.status -class status = - object (self) - inherit NCicCoercion.status - inherit NCicLibrary.status - method set_rstatus : 'status. #g_status as 'status -> 'self - = fun o -> (self#set_coercion_status o)#set_library_status o - end +class status = NCicCoercion.status -type sstatus = status - -module Serializer = - struct - include NCicLibrary.Serializer(struct type status = sstatus end) - - let require ~baseuri status = - let rstatus = require ~baseuri (status : #status :> status) in - let status = status#set_coerc_db (rstatus#coerc_db) in - let status = status#set_uhint_db (rstatus#uhint_db) in - let status = status#set_timestamp (rstatus#timestamp) in - status - end - -class type g_dumpable_status = - object - inherit g_status - method dump: Serializer.obj list - end - -class dumpable_status = - object(self) - inherit status - val dump = ([] : Serializer.obj list) - method dump = dump - method set_dump v = {< dump = v >} - method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self - = fun o -> (self#set_dump o#dump)#set_rstatus o - end diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 40974aac2..631e629e5 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -11,36 +11,7 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -class type g_status = - object - inherit NCicCoercion.g_status - inherit NCicLibrary.g_status - end +class type g_status = NCicCoercion.status -class status : - object ('self) - inherit NCicCoercion.status - inherit NCicLibrary.status - inherit g_status - method set_rstatus: #g_status -> 'self - end +class status : NCicCoercion.status -module Serializer: - sig - include NCicLibrary.Serializer with type status = status - val require: baseuri:NUri.uri -> (#status as 'status) -> 'status - end - -class type g_dumpable_status = - object - inherit g_status - method dump: Serializer.obj list - end - -class dumpable_status : - object ('self) - inherit status - inherit g_dumpable_status - method set_dump: Serializer.obj list -> 'self - method set_dumpable_status: #g_dumpable_status -> 'self - end diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index b6bba823f..e47b1b713 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -88,7 +88,7 @@ let save_moo grafite_status = GrafiteMarshal.save_moo moo_fname grafite_status#moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname grafite_status#lstatus.LexiconEngine.lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index f9c9af359..ba6840ee5 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -251,7 +251,7 @@ let main () = in GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; exit 0 end with diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 6d01fc460..0b8b58c0d 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -274,7 +274,7 @@ let compile atstart options fname = (* FG: we do not generate .moo when dumping .mma files *) GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) grafite_status#dump end; let tm = Unix.gmtime elapsed in -- 2.39.2