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 []
;;
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
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 = []
};
}
}
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
| 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
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;;
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
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
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)
(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
~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
type extra_status = {
lstatus : LexiconEngine.status;
- rstatus : NRstatus.refiner_status;
+ rstatus : NRstatus.dumpable_refiner_status;
}
type extra_status = {
lstatus : LexiconEngine.status;
- rstatus : NRstatus.refiner_status;
+ rstatus : NRstatus.dumpable_refiner_status;
}
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
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];
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)
(* 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
;;
;;
let clear_cache () = cache := NUri.UriMap.empty;;
-
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 *)
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
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
+}
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
}
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)
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 }
;;
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
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
;;
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
(* 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
projects / helm.git / commitdiff