Glob-ops: a name-mapping operation for pattern-matching binders.

2 files changed, 53 insertions, 0 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index fd51545b2f..588810eaa1 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -328,6 +328,51 @@ let free_glob_vars  =
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
 
+(** Mapping of names in binders *)
+
+(* spiwack: I used a smartmap-style kind of mapping here, because the
+   operation will be the identity almost all of the time (with any
+   term outside of Ltac to begin with). But to be honest, there would
+   probably be no significant penalty in doing reallocation as
+   pattern-matching expressions are usually rather small. *)
+
+let map_inpattern_binders f ((loc,id,nal) as x) =
+  let r = CList.smartmap f nal in
+  if r == nal then x
+  else loc,id,r
+
+let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple =
+  let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in
+  if r == inp then x
+  else c,(f na, r)
+
+let rec map_case_pattern_binders f = function
+  | PatVar (loc,na) as x ->
+      let r = f na in
+      if r == na then x
+      else PatVar (loc,r)
+  | PatCstr (loc,c,ps,na) as x ->
+      let rna = f na in
+      let rps =
+        CList.smartmap (fun p -> map_case_pattern_binders f p) ps
+      in
+      if rna == na && rps == ps then x
+      else PatCstr(loc,c,rps,rna)
+
+let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause =
+  (* spiwack: not sure if I must do something with the list of idents.
+     It is intended to be a superset of the free variable of the
+     right-hand side, if I understand correctly. But I'm not sure when
+     or how they are used. *)
+  let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in
+  if r == cll then x
+  else loc,il,r,rhs
+
+let map_pattern_binders f tomatch branches =
+  CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch,
+  CList.smartmap (fun br -> map_cases_branch_binders f br) branches
+
+(** /mapping of names in binders *)
 
 let loc_of_glob_constr = function
   | GRef (loc,_,_) -> loc
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 9e0aac909f..41d1d51a54 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -37,6 +37,14 @@ val occur_glob_constr : Id.t -> glob_constr -> bool
 val free_glob_vars : glob_constr -> Id.t list
 val loc_of_glob_constr : glob_constr -> Loc.t
 
+(** [map_pattern_binders f m c] applies [f] to all the binding names
+    in a pattern-matching expression ({!Glob_term.GCases}) represented
+    here by its relevant components [m] and [c]. It is used to
+    interpret Ltac-bound names both in pretyping and printing of
+    terms. *)
+val map_pattern_binders : (name -> name) ->
+  tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
+
 (** Conversion from glob_constr to cases pattern, if possible
 
     Take the current alias as parameter,