From 302adae094bbf76d8c951c557c85acb12a97aedc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 28 Apr 2018 21:27:15 +0200 Subject: Split off Universes functions about substitutions and constraints --- engine/eConstr.ml | 36 ++--- engine/eConstr.mli | 6 +- engine/engine.mllib | 2 + engine/evarutil.ml | 16 +-- engine/evarutil.mli | 2 +- engine/evd.ml | 12 +- engine/evd.mli | 8 +- engine/termops.ml | 2 +- engine/uState.ml | 26 ++-- engine/uState.mli | 6 +- engine/univProblem.ml | 166 +++++++++++++++++++++++ engine/univProblem.mli | 55 ++++++++ engine/univSubst.ml | 177 +++++++++++++++++++++++++ engine/univSubst.mli | 53 ++++++++ engine/universes.ml | 353 +++++-------------------------------------------- engine/universes.mli | 180 +++++++++++++------------ 16 files changed, 640 insertions(+), 460 deletions(-) create mode 100644 engine/univProblem.ml create mode 100644 engine/univProblem.mli create mode 100644 engine/univSubst.ml create mode 100644 engine/univSubst.mli (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index d30cb74d7..2ab545612 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -446,28 +446,28 @@ let compare_constr sigma cmp c1 c2 = compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2) let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs = - let open Universes in + let open UnivProblem in if not nargs_ok then enforce_eq_instances_univs false u u' cstrs else CArray.fold_left3 (fun cstrs v u u' -> let open Univ.Variance in match v with - | Irrelevant -> Constraints.add (UWeak (u,u')) cstrs + | Irrelevant -> Set.add (UWeak (u,u')) cstrs | Covariant -> let u = Univ.Universe.make u in let u' = Univ.Universe.make u' in (match cv_pb with - | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs - | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs) + | Reduction.CONV -> Set.add (UEq (u,u')) cstrs + | Reduction.CUMUL -> Set.add (ULe (u,u')) cstrs) | Invariant -> let u = Univ.Universe.make u in let u' = Univ.Universe.make u' in - Constraints.add (UEq (u,u')) cstrs) + Set.add (UEq (u,u')) cstrs) cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u') let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = - let open Universes in + let open UnivProblem in match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0); @@ -480,7 +480,7 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs = compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = - let open Universes in + let open UnivProblem in match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> cstrs @@ -491,7 +491,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs = if not (Int.equal num_cnstr_args nargs) then enforce_eq_instances_univs false u1 u2 cstrs else - Array.fold_left2 (fun cstrs u1 u2 -> Universes.(Constraints.add (UWeak (u1,u2)) cstrs)) + Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs)) cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2) let eq_universes env sigma cstrs cv_pb ref nargs l l' = @@ -499,8 +499,8 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = else let l = Evd.normalize_universe_instance sigma l and l' = Evd.normalize_universe_instance sigma l' in - let open Universes in let open GlobRef in + let open UnivProblem in match ref with | VarRef _ -> assert false (* variables don't have instances *) | ConstRef _ -> @@ -515,11 +515,11 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' = true let test_constr_universes env sigma leq m n = - let open Universes in + let open UnivProblem in let kind c = kind_upto sigma c in - if m == n then Some Constraints.empty + if m == n then Some Set.empty else - let cstrs = ref Constraints.empty in + let cstrs = ref Set.empty in let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l' and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in @@ -527,7 +527,7 @@ let test_constr_universes env sigma leq m n = let s1 = ESorts.kind sigma (ESorts.make s1) in let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true - else (cstrs := Constraints.add + else (cstrs := Set.add (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in @@ -536,7 +536,7 @@ let test_constr_universes env sigma leq m n = let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else - (cstrs := Constraints.add + (cstrs := Set.add (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs; true) in @@ -574,15 +574,15 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' nargs m n let eq_constr_universes_proj env sigma m n = - let open Universes in - if m == n then Some Constraints.empty + let open UnivProblem in + if m == n then Some Set.empty else - let cstrs = ref Constraints.empty in + let cstrs = ref Set.empty in let eq_universes ref l l' = eq_universes env sigma cstrs Reduction.CONV ref l l' in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else - (cstrs := Constraints.add + (cstrs := Set.add (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs; true) in diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 743888a9b..b0e834b2e 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -201,11 +201,11 @@ val whd_evar : Evd.evar_map -> constr -> constr val eq_constr : Evd.evar_map -> t -> t -> bool val eq_constr_nounivs : Evd.evar_map -> t -> t -> bool -val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option -val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option +val leq_constr_universes : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option (** [eq_constr_universes_proj] can equate projections and their eta-expanded constant form. *) -val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> Universes.Constraints.t option +val eq_constr_universes_proj : Environ.env -> Evd.evar_map -> t -> t -> UnivProblem.Set.t option val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool diff --git a/engine/engine.mllib b/engine/engine.mllib index 512908e13..befd49dc9 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,5 +1,7 @@ UnivNames UnivGen +UnivSubst +UnivProblem Universes Univops UState diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 2b202ef3e..cb2d01bdf 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -86,7 +86,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=nf_evar sigma v;utj_type=t} let nf_evars_universes evm = - Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) + UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm) (Evd.universe_subst evm) let nf_evars_and_universes evm = @@ -830,13 +830,13 @@ let subterm_source evk ?where (loc,k) = (* Add equality constraints for covariant/invariant positions. For irrelevant positions, unify universes when flexible. *) let compare_cumulative_instances cv_pb variances u u' sigma = - let open Universes in + let open UnivProblem in let cstrs = Univ.Constraint.empty in - let soft = Constraints.empty in + let soft = Set.empty in let cstrs, soft = Array.fold_left3 (fun (cstrs, soft) v u u' -> let open Univ.Variance in match v with - | Irrelevant -> cstrs, Constraints.add (UWeak (u,u')) soft + | Irrelevant -> cstrs, Set.add (UWeak (u,u')) soft | Covariant when cv_pb == Reduction.CUMUL -> Univ.Constraint.add (u,Univ.Le,u') cstrs, soft | Covariant | Invariant -> Univ.Constraint.add (u,Univ.Eq,u') cstrs, soft) @@ -848,10 +848,10 @@ let compare_cumulative_instances cv_pb variances u u' sigma = | exception Univ.UniverseInconsistency p -> Inr p let compare_constructor_instances evd u u' = - let open Universes in + let open UnivProblem in let soft = - Array.fold_left2 (fun cs u u' -> Constraints.add (UWeak (u,u')) cs) - Constraints.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') + Array.fold_left2 (fun cs u u' -> Set.add (UWeak (u,u')) cs) + Set.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') in Evd.add_universe_constraints evd soft @@ -870,7 +870,7 @@ let eq_constr_univs_test sigma1 sigma2 t u = with Univ.UniverseInconsistency _ | UniversesDiffer -> None in let ans = - Universes.eq_constr_univs_infer_with + UnivProblem.eq_constr_univs_infer_with (fun t -> kind_of_term_upto sigma1 t) (fun u -> kind_of_term_upto sigma2 u) (universes sigma2) fold t u sigma2 diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 7dd98bac9..3ab2d3e34 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -284,5 +284,5 @@ val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val e_new_global : evar_map ref -> GlobRef.t -> constr [@@ocaml.deprecated "Use [Evd.new_global]"] -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst [@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] diff --git a/engine/evd.ml b/engine/evd.ml index b2b8e7ccc..03b843655 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -843,12 +843,12 @@ let universe_rigidity evd l = let normalize_universe evd = let vars = UState.subst evd.universes in - let normalize = Universes.normalize_universe_opt_subst vars in + let normalize = UnivSubst.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = let vars = UState.subst evd.universes in - let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in + let normalize = UnivSubst.level_subst_of (UnivSubst.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l let normalize_sort evars s = @@ -866,7 +866,7 @@ let set_eq_sort env d s1 s2 = | Some (u1, u2) -> if not (type_in_type env) then add_universe_constraints d - (Universes.Constraints.singleton (Universes.UEq (u1,u2))) + (UnivProblem.Set.singleton (UnivProblem.UEq (u1,u2))) else d @@ -878,7 +878,7 @@ let set_leq_level d u1 u2 = let set_eq_instances ?(flex=false) d u1 u2 = add_universe_constraints d - (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty) + (UnivProblem.enforce_eq_instances_univs flex u1 u2 UnivProblem.Set.empty) let set_leq_sort env evd s1 s2 = let s1 = normalize_sort evd s1 @@ -887,7 +887,7 @@ let set_leq_sort env evd s1 s2 = | None -> evd | Some (u1, u2) -> if not (type_in_type env) then - add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2))) + add_universe_constraints evd (UnivProblem.Set.singleton (UnivProblem.ULe (u1,u2))) else evd let check_eq evd s s' = @@ -1297,7 +1297,7 @@ module MiniEConstr = struct | Some _ as v -> v | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") in - Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c + UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c let of_named_decl d = d let unsafe_to_named_decl d = d diff --git a/engine/evd.mli b/engine/evd.mli index 7ce525744..b2670ee51 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -354,7 +354,7 @@ val whd_sort_variable : evar_map -> econstr -> econstr exception UniversesDiffer -val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map +val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map (** Add the given universe unification constraints to the evar map. @raise UniversesDiffer in case a first-order unification fails. @raise UniverseInconsistency . @@ -543,7 +543,7 @@ val empty_evar_universe_context : UState.t val union_evar_universe_context : UState.t -> UState.t -> UState.t [@@ocaml.deprecated "Alias of UState.union"] -val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +val evar_universe_context_subst : UState.t -> UnivSubst.universe_opt_subst [@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t [@@ocaml.deprecated "Alias of UState.constrain_variables"] @@ -603,7 +603,7 @@ val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t -val universe_subst : evar_map -> Universes.universe_opt_subst +val universe_subst : evar_map -> UnivSubst.universe_opt_subst val universes : evar_map -> UGraph.t (** [to_universe_context evm] extracts the local universes and @@ -622,7 +622,7 @@ val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map -val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map +val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/engine/termops.ml b/engine/termops.ml index 9e975da58..c271d9d99 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -306,7 +306,7 @@ let pr_evar_universe_context ctx = str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ str "WEAK CONSTRAINTS:"++brk(0,1)++ h 0 (UState.pr_weak prl ctx) ++ fnl ()) diff --git a/engine/uState.ml b/engine/uState.ml index 839bb5ae9..6111ec7ed 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -27,7 +27,7 @@ type t = { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) - uctx_univ_variables : Universes.universe_opt_subst; + uctx_univ_variables : UnivSubst.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.LSet.t; (** The subset of unification variables that can be instantiated with @@ -152,7 +152,8 @@ let drop_weak_constraints = ref false let process_universe_constraints ctx cstrs = let open Univ in - let open Universes in + let open UnivSubst in + let open UnivProblem in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in @@ -203,7 +204,7 @@ let process_universe_constraints ctx cstrs = in let unify_universes cst local = let cst = nf_constraint cst in - if Constraints.is_trivial cst then local + if UnivProblem.is_trivial cst then local else match cst with | ULe (l, r) -> @@ -241,7 +242,7 @@ let process_universe_constraints ctx cstrs = | UEq (l, r) -> equalize_universes l r local in let local = - Constraints.fold unify_universes cstrs Univ.Constraint.empty + UnivProblem.Set.fold unify_universes cstrs Univ.Constraint.empty in !vars, !weak, local @@ -249,13 +250,14 @@ let add_constraints ctx cstrs = let univs, local = ctx.uctx_local in let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> let l = Univ.Universe.make l and r = Univ.Universe.make r in - let cstr' = match d with + let cstr' = let open UnivProblem in + match d with | Univ.Lt -> - Universes.ULe (Univ.Universe.super l, r) - | Univ.Le -> Universes.ULe (l, r) - | Univ.Eq -> Universes.UEq (l, r) - in Universes.Constraints.add cstr' acc) - cstrs Universes.Constraints.empty + ULe (Univ.Universe.super l, r) + | Univ.Le -> ULe (l, r) + | Univ.Eq -> UEq (l, r) + in UnivProblem.Set.add cstr' acc) + cstrs UnivProblem.Set.empty in let vars, weak, local' = process_universe_constraints ctx cstrs' in { ctx with @@ -549,11 +551,11 @@ let is_sort_variable uctx s = | _ -> None let subst_univs_context_with_def def usubst (ctx, cst) = - (Univ.LSet.diff ctx def, Universes.subst_univs_constraints usubst cst) + (Univ.LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) let normalize_variables uctx = let normalized_variables, undef, def, subst = - Universes.normalize_univ_variables uctx.uctx_univ_variables + UnivSubst.normalize_univ_variables uctx.uctx_univ_variables in let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in let ctx_local', univs = Universes.refresh_constraints uctx.uctx_initial_universes ctx_local in diff --git a/engine/uState.mli b/engine/uState.mli index b1fcefb0a..11aaaf389 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,7 +44,7 @@ val context_set : t -> Univ.ContextSet.t (** The local context of the state, i.e. a set of bound variables together with their associated constraints. *) -val subst : t -> Universes.universe_opt_subst +val subst : t -> UnivSubst.universe_opt_subst (** The local universes that are unification variables *) val ugraph : t -> UGraph.t @@ -79,7 +79,7 @@ val add_constraints : t -> Univ.Constraint.t -> t @raise UniversesDiffer when universes differ *) -val add_universe_constraints : t -> Universes.Constraints.t -> t +val add_universe_constraints : t -> UnivProblem.Set.t -> t (** @raise UniversesDiffer when universes differ *) @@ -104,7 +104,7 @@ val univ_flexible : rigid val univ_flexible_alg : rigid val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t -val merge_subst : t -> Universes.universe_opt_subst -> t +val merge_subst : t -> UnivSubst.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t diff --git a/engine/univProblem.ml b/engine/univProblem.ml new file mode 100644 index 000000000..bc2edc13d --- /dev/null +++ b/engine/univProblem.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Universe.equal u v + | ULub (u, v) | UWeak (u, v) -> Level.equal u v + +let subst_univs fn = function + | ULe (u, v) -> + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in + if Universe.equal u' v' then None + else Some (ULe (u',v')) + | UEq (u, v) -> + let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in + if Universe.equal u' v' then None + else Some (ULe (u',v')) + | ULub (u, v) -> + let u' = level_subst_of fn u and v' = level_subst_of fn v in + if Level.equal u' v' then None + else Some (ULub (u',v')) + | UWeak (u, v) -> + let u' = level_subst_of fn u and v' = level_subst_of fn v in + if Level.equal u' v' then None + else Some (UWeak (u',v')) + +module Set = struct + module S = Set.Make( + struct + type nonrec t = t + + let compare x y = + match x, y with + | ULe (u, v), ULe (u', v') -> + let i = Universe.compare u u' in + if Int.equal i 0 then Universe.compare v v' + else i + | UEq (u, v), UEq (u', v') -> + let i = Universe.compare u u' in + if Int.equal i 0 then Universe.compare v v' + else if Universe.equal u v' && Universe.equal v u' then 0 + else i + | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') -> + let i = Level.compare u u' in + if Int.equal i 0 then Level.compare v v' + else if Level.equal u v' && Level.equal v u' then 0 + else i + | ULe _, _ -> -1 + | _, ULe _ -> 1 + | UEq _, _ -> -1 + | _, UEq _ -> 1 + | ULub _, _ -> -1 + | _, ULub _ -> 1 + end) + + include S + + let add cst s = + if is_trivial cst then s + else add cst s + + let pr_one = let open Pp in function + | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v + | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v + | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v + | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v + + let pr c = + let open Pp in + fold (fun cst pp_std -> + pp_std ++ pr_one cst ++ fnl ()) c (str "") + + let equal x y = + x == y || equal x y + + let subst_univs subst csts = + fold + (fun c -> Option.fold_right add (subst_univs subst c)) + csts empty +end + +type 'a accumulator = Set.t -> 'a -> 'a option +type 'a constrained = 'a * Set.t + +type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t + +let enforce_eq_instances_univs strict x y c = + let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in + let ax = Instance.to_array x and ay = Instance.to_array y in + if Array.length ax != Array.length ay then + CErrors.anomaly Pp.(str "Invalid argument: enforce_eq_instances_univs called with" ++ + str " instances of different lengths."); + CArray.fold_right2 + (fun x y -> Set.add (mk x y)) + ax ay c + +let to_constraints ~force_weak g s = + let invalid () = + raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") + in + let tr cst acc = + match cst with + | ULub (l, l') -> Constraint.add (l, Eq, l') acc + | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc + | UWeak _-> acc + | ULe (l, l') -> + begin match Universe.level l, Universe.level l' with + | Some l, Some l' -> Constraint.add (l, Le, l') acc + | None, Some _ -> enforce_leq l l' acc + | _, None -> + if UGraph.check_leq g l l' + then acc + else invalid () + end + | UEq (l, l') -> + begin match Universe.level l, Universe.level l' with + | Some l, Some l' -> Constraint.add (l, Eq, l') acc + | None, _ | _, None -> + if UGraph.check_eq g l l' + then acc + else invalid () + end + in + Set.fold tr s Constraint.empty + + +(** 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 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 accu in + let eq_universes _ _ = 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 + match fold (Set.singleton (UEq (u1, u2))) !cstrs with + | None -> false + | Some accu -> cstrs := accu; true + in + let rec eq_constr' nargs m n = + Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n + in + let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in + if res then Some !cstrs else None diff --git a/engine/univProblem.mli b/engine/univProblem.mli new file mode 100644 index 000000000..ffaebe15a --- /dev/null +++ b/engine/univProblem.mli @@ -0,0 +1,55 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* bool + +module Set : sig + include Set.S with type elt = t + + val pr : t -> Pp.t + + val subst_univs : universe_subst_fn -> t -> t +end + +type 'a accumulator = Set.t -> 'a -> 'a option +type 'a constrained = 'a * Set.t +type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t + +val enforce_eq_instances_univs : bool -> Instance.t constraint_function + +(** With [force_weak] UWeak constraints are turned into equalities, + otherwise they're forgotten. *) +val to_constraints : force_weak:bool -> UGraph.t -> Set.t -> Constraint.t + +(** [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 + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + UGraph.t -> 'a accumulator -> constr -> constr -> 'a -> 'a option diff --git a/engine/univSubst.ml b/engine/univSubst.ml new file mode 100644 index 000000000..6a433d9fb --- /dev/null +++ b/engine/univSubst.ml @@ -0,0 +1,177 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* enforce_eq u v + | Le -> enforce_leq u v + | Lt -> enforce_leq (super u) v + +let subst_univs_level fn l = + try Some (fn l) + with Not_found -> None + +let subst_univs_constraint fn (u,d,v as c) cstrs = + let u' = subst_univs_level fn u in + let v' = subst_univs_level fn v in + match u', v' with + | None, None -> Constraint.add c cstrs + | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs + | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs + | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs + +let subst_univs_constraints subst csts = + Constraint.fold + (fun c cstrs -> subst_univs_constraint subst c cstrs) + csts Constraint.empty + +let level_subst_of f = + fun l -> + try let u = f l in + match Universe.level u with + | None -> l + | Some l -> l + with Not_found -> l + +let subst_univs_fn_constr f c = + let changed = ref false in + let fu = Univ.subst_univs_universe f in + let fi = Univ.Instance.subst_fn (level_subst_of f) in + let rec aux t = + match kind t with + | Sort (Sorts.Type u) -> + let u' = fu u in + if u' == u then t else + (changed := true; mkSort (Sorts.sort_of_univ u')) + | Const (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkConstU (c, u')) + | Ind (i, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkIndU (i, u')) + | Construct (c, u) -> + let u' = fi u in + if u' == u then t + else (changed := true; mkConstructU (c, u')) + | _ -> map aux t + in + let c' = aux c in + if !changed then c' else c + +let subst_univs_constr subst c = + if Univ.is_empty_subst subst then c + else + let f = Univ.make_subst subst in + subst_univs_fn_constr f c + +let subst_univs_constr = + if Flags.profile then + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr + else subst_univs_constr + +let normalize_univ_variable ~find = + let rec aux cur = + let b = find cur in + let b' = subst_univs_universe aux b in + if Universe.equal b' b then b + else b' + in aux + +let normalize_univ_variable_opt_subst ectx = + let find l = + match Univ.LMap.find l ectx with + | Some b -> b + | None -> raise Not_found + in + normalize_univ_variable ~find + +let normalize_univ_variable_subst subst = + let find l = Univ.LMap.find l subst in + normalize_univ_variable ~find + +let normalize_universe_opt_subst subst = + let normlevel = normalize_univ_variable_opt_subst subst in + subst_univs_universe normlevel + +let normalize_universe_subst subst = + let normlevel = normalize_univ_variable_subst subst in + subst_univs_universe normlevel + +let normalize_opt_subst ctx = + let normalize = normalize_universe_opt_subst ctx in + Univ.LMap.mapi (fun u -> function + | None -> None + | Some v -> Some (normalize v)) ctx + +type universe_opt_subst = Universe.t option universe_map + +let subst_univs_fn_puniverses f (c, u as cu) = + let u' = Instance.subst_fn f u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_opt_subst f subst = + let subst = normalize_univ_variable_opt_subst subst in + let lsubst = level_subst_of subst in + let rec aux c = + match kind c with + | Evar (evk, args) -> + let args = Array.map aux args in + (match try f (evk, args) with Not_found -> None with + | None -> mkEvar (evk, args) + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> Constr.map aux c + in aux + +let make_opt_subst s = + fun x -> + (match Univ.LMap.find x s with + | Some u -> u + | None -> raise Not_found) + +let subst_opt_univs_constr s = + let f = make_opt_subst s in + subst_univs_fn_constr f + +let normalize_univ_variables ctx = + let ctx = normalize_opt_subst ctx in + let undef, def, subst = + Univ.LMap.fold (fun u v (undef, def, subst) -> + match v with + | None -> (Univ.LSet.add u undef, def, subst) + | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) + ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) + in ctx, undef, def, subst + +let pr_universe_body = function + | None -> mt () + | Some v -> str" := " ++ Univ.Universe.pr v + +let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body diff --git a/engine/univSubst.mli b/engine/univSubst.mli new file mode 100644 index 000000000..26e8d1db9 --- /dev/null +++ b/engine/univSubst.mli @@ -0,0 +1,53 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* universe_level_subst_fn +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t + +val subst_univs_constr : universe_subst -> constr -> constr + +type universe_opt_subst = Universe.t option universe_map + +val make_opt_subst : universe_opt_subst -> universe_subst_fn + +val subst_opt_univs_constr : universe_opt_subst -> constr -> constr + +val normalize_univ_variables : universe_opt_subst -> + universe_opt_subst * LSet.t * LSet.t * universe_subst + +val normalize_univ_variable : + find:(Level.t -> Universe.t) -> + Level.t -> Universe.t + +val normalize_univ_variable_opt_subst : universe_opt_subst -> + (Level.t -> Universe.t) + +val normalize_univ_variable_subst : universe_subst -> + (Level.t -> Universe.t) + +val normalize_universe_opt_subst : universe_opt_subst -> + (Universe.t -> Universe.t) + +val normalize_universe_subst : universe_subst -> + (Universe.t -> Universe.t) + +val normalize_opt_subst : universe_opt_subst -> universe_opt_subst + +(** Full universes substitutions into terms *) + +val nf_evars_and_universes_opt_subst : (existential -> constr option) -> + universe_opt_subst -> constr -> constr + +(** Pretty-printing *) + +val pr_universe_opt_subst : universe_opt_subst -> Pp.t diff --git a/engine/universes.ml b/engine/universes.ml index 01660fe04..009328571 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -8,11 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Sorts open Util -open Pp -open Constr open Univ +open UnivSubst (* To disallow minimization to Set *) @@ -27,190 +25,6 @@ let _ = optread = is_set_minimization; optwrite = (:=) set_minimization }) -type universe_constraint = - | ULe of Universe.t * Universe.t - | UEq of Universe.t * Universe.t - | ULub of Level.t * Level.t - | UWeak of Level.t * Level.t - -module Constraints = struct - module S = Set.Make( - struct - type t = universe_constraint - - let compare x y = - match x, y with - | ULe (u, v), ULe (u', v') -> - let i = Universe.compare u u' in - if Int.equal i 0 then Universe.compare v v' - else i - | UEq (u, v), UEq (u', v') -> - let i = Universe.compare u u' in - if Int.equal i 0 then Universe.compare v v' - else if Universe.equal u v' && Universe.equal v u' then 0 - else i - | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') -> - let i = Level.compare u u' in - if Int.equal i 0 then Level.compare v v' - else if Level.equal u v' && Level.equal v u' then 0 - else i - | ULe _, _ -> -1 - | _, ULe _ -> 1 - | UEq _, _ -> -1 - | _, UEq _ -> 1 - | ULub _, _ -> -1 - | _, ULub _ -> 1 - end) - - include S - - let is_trivial = function - | ULe (u, v) | UEq (u, v) -> Universe.equal u v - | ULub (u, v) | UWeak (u, v) -> Level.equal u v - - let add cst s = - if is_trivial cst then s - else add cst s - - let pr_one = function - | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v - | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v - | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v - | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v - - let pr c = - fold (fun cst pp_std -> - pp_std ++ pr_one cst ++ fnl ()) c (str "") - - let equal x y = - x == y || equal x y - -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 - -let enforce_eq_instances_univs strict x y c = - let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in - let ax = Instance.to_array x and ay = Instance.to_array y in - if Array.length ax != Array.length ay then - CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++ - Pp.str " instances of different lengths."); - CArray.fold_right2 - (fun x y -> Constraints.add (mk x y)) - ax ay c - -let enforce_univ_constraint (u,d,v) = - match d with - | Eq -> enforce_eq u v - | Le -> enforce_leq u v - | Lt -> enforce_leq (super u) v - -let subst_univs_level fn l = - try Some (fn l) - with Not_found -> None - -let subst_univs_constraint fn (u,d,v as c) cstrs = - let u' = subst_univs_level fn u in - let v' = subst_univs_level fn v in - match u', v' with - | None, None -> Constraint.add c cstrs - | Some u, None -> enforce_univ_constraint (u,d,Universe.make v) cstrs - | None, Some v -> enforce_univ_constraint (Universe.make u,d,v) cstrs - | Some u, Some v -> enforce_univ_constraint (u,d,v) cstrs - -let subst_univs_constraints subst csts = - Constraint.fold - (fun c cstrs -> subst_univs_constraint subst c cstrs) - csts Constraint.empty - -let level_subst_of f = - fun l -> - try let u = f l in - match Universe.level u with - | None -> l - | Some l -> l - with Not_found -> l - -let subst_univs_universe_constraint fn = function - | ULe (u, v) -> - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in - if Universe.equal u' v' then None - else Some (ULe (u',v')) - | UEq (u, v) -> - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in - if Universe.equal u' v' then None - else Some (ULe (u',v')) - | ULub (u, v) -> - let u' = level_subst_of fn u and v' = level_subst_of fn v in - if Level.equal u' v' then None - else Some (ULub (u',v')) - | UWeak (u, v) -> - let u' = level_subst_of fn u and v' = level_subst_of fn v in - if Level.equal u' v' then None - else Some (UWeak (u',v')) - -let subst_univs_universe_constraints subst csts = - Constraints.fold - (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c)) - csts Constraints.empty - -let to_constraints ~force_weak g s = - let invalid () = - raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") - in - let tr cst acc = - match cst with - | ULub (l, l') -> Constraint.add (l, Eq, l') acc - | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc - | UWeak _-> acc - | ULe (l, l') -> - begin match Universe.level l, Universe.level l' with - | Some l, Some l' -> Constraint.add (l, Le, l') acc - | None, Some _ -> enforce_leq l l' acc - | _, None -> - if UGraph.check_leq g l l' - then acc - else invalid () - end - | UEq (l, l') -> - begin match Universe.level l, Universe.level l' with - | Some l, Some l' -> Constraint.add (l, Eq, l') acc - | None, _ | _, None -> - if UGraph.check_eq g l l' - then acc - else invalid () - end - in - Constraints.fold tr s Constraint.empty - -(** 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 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 accu in - let eq_universes _ _ = 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 - match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with - | None -> false - | Some accu -> cstrs := accu; true - in - let rec eq_constr' nargs m n = - Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n - in - let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in - if res then Some !cstrs else None (** Simplification *) @@ -243,136 +57,6 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) -let subst_univs_fn_constr f c = - let changed = ref false in - let fu = Univ.subst_univs_universe f in - let fi = Univ.Instance.subst_fn (level_subst_of f) in - let rec aux t = - match kind t with - | Sort (Sorts.Type u) -> - let u' = fu u in - if u' == u then t else - (changed := true; mkSort (Sorts.sort_of_univ u')) - | Const (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkConstU (c, u')) - | Ind (i, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkIndU (i, u')) - | Construct (c, u) -> - let u' = fi u in - if u' == u then t - else (changed := true; mkConstructU (c, u')) - | _ -> map aux t - in - let c' = aux c in - if !changed then c' else c - -let subst_univs_constr subst c = - if Univ.is_empty_subst subst then c - else - let f = Univ.make_subst subst in - subst_univs_fn_constr f c - -let subst_univs_constr = - if Flags.profile then - let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in - CProfile.profile2 subst_univs_constr_key subst_univs_constr - else subst_univs_constr - -let normalize_univ_variable ~find = - let rec aux cur = - let b = find cur in - let b' = subst_univs_universe aux b in - if Universe.equal b' b then b - else b' - in aux - -let normalize_univ_variable_opt_subst ectx = - let find l = - match Univ.LMap.find l ectx with - | Some b -> b - | None -> raise Not_found - in - normalize_univ_variable ~find - -let normalize_univ_variable_subst subst = - let find l = Univ.LMap.find l subst in - normalize_univ_variable ~find - -let normalize_universe_opt_subst subst = - let normlevel = normalize_univ_variable_opt_subst subst in - subst_univs_universe normlevel - -let normalize_universe_subst subst = - let normlevel = normalize_univ_variable_subst subst in - subst_univs_universe normlevel - -let normalize_opt_subst ctx = - let normalize = normalize_universe_opt_subst ctx in - Univ.LMap.mapi (fun u -> function - | None -> None - | Some v -> Some (normalize v)) ctx - -type universe_opt_subst = Universe.t option universe_map - -let subst_univs_fn_puniverses f (c, u as cu) = - let u' = Instance.subst_fn f u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_opt_subst f subst = - let subst = normalize_univ_variable_opt_subst subst in - let lsubst = level_subst_of subst in - let rec aux c = - match kind c with - | Evar (evk, args) -> - let args = Array.map aux args in - (match try f (evk, args) with Not_found -> None with - | None -> mkEvar (evk, args) - | Some c -> aux c) - | Const pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> Constr.map aux c - in aux - -let make_opt_subst s = - fun x -> - (match Univ.LMap.find x s with - | Some u -> u - | None -> raise Not_found) - -let subst_opt_univs_constr s = - let f = make_opt_subst s in - subst_univs_fn_constr f - -let normalize_univ_variables ctx = - let ctx = normalize_opt_subst ctx in - let undef, def, subst = - Univ.LMap.fold (fun u v (undef, def, subst) -> - match v with - | None -> (Univ.LSet.add u undef, def, subst) - | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) - ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) - in ctx, undef, def, subst - -let pr_universe_body = function - | None -> mt () - | Some v -> str" := " ++ Univ.Universe.pr v - -let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body - (* Eq < Le < Lt *) let compare_constraint_type d d' = match d, d' with @@ -448,6 +132,7 @@ let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t let _pr_constraints_map (cmap:constraints_map) = + let open Pp in LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ @@ -763,3 +448,37 @@ let extend_context = UnivGen.extend_context let constr_of_global = UnivGen.constr_of_global let constr_of_reference = UnivGen.constr_of_global let type_of_global = UnivGen.type_of_global + +(** UnivSubst *) + +let level_subst_of = UnivSubst.level_subst_of +let subst_univs_constraints = UnivSubst.subst_univs_constraints +let subst_univs_constr = UnivSubst.subst_univs_constr +type universe_opt_subst = UnivSubst.universe_opt_subst +let make_opt_subst = UnivSubst.make_opt_subst +let subst_opt_univs_constr = UnivSubst.subst_opt_univs_constr +let normalize_univ_variables = UnivSubst.normalize_univ_variables +let normalize_univ_variable = UnivSubst.normalize_univ_variable +let normalize_univ_variable_opt_subst = UnivSubst.normalize_univ_variable_opt_subst +let normalize_univ_variable_subst = UnivSubst.normalize_univ_variable_subst +let normalize_universe_opt_subst = UnivSubst.normalize_universe_opt_subst +let normalize_universe_subst = UnivSubst.normalize_universe_subst +let nf_evars_and_universes_opt_subst = UnivSubst.nf_evars_and_universes_opt_subst +let pr_universe_opt_subst = UnivSubst.pr_universe_opt_subst + +(** UnivProblem *) + +type universe_constraint = UnivProblem.t = + | ULe of Universe.t * Universe.t + | UEq of Universe.t * Universe.t + | ULub of Level.t * Level.t + | UWeak of Level.t * Level.t + +module Constraints = UnivProblem.Set +type 'a constraint_accumulator = 'a UnivProblem.accumulator +type 'a universe_constrained = 'a UnivProblem.constrained +type 'a universe_constraint_function = 'a UnivProblem.constraint_function +let subst_univs_universe_constraints = UnivProblem.Set.subst_univs +let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs +let to_constraints = UnivProblem.to_constraints +let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with diff --git a/engine/universes.mli b/engine/universes.mli index bd315f277..3e397ed57 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -8,64 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names open Constr open Environ open Univ +open UnivSubst (** Unordered pairs of universe levels (ie (u,v) = (v,u)) *) module UPairSet : CSet.S with type elt = (Level.t * Level.t) (** Universes *) -(** {6 Constraints for type inference} - - When doing conversion of universes, not only do we have =/<= constraints but - also Lub constraints which correspond to unification of two levels which might - not be necessary if unfolding is performed. - - UWeak constraints come from irrelevant universes in cumulative polymorphism. -*) - -type universe_constraint = - | ULe of Universe.t * Universe.t - | UEq of Universe.t * Universe.t - | ULub of Level.t * Level.t - | UWeak of Level.t * Level.t - -module Constraints : sig - include Set.S with type elt = universe_constraint - - val is_trivial : universe_constraint -> bool - - val pr : t -> Pp.t -end - -type universe_constraints = Constraints.t -[@@ocaml.deprecated "Use Constraints.t"] - -type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option -type 'a universe_constrained = 'a * Constraints.t -type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t - -val subst_univs_universe_constraints : universe_subst_fn -> - Constraints.t -> Constraints.t - -val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function - -(** With [force_weak] UWeak constraints are turned into equalities, - otherwise they're forgotten. *) -val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t - -(** [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 - subterms of [m] and [n], arguments. *) -val eq_constr_univs_infer_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option - (** Simplification and pruning of constraints: [normalize_context_set ctx us] @@ -77,53 +30,14 @@ val eq_constr_univs_infer_with : (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -val level_subst_of : universe_subst_fn -> universe_level_subst_fn -val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t - -val subst_univs_constr : universe_subst -> constr -> constr - -type universe_opt_subst = Universe.t option universe_map - -val make_opt_subst : universe_opt_subst -> universe_subst_fn - -val subst_opt_univs_constr : universe_opt_subst -> constr -> constr - val normalize_context_set : UGraph.t -> ContextSet.t -> universe_opt_subst (* The defined and undefined variables *) -> LSet.t (* univ variables that can be substituted by algebraics *) -> UPairSet.t (* weak equality constraints *) -> (universe_opt_subst * LSet.t) in_universe_context_set -val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * LSet.t * LSet.t * universe_subst - -val normalize_univ_variable : - find:(Level.t -> Universe.t) -> - Level.t -> Universe.t - -val normalize_univ_variable_opt_subst : universe_opt_subst -> - (Level.t -> Universe.t) - -val normalize_univ_variable_subst : universe_subst -> - (Level.t -> Universe.t) - -val normalize_universe_opt_subst : universe_opt_subst -> - (Universe.t -> Universe.t) - -val normalize_universe_subst : universe_subst -> - (Universe.t -> Universe.t) - -(** Full universes substitutions into terms *) - -val nf_evars_and_universes_opt_subst : (existential -> constr option) -> - universe_opt_subst -> constr -> constr - val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t -(** Pretty-printing *) - -val pr_universe_opt_subst : universe_opt_subst -> Pp.t - (** *********************************** Deprecated *) [@@@ocaml.warning "-3"] @@ -246,3 +160,95 @@ val constr_of_reference : Globnames.global_reference -> constr val type_of_global : Globnames.global_reference -> types in_universe_context_set [@@ocaml.deprecated "Use [UnivGen.type_of_global]"] + +(** ****** Deprecated: moved to [UnivSubst] *) + +val level_subst_of : universe_subst_fn -> universe_level_subst_fn +[@@ocaml.deprecated "Use [UnivSubst.level_subst_of]"] + +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t +[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constraints]"] + +val subst_univs_constr : universe_subst -> constr -> constr +[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constr]"] + +type universe_opt_subst = UnivSubst.universe_opt_subst +[@@ocaml.deprecated "Use [UnivSubst.universe_opt_subst]"] + +val make_opt_subst : universe_opt_subst -> universe_subst_fn +[@@ocaml.deprecated "Use [UnivSubst.make_opt_subst]"] + +val subst_opt_univs_constr : universe_opt_subst -> constr -> constr +[@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"] + +val normalize_univ_variables : universe_opt_subst -> + universe_opt_subst * LSet.t * LSet.t * universe_subst +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"] + +val normalize_univ_variable : + find:(Level.t -> Universe.t) -> + Level.t -> Universe.t +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable]"] + +val normalize_univ_variable_opt_subst : universe_opt_subst -> + (Level.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_opt_subst]"] + +val normalize_univ_variable_subst : universe_subst -> + (Level.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_subst]"] + +val normalize_universe_opt_subst : universe_opt_subst -> + (Universe.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_opt_subst]"] + +val normalize_universe_subst : universe_subst -> + (Universe.t -> Universe.t) +[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_subst]"] + +val nf_evars_and_universes_opt_subst : (existential -> constr option) -> + universe_opt_subst -> constr -> constr +[@@ocaml.deprecated "Use [UnivSubst.nf_evars_and_universes_opt_subst]"] + +val pr_universe_opt_subst : universe_opt_subst -> Pp.t +[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"] + +(** ****** Deprecated: moved to [UnivProblem] *) + +type universe_constraint = UnivProblem.t = + | ULe of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.ULe]"] + | UEq of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.UEq]"] + | ULub of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.ULub]"] + | UWeak of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.UWeak]"] +[@@ocaml.deprecated "Use [UnivProblem.t]"] + +module Constraints = UnivProblem.Set +[@@ocaml.deprecated "Use [UnivProblem.Set]"] + +type 'a constraint_accumulator = 'a UnivProblem.accumulator +[@@ocaml.deprecated "Use [UnivProblem.accumulator]"] +type 'a universe_constrained = 'a UnivProblem.constrained +[@@ocaml.deprecated "Use [UnivProblem.constrained]"] +type 'a universe_constraint_function = 'a UnivProblem.constraint_function +[@@ocaml.deprecated "Use [UnivProblem.constraint_function]"] + +val subst_univs_universe_constraints : universe_subst_fn -> + Constraints.t -> Constraints.t +[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"] + +val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function +[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"] + +(** With [force_weak] UWeak constraints are turned into equalities, + otherwise they're forgotten. *) +val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t +[@@ocaml.deprecated "Use [UnivProblem.to_constraints]"] + +(** [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 + subterms of [m] and [n], arguments. *) +val eq_constr_univs_infer_with : + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> + UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option +[@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"] -- cgit v1.2.3