[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.
coq · Dec 17, 2017 · bccdf47 · bccdf47
1 parent 741a93a
commit bccdf47
Show file tree

Hide file tree

Showing 19 changed files with 51 additions and 38 deletions.
diff --git a/API/API.mli b/API/API.mli
@@ -3074,7 +3074,7 @@ sig
 
   val applist : constr * constr list -> constr
 
-  val to_constr : Evd.evar_map -> constr -> Constr.t
+  val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> constr -> Constr.t
 
   val push_rel : rel_declaration -> Environ.env -> Environ.env
 

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
@@ -38,7 +38,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
@@ -108,11 +108,15 @@ 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 rec to_constr ?(abort_on_undefined_evars=true) sigma 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 ~abort_on_undefined_evars sigma 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 ~abort_on_undefined_evars sigma c) c
   end
 | Sort (Sorts.Type u) ->
   let u' = Evd.normalize_universe sigma u in
@@ -126,7 +130,7 @@ 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 ~abort_on_undefined_evars sigma c) c
 
 let of_named_decl d = d
 let unsafe_to_named_decl d = d

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
@@ -66,8 +66,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. See {!Evarutil.nf_evar}. *)
+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
@@ -70,9 +70,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;

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
@@ -88,7 +88,7 @@ let rec decompose_term env sigma t=
 	decompose_term env sigma c
     | _ ->
        let t = Termops.strip_outer_cast sigma t in
-       if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
+       if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found
 
 (* decompose equality in members and type *)
 open Termops

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
@@ -75,14 +75,14 @@ module CM=Map.Make(Constr)
 module History=Set.Make(Hitem)
 
 let cm_add sigma typ nam cm=
-  let typ = EConstr.to_constr sigma typ in
+  let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in CM.add typ (nam::l) cm
   with
       Not_found->CM.add typ [nam] cm
 
 let cm_remove sigma typ nam cm=
-  let typ = EConstr.to_constr sigma typ in
+  let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   try
     let l=CM.find typ cm in
     let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
@@ -150,7 +150,7 @@ let re_add_formula_list sigma lf seq=
      redexes=List.fold_right HP.add lf seq.redexes;
      context=List.fold_right do_one lf seq.context}
 
-let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
+let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context)
 
 (*let rev_left seq=
   try

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
@@ -286,7 +286,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
@@ -569,7 +569,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
@@ -579,7 +579,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

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
@@ -2586,7 +2586,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
@@ -1590,14 +1590,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
@@ -116,7 +116,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 =
@@ -1144,7 +1144,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
@@ -168,7 +168,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
@@ -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
@@ -38,7 +38,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
   EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
@@ -130,7 +130,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
@@ -182,7 +182,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/tactics/hints.ml b/tactics/hints.ml
@@ -790,7 +790,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
     match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
+	let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -812,7 +812,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
+	let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in

diff --git 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
@@ -85,7 +85,8 @@ let interp_definition pl bl poly red_option c ctypopt =
   (* universe minimization *)
   let evd = Evd.nf_constraints evd in
   (* Unless program mode the body and type are ready, substitute evars *)
-  let body = to_constr evd (it_mkLambda_or_LetIn c ctx) in
+  (* XXX: Indeed in program mode the term is not ground *)
+  let body = to_constr ~abort_on_undefined_evars:false evd (it_mkLambda_or_LetIn c ctx) in
   let tyopt = Option.map (fun ty -> to_constr evd (it_mkProd_or_LetIn ty ctx)) tyopt in
   (* Keep only useful universes (NB: if program mode evars may remain) *)
   let bodyvars = universes_of_constr env evd (of_constr body) in

diff --git 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
@@ -632,8 +632,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

diff --git a/vernac/record.ml b/vernac/record.ml
@@ -70,7 +70,7 @@ let interp_fields_evars env sigma impls_env nots l =
       let impls =
 	match i with
 	| Anonymous -> impls
-        | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls
+        | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr ~abort_on_undefined_evars:false sigma t') impl) impls
       in
       let d = match b' with
 	      | None -> LocalAssum (i,t')
@@ -144,7 +144,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let assums = List.filter is_local_assum newps in
   let params = List.map (RelDecl.get_name %> Name.get_id) assums in
   let ty = Inductive (params,(finite != BiFinite)) in
-  let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in
+  let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr ~abort_on_undefined_evars:false sigma arity] [imps] in
   let env2,sigma,impls,newfs,data =
     interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs)
   in