diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 86 |
1 files changed, 52 insertions, 34 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index d37b49e2dc..b621a3fe2f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -222,7 +222,7 @@ let map_evar_body f = function let map_evar_info f evi = {evi with evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val f evi.evar_hyps; + evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps; evar_concl = f evi.evar_concl; evar_candidates = Option.map (List.map f) evi.evar_candidates } @@ -430,6 +430,14 @@ type evar_flags = restricted_evars : Evar.t Evar.Map.t; typeclass_evars : Evar.Set.t } +type side_effect_role = +| Schema of inductive * string + +type side_effects = { + seff_private : Safe_typing.private_constants; + seff_roles : side_effect_role Cmap.t; +} + type evar_map = { (* Existential variables *) defn_evars : evar_info EvMap.t; @@ -444,7 +452,7 @@ type evar_map = { metas : clbinding Metamap.t; evar_flags : evar_flags; (** Interactive proofs *) - effects : Safe_typing.private_constants; + effects : side_effects; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -672,6 +680,11 @@ let empty_evar_flags = restricted_evars = Evar.Map.empty; typeclass_evars = Evar.Set.empty } +let empty_side_effects = { + seff_private = Safe_typing.empty_private_constants; + seff_roles = Cmap.empty; +} + let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; @@ -680,7 +693,7 @@ let empty = { last_mods = Evar.Set.empty; evar_flags = empty_evar_flags; metas = Metamap.empty; - effects = Safe_typing.empty_private_constants; + effects = empty_side_effects; evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; @@ -823,33 +836,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = | Evar (evk2,_) -> fst (evar_source evk2 evd) | _ -> None -(** The following functions return the set of evars immediately - contained in the object *) - -(* excluding defined evars *) - -let evars_of_term c = - let rec evrec acc c = - match kind c with - | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) - | _ -> Constr.fold evrec acc c - in - evrec Evar.Set.empty c - -let evars_of_named_context nc = - Context.Named.fold_outside - (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term constr))) - nc - ~init:Evar.Set.empty - -let evars_of_filtered_evar_info evi = - Evar.Set.union (evars_of_term evi.evar_concl) - (Evar.Set.union - (match evi.evar_body with - | Evar_empty -> Evar.Set.empty - | Evar_defined b -> evars_of_term b) - (evars_of_named_context (evar_filtered_context evi))) - (**********************************************************) (* Sort variables *) @@ -1038,12 +1024,17 @@ exception UniversesDiffer = UState.UniversesDiffer (**********************************************************) (* Side effects *) +let concat_side_effects eff eff' = { + seff_private = Safe_typing.concat_private eff.seff_private eff'.seff_private; + seff_roles = Cmap.fold Cmap.add eff.seff_roles eff'.seff_roles; +} + let emit_side_effects eff evd = - { evd with effects = Safe_typing.concat_private eff evd.effects; - universes = UState.emit_side_effects eff evd.universes } + let effects = concat_side_effects eff evd.effects in + { evd with effects; universes = UState.emit_side_effects eff.seff_private evd.universes } let drop_side_effects evd = - { evd with effects = Safe_typing.empty_private_constants; } + { evd with effects = empty_side_effects; } let eval_side_effects evd = evd.effects @@ -1404,3 +1395,30 @@ module MiniEConstr = struct let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d end + +(** The following functions return the set of evars immediately + contained in the object *) + +(* excluding defined evars *) + +let evars_of_term evd c = + let rec evrec acc c = + match MiniEConstr.kind evd c with + | Evar (n, l) -> Evar.Set.add n (Array.fold_left evrec acc l) + | _ -> Constr.fold evrec acc c + in + evrec Evar.Set.empty c + +let evars_of_named_context evd nc = + Context.Named.fold_outside + (NamedDecl.fold_constr (fun constr s -> Evar.Set.union s (evars_of_term evd constr))) + nc + ~init:Evar.Set.empty + +let evars_of_filtered_evar_info evd evi = + Evar.Set.union (evars_of_term evd evi.evar_concl) + (Evar.Set.union + (match evi.evar_body with + | Evar_empty -> Evar.Set.empty + | Evar_defined b -> evars_of_term evd b) + (evars_of_named_context evd (evar_filtered_context evi))) |