aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarutil.ml22
-rw-r--r--pretyping/evarutil.mli10
-rw-r--r--pretyping/evd.ml29
-rw-r--r--pretyping/evd.mli3
-rw-r--r--pretyping/typeclasses.ml5
-rw-r--r--pretyping/typeclasses.mli3
6 files changed, 37 insertions, 35 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a4eae5fdff..128a7e55c4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -355,47 +355,41 @@ let new_pure_evar_full evd evi =
let evd = Evd.add evd evk evi in
(evd, evk)
-let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
+let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates ?store typ =
let newevk = new_untyped_evar() in
- let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in
+ let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in
(evd,newevk)
-let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
+let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance =
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
+ let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates ?store typ in
(evd,mkEvar (newevk,Array.of_list 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 evd env ?src ?filter ?candidates typ =
+let new_evar evd env ?src ?filter ?candidates ?store typ =
let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
let candidates = Option.map (List.map (subst2 subst vsubst)) candidates 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 instance
+ new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance
let new_type_evar ?src ?filter rigid evd env =
let evd', s = new_sort_variable rigid evd in
let evd', e = new_evar evd' env ?src ?filter (mkSort s) in
evd', (e, s)
- (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?candidates ty =
- let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
- evdref := evd';
- ev
-
let e_new_type_evar evdref ?src ?filter rigid env =
let evd', c = new_type_evar ?src ?filter rigid !evdref env in
evdref := evd';
c
(* The same using side-effect *)
-let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ty =
- let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
+let e_new_evar evdref env ?(src=default_source) ?filter ?candidates ?store ty =
+ let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ?store ty in
evdref := evd';
ev
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d197ad2efe..7715691b0c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -23,18 +23,18 @@ val mk_new_meta : unit -> constr
(** {6 Creating a fresh evar given their type and context} *)
val new_evar :
evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> types -> evar_map * constr
+ ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr
val new_pure_evar :
evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> types -> evar_map * evar
+ ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar
val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar
(** the same with side-effects *)
val e_new_evar :
evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
- ?candidates:constr list -> types -> constr
+ ?candidates:constr list -> ?store:Store.t -> types -> constr
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
@@ -57,7 +57,9 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr
of [inst] are typed in the occurrence context and their type (seen
as a telescope) is [sign] *)
val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types ->
+ ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list ->
+ ?store:Store.t -> constr list -> evar_map * constr
val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1bd995d5d1..5a9281c890 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -295,7 +295,6 @@ let is_empty_evar_universe_context ctx =
let union_evar_universe_context ctx ctx' =
if ctx == ctx' then ctx
- else if is_empty_evar_universe_context ctx then ctx'
else if is_empty_evar_universe_context ctx' then ctx
else
let local =
@@ -331,7 +330,7 @@ let diff_evar_universe_context ctx' ctx =
Univ.LSet.diff ctx'.uctx_univ_algebraic ctx.uctx_univ_algebraic;
uctx_univ_template =
Univ.LSet.diff ctx'.uctx_univ_template ctx.uctx_univ_template;
- uctx_universes = Univ.empty_universes;
+ uctx_universes = ctx.uctx_initial_universes;
uctx_initial_universes = ctx.uctx_initial_universes }
(* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *)
@@ -354,7 +353,7 @@ let instantiate_variable l b v =
exception UniversesDiffer
-let process_universe_constraints univs vars alg templ local cstrs =
+let process_universe_constraints univs vars alg templ cstrs =
let vars = ref vars in
let normalize = Universes.normalize_universe_opt_subst vars in
let rec unify_universes fo l d r local =
@@ -370,10 +369,11 @@ let process_universe_constraints univs vars alg templ local cstrs =
if Univ.check_leq univs l r then
(** Keep Prop/Set <= var around if var might be instantiated by prop or set
later. *)
- if Univ.is_small_univ l && not (Univ.is_small_univ r) then
- match Univ.Universe.level l, Univ.Universe.level r with
- | Some l, Some r -> Univ.Constraint.add (l,Univ.Le,r) local
- | _, _ -> local
+ if Univ.is_small_univ l then
+ match Univ.Universe.level r with
+ | Some r when Univ.LMap.mem r !vars ->
+ Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
+ | _ -> local
else local
else
match Univ.Universe.level r with
@@ -423,7 +423,7 @@ let process_universe_constraints univs vars alg templ local cstrs =
in
let local =
Univ.UniverseConstraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
- cstrs local
+ cstrs Univ.Constraint.empty
in
!vars, local
@@ -440,7 +440,7 @@ let add_constraints_context ctx cstrs =
let vars, local' =
process_universe_constraints ctx.uctx_universes
ctx.uctx_univ_variables ctx.uctx_univ_algebraic
- ctx.uctx_univ_template local cstrs'
+ ctx.uctx_univ_template cstrs'
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
@@ -454,7 +454,7 @@ let add_universe_constraints_context ctx cstrs =
let vars, local' =
process_universe_constraints ctx.uctx_universes
ctx.uctx_univ_variables ctx.uctx_univ_algebraic
- ctx.uctx_univ_template local cstrs
+ ctx.uctx_univ_template cstrs
in
{ ctx with uctx_local = (univs, Univ.Constraint.union local local');
uctx_univ_variables = vars;
@@ -769,7 +769,8 @@ let define evk body evd =
in
{ evd with defn_evars; undf_evars; last_mods; }
-let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter = Filter.identity) ?candidates evd =
+let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole))
+ ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd =
let () = match Filter.repr filter with
| None -> ()
| Some filter ->
@@ -782,7 +783,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?(filter
evar_filter = filter;
evar_source = src;
evar_candidates = candidates;
- evar_extra = Store.empty; }
+ evar_extra = store; }
in
{ evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; }
@@ -1128,9 +1129,9 @@ let set_leq_sort evd s1 s2 =
| Prop c, Prop c' ->
if c == Null && c' == Pos then evd
else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
- | _, _ ->
+ | _, _ ->
add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
-
+
let check_eq evd s s' =
Univ.check_eq evd.universes.uctx_universes s s'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fb348ae226..49a91f524e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -234,7 +234,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
val evar_declare :
named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
- ?filter:Filter.t -> ?candidates:constr list -> evar_map -> evar_map
+ ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t ->
+ evar_map -> evar_map
(** Convenience function. Just a wrapper around {!add}. *)
val evar_source : existential_key -> evar_map -> Evar_kinds.t located
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ada497ece7..8364387783 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -507,6 +507,9 @@ let is_implicit_arg = function
let resolvable = Store.field ()
+let set_resolvable s b =
+ Store.set s resolvable b
+
let is_resolvable evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
Option.default true (Store.get evi.evar_extra resolvable)
@@ -540,7 +543,7 @@ let mark_resolvability filter b sigma =
Evd.raw_map_undefined map sigma
let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
-let mark_resolvables sigma = mark_resolvability all_evars true sigma
+let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma
let has_typeclasses filter evd =
let check ev evi =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index a8ce9ca7c9..ebc6be45fb 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -92,11 +92,12 @@ val no_goals_or_obligations : evar_filter
(** Resolvability.
Only undefined evars can be marked or checked for resolvability. *)
+val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
val is_resolvable : evar_info -> bool
val mark_unresolvable : evar_info -> evar_info
val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
+val mark_resolvables : ?filter:evar_filter -> evar_map -> evar_map
val mark_resolvable : evar_info -> evar_info
-val mark_resolvables : evar_map -> evar_map
val is_class_evar : evar_map -> evar_info -> bool
val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-08 21:23:27 +0000