(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 =
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 []
;;
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
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
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;
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 = {
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
+ };
}
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
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;;
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
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)
(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
~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
type extra_status = {
lstatus : LexiconEngine.status;
- rstatus : NRstatus.dumpable_refiner_status;
+ rstatus : NRstatus.dumpable_status;
}
type extra_status = {
lstatus : LexiconEngine.status;
- rstatus : NRstatus.dumpable_refiner_status;
+ rstatus : NRstatus.dumpable_status;
}
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, ())
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, [], [], ())
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 ->
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) ->
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
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);;
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 =
) il)
in
aliases := references @ !aliases;
- !storage,!aliases,!cache
+ status#set_timestamp (!storage,!aliases,!cache)
;;
let get_obj u =
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) *)
val clear_cache : unit -> unit
-val time_travel: timestamp -> unit
+val time_travel: #status -> unit
val decompile: baseuri:NUri.uri -> unit
module type Serializer =
val nparamod :
- NRstatus.refiner_status ->
+ #NRstatus.status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
(NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
unit
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
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:" ^
*)
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
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 _::_)) -> []
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 ->
| 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
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 *)
(* menv, subst,refined term, type *)
val typeof_obj :
- NRstatus.refiner_status ->
+ #NRstatus.status ->
?localise:(NCic.term -> Stdpp.location) ->
NCic.obj -> NCic.obj
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]) ;;
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
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)
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 *
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 *)
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 ->
(* $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
(* $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
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)
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 }
;;
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
(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
;;
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
;;
| 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
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
projects / helm.git / commitdiff