From f6c887944d48d718f372a57f1609f3d059908aa8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Jun 2009 17:37:05 +0000 Subject: [PATCH] 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 --- .../grafite_engine/grafiteEngine.ml | 25 +++++--- .../components/grafite_engine/grafiteSync.ml | 5 +- .../components/grafite_engine/grafiteTypes.ml | 41 ++++++------- .../grafite_engine/grafiteTypes.mli | 4 +- .../grafite_parser/grafiteDisambiguate.ml | 6 +- .../components/grafite_parser/nEstatus.ml | 2 +- .../components/grafite_parser/nEstatus.mli | 2 +- .../components/ng_kernel/nCicLibrary.ml | 59 ++++++++++++++----- .../components/ng_kernel/nCicLibrary.mli | 13 +++- helm/software/components/ng_refiner/check.ml | 7 +-- .../components/ng_refiner/nRstatus.ml | 8 ++- .../components/ng_refiner/nRstatus.mli | 8 ++- .../components/ng_tactics/nTacStatus.ml | 6 +- helm/software/matita/matitaGui.ml | 2 +- helm/software/matita/matitaWiki.ml | 2 +- helm/software/matita/matitacLib.ml | 2 +- 16 files changed, 122 insertions(+), 70 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 9b454f294..bb01585d1 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -470,16 +470,22 @@ let coercion_moo_statement_of (uri,arity, saturations,_) = GrafiteAst.Coercion (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations) +let basic_eval_unification_hint (t,n) status = + let hstatus = + NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n + in + { status with NRstatus.uhint_db = hstatus } +;; + +let inject_unification_hint = + NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint +;; + let eval_unification_hint status t n = - let aux status = - let hstatus = - NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n - in - { status with NRstatus.uhint_db = hstatus } in - let rstatus = aux (GrafiteTypes.get_rstatus status) in + let rstatus = + basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in let status = GrafiteTypes.set_rstatus rstatus status in - let dump = GrafiteTypes.get_dump status in - let dump = fun status -> aux (dump status) in + let dump = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in let status = GrafiteTypes.set_dump dump status in status,`Old [] ;; @@ -736,7 +742,8 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status = eval_from_moo.efm_go status moopath in let rstatus = GrafiteTypes.get_rstatus status in let rstatus = - NCicLibrary.require ~baseuri:(NUri.uri_of_string baseuri) rstatus in + NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus + in let status = GrafiteTypes.set_rstatus rstatus status in (* debug let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index 60bfc6921..de578d7ca 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -184,10 +184,11 @@ let initial_status lexicon_status baseuri = { ng_status = GrafiteTypes.CommandMode { NEstatus.lstatus = lexicon_status; NEstatus.rstatus = { + NRstatus.refiner_status = { NRstatus.uhint_db = NCicUnifHint.empty_db; NRstatus.coerc_db = NCicCoercion.empty_db; - NRstatus.library_db = NCicLibrary.time0; - NRstatus.dump = fun x -> x; + NRstatus.library_db = NCicLibrary.time0 }; + NRstatus.dump = [] }; } } diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 6a57c4a00..0b9a4a7da 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -78,22 +78,6 @@ let set_lexicon new_lexicon_status new_grafite_status = new_lexicon_status }}}} ;; -let set_coercions db new_grafite_status = - { new_grafite_status with ng_status = - match new_grafite_status.ng_status with - | CommandMode estatus -> - CommandMode - { estatus with NEstatus.rstatus = - { estatus.NEstatus.rstatus with NRstatus.coerc_db = db }} - | ProofMode t -> - ProofMode - { t with NTacStatus.istatus = - { t.NTacStatus.istatus with NTacStatus.estatus = - { t.NTacStatus.istatus.NTacStatus.estatus with NEstatus.rstatus = - { t.NTacStatus.istatus.NTacStatus.estatus.NEstatus.rstatus with NRstatus.coerc_db = db - }}}}} -;; - let get_estatus x = match x.ng_status with | ProofMode t -> t.NTacStatus.istatus.NTacStatus.estatus @@ -110,19 +94,32 @@ let set_estatus e x = | CommandMode _ -> CommandMode e} ;; -let get_rstatus x = (get_estatus x).NEstatus.rstatus;; +let get_dstatus x = (get_estatus x).NEstatus.rstatus;; + +let get_rstatus x = (get_dstatus x).NRstatus.refiner_status;; let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;; let get_library_db x = (get_rstatus x).NRstatus.library_db;; -let get_dump x = (get_rstatus x).NRstatus.dump;; +let get_dump x = (get_dstatus x).NRstatus.dump;; -let set_rstatus h x = +let set_dstatus h x = let estatus = get_estatus x in set_estatus { estatus with NEstatus.rstatus = h } x ;; +let set_rstatus h x = + let dstatus = get_dstatus x in + set_dstatus { dstatus with NRstatus.refiner_status = h } x +;; + +let set_coercions db x = + let rstatus = get_rstatus x in + set_rstatus { rstatus with NRstatus.coerc_db = db } x +;; + + let set_hstatus h x = let rstatus = get_rstatus x in set_rstatus { rstatus with NRstatus.uhint_db = h} x @@ -275,8 +272,4 @@ let dump_status status = List.iter (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects -let get_coercions new_grafite_status = - let e = get_estatus new_grafite_status in - e.NEstatus.rstatus.NRstatus.coerc_db -;; - +let get_coercions x = (get_rstatus x).NRstatus.coerc_db;; diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli index 4d693ea6b..4caba49d1 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -78,7 +78,7 @@ val get_estatus : status -> NEstatus.extra_status val get_rstatus : status -> NRstatus.refiner_status val get_hstatus : status -> NCicUnifHint.db val get_library_db : status -> NCicLibrary.timestamp -val get_dump : status -> (NRstatus.refiner_status -> NRstatus.refiner_status) +val get_dump : status -> NRstatus.Serializer.obj list val get_coercions: status -> NCicCoercion.db val set_stack: Continuationals.Stack.t -> status -> status @@ -89,5 +89,5 @@ val set_estatus : NEstatus.extra_status -> status -> status val set_rstatus : NRstatus.refiner_status -> status -> status val set_hstatus : NCicUnifHint.db -> status -> status val set_library_db : NCicLibrary.timestamp -> status -> status -val set_dump : (NRstatus.refiner_status -> NRstatus.refiner_status) -> status -> status +val set_dump : NRstatus.Serializer.obj list -> status -> status diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 5002e58ab..b302da1f2 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -200,7 +200,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing let diff, metasenv, subst, cic = singleton "first" (NCicDisambiguate.disambiguate_term - ~rdb:estatus.NEstatus.rstatus + ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases ~expty ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) @@ -688,7 +688,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) = (try (match NCicDisambiguate.disambiguate_obj - ~rdb:estatus.NEstatus.rstatus + ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status ~lookup_in_library:nlookup_in_library ~description_of_alias:LexiconAst.description_of_alias ~mk_choice:ncic_mk_choice @@ -783,7 +783,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = ~mk_choice:ncic_mk_choice ~mk_implicit ~uri:(OCic2NCic.nuri_of_ouri uri) - ~rdb:estatus.NEstatus.rstatus + ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) (text,prefix_len,obj)) in diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml index a225f439d..a49174b11 100644 --- a/helm/software/components/grafite_parser/nEstatus.ml +++ b/helm/software/components/grafite_parser/nEstatus.ml @@ -13,6 +13,6 @@ type extra_status = { lstatus : LexiconEngine.status; - rstatus : NRstatus.refiner_status; + rstatus : NRstatus.dumpable_refiner_status; } diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli index a225f439d..a49174b11 100644 --- a/helm/software/components/grafite_parser/nEstatus.mli +++ b/helm/software/components/grafite_parser/nEstatus.mli @@ -13,6 +13,6 @@ type extra_status = { lstatus : LexiconEngine.status; - rstatus : NRstatus.refiner_status; + rstatus : NRstatus.dumpable_refiner_status; } diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index cff822316..414e5c5de 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -26,8 +26,6 @@ let cache = ref NUri.UriMap.empty;; let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;; -let magic = 0;; - let path_of_baseuri baseuri = let uri = NUri.string_of_uri baseuri in let path = String.sub uri 4 (String.length uri - 4) in @@ -37,6 +35,18 @@ let path_of_baseuri baseuri = path ^ ".ng" ;; +let magic = 0;; + +let require0 ~baseuri = + let ch = open_in (path_of_baseuri baseuri) in + let mmagic,dump = Marshal.from_channel ch in + close_in ch; + if mmagic <> magic then + raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library.")) + else + dump +;; + let serialize ~baseuri dump = let ch = open_out (path_of_baseuri baseuri) in Marshal.to_channel ch (magic,dump) [Marshal.Closures]; @@ -47,18 +57,40 @@ let serialize ~baseuri dump = Marshal.to_channel ch (magic,obj) []; close_out ch ) !storage; - time_travel time0; + time_travel time0 ;; -let require ~baseuri = - let ch = open_in (path_of_baseuri baseuri) in - let mmagic,dump = Marshal.from_channel ch in - close_in ch; - if mmagic <> magic then - raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library.")) - else - dump -;; +module type Serializer = + sig + type status + type obj + val register: string -> ('a -> 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) = + struct + type status = S.status + type obj = Obj.t + + let require1 = ref (fun _ -> assert false (* unknown data*)) + let already_registered = ref [] + + let register tag require = + assert (not (List.mem tag !already_registered)); + already_registered := tag :: !already_registered; + require1 := + (fun (tag',data) as x -> + if tag=tag' then Obj.magic require data else Obj.magic !require1 x); + Obj.magic (fun x -> tag,x) + + let serialize = serialize + + let require ~baseuri status = + let dump = require0 ~baseuri in + List.fold_right (Obj.magic !require1) dump status +end let decompile ~baseuri = Unix.unlink (path_of_baseuri baseuri) @@ -67,7 +99,7 @@ let decompile ~baseuri = (* the miracles of Marshal... *) let fetch_obj uri = - let obj = require ~baseuri:uri in + let obj = require0 ~baseuri:uri in (* here we need to refresh the URIs! *) obj ;; @@ -141,4 +173,3 @@ let get_obj u = ;; let clear_cache () = cache := NUri.UriMap.empty;; - diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 11a608e1d..f94c65682 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -25,8 +25,17 @@ val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) val clear_cache : unit -> unit val time_travel: timestamp -> unit -val serialize: baseuri:NUri.uri -> ('status -> 'status) -> unit -val require: baseuri:NUri.uri -> 'status -> 'status val decompile: baseuri:NUri.uri -> unit +module type Serializer = + sig + type status + type obj + val register: string -> ('a -> 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): Serializer with type status= S.status + (* EOF *) diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index bd7f72e70..6aba5a993 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -272,10 +272,9 @@ let _ = let bo = curryfy [] bo in (try let rdb = { - NRstatus.uhint_db = NCicUnifHint.empty_db; - NRstatus.coerc_db = NCicCoercion.empty_db; - NRstatus.library_db = NCicLibrary.time0; - NRstatus.dump = fun x -> x + NRstatus.uhint_db = NCicUnifHint.empty_db; + NRstatus.coerc_db = NCicCoercion.empty_db; + NRstatus.library_db = NCicLibrary.time0 } in let metasenv, subst, bo, infty = NCicRefiner.typeof rdb [] [] [] bo None diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 0ef8755f4..26ef2684c 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -15,6 +15,12 @@ type refiner_status = { coerc_db : NCicCoercion.db; uhint_db : NCicUnifHint.db; library_db : NCicLibrary.timestamp; - dump: refiner_status -> refiner_status } +module Serializer = + NCicLibrary.Serializer(struct type status = refiner_status end) + +type dumpable_refiner_status = { + refiner_status : refiner_status; + dump: Serializer.obj list +} diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 6cf9ddd4f..729f6ba6e 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -15,5 +15,11 @@ type refiner_status = { coerc_db : NCicCoercion.db; uhint_db : NCicUnifHint.db; library_db : NCicLibrary.timestamp; - dump: refiner_status -> refiner_status +} + +module Serializer: NCicLibrary.Serializer with type status = refiner_status + +type dumpable_refiner_status = { + refiner_status : refiner_status; + dump: Serializer.obj list } diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 6aaf4a4a8..ba0308068 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -84,7 +84,7 @@ let relocate status destination (name,source,t as orig) = NCicMetaSubst.delift ~unify:(fun m s c t1 t2 -> try Some (NCicUnification.unify - status.estatus.NEstatus.rstatus m s c t1 t2) + status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2) with | NCicUnification.UnificationFailure _ | NCicUnification.Uncertain _ -> None) @@ -147,7 +147,7 @@ let unify status ctx a b = let status, (_,_,b) = relocate status ctx b in let n,h,metasenv,subst,o = status.pstatus in let metasenv, subst = - NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b + NCicUnification.unify status.estatus.NEstatus.rstatus.NRstatus.refiner_status metasenv subst ctx a b in { status with pstatus = n,h,metasenv,subst,o } ;; @@ -160,7 +160,7 @@ let refine status ctx term expty = let status, (n,_, e) = relocate status ctx e in status, n, Some e in let name,height,metasenv,subst,obj = status.pstatus in - let rdb = status.estatus.NEstatus.rstatus in + let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in let metasenv, subst, t, ty = NCicRefiner.typeof rdb metasenv subst ctx term expty in diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 3c7db84cd..8acc424a9 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -89,7 +89,7 @@ let save_moo grafite_status = grafite_status.GrafiteTypes.moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev; - NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) + NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) (GrafiteTypes.get_dump grafite_status) | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index eb115636f..5ed1d41b4 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -254,7 +254,7 @@ let main () = in GrafiteMarshal.save_moo moo_fname moo_content_rev; LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; + NRstatus.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 7580ebf29..c0c3d0941 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; - NCicLibrary.serialize ~baseuri:(NUri.uri_of_string baseuri) + NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) (GrafiteTypes.get_dump grafite_status) end; let tm = Unix.gmtime elapsed in -- 2.39.2