Move CompactedDecl to ppconstr

SkySkimmer · SkySkimmer · commit dd2c97fcb184 · 2026-05-19T17:29:42.000+02:00
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
@@ -171,9 +171,7 @@ type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = (types, ESorts.t) Environ.punsafe_type_judgment
 type named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pt
 type rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt
-type compacted_declaration = (constr, types, ERelevance.t) Context.Compacted.Declaration.pt
 type named_context = (constr, types, ERelevance.t) Context.Named.pt
-type compacted_context = compacted_declaration list
 type rel_context = (constr, types, ERelevance.t) Context.Rel.pt
 type 'a binder_annot = ('a, ERelevance.t) Context.pbinder_annot
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
@@ -93,9 +93,7 @@ type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment
 type named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pt
 type rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt
-type compacted_declaration = (constr, types, ERelevance.t) Context.Compacted.Declaration.pt
 type named_context = (constr, types, ERelevance.t) Context.Named.pt
-type compacted_context = compacted_declaration list
 type rel_context = (constr, types, ERelevance.t) Context.Rel.pt
 type 'a binder_annot = ('a,ERelevance.t) Context.pbinder_annot
 
diff --git a/engine/termops.ml b/engine/termops.ml
@@ -22,7 +22,6 @@ open Environ
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-module CompactedDecl = Context.Compacted.Declaration
 
 module Internal = struct
 
@@ -1182,28 +1181,6 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 let mem_named_context_val id ctxt =
   try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false
 
-let compact_named_context sigma sign =
-  let compact l decl =
-    match decl, l with
-    | NamedDecl.LocalAssum (i,t), [] ->
-       [CompactedDecl.LocalAssum ([i],t)]
-    | NamedDecl.LocalDef (i,c,t), [] ->
-       [CompactedDecl.LocalDef ([i],c,t)]
-    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
-       if EConstr.eq_constr sigma t1 t2
-       then CompactedDecl.LocalAssum (i1::li, t2) :: q
-       else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
-    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
-       if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2
-       then CompactedDecl.LocalDef (i1::li, c2, t2) :: q
-       else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
-    | NamedDecl.LocalAssum (i,t), q ->
-       CompactedDecl.LocalAssum ([i],t) :: q
-    | NamedDecl.LocalDef (i,c,t), q ->
-       CompactedDecl.LocalDef ([i],c,t) :: q
-  in
-  sign |> Context.Named.fold_inside compact ~init:[] |> List.rev
-
 let clear_named_body id env =
   let open NamedDecl in
   let aux _ status = function
diff --git a/engine/termops.mli b/engine/termops.mli
@@ -194,7 +194,6 @@ val fold_named_context_both_sides :
   ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) ->
     Constr.named_context -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
-val compact_named_context : Evd.evar_map -> EConstr.named_context -> EConstr.compacted_context
 
 val clear_named_body : Id.t -> env -> env
 
diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml
@@ -207,7 +207,7 @@ let process_goal short sigma g =
     if short then [] else
       let hyps =
         List.rev_map process_hyp
-        (Termops.compact_named_context sigma (EConstr.named_context env))
+          (Ppconstr.compact_named_context sigma (EConstr.named_context env))
       in
       hyps
   in
diff --git a/kernel/constr.ml b/kernel/constr.ml
@@ -1383,10 +1383,8 @@ let hcons = HCons.hcons
 
 type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt
 type named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pt
-type compacted_declaration = (constr, types, Sorts.relevance) Context.Compacted.Declaration.pt
 type rel_context = rel_declaration list
 type named_context = named_declaration list
-type compacted_context = compacted_declaration list
 
 (** Minimalistic constr printer, typically for debugging *)
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
@@ -430,10 +430,8 @@ val eq_constr_nounivs : constr -> constr -> bool
 
 type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt
 type named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pt
-type compacted_declaration = (constr, types, Sorts.relevance) Context.Compacted.Declaration.pt
 type rel_context = rel_declaration list
 type named_context = named_declaration list
-type compacted_context = compacted_declaration list
 
 (** {6 Relocation and substitution } *)
 
diff --git a/kernel/context.ml b/kernel/context.ml
@@ -569,32 +569,3 @@ struct
   let instance mk l =
     Array.of_list (instance_list mk l)
 end
-
-module Compacted =
-  struct
-    module Declaration =
-      struct
-        type ('constr, 'types, 'r) pt =
-          | LocalAssum of (Id.t,'r) pbinder_annot list * 'types
-          | LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types
-
-        let map_constr f = function
-          | LocalAssum (ids, ty) as decl ->
-             let ty' = f ty in
-             if ty == ty' then decl else LocalAssum (ids, ty')
-          | LocalDef (ids, c, ty) as decl ->
-             let ty' = f ty in
-             let c' = f c in
-             if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
-
-        let of_named_decl = function
-          | Named.Declaration.LocalAssum (id,t) ->
-              LocalAssum ([id],t)
-          | Named.Declaration.LocalDef (id,v,t) ->
-              LocalDef ([id],v,t)
-      end
-
-    type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
-
-    let fold f l ~init = List.fold_right f l init
-  end
diff --git a/kernel/context.mli b/kernel/context.mli
@@ -370,20 +370,3 @@ sig
   (** [instance_list] is like [instance] but returning a list. *)
   val instance_list : (Id.t -> 'v) -> ('c, 't, 'r) pt -> 'v list
 end
-
-module Compacted :
-sig
-  module Declaration :
-  sig
-    type ('constr, 'types, 'r) pt =
-      | LocalAssum of (Id.t,'r) pbinder_annot list * 'types
-      | LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types
-
-    val map_constr : ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt
-    val of_named_decl : ('c, 't, 'r) Named.Declaration.pt -> ('c, 't, 'r) pt
-  end
-
-  type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
-
-  val fold : (('c, 't, 'r) Declaration.pt -> 'a -> 'a) -> ('c, 't, 'r) pt -> init:'a -> 'a
-end
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
@@ -855,3 +855,42 @@ let pr_lconstr_pattern_expr ~flags env sigma c : Pp.t = !term_pr.pr_lconstr_patt
 let pr_cases_pattern_expr ~flags c : Pp.t = pr_patt ~flags (pr ~flags no_after ltop) no_after ltop c
 
 let pr_binders ~flags env sigma l : Pp.t = pr_undelimited_binders ~flags spc true (pr_expr ~flags env sigma no_after ltop) l
+
+module CompactedDecl = struct
+  type t =
+    | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types
+    | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types
+
+  let of_named_decl = function
+    | Context.Named.Declaration.LocalAssum (id,t) ->
+      LocalAssum ([id],t)
+    | Context.Named.Declaration.LocalDef (id,v,t) ->
+      LocalDef ([id],v,t)
+
+  let to_tuple = function
+    | LocalAssum (ids, t) -> ids, None, t
+    | LocalDef (ids, b, t) -> ids, Some b, t
+end
+
+let compact_named_context sigma sign =
+  let module NamedDecl = Context.Named.Declaration in
+  let compact l decl =
+    match decl, l with
+    | NamedDecl.LocalAssum (i,t), [] ->
+       [CompactedDecl.LocalAssum ([i],t)]
+    | NamedDecl.LocalDef (i,c,t), [] ->
+       [CompactedDecl.LocalDef ([i],c,t)]
+    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
+       if EConstr.eq_constr sigma t1 t2
+       then CompactedDecl.LocalAssum (i1::li, t2) :: q
+       else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
+    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
+       if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2
+       then CompactedDecl.LocalDef (i1::li, c2, t2) :: q
+       else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
+    | NamedDecl.LocalAssum (i,t), q ->
+       CompactedDecl.LocalAssum ([i],t) :: q
+    | NamedDecl.LocalDef (i,c,t), q ->
+       CompactedDecl.LocalDef ([i],c,t) :: q
+  in
+  sign |> Context.Named.fold_inside compact ~init:[] |> List.rev
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
@@ -96,3 +96,17 @@ val modular_constr_pr :
   flags:flags ->
   ((unit->Pp.t) -> int option -> entry_relative_level -> constr_expr -> Pp.t) ->
   (unit->Pp.t) -> int option -> entry_relative_level -> constr_expr -> Pp.t
+
+module CompactedDecl : sig
+  type t =
+    | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types
+    | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types
+
+  val of_named_decl : EConstr.named_declaration -> t
+
+  val to_tuple : t ->
+    Id.t EConstr.binder_annot list *
+    EConstr.constr option *
+    EConstr.types
+end
+val compact_named_context : Evd.evar_map -> EConstr.named_context -> CompactedDecl.t list
diff --git a/printing/printer.ml b/printing/printer.ml
@@ -22,7 +22,7 @@ open Declarations
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-module CompactedDecl = Context.Compacted.Declaration
+module CompactedDecl = Ppconstr.CompactedDecl
 
 (* This is set on by proofgeneral proof-tree mode. But may be used for
    other purposes *)
@@ -363,33 +363,28 @@ let get_compact_context,set_compact_context =
   let compact_context = ref false in
   (fun () -> !compact_context),(fun b  -> compact_context := b)
 
-let pr_compacted_decl ?flags env sigma decl =
+let pr_ecompacted_decl ?flags env sigma decl =
   let ids, pbody, typ = match decl with
     | CompactedDecl.LocalAssum (ids, typ) ->
        ids, None, typ
     | CompactedDecl.LocalDef (ids,c,typ) ->
        (* Force evaluation *)
-       let pb = pr_lconstr_env ?flags ~inctx:true env sigma c in
-       let pb = if isCast c then surround pb else pb in
+       let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in
+       let pb = if EConstr.isCast sigma c then surround pb else pb in
        ids, Some pb, typ in
   let pids =
     hov 0 (prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids) in
-  let pt = pr_ltype_env ?flags env sigma typ in
+  let pt = pr_letype_env ?flags env sigma typ in
   match pbody with
   | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt)
   | Some pbody ->
      hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt)
 
-let pr_ecompacted_decl ?flags env sigma (decl:EConstr.compacted_declaration) =
-  let Refl = EConstr.Unsafe.eq in
-  pr_compacted_decl ?flags env sigma decl
-
-let pr_named_decl ?flags env sigma decl =
-  decl |> CompactedDecl.of_named_decl |> pr_compacted_decl ?flags env sigma
+let pr_enamed_decl ?flags env sigma decl =
+  decl |> CompactedDecl.of_named_decl |> pr_ecompacted_decl ?flags env sigma
 
-let pr_enamed_decl ?flags env sigma (decl:EConstr.named_declaration) =
-  let Refl = EConstr.Unsafe.eq in
-  pr_named_decl ?flags env sigma decl
+let pr_named_decl ?flags env sigma (decl:Constr.named_declaration) =
+  pr_enamed_decl ?flags env sigma (EConstr.of_named_decl decl)
 
 let pr_rel_decl ?flags env sigma decl =
   let na = RelDecl.get_name decl in
@@ -441,11 +436,11 @@ let pr_rel_context_of ?flags env sigma =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited ?flags env sigma =
   let sign_env =
-    Context.Compacted.fold
+    List.fold_right
       (fun d pps ->
          let pidt =  pr_ecompacted_decl ?flags env sigma d in
          (pps ++ fnl () ++ pidt))
-      (Termops.compact_named_context sigma (EConstr.named_context env)) ~init:(mt ())
+      (compact_named_context sigma (EConstr.named_context env)) (mt ())
   in
   let db_env =
     fold_rel_context
@@ -496,7 +491,7 @@ and bld_sign_env_id ?flags env sigma ctxt pps is_start =
    spaces between simple hyps, and newline otherwise *)
 let pr_context_limit_compact ?n ?flags env sigma =
   let ctxt = EConstr.named_context env in
-  let ctxt = Termops.compact_named_context sigma ctxt in
+  let ctxt = compact_named_context sigma ctxt in
   let lgth = List.length ctxt in
   let n_capped =
     match n with
diff --git a/printing/printer.mli b/printing/printer.mli
@@ -192,15 +192,13 @@ val pr_ne_context_of : Pp.t -> ?flags:PrintingFlags.t -> env -> evar_map -> Pp.t
 
 val pr_named_decl : ?flags:PrintingFlags.t ->
   env -> evar_map -> Constr.named_declaration -> Pp.t
-val pr_compacted_decl : ?flags:PrintingFlags.t ->
-  env -> evar_map -> Constr.compacted_declaration -> Pp.t
 val pr_rel_decl : ?flags:PrintingFlags.t ->
   env -> evar_map -> Constr.rel_declaration -> Pp.t
 
 val pr_enamed_decl : ?flags:PrintingFlags.t ->
   env -> evar_map -> EConstr.named_declaration -> Pp.t
 val pr_ecompacted_decl : ?flags:PrintingFlags.t ->
-  env -> evar_map -> EConstr.compacted_declaration -> Pp.t
+  env -> evar_map -> Ppconstr.CompactedDecl.t -> Pp.t
 val pr_erel_decl : ?flags:PrintingFlags.t ->
   env -> evar_map -> EConstr.rel_declaration -> Pp.t
 
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
@@ -233,13 +233,6 @@ type goal = { ty: EConstr.t; env : Environ.env; sigma : Evd.evar_map; }
 
 (* XXX: Port to proofview, one day. *)
 (* open Proofview *)
-module CDC = Context.Compacted.Declaration
-
-let to_tuple : EConstr.compacted_declaration -> (Names.Id.t EConstr.binder_annot list * 'pc option * 'pc) =
-  let open CDC in function
-    | LocalAssum(idl, tm)   -> (idl, None, tm)
-    | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm)
-
 let make_goal env sigma g =
   let evi = Evd.find_undefined sigma g in
   let env = Evd.evar_filtered_env env evi in
@@ -297,7 +290,7 @@ let goal_info ~flags goal =
   let map = ref CString.Map.empty in
   let line_idents = ref [] in
   let build_hyp_info env sigma hyp =
-    let (names, body, ty) = to_tuple hyp in
+    let (names, body, ty) = Ppconstr.CompactedDecl.to_tuple hyp in
     let open Pp in
     let idents = List.map (fun x -> Names.Id.to_string x.Context.binder_name) names in
 
@@ -318,7 +311,7 @@ let goal_info ~flags goal =
   try
     let { ty=ty; env=env; sigma } = goal in
     (* compaction is usually desired [eg for better display] *)
-    let hyps = Termops.compact_named_context sigma (EConstr.named_context env) in
+    let hyps = Ppconstr.compact_named_context sigma (EConstr.named_context env) in
     let () = List.iter (build_hyp_info env sigma) (List.rev hyps) in
     let concl_pp = pp_of_type ~flags env sigma ty in
     ( List.rev !line_idents, !map, concl_pp )
