From 8bc5bc0e8375a85736f6a5df317d129d5efa8de4 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 17 Jun 2009 11:47:59 +0000 Subject: [PATCH] Initial implementation of statuses using objects in place of nested records. So nicer! The only major problem is that the NCicLibrary functor does not return a function #status as 'status -> 'status, but a function status -> status. Thus I have to painfully wrap NCicLibrary.Realizer(...).require in NRstatus. TO REMEMBER: - every function that works on a data type that used to be put in the status (e.g. a db) must now work on a functional class with just two members (db and set_db). Moreover, every function in the module must work on the open variants of the class type, i.e. #status --- .../grafite_engine/grafiteEngine.ml | 38 +++++++++--------- .../components/grafite_engine/grafiteSync.ml | 21 ++++------ .../components/grafite_engine/grafiteTypes.ml | 40 ------------------- .../grafite_engine/grafiteTypes.mli | 13 +----- .../grafite_parser/grafiteDisambiguate.ml | 6 +-- .../components/grafite_parser/nEstatus.ml | 2 +- .../components/grafite_parser/nEstatus.mli | 2 +- .../ng_disambiguation/nCicDisambiguate.ml | 11 +++-- .../ng_disambiguation/nCicDisambiguate.mli | 4 +- .../components/ng_kernel/nCicLibrary.ml | 18 +++++++-- .../components/ng_kernel/nCicLibrary.mli | 11 +++-- .../components/ng_paramodulation/paramod.mli | 2 +- helm/software/components/ng_refiner/check.ml | 6 +-- .../components/ng_refiner/nCicCoercion.ml | 34 ++++++++++------ .../components/ng_refiner/nCicCoercion.mli | 17 +++++--- .../components/ng_refiner/nCicRefiner.ml | 3 +- .../components/ng_refiner/nCicRefiner.mli | 4 +- .../components/ng_refiner/nCicUnifHint.ml | 15 ++++--- .../components/ng_refiner/nCicUnifHint.mli | 15 ++++--- .../components/ng_refiner/nCicUnification.ml | 3 +- .../components/ng_refiner/nCicUnification.mli | 2 +- .../components/ng_refiner/nRstatus.ml | 35 +++++++++++----- .../components/ng_refiner/nRstatus.mli | 27 ++++++++----- .../components/ng_tactics/nTacStatus.ml | 6 +-- .../components/ng_tactics/nTactics.ml | 2 +- helm/software/matita/matitaGui.ml | 2 +- helm/software/matita/matitaWiki.ml | 2 +- helm/software/matita/matitacLib.ml | 2 +- 28 files changed, 170 insertions(+), 173 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 6e6a5bc73..e0bcd031e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -471,10 +471,7 @@ let coercion_moo_statement_of (uri,arity, saturations,_) = (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 } + NCicUnifHint.add_user_provided_hint status t n ;; let inject_unification_hint = @@ -491,11 +488,11 @@ let eval_unification_hint status t n = assert (metasenv=[]); let t = NCicUntrusted.apply_subst subst [] t in let status = GrafiteTypes.set_estatus estatus 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 = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in - let status = GrafiteTypes.set_dump dump status in + let dstatus = + basic_eval_unification_hint (t,n) (GrafiteTypes.get_dstatus status) in + let dump = inject_unification_hint (t,n)::dstatus#dump in + let dstatus = dstatus#set_dump dump in + let status = GrafiteTypes.set_dstatus dstatus status in status,`Old [] ;; @@ -748,11 +745,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status raise (IncludedFileNotCompiled (moopath_rw,baseuri)) in let status = eval_from_moo.efm_go status moopath in - let rstatus = GrafiteTypes.get_rstatus status in - let rstatus = - NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus - in - let status = GrafiteTypes.set_rstatus rstatus status in + let dstatus = GrafiteTypes.get_dstatus status in + let dstatus = + NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) + dstatus in + let status = GrafiteTypes.set_dstatus dstatus status in (* debug let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in @@ -830,17 +827,18 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status in let obj = uri,height,[],[],obj_kind in NCicTypeChecker.typecheck_obj obj; - let timestamp = NCicLibrary.add_obj uri obj in + let dstatus = estatus.NEstatus.rstatus in + let dstatus = NCicLibrary.add_obj dstatus uri obj in let objs = NCicElim.mk_elims obj in let timestamp,uris_rev = List.fold_left - (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj -> + (fun (dstatus,uris_rev) (uri,_,_,_,_) as obj -> NCicTypeChecker.typecheck_obj obj; - let timestamp = NCicLibrary.add_obj uri obj in - timestamp,uri::uris_rev - ) (timestamp,[]) objs in + let dstatus = NCicLibrary.add_obj dstatus uri obj in + dstatus,uri::uris_rev + ) (dstatus,[]) objs in let uris = uri::List.rev uris_rev in - GrafiteTypes.set_library_db timestamp + GrafiteTypes.set_dstatus dstatus {status with GrafiteTypes.ng_status = GrafiteTypes.CommandMode estatus },`New uris diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index de578d7ca..94170493b 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -147,12 +147,11 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity objects = lemmas @ status.GrafiteTypes.objects; } in - let db = + let dstatus = NCicCoercion.index_old_db (CoercDb.dump ()) - (GrafiteTypes.get_coercions status) - in - let status = GrafiteTypes.set_coercions db status in - status, lemmas + (GrafiteTypes.get_dstatus status) in + let status = GrafiteTypes.set_dstatus dstatus status in + status, lemmas let prefer_coercion s u = CoercDb.prefer u; @@ -171,7 +170,7 @@ let time_travel ~present ~past = uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in List.iter LibrarySync.remove_obj objs_to_remove; CoercDb.restore past.GrafiteTypes.coercions; - NCicLibrary.time_travel (GrafiteTypes.get_library_db past) + NCicLibrary.time_travel (GrafiteTypes.get_dstatus past) ;; let initial_status lexicon_status baseuri = { @@ -183,14 +182,8 @@ let initial_status lexicon_status baseuri = { baseuri = 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 = [] - }; - } + NEstatus.rstatus = new NRstatus.dumpable_status + }; } diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml index 0b9a4a7da..6033be8c2 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.ml +++ b/helm/software/components/grafite_engine/grafiteTypes.ml @@ -96,49 +96,11 @@ let set_estatus e x = 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_dstatus x).NRstatus.dump;; - 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 -;; - -let set_library_db h x = - let rstatus = get_rstatus x in - set_rstatus { rstatus with NRstatus.library_db = h} x -;; - -let set_dump h x = - let estatus = get_estatus x in - set_estatus - { estatus with NEstatus.rstatus = - { estatus.NEstatus.rstatus with - NRstatus.dump = h}} - x -;; - let get_current_proof status = match status.proof_status with | Incomplete_proof { proof = p } -> p @@ -271,5 +233,3 @@ let dump_status status = HLog.message "status.objects:\n"; List.iter (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects - -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 4caba49d1..8ed9fe489 100644 --- a/helm/software/components/grafite_engine/grafiteTypes.mli +++ b/helm/software/components/grafite_engine/grafiteTypes.mli @@ -75,19 +75,10 @@ val get_proof_context : status -> int -> Cic.context val get_proof_conclusion : status -> int -> Cic.term val get_lexicon : status -> LexiconEngine.status 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.Serializer.obj list -val get_coercions: status -> NCicCoercion.db +val get_dstatus : status -> NRstatus.dumpable_status val set_stack: Continuationals.Stack.t -> status -> status val set_metasenv: Cic.metasenv -> status -> status val set_lexicon : LexiconEngine.status -> status -> status -val set_coercions: NCicCoercion.db -> status -> status 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.Serializer.obj list -> status -> status - +val set_dstatus : NRstatus.dumpable_status -> status -> status diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 0dfab7a37..4aadd7077 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.NRstatus.refiner_status + ~rdb:estatus.NEstatus.rstatus ~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.NRstatus.refiner_status + ~rdb:estatus.NEstatus.rstatus ~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.NRstatus.refiner_status + ~rdb:estatus.NEstatus.rstatus ~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 a49174b11..2ae7d01e4 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.dumpable_refiner_status; + rstatus : NRstatus.dumpable_status; } diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli index a49174b11..2ae7d01e4 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.dumpable_refiner_status; + rstatus : NRstatus.dumpable_status; } diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 108c845c6..5fa3b8188 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -47,9 +47,8 @@ let refine_term in let metasenv, subst, term, _ = NCicRefiner.typeof - { rdb with NRstatus.coerc_db = - if use_coercions then rdb.NRstatus.coerc_db - else NCicCoercion.empty_db } + (rdb#set_coerc_db + (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db)) metasenv subst context term expty ~localise in Disambiguate.Ok (term, metasenv, subst, ()) @@ -79,9 +78,9 @@ let refine_obj try let obj = NCicRefiner.typeof_obj - { rdb with NRstatus.coerc_db = - if use_coercions then rdb.NRstatus.coerc_db - else NCicCoercion.empty_db } + (rdb#set_coerc_db + (if use_coercions then rdb#coerc_db + else NCicCoercion.empty_db)) obj ~localise in Disambiguate.Ok (obj, [], [], ()) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli index 0eb018b9d..b86849f35 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli @@ -21,7 +21,7 @@ val disambiguate_term : mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'alias DisambiguateTypes.Environment.t -> universe:'alias list DisambiguateTypes.Environment.t option -> - rdb:NRstatus.refiner_status -> + rdb:#NRstatus.status -> lookup_in_library:( DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> @@ -40,7 +40,7 @@ val disambiguate_obj : mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) -> aliases:'a DisambiguateTypes.Environment.t -> universe:'a list DisambiguateTypes.Environment.t option -> - rdb:NRstatus.refiner_status -> + rdb:#NRstatus.status -> lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type -> DisambiguateTypes.input_or_locate_uri_type -> DisambiguateTypes.Environment.key -> 'a list) -> diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index cc13dde6e..1cb3a118b 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -23,7 +23,17 @@ let storage = ref [];; let aliases = ref [];; let cache = ref NUri.UriMap.empty;; -let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;; +class status = + object + val timestamp = (time0 : timestamp) + method timestamp = timestamp + method set_timestamp v = {< timestamp = v >} + end + +let time_travel status = + let sto,ali,cac = status#timestamp in + storage := sto; aliases := ali; cache := cac +;; let path_of_baseuri baseuri = let uri = NUri.string_of_uri baseuri in @@ -56,7 +66,7 @@ let serialize ~baseuri dump = Marshal.to_channel ch (magic,obj) []; close_out ch ) !storage; - time_travel time0 + time_travel (new status) ;; let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; @@ -139,7 +149,7 @@ let aliases_of uri = Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri))) ;; -let add_obj u obj = +let add_obj status u obj = storage := (u,obj)::!storage; let _,height,_,_,obj = obj in let references = @@ -170,7 +180,7 @@ let add_obj u obj = ) il) in aliases := references @ !aliases; - !storage,!aliases,!cache + status#set_timestamp (!storage,!aliases,!cache) ;; let get_obj u = diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 526632565..dfd17f15b 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -14,9 +14,14 @@ exception LibraryOutOfSync of string Lazy.t type timestamp -val time0: timestamp -val add_obj: NUri.uri -> NCic.obj -> timestamp +class status : + object ('self) + method timestamp: timestamp + method set_timestamp: timestamp -> 'self + end + +val add_obj: #status as 'status -> NUri.uri -> NCic.obj -> 'status val aliases_of: NUri.uri -> NReference.reference list val resolve: string -> NReference.reference list (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) @@ -24,7 +29,7 @@ val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) val clear_cache : unit -> unit -val time_travel: timestamp -> unit +val time_travel: #status -> unit val decompile: baseuri:NUri.uri -> unit module type Serializer = diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index dd866f8db..69299b13f 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -1,5 +1,5 @@ val nparamod : - NRstatus.refiner_status -> + #NRstatus.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> (NCic.term * NCic.term) -> (NCic.term * NCic.term) list -> unit diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 6aba5a993..2ab8185ab 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -271,11 +271,7 @@ let _ = prerr_endline ("start: " ^ NUri.string_of_uri u); 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 - } in + let rdb = new NRstatus.status in let metasenv, subst, bo, infty = NCicRefiner.typeof rdb [] [] [] bo None in diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index e62d4eed3..29f28ba5c 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -24,7 +24,17 @@ module DB = type db = DB.t * DB.t -let index_coercion (db_src,db_tgt) c src tgt arity arg = +let empty_db = DB.empty,DB.empty + +class status = + object + val db = empty_db + method coerc_db = db + method set_coerc_db v = {< db = v >} + end + +let index_coercion status c src tgt arity arg = + let db_src,db_tgt = status#coerc_db in let data = (c,arity,arg) in (* prerr_endline ("INDEX:" ^ @@ -34,14 +44,14 @@ let index_coercion (db_src,db_tgt) c src tgt arity arg = *) let db_src = DB.index db_src src data in let db_tgt = DB.index db_tgt tgt data in - db_src, db_tgt + status#set_coerc_db (db_src, db_tgt) ;; -let index_old_db odb db = +let index_old_db odb (status : #status) = List.fold_left - (fun db (_,tgt,clist) -> + (fun status (_,tgt,clist) -> List.fold_left - (fun db (uri,_,arg) -> + (fun status (uri,_,arg) -> try let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in @@ -67,18 +77,16 @@ let index_old_db odb db = NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t); assert false in - index_coercion db c src tgt arity arg + index_coercion status c src tgt arity arg with | NCicEnvironment.BadDependency _ - | NCicTypeChecker.TypeCheckerFailure _ -> db) - db clist) - db (CoercDb.to_list odb) + | NCicTypeChecker.TypeCheckerFailure _ -> status) + status clist) + status (CoercDb.to_list odb) ;; -let empty_db = (DB.empty,DB.empty) ;; - - -let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty = +let look_for_coercion status metasenv subst context infty expty = + let db_src,db_tgt = status#coerc_db in match infty, expty with | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli index 73c88005c..1a31172d2 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.mli +++ b/helm/software/components/ng_refiner/nCicCoercion.mli @@ -13,19 +13,26 @@ type db +class status : + object ('self) + method coerc_db: db + method set_coerc_db: db -> 'self + end + +val empty_db: db + (* index (\x.c ?? x ??): A -> B index_coercion db c A B \arity_left(c ??x??) \position(x,??x??) *) val index_coercion: - db -> NCic.term -> NCic.term -> NCic.term -> int -> int -> db + #status as 'status -> + NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status (* gets the old imperative coercion DB (list format) *) -val index_old_db: CoercDb.coerc_db -> db -> db - -val empty_db : db +val index_old_db: CoercDb.coerc_db -> (#status as 'status) -> 'status val look_for_coercion: - db -> + #status -> NCic.metasenv -> NCic.substitution -> NCic.context -> (* inferred type, expected type *) NCic.term -> NCic.term -> diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 0f835961e..ffa2422e4 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -376,8 +376,7 @@ and try_coercions rdb | NCicUnification.Uncertain _ as exc -> first exc tl in first exc - (NCicCoercion.look_for_coercion - rdb.NRstatus.coerc_db metasenv subst context infty expty) + (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty) and force_to_sort rdb metasenv subst context t orig_t localise ty = match NCicReduction.whd ~subst context ty with diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli index b601db963..b75ee3a81 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.mli +++ b/helm/software/components/ng_refiner/nCicRefiner.mli @@ -16,7 +16,7 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;; exception AssertFailure of string Lazy.t;; val typeof : - NRstatus.refiner_status -> + #NRstatus.status -> ?localise:(NCic.term -> Stdpp.location) -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term option -> (* term, expected type *) @@ -24,7 +24,7 @@ val typeof : (* menv, subst,refined term, type *) val typeof_obj : - NRstatus.refiner_status -> + #NRstatus.status -> ?localise:(NCic.term -> Stdpp.location) -> NCic.obj -> NCic.obj diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml index c09e08d3c..ccccfca88 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.ml +++ b/helm/software/components/ng_refiner/nCicUnifHint.ml @@ -24,6 +24,13 @@ module DB = type db = DB.t +class status = + object + val db = DB.empty + method uhint_db = db + method set_uhint_db v = {< db = v >} + end + let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");; let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;; @@ -57,11 +64,9 @@ let index_hint hdb context t1 t2 precedence = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data); *) - DB.index hdb src (precedence, data) + hdb#set_uhint_db (DB.index hdb#uhint_db src (precedence, data)) ;; -let empty_db = DB.empty ;; - let add_user_provided_hint db t precedence = let c, a, b = let rec aux ctx = function @@ -176,8 +181,8 @@ let look_for_hint hdb metasenv subst context t1 t2 = String.concat "|" (List.map (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[]) (HintSet.elements ds)))); *) - let candidates1 = DB.retrieve_unifiables hdb (pair t1 t2) in - let candidates2 = DB.retrieve_unifiables hdb (pair t2 t1) in + let candidates1 = DB.retrieve_unifiables hdb#uhint_db (pair t1 t2) in + let candidates2 = DB.retrieve_unifiables hdb#uhint_db (pair t2 t1) in let candidates1 = List.map (fun (prec,ty) -> prec,true,saturate ~delta:max_int metasenv subst context ty 0) diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli index 21820ace4..f7257d8f8 100644 --- a/helm/software/components/ng_refiner/nCicUnifHint.mli +++ b/helm/software/components/ng_refiner/nCicUnifHint.mli @@ -13,15 +13,20 @@ type db -val index_hint: - db -> NCic.context -> NCic.term -> NCic.term -> int -> db +class status : + object ('self) + method uhint_db: db + method set_uhint_db: db -> 'self + end -val add_user_provided_hint : db -> NCic.term -> int -> db +val index_hint: + #status as 'status -> NCic.context -> NCic.term -> NCic.term -> int -> 'status -val empty_db : db +val add_user_provided_hint : + #status as 'status -> NCic.term -> int -> 'status val look_for_hint: - db -> + #status -> NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> (NCic.metasenv * diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 9ee056aed..bfa1388a9 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -490,8 +490,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = NCicPp.ppterm ~metasenv ~subst ~context t2); *) let candidates = - NCicUnifHint.look_for_hint - rdb.NRstatus.uhint_db metasenv subst context t1 t2 + NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2 in let rec cand_iter = function | [] -> None (* raise exc *) diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli index 23728e4f8..a6ddfaeed 100644 --- a/helm/software/components/ng_refiner/nCicUnification.mli +++ b/helm/software/components/ng_refiner/nCicUnification.mli @@ -16,7 +16,7 @@ exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; val unify : - NRstatus.refiner_status -> + #NRstatus.status -> ?test_eq_only:bool -> (* default: false *) NCic.metasenv -> NCic.substitution -> NCic.context -> NCic.term -> NCic.term -> diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml index 26ef2684c..736de4aa0 100644 --- a/helm/software/components/ng_refiner/nRstatus.ml +++ b/helm/software/components/ng_refiner/nRstatus.ml @@ -11,16 +11,31 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -type refiner_status = { - coerc_db : NCicCoercion.db; - uhint_db : NCicUnifHint.db; - library_db : NCicLibrary.timestamp; -} +class status = + object + inherit NCicUnifHint.status + inherit NCicCoercion.status + inherit NCicLibrary.status + end + +type sstatus = status module Serializer = - NCicLibrary.Serializer(struct type status = refiner_status end) + 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_uhint_db (rstatus#uhint_db) in + let status = status#set_coerc_db (rstatus#coerc_db) in + let status = status#set_timestamp (rstatus#timestamp) in + status + end -type dumpable_refiner_status = { - refiner_status : refiner_status; - dump: Serializer.obj list -} +class dumpable_status = + object + inherit status + val dump = ([] : Serializer.obj list) + method dump = dump + method set_dump v = {< dump = v >} + end diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli index 729f6ba6e..522d7e901 100644 --- a/helm/software/components/ng_refiner/nRstatus.mli +++ b/helm/software/components/ng_refiner/nRstatus.mli @@ -11,15 +11,22 @@ (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *) -type refiner_status = { - coerc_db : NCicCoercion.db; - uhint_db : NCicUnifHint.db; - library_db : NCicLibrary.timestamp; -} +class status : + object + inherit NCicUnifHint.status + inherit NCicCoercion.status + inherit NCicLibrary.status + end -module Serializer: NCicLibrary.Serializer with type status = refiner_status +module Serializer: + sig + include NCicLibrary.Serializer with type status = status + val require: baseuri:NUri.uri -> (#status as 'status) -> 'status + end -type dumpable_refiner_status = { - refiner_status : refiner_status; - dump: Serializer.obj list -} +class dumpable_status : + object ('self) + inherit status + method dump: Serializer.obj list + method set_dump: Serializer.obj list -> 'self + end diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index ba0308068..6aaf4a4a8 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.NRstatus.refiner_status m s c t1 t2) + status.estatus.NEstatus.rstatus 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.NRstatus.refiner_status metasenv subst ctx a b + NCicUnification.unify status.estatus.NEstatus.rstatus 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.NRstatus.refiner_status in + let rdb = status.estatus.NEstatus.rstatus in let metasenv, subst, t, ty = NCicRefiner.typeof rdb metasenv subst ctx term expty in diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index b6b933211..e751cca58 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -568,7 +568,7 @@ let auto ~params:(l,_) status goal = (status, (t,ty) :: l)) (status,[]) l in - let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in + let rdb = status.estatus.NEstatus.rstatus in Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l; status ;; diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 8acc424a9..e71eb4104 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -90,7 +90,7 @@ let save_moo grafite_status = LexiconMarshal.save_lexicon lexicon_fname (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev; NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - (GrafiteTypes.get_dump grafite_status) + (GrafiteTypes.get_dstatus grafite_status)#dump | _ -> clean_current_baseuri grafite_status ;; diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 5ed1d41b4..7575eca10 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -227,7 +227,7 @@ let main () = | s::_ -> s.proof_status, s.moo_content_rev, (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev, - GrafiteTypes.get_dump s + (GrafiteTypes.get_dstatus s)#dump | _ -> assert false in if proof_status <> GrafiteTypes.No_proof then diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index c0c3d0941..e26a3f89d 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -275,7 +275,7 @@ let compile atstart options fname = 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) - (GrafiteTypes.get_dump grafite_status) + (GrafiteTypes.get_dstatus grafite_status)#dump end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in -- 2.39.2