diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-04 15:54:28 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-31 18:44:19 +0200 |
commit | 9f723f14e5342c1303646b5ea7bb5c0012a090ef (patch) | |
tree | d6a6a82ab8b73e975588a547eb15a5a2f83fd4c7 /pretyping | |
parent | 2d2d16430822f1768ce4f3c62ef0750b94e4747f (diff) |
[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.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 3 | ||||
-rw-r--r-- | pretyping/evarsolve.ml | 4 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
-rw-r--r-- | pretyping/retyping.ml | 2 | ||||
-rw-r--r-- | pretyping/tacred.ml | 2 | ||||
-rw-r--r-- | pretyping/typing.ml | 6 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 4 |
7 files changed, 13 insertions, 12 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 73be9d6b7..b16f1a9ed 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2581,7 +2581,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in let j = { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; - uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); } + (* XXX: is this normalization needed? *) + uj_type = Evarutil.nf_evar !evdref tycon; } in j (**************************************************************************) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 96d80741a..0c109b026 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1592,14 +1592,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = Id.Set.subset (collect_vars evd rhs) !names in let body = - if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) + if fast rhs then nf_evar evd rhs (** FIXME? *) else let t' = imitate (env,0) rhs in if !progress then (recheck_applications conv_algo (evar_env evi) evdref t'; t') else t' in (!evdref,body) - + (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, * [define] tries to find an instance lhs such that diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4962b89a0..2c371d5cf 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -117,7 +117,7 @@ open ExtraEnv exception Found of int array let nf_fix sigma (nas, cs, ts) = - let inj c = EConstr.to_constr sigma c in + let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in (nas, Array.map inj cs, Array.map inj ts) let search_guard ?loc env possible_indexes fixdefs = @@ -1150,7 +1150,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D (* Correction of bug #5315 : we need to define an evar for *all* holes *) let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in let ev,_ = destEvar !evdref evkt in - evdref := Evd.define ev (to_constr !evdref v) !evdref; + evdref := Evd.define ev (to_constr ~abort_on_undefined_evars:false !evdref v) !evdref; (* End of correction of bug #5315 *) { utj_val = v; utj_type = s } diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3582b6447..95aa5ebef 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma = and type_of_global_reference_knowing_parameters env c args = let argtyps = - Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in + Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in match EConstr.kind sigma c with | Ind (ind, u) -> let u = EInstance.kind sigma u in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 518d2f604..977713fd8 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -558,7 +558,7 @@ let match_eval_ref_value env sigma constr stack = else None | Proj (p, c) when not (Projection.unfolded p) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr) (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef (Projection.constant p)) then Some (mkProj (Projection.unfold p, c)) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 4c834f2f8..c4eb6af89 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -35,7 +35,7 @@ let meta_type evd mv = let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in + let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = @@ -155,7 +155,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in let () = e_is_correct_arity env evdref c pj ind specif params in - let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in + let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in @@ -207,7 +207,7 @@ let enrich_env env evdref = Environ.env_of_pre_env penv' let check_fix env sigma pfix = - let inj c = EConstr.to_constr sigma c in + let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in let (idx, (ids, cs, ts)) = pfix in check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts)) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 3c9b8bc33..f314ae0d6 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -381,8 +381,8 @@ let cbv_vm env sigma c t = if Termops.occur_meta sigma c then CErrors.user_err Pp.(str "vm_compute does not support metas."); (** This evar-normalizes terms beforehand *) - let c = EConstr.to_constr sigma c in - let t = EConstr.to_constr sigma t in + let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in + let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in let v = Vconv.val_of_constr env c in EConstr.of_constr (nf_val env sigma v t) |