From db7ecce6c398a42f14557067bf18b61cf75da80e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 May 2012 13:52:13 +0000 Subject: [PATCH] Thanks to Guarrigue, code for Serializer functor simplified using private types. The type system of OCaml is more and more misterious... --- .../components/grafite_engine/grafiteTypes.ml | 7 +---- matita/components/ng_library/nCicLibrary.ml | 28 ++++++++----------- matita/components/ng_library/nCicLibrary.mli | 2 +- 3 files changed, 13 insertions(+), 24 deletions(-) diff --git a/matita/components/grafite_engine/grafiteTypes.ml b/matita/components/grafite_engine/grafiteTypes.ml index 7cb6bef0c..e3086b2d7 100644 --- a/matita/components/grafite_engine/grafiteTypes.ml +++ b/matita/components/grafite_engine/grafiteTypes.ml @@ -51,9 +51,4 @@ class virtual status = fun (b : string) -> method set_ng_mode v = {< ng_mode = v >} end -module Serializer = - NCicLibrary.Serializer(struct - type dumpable_s = status - let get status = (status : #status :> NCicLibrary.dumpable_status) - let set (status : dumpable_s) dump_status = status#set_dumpable_status dump_status - end) +module Serializer = NCicLibrary.Serializer(struct type dumpable_s = status end) diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml index a7129177e..729d62d0e 100644 --- a/matita/components/ng_library/nCicLibrary.ml +++ b/matita/components/ng_library/nCicLibrary.ml @@ -215,7 +215,7 @@ module type SerializerType = val dependencies_of: baseuri:NUri.uri -> string list end -module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status val set: dumpable_s -> dumpable_status -> dumpable_s end) = +module Serializer(D: sig type dumpable_s = private #dumpable_status end) = struct type dumpable_status = D.dumpable_s type 'a register_type = @@ -247,7 +247,6 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status end let serialize ~baseuri status = - let status = D.get status in let ch = open_out (ng_path_of_baseuri baseuri) in Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) []; close_out ch; @@ -265,12 +264,10 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status let require2 ~baseuri ~alias_only status = try - let s = D.get status in let status = - D.set status - (s#set_dump - {s#dump with - includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in + status#set_dump + {status#dump with + includes = baseuri::List.filter ((<>) baseuri) status#dump.includes} in let _dependencies,dump = require0 ~baseuri in List.fold_right (!require1 ~alias_only) dump status with @@ -283,7 +280,7 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_ ~refresh_uri_in_reference:_ ~alias_only status = let baseuri = refresh_uri baseuri in - if not alias_only && List.mem baseuri (get_transitively_included (D.get status)) then status + if not alias_only && List.mem baseuri (get_transitively_included status) then status else (HLog.warn ("include " ^ (if alias_only then "alias " else "") ^ fname); let status = require2 ~baseuri ~alias_only status in @@ -293,21 +290,18 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status register#run "include" aux let require ~baseuri ~fname ~alias_only status = - if not alias_only && List.mem baseuri (get_transitively_included (D.get status)) then status + if not alias_only && List.mem baseuri (get_transitively_included status) then status else (let status = if not alias_only then - let s = D.get status in - D.set status - (s#set_dump {s#dump with dependencies = fname::s#dump.dependencies}) + status#set_dump + {status#dump with dependencies = fname::status#dump.dependencies} else status in let status = require2 ~baseuri ~alias_only status in - let s = D.get status in - D.set status - (s#set_dump - {s#dump with - objs = record_include (baseuri,fname)::s#dump.objs })) + status#set_dump + {status#dump with + objs = record_include (baseuri,fname)::status#dump.objs }) end let fetch_obj status uri = diff --git a/matita/components/ng_library/nCicLibrary.mli b/matita/components/ng_library/nCicLibrary.mli index ee1ed3ece..3d9ab02cb 100644 --- a/matita/components/ng_library/nCicLibrary.mli +++ b/matita/components/ng_library/nCicLibrary.mli @@ -77,7 +77,7 @@ module type SerializerType = val dependencies_of: baseuri:NUri.uri -> string list end -module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status val set: dumpable_s -> dumpable_status -> dumpable_s end) : +module Serializer(D: sig type dumpable_s = private #dumpable_status end) : SerializerType with type dumpable_status = D.dumpable_s val refresh_uri: NUri.uri -> NUri.uri -- 2.39.2