Printing function for [uconstr].

The core is a "detyping" function for [closed_glob_constr]. Which interpretes the variable names according to the Ltac context, and apply the standard detyping procedure to typed terms in the closure.

4 files changed, 76 insertions, 0 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2d7c7b146..89589bfac 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -687,6 +687,64 @@ let detype_names isgoal avoid nenv env sigma t =
 let detype ?(lax=false) isgoal avoid env sigma t =
   detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
 
+let detype_closed_glob ?lax isgoal avoid env sigma t =
+  let convert_id cl id =
+    try Id.Map.find id cl.idents
+    with Not_found -> id
+  in
+  let convert_name cl = function
+    | Name id -> Name (convert_id cl id)
+    | Anonymous -> Anonymous
+  in
+  let rec detype_closed_glob cl = function
+    | GVar (loc,id) ->
+        (* if [id] is bound to a name. *)
+        begin try
+          GVar(loc,Id.Map.find id cl.idents)
+        (* if [id] is bound to a typed term *)
+        with Not_found -> try
+          (* assumes [detype] does not raise [Not_found] exceptions *)
+          let (b,c) = Id.Map.find id cl.typed in
+          (* spiwack: I'm not sure it is the right thing to do,
+             but I'm computing the detyping environment like
+             [Printer.pr_constr_under_binders_env] does. *)
+          let assums = List.map (fun id -> (Name id,(* dummy *) mkProp)) b in
+          let env = Termops.push_rels_assum assums env in
+          detype ?lax isgoal avoid env sigma c
+        (* if [id] is bound to a [closed_glob_constr]. *)
+        with Not_found -> try
+          let {closure;term} = Id.Map.find id cl.untyped in
+          detype_closed_glob closure term
+        (* Otherwise [id] stands for itself *)
+        with Not_found ->
+         GVar(loc,id)
+        end
+    | GLambda (loc,id,k,t,c) ->
+        let id = convert_name cl id in
+        GLambda(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
+    | GProd (loc,id,k,t,c) ->
+        let id = convert_name cl id in
+        GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
+    | GLetIn (loc,id,b,e) ->
+        let id = convert_name cl id in
+        GLetIn(loc,id,detype_closed_glob cl b, detype_closed_glob cl e)
+    | GLetTuple (loc,ids,(n,r),b,e) ->
+        let ids = List.map (convert_name cl) ids in
+        let n = convert_name cl n in
+        GLetTuple (loc,ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e)
+    | GCases (loc,sty,po,tml,eqns) ->
+        let (tml,eqns) =
+          Glob_ops.map_pattern_binders (fun na -> convert_name cl na) tml eqns
+        in
+        let (tml,eqns) =
+          Glob_ops.map_pattern (fun c -> detype_closed_glob cl c) tml eqns
+        in
+        GCases(loc,sty,po,tml,eqns)
+    | c ->
+        Glob_ops.map_glob_constr (detype_closed_glob cl) c
+  in
+  detype_closed_glob t.closure t.term
+
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 8a8312990..064b6a5ae 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -45,6 +45,8 @@ val detype_sort : sorts -> glob_sort
 val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
   evar_map -> rel_context -> glob_decl list
 
+val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
+
 (** look for the index of a named var or a nondep var as it is renamed *)
 val lookup_name_as_displayed  : env -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 588810eaa..4f54facf6 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -374,6 +374,15 @@ let map_pattern_binders f tomatch branches =
 
 (** /mapping of names in binders *)
 
+let map_tomatch f (c,pp) : tomatch_tuple = f c , pp
+
+let map_cases_branch f (loc,il,cll,rhs) : cases_clause =
+  loc , il , cll , f rhs
+
+let map_pattern f tomatch branches =
+  List.map (fun tm -> map_tomatch f tm) tomatch,
+  List.map (fun br -> map_cases_branch f br) branches
+
 let loc_of_glob_constr = function
   | GRef (loc,_,_) -> loc
   | GVar (loc,_) -> loc
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 41d1d51a5..5d84921d5 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -45,6 +45,13 @@ val loc_of_glob_constr : glob_constr -> Loc.t
 val map_pattern_binders : (name -> name) ->
   tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
 
+(** [map_pattern f m c] applies [f] to the return predicate and the
+    right-hand side of a pattern-matching expression
+    ({!Glob_term.GCases}) represented here by its relevant components
+    [m] and [c]. *)
+val map_pattern : (glob_constr -> glob_constr) ->
+  tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses)
+
 (** Conversion from glob_constr to cases pattern, if possible
 
     Take the current alias as parameter,