aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml7
-rw-r--r--engine/evarutil.ml25
-rw-r--r--engine/evarutil.mli11
-rw-r--r--engine/evd.ml19
-rw-r--r--engine/evd.mli11
-rw-r--r--engine/geninterp.ml2
-rw-r--r--engine/geninterp.mli2
-rw-r--r--engine/logic_monad.mli10
-rw-r--r--engine/namegen.ml40
-rw-r--r--engine/namegen.mli21
-rw-r--r--engine/proofview.ml10
-rw-r--r--engine/proofview.mli4
-rw-r--r--engine/proofview_monad.ml2
-rw-r--r--engine/proofview_monad.mli4
-rw-r--r--engine/termops.ml29
-rw-r--r--engine/termops.mli39
-rw-r--r--engine/uState.ml122
-rw-r--r--engine/uState.mli28
-rw-r--r--engine/universes.ml83
-rw-r--r--engine/universes.mli25
20 files changed, 252 insertions, 242 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7b879a8031..a54c082979 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -566,7 +566,6 @@ let compare_constr sigma cmp c1 c2 =
let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
-(** TODO: factorize with universes.ml *)
let test_constr_universes sigma leq m n =
let open Universes in
let kind c = kind_upto sigma c in
@@ -574,14 +573,20 @@ let test_constr_universes sigma leq m n =
else
let cstrs = ref Constraints.empty in
let eq_universes strict l l' =
+ let l = EInstance.kind sigma (EInstance.make l) in
+ let l' = EInstance.kind sigma (EInstance.make l') in
cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
let eq_sorts s1 s2 =
+ 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
(Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs;
true)
in
let leq_sorts s1 s2 =
+ 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
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 2afc12cd36..eabfb7b398 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -412,6 +412,14 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
evd, mkEvar (newevk,Array.of_list instance)
+let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+ let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
+ let instance =
+ match filter with
+ | None -> instance
+ | Some filter -> Filter.filter_list filter instance in
+ new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance
+
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
@@ -470,8 +478,6 @@ type clear_dependency_error =
exception ClearDependencyError of Id.t * clear_dependency_error
-let cleared = Store.field ()
-
exception Depends of Id.t
let rec check_and_clear_in_constr env evdref err ids global c =
@@ -544,13 +550,6 @@ let rec check_and_clear_in_constr env evdref err ids global c =
let evd = !evdref in
let (evd,_) = restrict_evar evd evk filter None in
evdref := evd;
- (* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
- let evi = Evd.find !evdref evk in
- let extra = evi.evar_extra in
- let extra' = Store.set extra cleared true in
- let evi' = { evi with evar_extra = extra' } in
- evdref := Evd.add !evdref evk evi' ;
- (* spiwack: /hacking session *)
Evd.existential_value !evdref ev
| _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c
@@ -657,11 +656,9 @@ let rec advance sigma evk =
match evi.evar_body with
| Evar_empty -> Some evk
| Evar_defined v ->
- if Option.default false (Store.get evi.evar_extra cleared) then
- let (evk,_) = Term.destEvar v in
- advance sigma evk
- else
- None
+ match is_restricted_evar evi with
+ | Some evk -> advance sigma evk
+ | None -> None
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index a8b6b5861c..ee0fae3d46 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -21,6 +21,13 @@ val new_meta : unit -> metavariable
val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
+
+val new_evar_from_context :
+ named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+ ?candidates:constr list -> ?store:Store.t ->
+ ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?principal:bool -> types -> evar_map * EConstr.t
+
val new_evar :
env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list -> ?store:Store.t ->
@@ -197,10 +204,6 @@ type clear_dependency_error =
exception ClearDependencyError of Id.t * clear_dependency_error
-(* spiwack: marks an evar that has been "defined" by clear.
- used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
-val cleared : bool Store.field
-
val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
Id.Set.t -> named_context_val * types
diff --git a/engine/evd.ml b/engine/evd.ml
index cfc9aa6351..324f883e8e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -630,7 +630,9 @@ let evar_source evk d = (find d evk).evar_source
let evar_ident evk evd = EvNames.ident evk evd.evar_names
let evar_key id evd = EvNames.key id evd.evar_names
-let define_aux def undef evk body =
+let restricted = Store.field ()
+
+let define_aux ?dorestrict def undef evk body =
let oldinfo =
try EvMap.find evk undef
with Not_found ->
@@ -640,7 +642,10 @@ let define_aux def undef evk body =
anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
in
let () = assert (oldinfo.evar_body == Evar_empty) in
- let newinfo = { oldinfo with evar_body = Evar_defined body } in
+ let evar_extra = match dorestrict with
+ | Some evk' -> Store.set oldinfo.evar_extra restricted evk'
+ | None -> oldinfo.evar_extra in
+ let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in
EvMap.add evk newinfo def, EvMap.remove evk undef
(* define the existential of section path sp as the constr body *)
@@ -653,6 +658,9 @@ let define evk body evd =
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
{ evd with defn_evars; undf_evars; last_mods; evar_names }
+let is_restricted_evar evi =
+ Store.get evi.evar_extra restricted
+
let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
@@ -667,7 +675,7 @@ let restrict evk filter ?candidates ?src evd =
let ctxt = Filter.filter_list filter (evar_context evar_info) in
let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
let body = mkEvar(evk',id_inst) in
- let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+ let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in
{ evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
defn_evars; last_mods; evar_names }, evk'
@@ -748,7 +756,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..96e4b6acce 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -31,7 +31,7 @@ open Environ
(** {6 Evars} *)
type evar = existential_key
-(** Existential variables. TODO: Should be made opaque one day. *)
+(** Existential variables. *)
val string_of_existential : evar -> string
@@ -244,6 +244,9 @@ val restrict : evar -> Filter.t -> ?candidates:constr list ->
(** Restrict an undefined evar into a new evar by filtering context and
possibly limiting the instances to a set of candidates *)
+val is_restricted_evar : evar_info -> evar option
+(** Tell if an evar comes from restriction of another evar, and if yes, which *)
+
val downcast : evar -> types -> evar_map -> evar_map
(** Change the type of an undefined evar to a new type assumed to be a
subtype of its current type; subtyping must be ensured by caller *)
@@ -493,7 +496,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 +550,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/geninterp.ml b/engine/geninterp.ml
index 9964433a80..e79e258fbc 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -32,7 +32,7 @@ struct
let repr = ValT.repr
let create = ValT.create
- let pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+ let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t)
let typ_list = ValT.create "list"
let typ_opt = ValT.create "option"
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
index 9a925dcd89..492e372adb 100644
--- a/engine/geninterp.mli
+++ b/engine/geninterp.mli
@@ -30,7 +30,7 @@ sig
val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
val repr : 'a typ -> string
- val pr : 'a typ -> Pp.std_ppcmds
+ val pr : 'a typ -> Pp.t
val typ_list : t list typ
val typ_opt : t option typ
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index aaebe4c1b0..8c8f9fe935 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -57,11 +57,11 @@ module NonLogical : sig
val print_char : char -> unit t
(** Loggers. The buffer is also flushed. *)
- val print_debug : Pp.std_ppcmds -> unit t
- val print_warning : Pp.std_ppcmds -> unit t
- val print_notice : Pp.std_ppcmds -> unit t
- val print_info : Pp.std_ppcmds -> unit t
- val print_error : Pp.std_ppcmds -> unit t
+ val print_debug : Pp.t -> unit t
+ val print_warning : Pp.t -> unit t
+ val print_notice : Pp.t -> unit t
+ val print_info : Pp.t -> unit t
+ val print_error : Pp.t -> unit t
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
diff --git a/engine/namegen.ml b/engine/namegen.ml
index a75fe721f7..2e62b89011 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -43,6 +43,8 @@ let default_non_dependent_ident = Id.of_string default_non_dependent_string
let default_dependent_ident = Id.of_string "x"
+let default_generated_non_letter_string = "x"
+
(**********************************************************************)
(* Globality of identifiers *)
@@ -107,7 +109,17 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
hdrec c
let lowercase_first_char id = (* First character of a constr *)
- Unicode.lowercase_first_char (Id.to_string id)
+ let s = Id.to_string id in
+ match Unicode.split_at_first_letter s with
+ | None ->
+ (* General case: nat -> n *)
+ Unicode.lowercase_first_char s
+ | Some (s,s') ->
+ if String.length s' = 0 then
+ (* No letter, e.g. __, or __'_, etc. *)
+ default_generated_non_letter_string
+ else
+ s ^ Unicode.lowercase_first_char s'
let sort_hdchar = function
| Prop(_) -> "P"
@@ -239,7 +251,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 +265,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 +283,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 +314,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 +322,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 +333,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 +383,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 +391,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/proofview.ml b/engine/proofview.ml
index b4e2160f4e..598358c472 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -153,8 +153,12 @@ let focus i j sp =
( { sp with comb = new_comb } , context )
(** [undefined defs l] is the list of goals in [l] which are still
- unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (Evarutil.advance defs) l
+ unsolved (after advancing cleared goals). Note that order matters. *)
+let undefined defs l =
+ List.fold_right (fun evk l ->
+ match Evarutil.advance defs evk with
+ | Some evk -> List.add_set Evar.equal evk l
+ | None -> l) l []
(** Unfocuses a proofview with respect to a context. *)
let unfocus c sp =
@@ -332,7 +336,7 @@ exception NoSuchGoals of int
(* This hook returns a string to be appended to the usual message.
Primarily used to add a suggestion about the right bullet to use to
focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ())
+let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ())
let set_nosuchgoals_hook f = nosuchgoals_hook := f
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 957c9213c4..d92d0a7d53 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -235,7 +235,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
This hook is used to add a suggestion about bullets when
applicable. *)
exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
+val set_nosuchgoals_hook: (int -> Pp.t) -> unit
val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
@@ -526,7 +526,7 @@ module Trace : sig
val log : Proofview_monad.lazy_msg -> unit tactic
val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic
- val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds
+ val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.t
end
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 1b737b6f4d..d0f4712258 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -62,7 +62,7 @@ end
(** We typically label nodes of [Trace.tree] with messages to
print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
+type lazy_msg = unit -> Pp.t
let pr_lazy_msg msg = msg ()
(** Info trace. *)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 554583421b..e7123218b1 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -43,7 +43,7 @@ end
(** We typically label nodes of [Trace.tree] with messages to
print. But we don't want to compute the result. *)
-type lazy_msg = unit -> Pp.std_ppcmds
+type lazy_msg = unit -> Pp.t
(** Info trace. *)
module Info : sig
@@ -58,7 +58,7 @@ module Info : sig
type state = tag Trace.incr
type tree = tag Trace.forest
- val print : tree -> Pp.std_ppcmds
+ val print : tree -> Pp.t
(** [collapse n t] flattens the first [n] levels of [Tactic] in an
info trace, effectively forgetting about the [n] top level of
diff --git a/engine/termops.ml b/engine/termops.ml
index 1aba2bbdd1..b7fa2dc4a4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -994,12 +994,14 @@ let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
(* flattens application lists throwing casts in-between *)
let collapse_appl sigma c = match EConstr.kind sigma c with
| App (f,cl) ->
+ if EConstr.isCast sigma f then
let rec collapse_rec f cl2 =
match EConstr.kind sigma (strip_outer_cast sigma f) with
| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
| _ -> EConstr.mkApp (f,cl2)
in
collapse_rec f cl
+ else c
| _ -> c
(* First utilities for avoiding telescope computation for subst_term *)
@@ -1069,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
@@ -1145,9 +1147,6 @@ let is_template_polymorphic env sigma f =
| Ind (ind, u) ->
if not (EConstr.EInstance.is_empty u) then false
else Environ.template_polymorphic_ind ind env
- | Const (cst, u) ->
- if not (EConstr.EInstance.is_empty u) then false
- else Environ.template_polymorphic_constant cst env
| _ -> false
let base_sort_cmp pb s0 s1 =
@@ -1166,6 +1165,24 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
| Cast (c,_,_) -> is_Prop sigma c
| _ -> false
+let rec is_Set sigma c = match EConstr.kind sigma c with
+ | Sort u ->
+ begin match EConstr.ESorts.kind sigma u with
+ | Prop Pos -> true
+ | _ -> false
+ end
+ | Cast (c,_,_) -> is_Set sigma c
+ | _ -> false
+
+let rec is_Type sigma c = match EConstr.kind sigma c with
+ | Sort u ->
+ begin match EConstr.ESorts.kind sigma u with
+ | Type _ -> true
+ | _ -> false
+ end
+ | Cast (c,_,_) -> is_Type sigma c
+ | _ -> false
+
(* eq_constr extended with universe erasure *)
let compare_constr_univ sigma f cv_pb t1 t2 =
let open EConstr in
diff --git a/engine/termops.mli b/engine/termops.mli
index c19a2d15a5..ef2c52a455 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -9,16 +9,15 @@
(** This file defines various utilities for term manipulation that are not
needed in the kernel. *)
-open Pp
open Names
open Term
open Environ
open EConstr
(** printers *)
-val print_sort : sorts -> std_ppcmds
-val pr_sort_family : sorts_family -> std_ppcmds
-val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds
+val print_sort : sorts -> Pp.t
+val pr_sort_family : sorts_family -> Pp.t
+val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t
(** about contexts *)
val push_rel_assum : Name.t * types -> env -> env
@@ -268,6 +267,8 @@ val isGlobalRef : Evd.evar_map -> constr -> bool
val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool
val is_Prop : Evd.evar_map -> constr -> bool
+val is_Set : Evd.evar_map -> constr -> bool
+val is_Type : Evd.evar_map -> constr -> bool
(** Combinators on judgments *)
@@ -279,25 +280,25 @@ val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns
open Evd
-val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+val pr_existential_key : evar_map -> evar -> Pp.t
val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
-val pr_evar_info : evar_info -> Pp.std_ppcmds
-val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds
-val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds
+val pr_evar_info : evar_info -> Pp.t
+val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t
+val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t
val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
- evar_map -> Pp.std_ppcmds
-val pr_metaset : Metaset.t -> Pp.std_ppcmds
-val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
-val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
+ evar_map -> Pp.t
+val pr_metaset : Metaset.t -> Pp.t
+val pr_evar_universe_context : evar_universe_context -> Pp.t
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
(** debug printer: do not use to display terms to the casual user... *)
-val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit
-val print_constr : constr -> std_ppcmds
-val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds
-val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
-val print_rel_context : env -> std_ppcmds
-val print_env : env -> std_ppcmds
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+val print_constr : constr -> Pp.t
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+val print_named_context : env -> Pp.t
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t
+val print_rel_context : env -> Pp.t
+val print_env : env -> Pp.t
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 3776e4c9fd..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,12 +118,29 @@ 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
(** {5 Pretty-printing} *)
-val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds
+val pr_uctx_level : t -> Univ.Level.t -> Pp.t
diff --git a/engine/universes.ml b/engine/universes.ml
index 08461a2186..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
@@ -131,47 +131,6 @@ let to_constraints g s =
"to_constraints: non-trivial algebraic constraint between universes")
in Constraints.fold tr s Constraint.empty
-let test_constr_univs_infer leq univs fold m n accu =
- if m == n then Some accu
- else
- 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
- 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
- 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
- in
- let res =
- if leq then
- let rec compare_leq m n =
- Constr.compare_head_gen_leq eq_universes leq_sorts
- eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- compare_leq m n
- else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- if res then Some !cstrs else None
-
-let eq_constr_univs_infer univs fold m n accu =
- test_constr_univs_infer false univs fold m n accu
-
-let leq_constr_univs_infer univs fold m n accu =
- test_constr_univs_infer true univs fold m n accu
-
(** 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 =
@@ -197,42 +156,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
if res then Some !cstrs else None
-let test_constr_universes leq m n =
- if m == n then Some Constraints.empty
- else
- let cstrs = ref Constraints.empty in
- let eq_universes strict l l' =
- cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
- let eq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else (cstrs := Constraints.add
- (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs;
- true)
- in
- let leq_sorts s1 s2 =
- if Sorts.equal s1 s2 then true
- else
- (cstrs := Constraints.add
- (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs;
- 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 =
- if leq then
- let rec compare_leq m n =
- Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
- and leq_constr' m n = m == n || compare_leq m n in
- compare_leq m n
- else
- Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
- in
- if res then Some !cstrs else None
-
-let eq_constr_universes m n = test_constr_universes false m n
-let leq_constr_universes m n = test_constr_universes true m n
-
let compare_head_gen_proj env equ eqs eqc' m n =
match kind_of_term m, kind_of_term n with
| Proj (p, c), App (f, args)
@@ -419,7 +342,7 @@ let type_of_reference env r =
| VarRef id -> Environ.named_type id env, ContextSet.empty
| ConstRef c ->
let cb = Environ.lookup_constant c env in
- let ty = Typeops.type_of_constant_type env cb.const_type in
+ let ty = cb.const_type in
begin
match cb.const_universes with
| Monomorphic_const _ -> ty, ContextSet.empty
diff --git a/engine/universes.mli b/engine/universes.mli
index 0f6e419d00..8b2217d446 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -17,7 +17,7 @@ val is_set_minimization : unit -> bool
(** Universes *)
-val pr_with_global_universes : Level.t -> Pp.std_ppcmds
+val pr_with_global_universes : Level.t -> Pp.t
(** Local universe name <-> level mapping *)
@@ -52,7 +52,7 @@ type universe_constraint = universe * universe_constraint_type * universe
module Constraints : sig
include Set.S with type elt = universe_constraint
- val pr : t -> Pp.std_ppcmds
+ val pr : t -> Pp.t
end
type universe_constraints = Constraints.t
@@ -67,11 +67,6 @@ val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_f
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 : 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
subterms of [m] and [n], arguments. *)
@@ -80,20 +75,6 @@ val eq_constr_univs_infer_with :
(constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
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 : 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]. *)
-val eq_constr_universes : constr -> constr -> universe_constraints option
-
-(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
- alpha, casts, application grouping and the universe constraints in [c]. *)
-val leq_constr_universes : constr -> constr -> universe_constraints option
-
(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
application grouping and the universe constraints in [c]. *)
val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
@@ -203,7 +184,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s
(** Pretty-printing *)
-val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
+val pr_universe_opt_subst : universe_opt_subst -> Pp.t
(** {6 Support for template polymorphism } *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 02:30:22 +0000