diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.mli | 2 | ||||
| -rw-r--r-- | library/universes.ml | 83 | ||||
| -rw-r--r-- | library/universes.mli | 13 |
3 files changed, 48 insertions, 50 deletions
diff --git a/library/global.mli b/library/global.mli index 03469bea4..09ed4eb0a 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/universes.ml b/library/universes.ml index a8e9478e1..96937b3b3 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_small_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 -> @@ -1021,7 +1016,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 45672ef46..7b17b8898 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 *) |