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. --- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssr/ssrequality.ml | 11 +++++++---- plugins/ssr/ssripats.ml | 2 +- plugins/ssr/ssrview.ml | 2 +- 4 files changed, 10 insertions(+), 7 deletions(-) (limited to 'plugins/ssr') diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d5118da4c..e07bc48a4 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -504,7 +504,7 @@ let nf_evar sigma t = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t)) let pf_abs_evars2 gl rigid (sigma, c0) = - let c0 = EConstr.to_constr sigma c0 in + let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in let sigma0, ucst = project gl, Evd.evar_universe_context sigma in let nenv = env_size (pf_env gl) in let abs_evar n k = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 57635edac..2f0433b64 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl = let foldtac occ rdx ft gl = let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let sigma, t = ft in - let t = EConstr.to_constr sigma t in + let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in let fold, conclude = match rdx with | Some (_, (In_T _ | In_X_In_T _)) | None -> let ise = Evd.create_evar_defs sigma in @@ -557,7 +557,7 @@ let rwrxtac occ rdx_pat dir rule gl = let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = let sigma, pat = let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in - mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in + mk_tpattern env sigma0 (sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma r) (rw_progress rhs) d (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in @@ -567,7 +567,7 @@ let rwrxtac occ rdx_pat dir rule gl = let r = ref None in (fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h), (fun concl -> closed0_check concl e gl; - let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ev c)) , x) in + let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in let concl0 = EConstr.Unsafe.to_constr concl0 in let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in let (d, r), rdx = conclude concl in @@ -589,7 +589,10 @@ let ssrinstancesofrule ist dir arg gl = let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) = let sigma, pat = let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in - mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in + mk_tpattern env sigma0 + (sigma,EConstr.to_constr ~abort_on_undefined_evars:false sigma r) + (rw_progress rhs) d + (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in sigma, pats @ [pat] in let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 42566575c..8bba35440 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -410,7 +410,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin Goal.enter_one begin fun g -> let pat = Ssrmatching.interp_cpattern sigma0 t None in let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in - let cl = EConstr.to_constr sigma cl0 in + let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in let (c, ucst), cl = try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index aa614fbc1..afe03533d 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -254,7 +254,7 @@ let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in + let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in -- cgit v1.2.3