aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml22
-rw-r--r--engine/evarutil.mli6
-rw-r--r--engine/evd.ml96
-rw-r--r--engine/evd.mli23
-rw-r--r--engine/proofview.ml46
-rw-r--r--engine/proofview.mli6
-rw-r--r--engine/termops.ml10
7 files changed, 131 insertions, 78 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69830960a9..4e1636e321 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let new_pure_evar_full evd evi =
- let (evd, evk) = Evd.new_evar evd evi in
+let new_pure_evar_full evd ?typeclass_candidate evi =
+ let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
let evd = Evd.declare_future_goal evk evd in
(evd, evk)
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate
+ ?(principal=false) sign evd typ =
let default_naming = IntroAnonymous in
let naming = Option.default default_naming naming in
let name = match naming with
@@ -429,21 +430,22 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
evar_source = src;
evar_candidates = candidates }
in
- let (evd, newevk) = Evd.new_evar evd ?name evi in
+ let typeclass_candidate = if principal then Some false else typeclass_candidate in
+ let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
let evd =
if principal then Evd.declare_principal_goal newevk evd
else Evd.declare_future_goal newevk evd
in
(evd, newevk)
-let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance =
let open EConstr in
assert (not !Flags.debug ||
List.distinct (ids_of_named_context (named_context_of_val sign)));
- let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?principal typ in
+ let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in
evd, mkEvar (newevk,Array.of_list instance)
-let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
let instance =
match filter with
@@ -453,7 +455,7 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd t
(* [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 ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ =
let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
let map c = csubst_subst subst c in
let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -461,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance
+ new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance
let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
let (evd', s) = new_sort_variable rigid evd in
- let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
+ let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in
evd', (e, s)
let new_Type ?(rigid=Evd.univ_flexible) evd =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 49443164cc..0c8d8c9b8a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -29,6 +29,7 @@ val new_evar_from_context :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * EConstr.t
@@ -42,6 +43,7 @@ val new_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> types -> evar_map * EConstr.t
@@ -49,10 +51,11 @@ val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types -> evar_map * Evar.t
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
+val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
@@ -78,6 +81,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
val new_evar_instance :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
+ ?typeclass_candidate:bool ->
?principal:bool ->
named_context_val -> evar_map -> types ->
constr list -> evar_map * constr
diff --git a/engine/evd.ml b/engine/evd.ml
index 3a01706063..3a77a2b440 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -413,7 +413,7 @@ type goal_kind = ToShelve | ToGiveUp
type evar_flags =
{ obligation_evars : Evar.Set.t;
restricted_evars : Evar.t Evar.Map.t;
- unresolvable_evars : Evar.Set.t }
+ typeclass_evars : Evar.Set.t }
type evar_map = {
(** Existential variables *)
@@ -444,44 +444,44 @@ type evar_map = {
extras : Store.t;
}
+let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) ()
+
+let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c
+
(*** Lifting primitive from Evar.Map. ***)
let rename evk id evd =
{ evd with evar_names = EvNames.rename evk id evd.evar_names }
-let add_with_name ?name d e i = match i.evar_body with
+let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with
| Evar_empty ->
let evar_names = EvNames.add_name_undefined name e i d.evar_names in
- { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
+ let evar_flags =
+ if typeclass_candidate && is_maybe_typeclass d i.evar_concl then
+ let flags = d.evar_flags in
+ { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
+ else d.evar_flags
+ in
+ { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags }
| Evar_defined _ ->
let evar_names = EvNames.remove_name_defined e d.evar_names in
{ d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
-let add d e i = add_with_name d e i
+(** Evd.add is a low-level function mainly used to update the evar_info
+ associated to an evar, so we prevent registering its typeclass status. *)
+let add d e i = add_with_name ~typeclass_candidate:false d e i
-(*** Evar flags: resolvable, restricted or obligation flag *)
+(*** Evar flags: typeclasses, restricted or obligation flag *)
-let set_resolvable_evar evd evk b =
- let flags = evd.evar_flags in
- let unresolvable_evars = flags.unresolvable_evars in
- let unresolvable_evars =
- if b then Evar.Set.remove evk unresolvable_evars
- else Evar.Set.add evk unresolvable_evars
- in
- { evd with evar_flags = { flags with unresolvable_evars } }
+let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
-let is_resolvable_evar evd evk =
+let set_typeclass_evars evd tcs =
let flags = evd.evar_flags in
- not (Evar.Set.mem evk flags.unresolvable_evars)
+ { evd with evar_flags = { flags with typeclass_evars = tcs } }
-let inherit_unresolvable_evar evar_flags evk evk' =
- let evk_unres = Evar.Set.mem evk evar_flags.unresolvable_evars in
- let unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars in
- let unresolvable_evars =
- if evk_unres then Evar.Set.add evk' unresolvable_evars else unresolvable_evars
- in { evar_flags with unresolvable_evars }
-
-let unresolvable_evars evd = evd.evar_flags.unresolvable_evars
+let is_typeclass_evar evd evk =
+ let flags = evd.evar_flags in
+ Evar.Set.mem evk flags.typeclass_evars
let set_obligation_evar evd evk =
let flags = evd.evar_flags in
@@ -492,8 +492,31 @@ let is_obligation_evar evd evk =
let flags = evd.evar_flags in
Evar.Set.mem evk flags.obligation_evars
+(** Inheritance of flags: for evar-evar and restriction cases *)
+
+let inherit_evar_flags evar_flags evk evk' =
+ let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
+ let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+ if not (evk_obligation || evk_typeclass) then evar_flags
+ else
+ let typeclass_evars =
+ if evk_typeclass then
+ let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+ Evar.Set.add evk' typeclass_evars
+ else evar_flags.typeclass_evars
+ in
+ let obligation_evars =
+ if evk_obligation then
+ let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+ Evar.Set.add evk' obligation_evars
+ else evar_flags.obligation_evars
+ in
+ { evar_flags with obligation_evars; typeclass_evars }
+
+(** Removal: in all other cases of definition *)
+
let remove_evar_flags evk evar_flags =
- { unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars;
+ { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
(** Restriction information is kept. *)
restricted_evars = evar_flags.restricted_evars }
@@ -506,9 +529,9 @@ let evar_counter_summary_name = "evar counter"
let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
-let new_evar evd ?name evi =
+let new_evar evd ?name ?typeclass_candidate evi =
let evk = new_untyped_evar () in
- let evd = add_with_name evd ?name evk evi in
+ let evd = add_with_name evd ?name ?typeclass_candidate evk evi in
(evd, evk)
let remove d e =
@@ -630,7 +653,7 @@ let create_evar_defs sigma = { sigma with
let empty_evar_flags =
{ obligation_evars = Evar.Set.empty;
restricted_evars = Evar.Map.empty;
- unresolvable_evars = Evar.Set.empty }
+ typeclass_evars = Evar.Set.empty }
let empty = {
defn_evars = EvMap.empty;
@@ -698,16 +721,26 @@ let define_aux def undef evk body =
EvMap.add evk newinfo def, EvMap.remove evk undef
(* define the existential of section path sp as the constr body *)
-let define evk body evd =
+let define_gen evk body evd evar_flags =
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
| _ -> Evar.Set.add evk evd.last_mods
in
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
- let evar_flags = remove_evar_flags evk evd.evar_flags in
{ evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+ let evar_flags = remove_evar_flags evk evd.evar_flags in
+ define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+ let evk' = fst (destEvar body) in
+ let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+ define_gen evk body evd evar_flags
+
let is_restricted_evar evd evk =
try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
with Not_found -> None
@@ -715,6 +748,9 @@ let is_restricted_evar evd evk =
let declare_restricted_evar evar_flags evk evk' =
{ evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
+(* In case of restriction, we declare the restriction and inherit the obligation
+ and typeclass flags. *)
+
let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
@@ -731,7 +767,7 @@ let restrict evk filter ?candidates ?src evd =
let body = mkEvar(evk',id_inst) in
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
- let evar_flags = inherit_unresolvable_evar evar_flags evk evk' in
+ let evar_flags = inherit_evar_flags evar_flags evk evk' in
{ evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
defn_evars; last_mods; evar_names; evar_flags }, evk'
diff --git a/engine/evd.mli b/engine/evd.mli
index 87f74f660d..b0e3c2b869 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -139,7 +139,7 @@ val has_undefined : evar_map -> bool
there are uninstantiated evars in [sigma]. *)
val new_evar : evar_map ->
- ?name:Id.t -> evar_info -> evar_map * Evar.t
+ ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
(** Creates a fresh evar mapping to the given information. *)
val add : evar_map -> Evar.t -> evar_info -> evar_map
@@ -176,7 +176,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m
(** Same as {!raw_map}, but restricted to undefined evars. For efficiency
reasons. *)
-val define : Evar.t-> econstr -> evar_map -> evar_map
+val define : Evar.t -> econstr -> evar_map -> evar_map
(** Set the body of an evar to the given constr. It is expected that:
{ul
{- The evar is already present in the evarmap.}
@@ -184,6 +184,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map
{- All the evars present in the constr should be present in the evar map.}
} *)
+val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map
+(** Same as [define ev body evd], except the body must be an existential variable [ev'].
+ This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *)
+
val cmap : (econstr -> econstr) -> evar_map -> evar_map
(** Map the function on all terms in the evar map. *)
@@ -204,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t
val drop_all_defined : evar_map -> evar_map
+val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t
+
(** {6 Instantiating partial terms} *)
exception NotInstantiatedEvar
@@ -244,13 +250,16 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
(** Tell if an evar comes from restriction of another evar, and if yes, which *)
-val set_resolvable_evar : evar_map -> Evar.t -> bool -> evar_map
-(** Declare an evar resolvable or unresolvable for typeclass resolution *)
+val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map
+(** Mark the given set of evars as available for resolution.
+
+ Precondition: they should indeed refer to undefined typeclass evars.
+ *)
-val unresolvable_evars : evar_map -> Evar.Set.t
-(** The set of unresolvable evars *)
+val get_typeclass_evars : evar_map -> Evar.Set.t
+(** The set of undefined typeclass evars *)
-val is_resolvable_evar : evar_map -> Evar.t -> bool
+val is_typeclass_evar : evar_map -> Evar.t -> bool
(** Is the evar declared resolvable for typeclass resolution *)
val set_obligation_evar : evar_map -> Evar.t -> evar_map
diff --git a/engine/proofview.ml b/engine/proofview.ml
index aabc629ee4..304b2dff84 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -67,11 +67,8 @@ let dependent_init =
let rec aux = function
| TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
| TCons (env, sigma, typ, t) ->
- let (sigma, econstr) = Evarutil.new_evar env sigma ~src typ in
+ let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in
let (gl, _) = EConstr.destEvar sigma econstr in
- (* Goals are created with a store which marks them as unresolvable
- for type classes. *)
- let sigma = Evd.set_resolvable_evar sigma gl false in
let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
let entry = (econstr, typ) :: ret in
entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
@@ -743,23 +740,28 @@ let unshelve l p =
let l = undefined p.solution l in
{ p with comb = p.comb@l }
-let mark_in_evm ~goal evd content =
- let info = Evd.find evd content in
- let info =
+let mark_in_evm ~goal evd evars =
+ let evd =
if goal then
- { info with Evd.evar_source = match info.Evd.evar_source with
- (* Two kinds for goal evars:
- - GoalEvar (morally not dependent)
- - VarInstance (morally dependent of some name).
- This is a heuristic for naming these evars. *)
- | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
- Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
- | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
- | loc,_ -> loc,Evar_kinds.GoalEvar }
- else info
+ let mark evd content =
+ let info = Evd.find evd content in
+ let info =
+ { info with Evd.evar_source = match info.Evd.evar_source with
+ (* Two kinds for goal evars:
+ - GoalEvar (morally not dependent)
+ - VarInstance (morally dependent of some name).
+ This is a heuristic for naming these evars. *)
+ | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
+ Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
+ | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+ | loc,_ -> loc,Evar_kinds.GoalEvar }
+ in Evd.add evd content info
+ in CList.fold_left mark evd evars
+ else evd
in
- let evd = Evd.add evd content info in
- Evd.set_resolvable_evar evd content false
+ let tcs = Evd.get_typeclass_evars evd in
+ let evset = Evar.Set.of_list evars in
+ Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset)
let with_shelf tac =
let open Proof in
@@ -776,7 +778,7 @@ let with_shelf tac =
let sigma = Evd.restore_future_goals sigma fgoals in
(* Ensure we mark and return only unsolved goals *)
let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
- let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+ let sigma = mark_in_evm ~goal:false sigma gls' in
let npv = { npv with shelf; solution = sigma } in
Pv.set npv >> tclUNIT (gls', ans)
@@ -1030,7 +1032,7 @@ module Unsafe = struct
let reset_future_goals p =
{ p with solution = Evd.reset_future_goals p.solution }
- let mark_as_goal evd content =
+ let mark_as_goals evd content =
mark_in_evm ~goal:true evd content
let advance = Evarutil.advance
@@ -1038,7 +1040,7 @@ module Unsafe = struct
let undefined = undefined
let mark_as_unresolvable p gl =
- { p with solution = mark_in_evm ~goal:false p.solution gl }
+ { p with solution = mark_in_evm ~goal:false p.solution [gl] }
end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7bf6390f0e..cda4808a23 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -456,9 +456,9 @@ module Unsafe : sig
(** Clears the future goals store in the proof view. *)
val reset_future_goals : proofview -> proofview
- (** Give an evar the status of a goal (changes its source location
- and makes it unresolvable for type classes. *)
- val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+ (** Give the evars the status of a goal (changes their source location
+ and makes them unresolvable for type classes. *)
+ val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
(** Make an evar unresolvable for type classes. *)
val mark_as_unresolvable : proofview -> Evar.t -> proofview
diff --git a/engine/termops.ml b/engine/termops.ml
index c4b57e4dd2..5e220fd8f1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -365,18 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma =
else
str "CONSTRAINTS:" ++ brk (0, 1) ++
pr_evar_constraints sigma conv_pbs ++ fnl ()
- and unresolvables =
- let evars = Evd.unresolvable_evars sigma in
+ and typeclasses =
+ let evars = Evd.get_typeclass_evars sigma in
if Evar.Set.is_empty evars then mt ()
else
- str "UNRESOLVABLE:" ++ brk (0, 1) ++
- prlist_with_sep spc (pr_existential_key sigma) (Evar.Set.elements evars) ++ fnl ()
+ str "TYPECLASSES:" ++ brk (0, 1) ++
+ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl ()
and metas =
if List.is_empty (Evd.meta_list sigma) then mt ()
else
str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
in
- evs ++ svs ++ cstrs ++ unresolvables ++ metas
+ evs ++ svs ++ cstrs ++ typeclasses ++ metas
let pr_evar_list sigma l =
let open Evd in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:15:04 +0000