diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 5 | ||||
| -rw-r--r-- | engine/evd.mli | 6 | ||||
| -rw-r--r-- | engine/namegen.ml | 26 | ||||
| -rw-r--r-- | engine/namegen.mli | 21 | ||||
| -rw-r--r-- | engine/termops.ml | 6 | ||||
| -rw-r--r-- | engine/uState.ml | 122 | ||||
| -rw-r--r-- | engine/uState.mli | 26 | ||||
| -rw-r--r-- | engine/universes.ml | 4 |
8 files changed, 136 insertions, 80 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index cfc9aa6351..f1b5419dec 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -748,7 +748,10 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ?names evd = UState.universe_context ?names evd.universes +let universe_context ~names ~extensible evd = + UState.universe_context ~names ~extensible evd.universes + +let check_univ_decl evd decl = UState.check_univ_decl 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 3f00a3b0b2..abcabe8157 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,7 +493,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : @@ -547,11 +547,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> +val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +val check_univ_decl : evar_map -> UState.universe_decl -> + Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map diff --git a/engine/namegen.ml b/engine/namegen.ml index a75fe721f7..1dd29e6eae 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -239,7 +239,7 @@ let visible_ids sigma (nenv, c) = let next_name_away_in_cases_pattern sigma env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in let visible = visible_ids sigma env_t in - let bad id = Id.List.mem id avoid || is_constructor id + let bad id = Id.Set.mem id avoid || is_constructor id || Id.Set.mem id visible in next_ident_away_from id bad @@ -253,8 +253,8 @@ let next_name_away_in_cases_pattern sigma env_t na avoid = name is taken by finding a free subscript starting from 0 *) let next_ident_away_in_goal id avoid = - let id = if Id.List.mem id avoid then restart_subscript id else id in - let bad id = Id.List.mem id avoid || (is_global id && not (is_section_variable id)) in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable id)) in next_ident_away_from id bad let next_name_away_in_goal na avoid = @@ -271,16 +271,16 @@ let next_name_away_in_goal na avoid = beyond the current subscript *) let next_global_ident_away id avoid = - let id = if Id.List.mem id avoid then restart_subscript id else id in - let bad id = Id.List.mem id avoid || is_global id in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || is_global id in next_ident_away_from id bad (* 4- Looks for next fresh name outside a list; if name already used, looks for same name with lower available subscript *) let next_ident_away id avoid = - if Id.List.mem id avoid then - next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid) + if Id.Set.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -302,7 +302,7 @@ let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env sigma = (** FIXME: this is inefficient, but only used in printing *) - let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in + let avoid = ref (ids_of_named_context_val (named_context_val env)) in let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in @@ -310,7 +310,7 @@ let make_all_name_different env sigma = (fun decl newenv -> let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in - avoid := id::!avoid; + avoid := Id.Set.add id !avoid; push_rel (RelDecl.set_name (Name id) decl) newenv) rels ~init:env0 @@ -321,7 +321,7 @@ let make_all_name_different env sigma = let next_ident_away_for_default_printing sigma env_t id avoid = let visible = visible_ids sigma env_t in - let bad id = Id.List.mem id avoid || Id.Set.mem id visible in + let bad id = Id.Set.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad let next_name_away_for_default_printing sigma env_t na avoid = @@ -371,7 +371,7 @@ let compute_displayed_name_in sigma flags avoid na c = | _ -> let fresh_id = next_name_for_display sigma flags na avoid in let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::avoid) + (idopt, Id.Set.add fresh_id avoid) let compute_and_force_displayed_name_in sigma flags avoid na c = match na with @@ -379,11 +379,11 @@ let compute_and_force_displayed_name_in sigma flags avoid na c = (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - (Name fresh_id, fresh_id::avoid) + (Name fresh_id, Id.Set.add fresh_id avoid) let compute_displayed_let_name_in sigma flags avoid na c = let fresh_id = next_name_for_display sigma flags na avoid in - (Name fresh_id, fresh_id::avoid) + (Name fresh_id, Id.Set.add fresh_id avoid) let rename_bound_vars_as_displayed sigma avoid env c = let rec rename avoid env c = diff --git a/engine/namegen.mli b/engine/namegen.mli index 14846a9184..6fde90a39c 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -72,23 +72,22 @@ val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) -val next_ident_away : Id.t -> Id.t list -> Id.t +val next_ident_away : Id.t -> Id.Set.t -> Id.t (** Avoid clashing with a name already used in current module *) -val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t +val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t (** Avoid clashing with a name already used in current module but tolerate overwriting section variables, as in goals *) -val next_global_ident_away : Id.t -> Id.t list -> Id.t +val next_global_ident_away : Id.t -> Id.Set.t -> Id.t (** Default is [default_non_dependent_ident] *) -val next_name_away : Name.t -> Id.t list -> Id.t +val next_name_away : Name.t -> Id.Set.t -> Id.t -val next_name_away_with_default : string -> Name.t -> Id.t list -> - Id.t +val next_name_away_with_default : string -> Name.t -> Id.Set.t -> Id.t val next_name_away_with_default_using_types : string -> Name.t -> - Id.t list -> types -> Id.t + Id.Set.t -> types -> Id.t val set_reserved_typed_name : (types -> Name.t) -> unit @@ -103,13 +102,13 @@ type renaming_flags = val make_all_name_different : env -> evar_map -> env val compute_displayed_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_and_force_displayed_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_displayed_let_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val rename_bound_vars_as_displayed : - evar_map -> Id.t list -> Name.t list -> types -> types + evar_map -> Id.Set.t -> Name.t list -> types -> types (**********************************************************************) (* Naming strategy for arguments in Prop when eliminating inductive types *) diff --git a/engine/termops.ml b/engine/termops.ml index e2bdf72387..b7fa2dc4a4 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1071,9 +1071,9 @@ let replace_term_gen sigma eq_fun c by_c in_t = let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t let vars_of_env env = - let s = - Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s) - (named_context env) ~init:Id.Set.empty in + let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in + if List.is_empty (Environ.rel_context env) then s + else Context.Rel.fold_outside (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s diff --git a/engine/uState.ml b/engine/uState.ml index 63bd247d56..13a9bb3732 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -97,17 +97,9 @@ let subst ctx = ctx.uctx_univ_variables let ugraph ctx = ctx.uctx_universes -let algebraics ctx = ctx.uctx_univ_algebraic +let initial_graph ctx = ctx.uctx_initial_universes -let constrain_variables diff ctx = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - diff Univ.Constraint.empty +let algebraics ctx = ctx.uctx_univ_algebraic let add_uctx_names ?loc s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) @@ -240,6 +232,24 @@ let add_universe_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let constrain_variables diff ctx = + let univs, local = ctx.uctx_local in + let univs, vars, local = + Univ.LSet.fold + (fun l (univs, vars, cstrs) -> + try + match Univ.LMap.find l vars with + | Some u -> + (Univ.LSet.add l univs, + Univ.LMap.remove l vars, + Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + | None -> (univs, vars, cstrs) + with Not_found | Option.IsNone -> (univs, vars, cstrs)) + diff (univs, ctx.uctx_univ_variables, local) + in + { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + + let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> @@ -247,41 +257,63 @@ let pr_uctx_level uctx = with Not_found | Option.IsNone -> Universes.pr_with_global_universes l -let universe_context ?names ctx = - match names with - | None -> [], Univ.ContextSet.to_context ctx.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels ctx.uctx_local in - let newinst, map, left = - List.fold_right - (fun (loc,id) (newinst, map, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) - with Not_found -> - user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") - in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) - pl ([], [], levels) - in - if 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 ctx.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 ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) - else - let inst = Univ.Instance.of_array (Array.of_list newinst) in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints ctx.uctx_local) - in map, ctx +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let universe_context ~names ~extensible ctx = + let levels = Univ.ContextSet.levels ctx.uctx_local in + let newinst, left = + List.fold_right + (fun (loc,id) (newinst, acc) -> + let l = + try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + with Not_found -> + user_err ?loc ~hdr:"universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + in (l :: newinst, Univ.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 ctx.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 ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + else + let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let inst = Array.append (Array.of_list newinst) left in + let inst = Univ.Instance.of_array inst in + let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints ctx.uctx_local) in + map, ctx + +let check_implication uctx cstrs ctx = + 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 open Misctypes in + let pl, ctx = universe_context + ~names:decl.univdecl_instance + ~extensible:decl.univdecl_extensible_instance + uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx decl.univdecl_constraints ctx; + pl, ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in diff --git a/engine/uState.mli b/engine/uState.mli index d198fbfbe9..c44f2c1d74 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst val ugraph : t -> UGraph.t (** The current graph extended with the local constraints *) +val initial_graph : t -> UGraph.t +(** The initial graph with just the declarations of new universes. *) + val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) @@ -105,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t -val constrain_variables : Univ.LSet.t -> t -> Univ.constraints +val constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t @@ -115,9 +118,26 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** {5 TODO: Document me} *) +(** [universe_context names extensible ctx] + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to [names] come + first in the order defined by that list. + + If [extensible] is false, check that the universes of [names] are + the only local universes. -val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context + Also return the association list of universe names and universes + (including those not in [names]). *) +val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> + (Id.t * Univ.Level.t) list * Univ.universe_context + +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context + +(** {5 TODO: Document me} *) val update_sigma_env : t -> Environ.env -> t diff --git a/engine/universes.ml b/engine/universes.ml index 686411e7d5..7f5bf24b74 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -14,7 +14,7 @@ open Environ open Univ open Globnames -let pr_with_global_universes l = +let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l @@ -31,7 +31,7 @@ let universe_binders_of_global ref = let register_universe_binders ref l = universe_binders_table := Refmap.add ref l !universe_binders_table - + (* To disallow minimization to Set *) let set_minimization = ref true |