diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/libobject.ml | 21 | ||||
| -rw-r--r-- | library/libobject.mli | 5 | ||||
| -rw-r--r-- | library/summary.ml | 26 | ||||
| -rw-r--r-- | library/summary.mli | 4 | ||||
| -rw-r--r-- | library/universes.ml | 83 | ||||
| -rw-r--r-- | library/universes.mli | 13 |
8 files changed, 99 insertions, 57 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 7f607a51c9..d8c5ab5e74 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -371,7 +371,7 @@ let rec replace_module_object idl mp0 objs0 mp1 objs1 = match idl, objs0 with | _,[] -> [] | id::idl,(id',obj)::tail when Id.equal id id' -> - assert (object_has_tag obj "MODULE"); + assert (String.equal (object_tag obj) "MODULE"); let mp_id = MPdot(mp0, Label.of_id id) in let objs = match idl with | [] -> Lib.subst_objects (map_mp mp1 mp_id empty_delta_resolver) objs1 diff --git a/library/global.mli b/library/global.mli index 03469bea41..09ed4eb0a8 100644 --- a/library/global.mli +++ b/library/global.mli @@ -19,7 +19,7 @@ val env : unit -> Environ.env val env_is_initial : unit -> bool -val universes : unit -> Univ.universes +val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val val named_context : unit -> Context.named_context diff --git a/library/libobject.ml b/library/libobject.ml index 85c830ea2c..f0d281a2dd 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -8,6 +8,9 @@ open Libnames open Pp +open Util + +module Dyn = Dyn.Make(struct end) (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -70,15 +73,25 @@ type dynamic_object_declaration = { dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } -let object_tag = Dyn.tag -let object_has_tag = Dyn.has_tag +let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let declare_object_full odecl = let na = odecl.object_name in - let (infun,outfun) = Dyn.create na in + let tag = Dyn.create na in + let (infun, outfun) = make_dyn tag in let cacher (oname,lobj) = odecl.cache_function (oname,outfun lobj) and loader i (oname,lobj) = odecl.load_function i (oname,outfun lobj) and opener i (oname,lobj) = odecl.open_function i (oname,outfun lobj) @@ -158,3 +171,5 @@ let discharge_object ((_,lobj) as node) = let rebuild_object lobj = apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + +let dump = Dyn.dump diff --git a/library/libobject.mli b/library/libobject.mli index 099381897f..12b1a558f8 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -99,7 +99,6 @@ val declare_object : 'a object_declaration -> ('a -> obj) val object_tag : obj -> string -val object_has_tag : obj -> string -> bool val cache_object : object_name * obj -> unit val load_object : int -> object_name * obj -> unit @@ -109,3 +108,7 @@ val classify_object : obj -> obj substitutivity val discharge_object : object_name * obj -> obj option val rebuild_object : obj -> obj val relax : bool -> unit + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/summary.ml b/library/summary.ml index 8e2abbf15b..a922e155dd 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -10,6 +10,8 @@ open Pp open Errors open Util +module Dyn = Dyn.Make(struct end) + type marshallable = [ `Yes | `No | `Shallow ] type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -20,8 +22,19 @@ let summaries = ref Int.Map.empty let mangle id = id ^ "-SUMMARY" +let make_dyn (type a) (tag : a Dyn.tag) = + let infun x = Dyn.Dyn (tag, x) in + let outfun : (Dyn.t -> a) = fun dyn -> + let Dyn.Dyn (t, x) = dyn in + match Dyn.eq t tag with + | None -> assert false + | Some Refl -> x + in + (infun, outfun) + let internal_declare_summary hash sumname sdecl = - let (infun, outfun) = Dyn.create (mangle sumname) in + let tag = Dyn.create (mangle sumname) in + let (infun, outfun) = make_dyn tag in let dyn_freeze b = infun (sdecl.freeze_function b) and dyn_unfreeze sum = sdecl.unfreeze_function (outfun sum) and dyn_init = sdecl.init_function in @@ -164,8 +177,15 @@ let project_summary { summaries; ml_module } ?(complement=false) ids = List.filter (fun (id, _) -> List.mem id ids) summaries let pointer_equal l1 l2 = + let ptr_equal d1 d2 = + let Dyn.Dyn (t1, x1) = d1 in + let Dyn.Dyn (t2, x2) = d2 in + match Dyn.eq t1 t2 with + | None -> false + | Some Refl -> x1 == x2 + in CList.for_all2eq - (fun (id1,v1) (id2,v2) -> id1 = id2 && Dyn.pointer_equal v1 v2) l1 l2 + (fun (id1,v1) (id2,v2) -> id1 = id2 && ptr_equal v1 v2) l1 l2 (** All-in-one reference declaration + registration *) @@ -176,3 +196,5 @@ let ref ?(freeze=fun _ r -> r) ~name x = unfreeze_function = ((:=) r); init_function = (fun () -> r := x) }; r + +let dump = Dyn.dump diff --git a/library/summary.mli b/library/summary.mli index 48c9390d07..a35113fd2e 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -71,3 +71,7 @@ val unfreeze_summary : frozen_bits -> unit val surgery_summary : frozen -> frozen_bits -> frozen val project_summary : frozen -> ?complement:bool -> string list -> frozen_bits val pointer_equal : frozen_bits -> frozen_bits -> bool + +(** {6 Debug} *) + +val dump : unit -> (int * string) list diff --git a/library/universes.ml b/library/universes.ml index 3eae612c8c..b9b148b57b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -102,6 +102,7 @@ module Constraints = struct end type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints @@ -135,82 +136,76 @@ let to_constraints g s = | _, ULe, Some l' -> enforce_leq x y acc | _, ULub, _ -> acc | _, d, _ -> - let f = if d == ULe then check_leq else check_eq in + let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in if f g x y then acc else raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") in Constraints.fold tr s Constraint.empty -let eq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty +let eq_constr_univs_infer univs fold m n accu = + if m == n then Some accu else - let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let cstrs = ref accu in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) -let eq_constr_univs_infer_with kind1 kind2 univs m n = +let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = (* spiwack: duplicates the code of [eq_constr_univs_infer] because I haven't find a way to factor the code without destroying pointer-equality optimisations in [eq_constr_univs_infer]. Pointer equality is not sufficient to ensure equality up to [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) - let cstrs = ref Constraints.empty in - let eq_universes strict = Univ.Instance.check_eq univs in + let cstrs = ref accu in + let eq_universes strict = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in - res, !cstrs + if res then Some !cstrs else None -let leq_constr_univs_infer univs m n = - if m == n then true, Constraints.empty +let leq_constr_univs_infer univs fold m n accu = + if m == n then Some accu else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in + let cstrs = ref accu in + let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_eq univs u1 u2 then true - else (cstrs := Constraints.add (u1, UEq, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let leq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then - ((if Univ.is_type0_univ u1 then - cstrs := Constraints.add (u1, ULe, u2) !cstrs); - true) - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -220,7 +215,7 @@ let leq_constr_univs_infer univs m n = eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in - res, !cstrs + if res then Some !cstrs else None let eq_constr_universes m n = if m == n then true, Constraints.empty @@ -650,14 +645,14 @@ let normalize_univ_variable_opt_subst ectx = in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - ectx := Univ.LMap.add l (Some b) !ectx; b + try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_univ_variable_subst subst = let find l = Univ.LMap.find l !subst in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - subst := Univ.LMap.add l b !subst; b in + try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = @@ -869,27 +864,27 @@ let normalize_context_set ctx us algs = let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g) - ctx Univ.empty_universes + let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + ctx UGraph.empty_universes in let g = Univ.Constraint.fold (fun (l, d, r) g -> let g = if not (Level.is_small l || LSet.mem l ctx) then - try Univ.add_universe l false g - with Univ.AlreadyDeclared -> g + try UGraph.add_universe l false g + with UGraph.AlreadyDeclared -> g else g in let g = if not (Level.is_small r || LSet.mem r ctx) then - try Univ.add_universe r false g - with Univ.AlreadyDeclared -> g + try UGraph.add_universe r false g + with UGraph.AlreadyDeclared -> g else g in g) csts g in - let g = Univ.Constraint.fold Univ.enforce_constraint csts g in - Univ.constraints_of_universes g + let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + UGraph.constraints_of_universes g in let noneqs = Constraint.fold (fun (l,d,r as cstr) noneqs -> @@ -1027,7 +1022,7 @@ let refresh_constraints univs (ctx, cstrs) = Univ.Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in if is_trivial_leq c then acc - else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) + else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs)) cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') diff --git a/library/universes.mli b/library/universes.mli index 45672ef460..7b17b88987 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -63,6 +63,7 @@ module Constraints : sig end type universe_constraints = Constraints.t +type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option type 'a universe_constrained = 'a * universe_constraints type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints @@ -71,11 +72,12 @@ val subst_univs_universe_constraints : universe_subst_fn -> val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function -val to_constraints : universes -> universe_constraints -> constraints +val to_constraints : UGraph.t -> universe_constraints -> constraints (** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose @@ -83,12 +85,13 @@ val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_ val eq_constr_univs_infer_with : (constr -> (constr,types) kind_of_term) -> (constr -> (constr,types) kind_of_term) -> - Univ.universes -> constr -> constr -> bool universe_constrained + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] modulo alpha, casts, application grouping, the universe constraints in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained +val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> + constr -> constr -> 'a -> 'a option (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) @@ -223,7 +226,7 @@ val restrict_universe_context : universe_context_set -> universe_set -> universe val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst -val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes +val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_set * UGraph.t (** Pretty-printing *) |