From 9f723f14e5342c1303646b5ea7bb5c0012a090ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 4 Dec 2017 15:54:28 +0100 Subject: [econstr] Forbid calling `to_constr` in open terms. We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants. --- engine/eConstr.ml | 16 +++++++++++----- engine/eConstr.mli | 13 ++++++++----- engine/evarutil.ml | 4 ++-- 3 files changed, 21 insertions(+), 12 deletions(-) (limited to 'engine') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bd47a04f1..01b4fe851 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -40,7 +40,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type val whd_evar : Evd.evar_map -> t -> t val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t val of_constr : Constr.t -> t -val to_constr : evar_map -> t -> Constr.t +val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t val unsafe_to_constr : t -> Constr.t val unsafe_eq : (t, Constr.t) eq val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt @@ -110,11 +110,16 @@ let of_constr c = c let unsafe_to_constr c = c let unsafe_eq = Refl -let rec to_constr sigma c = match Constr.kind c with +let to_constr ?(abort_on_undefined_evars=true) sigma c = +let rec to_constr c = match Constr.kind c with | Evar ev -> begin match safe_evar_value sigma ev with - | Some c -> to_constr sigma c - | None -> Constr.map (fun c -> to_constr sigma c) c + | Some c -> to_constr c + | None -> + if abort_on_undefined_evars then + anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") + else + Constr.map (fun c -> to_constr c) c end | Sort (Sorts.Type u) -> let u' = Evd.normalize_universe sigma u in @@ -128,7 +133,8 @@ let rec to_constr sigma c = match Constr.kind c with | Construct (co, u) when not (Univ.Instance.is_empty u) -> let u' = Evd.normalize_universe_instance sigma u in if u' == u then c else mkConstructU (co, u') -| _ -> Constr.map (fun c -> to_constr sigma c) c +| _ -> Constr.map (fun c -> to_constr c) c +in to_constr c let of_named_decl d = d let unsafe_to_named_decl d = d diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 28c9dd3c2..dac937457 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -68,11 +68,14 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -val to_constr : Evd.evar_map -> t -> Constr.t -(** Returns the evar-normal form of the argument, and cast it as a theoretically - evar-free term. In practice this function does not check that the result - is actually evar-free, it is currently the duty of the caller to do so. - This might change in the future. *) +val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t +(** Returns the evar-normal form of the argument. Note that this + function is supposed to be called when the original term has not + more free-evars anymore. If you need compatibility with the old + semantics, set [abort_on_undefined_evars] to [false]. + + For getting the evar-normal form of a term with evars see + {!Evarutil.nf_evar}. *) val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 45760c6b4..c707b37b6 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -72,9 +72,9 @@ let flush_and_check_evars sigma c = (** Term exploration up to instantiation. *) let kind_of_term_upto = EConstr.kind_upto -let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t) +let nf_evar0 sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t) let whd_evar = EConstr.whd_evar -let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c) +let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr ~abort_on_undefined_evars:false sigma c) let j_nf_evar sigma j = { uj_val = nf_evar sigma j.uj_val; -- cgit v1.2.3