From 2338b758114eb40daf3fadf4fb016a9a1af541b6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 23 Jun 2009 16:00:55 +0000 Subject: [PATCH] undo/serialization for universes implemented --- .../grafite_engine/grafiteEngine.ml | 31 ++++++++++-- .../components/ng_kernel/nCicEnvironment.ml | 45 +++++++++++------ .../components/ng_kernel/nCicEnvironment.mli | 4 +- .../components/ng_kernel/nCicLibrary.ml | 48 +++++++++++++------ .../components/ng_kernel/nCicLibrary.mli | 4 +- 5 files changed, 98 insertions(+), 34 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index b6a8786f2..5d1ea5096 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -475,7 +475,10 @@ let basic_eval_unification_hint (t,n) status = ;; let inject_unification_hint = - let basic_eval_unification_hint (t,n) ~refresh_uri_in_term = + let basic_eval_unification_hint (t,n) + ~refresh_uri_in_universe + ~refresh_uri_in_term + = let t = refresh_uri_in_term t in basic_eval_unification_hint (t,n) in NRstatus.Serializer.register "unification_hints" basic_eval_unification_hint @@ -488,6 +491,29 @@ let eval_unification_hint status t n = let t = NCicUntrusted.apply_subst subst [] t in let status = basic_eval_unification_hint (t,n) status in let dump = inject_unification_hint (t,n)::status#dump in + let status = status#set_dump dump in + status,`New [] +;; + +let basic_eval_add_constraint (s,u1,u2) status = + NCicLibrary.add_constraint status s u1 u2 +;; + +let inject_constraint = + let basic_eval_add_constraint (s,u1,u2) + ~refresh_uri_in_universe + ~refresh_uri_in_term + = + let u1 = refresh_uri_in_universe u1 in + let u2 = refresh_uri_in_universe u2 in + basic_eval_add_constraint (s,u1,u2) + in + NRstatus.Serializer.register "constraints" basic_eval_add_constraint +;; + +let eval_add_constraint status s u1 u2 = + let status = basic_eval_add_constraint (s,u1,u2) status in + let dump = inject_constraint (s,u1,u2)::status#dump in let status = status#set_dump dump in status,`Old [] ;; @@ -727,8 +753,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) | _ -> status,`New []) | GrafiteAst.NUnivConstraint (loc,strict,u1,u2) -> - NCicEnvironment.add_constraint strict [false,u1] [false,u2]; - status, `New [u1;u2] + eval_add_constraint status strict [false,u1] [false,u2] ;; let rec eval_command = {ec_go = fun ~disambiguate_command opts status diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 2d5f03945..78abb6801 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -19,6 +19,10 @@ exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; +let cache = NUri.UriHash.create 313;; +let history = ref [];; +let frozen_list = ref [];; + let get_obj = ref (fun _ -> assert false);; let set_get_obj f = get_obj := f;; @@ -79,7 +83,8 @@ let add_constraint strict a b = ^ " to:\n" ^ pp_constraints ())))); universes := a2 :: b2 :: List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes; - le_constraints := (strict,a2,b2) :: !le_constraints) + le_constraints := (strict,a2,b2) :: !le_constraints); + history := (`Constr (strict,a,b))::!history; | _ -> raise (BadConstraint (lazy "trying to add a constraint on an inferred universe")) ;; @@ -112,20 +117,30 @@ let set_typecheck_obj f = end ;; -let cache = NUri.UriHash.create 313;; -let history = ref [];; -let frozen_list = ref [];; - -let invalidate_obj uri = +let invalidate_item item = + let item_eq a b = + match a, b with + | `Obj (u1,_), `Obj (u2,_) -> NUri.eq u1 u2 + | `Constr _, `Constr _ -> a=b (* MAKE EFFICIENT *) + | _ -> false + in let rec aux to_be_deleted = function [] -> assert false - | uri'::tl when NUri.eq uri uri' -> uri'::to_be_deleted,tl - | uri'::tl -> aux (uri'::to_be_deleted) tl + | item'::tl when item_eq item item' -> item'::to_be_deleted,tl + | item'::tl -> aux (item'::to_be_deleted) tl in let to_be_deleted,h = aux [] !history in history := h; - List.iter (fun uri -> NUri.UriHash.remove cache uri) to_be_deleted + List.iter + (function + | `Obj (uri,_) -> NUri.UriHash.remove cache uri + | `Constr (strict,[_,u1],[_,u2]) as c -> + let w = strict,u1,u2 in + if not(List.mem c !history) then + le_constraints := List.filter ((<>) w) !le_constraints; + | `Constr _ -> assert false + ) to_be_deleted ;; exception Propagate of NUri.uri * exn;; @@ -142,10 +157,10 @@ let check_and_add_obj ((u,_,_,_,_) as obj) = frozen_list := (u,obj)::saved_frozen_list; !typecheck_obj obj; frozen_list := saved_frozen_list; - let obj = `WellTyped obj in - NUri.UriHash.add cache u obj; - history := u::!history; - obj + let obj' = `WellTyped obj in + NUri.UriHash.add cache u obj'; + history := (`Obj (u,obj))::!history; + obj' with Sys.Break as e -> frozen_list := saved_frozen_list; @@ -157,7 +172,7 @@ let check_and_add_obj ((u,_,_,_,_) as obj) = " which is not well-typed"), match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in NUri.UriHash.add cache u exn; - history := u::!history; + history := (`Obj (u,obj))::!history; if saved_frozen_list = [] then exn else @@ -166,7 +181,7 @@ let check_and_add_obj ((u,_,_,_,_) as obj) = frozen_list := saved_frozen_list; let exn = `Exn e in NUri.UriHash.add cache u exn; - history := u::!history; + history := (`Obj (u,obj))::!history; if saved_frozen_list = [] then exn else diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index a9feb4d20..5252ddb8b 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -51,7 +51,9 @@ val get_checked_fixes_or_cofixes: NCic.inductiveFun list * NCic.f_attr * int (* invalidate the object and all those that entered the environment after it *) -val invalidate_obj: NUri.uri -> unit +val invalidate_item: + [ `Obj of NUri.uri * NCic.obj + | `Constr of bool * NCic.universe * NCic.universe ] -> unit val invalidate: unit -> unit diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 1efe173e7..43b4a78a3 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -13,14 +13,19 @@ exception LibraryOutOfSync of string Lazy.t -let magic = 1;; +let magic = 2;; let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; +let refresh_uri_in_universe = + List.map (fun (x,u) -> x, refresh_uri u) +;; + let rec refresh_uri_in_term = function - NCic.Const (NReference.Ref (u,spec)) -> + | NCic.Const (NReference.Ref (u,spec)) -> NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) + | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l)) | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t ;; @@ -57,11 +62,14 @@ let require0 ~baseuri = require_path (path_of_baseuri baseuri);; let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";; + type timestamp = - (NUri.uri * NCic.obj) list * + [ `Obj of NUri.uri * NCic.obj + | `Constr of bool * NCic.universe * NCic.universe] list * (NUri.uri * string * NReference.reference) list * NCic.obj NUri.UriMap.t * - NUri.uri list;; + NUri.uri list +;; let time0 = [],[],NUri.UriMap.empty,[];; let storage = ref [];; @@ -126,6 +134,7 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= let init = load_db;; + class status = object val timestamp = (time0 : timestamp) @@ -141,8 +150,7 @@ let time_travel status = let diff_len = List.length !storage - List.length sto in let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in if List.length to_be_deleted > 0 then - let u,_ = HExtlib.list_last to_be_deleted in - NCicEnvironment.invalidate_obj u; + NCicEnvironment.invalidate_item (HExtlib.list_last to_be_deleted); storage := sto; local_aliases := ali; cache := cac; includes := inc ;; @@ -151,10 +159,12 @@ let serialize ~baseuri dump = Marshal.to_channel ch (magic,dump) []; close_out ch; List.iter - (fun (uri,obj) -> - let ch = open_out (path_of_baseuri uri) in - Marshal.to_channel ch (magic,obj) []; - close_out ch + (function + | `Obj (uri,obj) -> + let ch = open_out (path_of_baseuri uri) in + Marshal.to_channel ch (magic,obj) []; + close_out ch + | `Constr _ -> () ) !storage; set_global_aliases (!local_aliases @ get_global_aliases ()); List.iter (fun u -> add_deps u [baseuri]) !includes; @@ -167,7 +177,7 @@ module type Serializer = type obj val register: string -> - ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> ('a -> obj) val serialize: baseuri:NUri.uri -> obj list -> unit val require: baseuri:NUri.uri -> status -> status @@ -187,7 +197,7 @@ module Serializer(S: sig type status end) = require1 := (fun (tag',data) as x -> if tag=tag' then - require (Obj.magic data) ~refresh_uri_in_term + require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term else !require1 x); (fun x -> tag,Obj.repr x) @@ -256,7 +266,7 @@ let aliases_of uri = let add_obj status ((u,_,_,_,_) as obj) = NCicEnvironment.check_and_add_obj obj; - storage := (u,obj)::!storage; + storage := (`Obj (u,obj))::!storage; let _,height,_,_,obj = obj in let references = match obj with @@ -289,8 +299,18 @@ let add_obj status ((u,_,_,_,_) as obj) = status#set_timestamp (!storage,!local_aliases,!cache,!includes) ;; +let add_constraint status strict u1 u2 = + NCicEnvironment.add_constraint strict u1 u2; + storage := (`Constr (strict,u1,u2)) :: !storage; + status#set_timestamp (!storage,!local_aliases,!cache,!includes) +;; + let get_obj u = - try List.assq u !storage + try + List.assq u + (HExtlib.filter_map + (function `Obj (u,o) -> Some (u,o) | _ -> None ) + !storage) with Not_found -> try fetch_obj u with Sys_error _ -> diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 91bf96c69..30dcc263c 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -24,6 +24,8 @@ class status : (* it also checks it and add it to the environment *) val add_obj: #status as 'status -> NCic.obj -> 'status +val add_constraint: + #status as 'status -> bool -> NCic.universe -> NCic.universe -> 'status val aliases_of: NUri.uri -> NReference.reference list val resolve: string -> NReference.reference list (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) @@ -40,7 +42,7 @@ module type Serializer = type obj val register: string -> - ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> + ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) -> ('a -> obj) val serialize: baseuri:NUri.uri -> obj list -> unit val require: baseuri:NUri.uri -> status -> status -- 2.39.2