Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.

This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation

The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.

We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.

1 files changed, 193 insertions, 0 deletions

diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
new file mode 100644
index 0000000000..1bb4551f7c
--- /dev/null
+++ b/pretyping/globEnv.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+open Names
+open Environ
+open EConstr
+open Evarutil
+open Termops
+open Vars
+open Ltac_pretype
+
+(** This files provides a level of abstraction for the kind of
+    environment used for type inference (so-called pretyping); in
+    particular:
+    - it supports that term variables can be interpreted as Ltac
+      variables pointing to the effective expected name
+    - it incrementally and lazily computes the renaming of rel
+      variables used to build purely-named evar contexts
+*)
+
+type t = {
+  static_env : env;
+  (** For locating indices *)
+  renamed_env : env;
+  (** For name management *)
+  extra : ext_named_context Lazy.t;
+  (** Delay the computation of the evar extended environment *)
+  lvar : ltac_var_map;
+}
+
+let make env sigma lvar =
+  let get_extra env sigma =
+    let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
+    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+      (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
+  {
+    static_env = env;
+    renamed_env = env;
+    extra = lazy (get_extra env sigma);
+    lvar = lvar;
+  }
+
+let env env = env.static_env
+
+let ltac_interp_name { ltac_idents ; ltac_genargs } = function
+  | Anonymous -> Anonymous
+  | Name id as na ->
+      try Name (Id.Map.find id ltac_idents)
+      with Not_found ->
+        if Id.Map.mem id ltac_genargs then
+          user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
+                    spc () ++ str "is not bound to an identifier." ++
+                    spc () ++str "It cannot be used in a binder.")
+        else na
+
+let push_rel sigma d env =
+  let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
+  let env = {
+    static_env = push_rel d env.static_env;
+    renamed_env = push_rel d' env.renamed_env;
+    extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+    lvar = env.lvar;
+    } in
+  d', env
+
+let push_rel_context ?(force_names=false) sigma ctx env =
+  let open Context.Rel.Declaration in
+  let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
+  let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
+  let env = {
+    static_env = push_rel_context ctx env.static_env;
+    renamed_env = push_rel_context ctx' env.renamed_env;
+    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+    lvar = env.lvar;
+    } in
+  ctx', env
+
+let push_rec_types sigma (lna,typarray) env =
+  let open Context.Rel.Declaration in
+  let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
+  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+  Array.map get_name ctx, env
+
+let e_new_evar env evdref ?src ?naming typ =
+  let open Context.Named.Declaration in
+  let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in
+  let (subst, _, nc) = Lazy.force env.extra in
+  let typ' = csubst_subst subst typ in
+  let instance = inst_rels @ inst_vars in
+  let sign = val_of_named_context nc in
+  let sigma = !evdref in
+  let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in
+  evdref := sigma;
+  e
+
+let hide_variable env expansion id =
+  let lvar = env.lvar in
+  if Id.Map.mem id lvar.ltac_genargs then
+    let lvar = match expansion with
+    | Name id' ->
+       (* We are typically in a situation [match id return P with ... end]
+          which we interpret as [match id' as id' return P with ... end],
+          with [P] interpreted in an environment where [id] is bound to [id'].
+          The variable is already bound to [id'], so nothing to do *)
+       lvar
+    | _ ->
+       (* We are typically in a situation [match id return P with ... end]
+          with [id] bound to a non-variable term [c]. We interpret as
+         [match c as id return P with ... end], and hides [id] while
+         interpreting [P], since it has become a binder and cannot be anymore be
+         substituted by a variable coming from the Ltac substitution. *)
+       { lvar with
+         ltac_uconstrs = Id.Map.remove id lvar.ltac_uconstrs;
+         ltac_constrs = Id.Map.remove id lvar.ltac_constrs;
+         ltac_genargs = Id.Map.remove id lvar.ltac_genargs } in
+    { env with lvar }
+  else
+    env
+
+let protected_get_type_of env sigma c =
+  try Retyping.get_type_of ~lax:true env sigma c
+  with Retyping.RetypeError _ ->
+    user_err
+      (str "Cannot reinterpret " ++ quote (print_constr c) ++
+       str " in the current environment.")
+
+let invert_ltac_bound_name env id0 id =
+  try mkRel (pi1 (lookup_rel_id id (rel_context env.static_env)))
+  with Not_found ->
+    user_err  (str "Ltac variable " ++ Id.print id0 ++
+                       str " depends on pattern variable name " ++ Id.print id ++
+                       str " which is not bound in current context.")
+
+let interp_ltac_variable ?loc typing_fun env sigma id =
+  (* Check if [id] is an ltac variable *)
+  try
+    let (ids,c) = Id.Map.find id env.lvar.ltac_constrs in
+    let subst = List.map (invert_ltac_bound_name env id) ids in
+    let c = substl subst c in
+      { uj_val = c; uj_type = protected_get_type_of env.renamed_env sigma c }
+  with Not_found ->
+  try
+    let {closure;term} = Id.Map.find id env.lvar.ltac_uconstrs in
+    let lvar = {
+      ltac_constrs = closure.typed;
+      ltac_uconstrs = closure.untyped;
+      ltac_idents = closure.idents;
+      ltac_genargs = Id.Map.empty; }
+    in
+    (* spiwack: I'm catching [Not_found] potentially too eagerly
+       here, as the call to the main pretyping function is caught
+       inside the try but I want to avoid refactoring this function
+       too much for now. *)
+    typing_fun {env with lvar} term
+  with Not_found ->
+  (* Check if [id] is a ltac variable not bound to a term *)
+  (* and build a nice error message *)
+  if Id.Map.mem id env.lvar.ltac_genargs then begin
+    let Geninterp.Val.Dyn (typ, _) = Id.Map.find id env.lvar.ltac_genargs in
+    user_err ?loc
+     (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \
+      bound to a " ++ Geninterp.Val.pr typ ++ str ".")
+  end;
+  raise Not_found
+
+module ConstrInterpObj =
+struct
+  type ('r, 'g, 't) obj =
+    unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+  let name = "constr_interp"
+  let default _ = None
+end
+
+module ConstrInterp = Genarg.Register(ConstrInterpObj)
+
+let register_constr_interp0 = ConstrInterp.register0
+
+let interp_glob_genarg env sigma ty arg =
+  let open Genarg in
+  let GenArg (Glbwit tag, arg) = arg in
+  let interp = ConstrInterp.obj tag in
+  interp env.lvar.ltac_genargs env.renamed_env sigma ty arg