diff options
-rw-r--r-- | engine/universes.ml | 20 | ||||
-rw-r--r-- | engine/universes.mli | 11 | ||||
-rw-r--r-- | kernel/univ.ml | 83 | ||||
-rw-r--r-- | kernel/univ.mli | 48 |
4 files changed, 162 insertions, 0 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index f20108186..955e1d8b5 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -1118,3 +1118,23 @@ let solve_constraints_system levels level_bounds level_min = done; done; v + + +(** Operations for universe_info_ind *) + +(** Given a universe context representing constraints of an inductive + this function produces a UInfoInd.t that with the trivial subtyping relation. *) +let univ_inf_ind_from_universe_context univcst = + let freshunivs = Instance.of_array + (Array.map (fun _ -> new_univ_level ()) + (Instance.to_array (UContext.instance univcst))) + in UInfoInd.from_universe_context univcst freshunivs + +(** This function adds universe constraints to the universe + constraints of the given universe_info_ind. However one must be + CAUTIOUS as it resets the subtyping constraints to equality. *) +let univ_inf_ind_union uinfind univcst' = + let freshunivs = Instance.of_array + (Array.map (fun _ -> new_univ_level ()) + (Instance.to_array (UContext.instance univcst'))) + in UInfoInd.union uinfind univcst' freshunivs diff --git a/engine/universes.mli b/engine/universes.mli index 83ca1ea60..17a9deb3a 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -227,3 +227,14 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds val solve_constraints_system : universe option array -> universe array -> universe array -> universe array + +(** Operations for universe_info_ind *) + +(** Given a universe context representing constraints of an inductive + this function produces a UInfoInd.t that with the trivial subtyping relation. *) +val univ_inf_ind_from_universe_context : universe_context -> universe_info_ind + +(** This function adds universe constraints to the universe + constraints of the given universe_info_ind. However one must be + CAUTIOUS as it resets the subtyping constraints to equality. *) +val univ_inf_ind_union : universe_info_ind -> universe_context -> universe_info_ind diff --git a/kernel/univ.ml b/kernel/univ.ml index d53dd8e73..e8b9ae33a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1028,6 +1028,83 @@ end type universe_context = UContext.t let hcons_universe_context = UContext.hcons +(** Universe info for inductive types: A context of universe levels + with universe constraints, representing local universe variables + and constraints, together with a context of universe levels with + universe constraints, representing conditions for subtyping used + for inductive types. + + This data structure maintains the invariant that the context for + subtyping constraints is exactly twice as big as the context for + universe constraints. *) +module UInfoInd = +struct + type t = universe_context * universe_context + + let make x = + if (Instance.length (UContext.instance (snd x))) = + (Instance.length (UContext.instance (fst x))) * 2 then x + else anomaly (Pp.str "Invalid subtyping information encountered!") + + let empty = (UContext.empty, UContext.empty) + let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst + + let halve_context (ctx : Instance.t) : Instance.t * Instance.t = + let len = Array.length (Instance.to_array ctx) in + let halflen = len / 2 in + (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen), + Instance.of_array (Array.sub (Instance.to_array ctx) halflen len)) + + let pr prl (univcst, subtypcst) = + if UContext.is_empty univcst then mt() else + let (ctx, ctx') = halve_context (UContext.instance subtypcst) in + (UContext.pr prl univcst) ++ + h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "}") + ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst))) + + let hcons (univcst, subtypcst) = + (UContext.hcons univcst, UContext.hcons subtypcst) + + let univ_context (univcst, subtypcst) = univcst + let subtyp_context (univcst, subtypcst) = subtypcst + + let create_trivial_subtyping ctx ctx' = + CArray.fold_left_i + (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst) + Constraint.empty (Instance.to_array ctx) + + (** This function takes a universe context representing constraints + of an inductive and a Instance.t of fresh universe names for the + subtyping (with the same length as the context in the given + universe context) and produces a UInfoInd.t that with the + trivial subtyping relation. *) + let from_universe_context univcst freshunivs = + let inst = (UContext.instance univcst) in + assert (Instance.length freshunivs = Instance.length inst); + (univcst, UContext.make (Instance.append inst freshunivs, + create_trivial_subtyping inst freshunivs)) + + (** This function adds universe constraints to the universe + constraints of the given universe_info_ind. However one must be + CAUTIOUS as it resets the subtyping constraints to equality. It + also requires fresh universes for the newly introduced + universes *) + let union (univcst, _) univcst' freshunivs = + assert (Instance.length freshunivs = Instance.length (UContext.instance univcst')); + let (ctx, ctx') = halve_context (UContext.instance univcst) in + let newctx' = Instance.append ctx' freshunivs in + let univcstunion = UContext.union univcst univcst' in + (univcstunion, subtyp_context (from_universe_context univcstunion newctx')) + + let dest x = x + + let size ((x,_), _) = Instance.length x + +end + +type universe_info_ind = UInfoInd.t +let hcons_universe_info_ind = UInfoInd.hcons + (** A set of universes with universe constraints. We linearize the set to a list after typechecking. Beware, representation could change. @@ -1203,6 +1280,10 @@ let subst_instance_constraints s csts = let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) +(** Substitute instance inst for ctx in universe constraints and subtyping constraints *) +let instantiate_univ_info_ind (univcst, subtpcst) = + (instantiate_univ_context univcst, instantiate_univ_context subtpcst) + let instantiate_univ_constraints u (_, csts) = subst_instance_constraints u csts @@ -1235,6 +1316,8 @@ let pr_constraints prl = Constraint.pr prl let pr_universe_context = UContext.pr +let pr_universe_info_ind = UInfoInd.pr + let pr_universe_context_set = ContextSet.pr let pr_universe_subst = diff --git a/kernel/univ.mli b/kernel/univ.mli index 1ccdebd50..630d0d949 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -315,6 +315,49 @@ end type universe_context = UContext.t +(** Universe info for inductive types: A context of universe levels + with universe constraints, representing local universe variables + and constraints, together with a context of universe levels with + universe constraints, representing conditions for subtyping used + for inductive types. + + This data structure maintains the invariant that the context for + subtyping constraints is exactly twice as big as the context for + universe constraints. *) +module UInfoInd : +sig + type t + + val make : universe_context * universe_context -> t + + val empty : t + val is_empty : t -> bool + + val univ_context : t -> universe_context + val subtyp_context : t -> universe_context + + val dest : t -> universe_context * universe_context + + (** This function takes a universe context representing constraints + of an inductive and a Instance.t of fresh universe names for the + subtyping (with the same length as the context in the given + universe context) and produces a UInfoInd.t that with the + trivial subtyping relation. *) + val from_universe_context : universe_context -> universe_instance -> t + + (** This function adds universe constraints to the universe + constraints of the given universe_info_ind. However one must be + CAUTIOUS as it resets the subtyping constraints to equality. It + also requires fresh universes for the newly introduced + universes *) + val union : t -> universe_context -> universe_instance -> t + + val size : t -> int + +end + +type universe_info_ind = UInfoInd.t + (** Universe contexts (as sets) *) module ContextSet : @@ -389,6 +432,9 @@ val abstract_universes : bool -> universe_context -> universe_level_subst * univ (** Get the instantiated graph. *) val instantiate_univ_context : universe_context -> universe_context +(** Get the instantiated graphs for both universe constraints and subtyping constraints. *) +val instantiate_univ_info_ind : universe_info_ind -> universe_info_ind + val instantiate_univ_constraints : universe_instance -> universe_context -> constraints (** {6 Pretty-printing of universes. } *) @@ -396,6 +442,7 @@ val instantiate_univ_constraints : universe_instance -> universe_context -> cons val pr_constraint_type : constraint_type -> Pp.std_ppcmds val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds +val pr_universe_info_ind : (Level.t -> Pp.std_ppcmds) -> universe_info_ind -> Pp.std_ppcmds val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> univ_inconsistency -> Pp.std_ppcmds @@ -410,6 +457,7 @@ val hcons_constraints : constraints -> constraints val hcons_universe_set : universe_set -> universe_set val hcons_universe_context : universe_context -> universe_context val hcons_universe_context_set : universe_context_set -> universe_context_set +val hcons_universe_info_ind : universe_info_ind -> universe_info_ind (******) |