diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 96 |
1 files changed, 66 insertions, 30 deletions
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' |