;;
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
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 []
;;
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
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;;
^ " 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"))
;;
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;;
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;
" 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
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
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
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
;;
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 [];;
let init = load_db;;
+
class status =
object
val timestamp = (time0 : timestamp)
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
;;
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;
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
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)
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
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 _ ->
(* 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) *)
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
projects / helm.git / commitdiff