diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 8 | ||||
| -rw-r--r-- | engine/uState.ml | 107 | ||||
| -rw-r--r-- | engine/uState.mli | 17 |
4 files changed, 100 insertions, 37 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index eb0f2e3e74..9ea2cc00f5 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -758,7 +758,10 @@ let universe_context_set d = UState.context_set d.universes let to_universe_context evd = UState.context evd.universes -let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl +let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes +let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes + +let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } diff --git a/engine/evd.mli b/engine/evd.mli index 49b6a75833..f06fb8d3b9 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -562,8 +562,12 @@ val universes : evar_map -> UGraph.t [Univ.ContextSet.to_context]. *) val to_universe_context : evar_map -> Univ.UContext.t -val check_univ_decl : evar_map -> UState.universe_decl -> - Univ.UContext.t +val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry + +(** NB: [ind_univ_entry] cannot create cumulative entries. *) +val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes + +val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/uState.ml b/engine/uState.ml index ff91493ee5..dadc004c5f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -87,6 +87,17 @@ let constraints ctx = snd ctx.uctx_local let context ctx = Univ.ContextSet.to_context ctx.uctx_local +let const_univ_entry ~poly uctx = + let open Entries in + if poly then Polymorphic_const_entry (context uctx) + else Monomorphic_const_entry (context_set uctx) + +(* does not support cumulativity since you need more info *) +let ind_univ_entry ~poly uctx = + let open Entries in + if poly then Polymorphic_ind_entry (context uctx) + else Monomorphic_ind_entry (context_set uctx) + let of_context_set ctx = { empty with uctx_local = ctx } let subst ctx = ctx.uctx_univ_variables @@ -260,58 +271,92 @@ let pr_uctx_level uctx = type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl +let error_unbound_universes left uctx = + let open Univ in + let n = LSet.cardinal left in + let loc = + try + let info = + LMap.find (LSet.choose left) (snd uctx.uctx_names) in + info.uloc + with Not_found -> None + in + user_err ?loc ~hdr:"universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ + LSet.pr (pr_uctx_level uctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + let universe_context ~names ~extensible uctx = - let levels = Univ.ContextSet.levels uctx.uctx_local in + let open Univ in + let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right (fun (loc,id) (newinst, acc) -> let l = try UNameMap.find id (fst uctx.uctx_names) - with Not_found -> - user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Id.print id ++ str" is not bound anymore.") - in (l :: newinst, Univ.LSet.remove l acc)) + with Not_found -> assert false + in (l :: newinst, LSet.remove l acc)) names ([], levels) in - if not extensible && not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - let loc = - try - let info = - Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in - info.uloc - with Not_found -> None - in - user_err ?loc ~hdr:"universe_context" - ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level uctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) + if not extensible && not (LSet.is_empty left) + then error_unbound_universes left uctx else - let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in let inst = Array.append (Array.of_list newinst) left in - let inst = Univ.Instance.of_array inst in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints uctx.uctx_local) in + let inst = Instance.of_array inst in + let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in ctx -let check_implication uctx cstrs ctx = +let check_universe_context_set ~names ~extensible uctx = + if extensible then () + else + let open Univ in + let left = List.fold_left (fun left (loc,id) -> + let l = + try UNameMap.find id (fst uctx.uctx_names) + with Not_found -> assert false + in LSet.remove l left) + (ContextSet.levels uctx.uctx_local) names + in + if not (LSet.is_empty left) + then error_unbound_universes left uctx + +let check_implication uctx cstrs cstrs' = let gr = initial_graph uctx in let grext = UGraph.merge_constraints cstrs gr in - let cstrs' = Univ.UContext.constraints ctx in if UGraph.check_constraints cstrs' grext then () else CErrors.user_err ~hdr:"check_univ_decl" (str "Universe constraints are not implied by the ones declared.") -let check_univ_decl uctx decl = +let check_mono_univ_decl uctx decl = + let open Misctypes in + let () = + let names = decl.univdecl_instance in + let extensible = decl.univdecl_extensible_instance in + check_universe_context_set ~names ~extensible uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx + decl.univdecl_constraints + (Univ.ContextSet.constraints uctx.uctx_local); + uctx.uctx_local + +let check_univ_decl ~poly uctx decl = let open Misctypes in - let ctx = universe_context - ~names:decl.univdecl_instance - ~extensible:decl.univdecl_extensible_instance - uctx + let ctx = + let names = decl.univdecl_instance in + let extensible = decl.univdecl_extensible_instance in + if poly + then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx) + else + let () = check_universe_context_set ~names ~extensible uctx in + Entries.Monomorphic_const_entry uctx.uctx_local in if not decl.univdecl_extensible_constraints then - check_implication uctx decl.univdecl_constraints ctx; + check_implication uctx + decl.univdecl_constraints + (Univ.ContextSet.constraints uctx.uctx_local); ctx let restrict ctx vars = diff --git a/engine/uState.mli b/engine/uState.mli index 5279c63884..4265f2b203 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -59,6 +59,13 @@ val constraints : t -> Univ.constraints val context : t -> Univ.UContext.t (** Shorthand for {!context_set} with {!Context_set.to_context}. *) +val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry +(** Pick from {!context} or {!context_set} based on [poly]. *) + +val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes +(** Pick from {!context} or {!context_set} based on [poly]. + Cannot create cumulative entries. *) + (** {5 Constraints handling} *) val add_constraints : t -> Univ.constraints -> t @@ -133,11 +140,15 @@ type universe_decl = If non extensible in [decl], check that the local universes (resp. universe constraints) in [ctx] are implied by [decl]. - Return a universe context containing the local universes of [ctx] - and their constraints. The universes corresponding to + Return a [Entries.constant_universes_entry] containing the local + universes of [ctx] and their constraints. + + When polymorphic, the universes corresponding to [decl.univdecl_instance] come first in the order defined by that list. *) -val check_univ_decl : t -> universe_decl -> Univ.UContext.t +val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry + +val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t (** {5 TODO: Document me} *) |