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. --- vernac/classes.ml | 2 +- vernac/comDefinition.ml | 4 ++-- vernac/comFixpoint.ml | 3 ++- vernac/comProgramFixpoint.ml | 8 +++++--- vernac/himsg.ml | 3 +-- 5 files changed, 11 insertions(+), 9 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 76d427add..3c133f317 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) (* Check that the type is free of evars now. *) Pretyping.check_evars env Evd.empty sigma termtype; let termtype = to_constr sigma termtype in - let term = Option.map (to_constr sigma) term in + let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index b18a60a1f..9aa61ab46 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -88,8 +88,8 @@ let interp_definition pl bl poly red_option c ctypopt = let evd = Evd.minimize_universes evd in (* Substitute evars and universes, and add parameters. Note: in program mode some evars may remain. *) - let ctx = List.map (EConstr.to_rel_decl evd) ctx in - let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in + let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in + let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a794c2db0..1466fa243 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -225,7 +225,8 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in let sigma, _ = nf_evars_and_universes sigma in - let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in + (* XXX: We still have evars here in Program *) + let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index b95741ca4..745f1df1d 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -229,7 +229,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = Lemmas.mk_hook (hook sigma) in - let fullcoqc = EConstr.to_constr sigma def in + (* XXX: Grounding non-ground terms here... bad bad *) + let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in let fullctyp = EConstr.to_constr sigma typ in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = @@ -261,9 +262,10 @@ let do_program_recursive local poly fixkind fixl ntns = let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) and typ = - EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) + (* Worrying... *) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 698ee4703..23c863cab 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -640,8 +640,7 @@ let explain_refiner_cannot_generalize env sigma ty = pr_leconstr_env env sigma ty ++ str "." let explain_no_occurrence_found env sigma c id = - let c = EConstr.to_constr sigma c in - str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ + str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++ str " in " ++ (match id with | Some id -> Id.print id -- cgit v1.2.3