Merge PR #18633: Reduce use of canonical name data in upper layers

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

interp/reserve.ml

@@ -17,16 +17,24 @@ open Names
 open Nameops
 open Notation_term
 open Notation_ops
-open Globnames
 
 type key =
   | RefKey of GlobRef.t
   | Oth
 
 (** TODO: share code from Notation *)
 
+let canonize_key env k = match k with
+| Oth -> Oth
+| RefKey gr ->
+  let gr' = Environ.QGlobRef.canonize env gr in
+  if gr' == gr then k else RefKey gr'
+
+let mkRefKey env gr =
+  RefKey (Environ.QGlobRef.canonize env gr)
+
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.UserOrd.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
@@ -61,26 +69,27 @@ struct
 end
 
 
-let keymap_add key data map =
+let keymap_add env key data map =
+  let key = canonize_key env key in
   let old = try KeyMap.find key map with Not_found -> ReservedSet.empty in
   KeyMap.add key (ReservedSet.add data old) map
 
 let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type"
 let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
 
-let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
-  | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), Some (List.length args)
+let notation_constr_key env = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
+  | NApp (NRef (ref,_),args) -> mkRefKey env ref, Some (List.length args)
   | NList (_,_,NApp (NRef (ref,_),args),_,_)
-  | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
-  | NRef (ref,_) -> RefKey(canonical_gr ref), None
+  | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) -> mkRefKey env ref, Some (List.length args)
+  | NRef (ref,_) -> mkRefKey env ref, None
   | _ -> Oth, None
 
-let add_reserved_type (id,t) =
-  let key = fst (notation_constr_key t) in
+let add_reserved_type env (id,t) =
+  let key = fst (notation_constr_key env t) in
   reserve_table := Id.Map.add id t !reserve_table;
-  reserve_revtable := keymap_add key (id, t) !reserve_revtable
+  reserve_revtable := keymap_add env key (id, t) !reserve_revtable
 
-let declare_reserved_type_binding {CAst.loc;v=id} t =
+let declare_reserved_type_binding env {CAst.loc;v=id} t =
   if not (Id.equal id (root_of_id id)) then
     user_err ?loc
       ((Id.print id ++ str
@@ -90,23 +99,24 @@ let declare_reserved_type_binding {CAst.loc;v=id} t =
     user_err ?loc
     ((Id.print id ++ str " is already bound to a type."))
   with Not_found -> () end;
-  add_reserved_type (id,t)
+  add_reserved_type env (id,t)
 
 let declare_reserved_type idl t =
-  List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl)
+  let env = Global.env () in
+  List.iter (fun id -> declare_reserved_type_binding env id t) (List.rev idl)
 
 let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
 
-let constr_key c =
-  try RefKey (canonical_gr (fst @@ Constr.destRef (fst (Constr.decompose_app c))))
+let constr_key env c =
+  try mkRefKey env (fst @@ Constr.destRef (fst (Constr.decompose_app c)))
   with Constr.DestKO -> Oth
 
 let revert_reserved_type t =
   try
+    let env = Global.env () in
     let t = EConstr.Unsafe.to_constr t in
-    let reserved = KeyMap.find (constr_key t) !reserve_revtable in
+    let reserved = KeyMap.find (constr_key env t) !reserve_revtable in
     let t = EConstr.of_constr t in
-    let env = Global.env () in
     let evd = Evd.from_env env in
     let t = Detyping.detype Detyping.Now Id.Set.empty env evd t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]

kernel/environ.ml

@@ -855,6 +855,7 @@ sig
   val equal : env -> t -> t -> bool
   val compare : env -> t -> t -> int
   val hash : env -> t -> int
+  val canonize : env -> t -> t
 end
 
 module QConstant =
@@ -863,6 +864,7 @@ struct
   let equal _env c1 c2 = Constant.CanOrd.equal c1 c2
   let compare _env c1 c2 = Constant.CanOrd.compare c1 c2
   let hash _env c = Constant.CanOrd.hash c
+  let canonize _env c = Constant.canonize c
 end
 
 module QMutInd =
@@ -871,6 +873,7 @@ struct
   let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2
   let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2
   let hash _env c = MutInd.CanOrd.hash c
+  let canonize _env c = MutInd.canonize c
 end
 
 module QInd =
@@ -879,6 +882,7 @@ struct
   let equal _env c1 c2 = Ind.CanOrd.equal c1 c2
   let compare _env c1 c2 = Ind.CanOrd.compare c1 c2
   let hash _env c = Ind.CanOrd.hash c
+  let canonize _env c = Ind.canonize c
 end
 
 module QConstruct =
@@ -887,6 +891,7 @@ struct
   let equal _env c1 c2 = Construct.CanOrd.equal c1 c2
   let compare _env c1 c2 = Construct.CanOrd.compare c1 c2
   let hash _env c = Construct.CanOrd.hash c
+  let canonize _env c = Construct.canonize c
 end
 
 module QProjection =
@@ -895,12 +900,14 @@ struct
   let equal _env c1 c2 = Projection.CanOrd.equal c1 c2
   let compare _env c1 c2 = Projection.CanOrd.compare c1 c2
   let hash _env c = Projection.CanOrd.hash c
+  let canonize _env c = Projection.canonize c
   module Repr =
   struct
     type t = Projection.Repr.t
     let equal _env c1 c2 = Projection.Repr.CanOrd.equal c1 c2
     let compare _env c1 c2 = Projection.Repr.CanOrd.compare c1 c2
     let hash _env c = Projection.Repr.CanOrd.hash c
+    let canonize _env c = Projection.Repr.canonize c
   end
 end
 
@@ -910,4 +917,5 @@ struct
   let equal _env c1 c2 = GlobRef.CanOrd.equal c1 c2
   let compare _env c1 c2 = GlobRef.CanOrd.compare c1 c2
   let hash _env c = GlobRef.CanOrd.hash c
+  let canonize _env c = GlobRef.canonize c
 end

kernel/environ.mli

@@ -287,6 +287,7 @@ sig
   val equal : env -> t -> t -> bool
   val compare : env -> t -> t -> int
   val hash : env -> t -> int
+  val canonize : env -> t -> t
 end
 
 module QConstant : QNameS with type t = Constant.t

kernel/names.ml

@@ -454,6 +454,7 @@ sig
   module CanOrd : EqType with type t = t
   module UserOrd : EqType with type t = t
   module SyntacticOrd : EqType with type t = t
+  val canonize : t -> t
 end
 
 (** For constant and inductive names, we use a kernel name couple (kn1,kn2)
@@ -490,6 +491,10 @@ module KerPair = struct
     | Same kn -> kn
     | Dual (kn,_) -> kn
 
+  let canonize kp = match kp with
+  | Same _ -> kp
+  | Dual (_, kn) -> Same kn
+
   let same kn = Same kn
   let make knu knc = if KerName.equal knu knc then Same knc else Dual (knu,knc)
 
@@ -656,6 +661,10 @@ struct
       Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
   end
 
+  let canonize ((mind, i) as ind) =
+    let mind' = MutInd.canonize mind in
+    if mind' == mind then ind else (mind', i)
+
 end
 
 module Construct =
@@ -702,6 +711,10 @@ struct
       Hashset.Combine.combine (Ind.SyntacticOrd.hash ind) (Int.hash i)
   end
 
+  let canonize ((ind, i) as cstr) =
+    let ind' = Ind.canonize ind in
+    if ind' == ind then cstr else (ind', i)
+
 end
 
 (** Designation of a (particular) inductive type. *)
@@ -876,6 +889,13 @@ struct
     let equal = CanOrd.equal
     let compare = CanOrd.compare
 
+    let canonize p =
+      let { proj_ind; proj_npars; proj_arg; proj_name } = p in
+      let proj_ind' = Ind.canonize proj_ind in
+      let proj_name' = Constant.canonize proj_name in
+      if proj_ind' == proj_ind && proj_name' == proj_name then p
+      else { proj_ind = proj_ind'; proj_name = proj_name'; proj_npars; proj_arg }
+
     module Self_Hashcons = struct
       type nonrec t = t
       type u = (inductive -> inductive) * (Constant.t -> Constant.t)
@@ -962,6 +982,10 @@ struct
       let hash = hash
     end
 
+  let canonize ((r, u) as p) =
+    let r' = Repr.canonize r in
+    if r' == r then p else (r',  u)
+
   module HashProjection = Hashcons.Make(Self_Hashcons)
 
   let hcons = Hashcons.simple_hcons HashProjection.generate HashProjection.hcons Repr.hcons
@@ -1078,6 +1102,18 @@ module GlobRef = struct
     let hash gr = GlobRefInternal.global_hash_gen Constant.SyntacticOrd.hash Ind.SyntacticOrd.hash Construct.SyntacticOrd.hash gr
   end
 
+  let canonize gr = match gr with
+  | VarRef _ -> gr
+  | ConstRef c ->
+    let c' = Constant.canonize c in
+    if c' == c then gr else ConstRef c'
+  | IndRef ind ->
+    let ind' = Ind.canonize ind in
+    if ind' == ind then gr else IndRef ind'
+  | ConstructRef c ->
+    let c' = Construct.canonize c in
+    if c' == c then gr else ConstructRef c'
+
   let is_bound = function
   | VarRef _ -> false
   | ConstRef cst -> ModPath.is_bound (Constant.modpath cst)

kernel/names.mli

@@ -365,6 +365,9 @@ sig
 
   module SyntacticOrd : EqType with type t = t
   (** Equality functions using both names, for low-level uses. *)
+
+  val canonize : t -> t
+  (** Returns the canonical version of the name *)
 end
 
 (** {6 Constant Names } *)

library/coqlib.ml

@@ -42,7 +42,7 @@ let has_ref s = CString.Map.mem s !table
 
 let check_ind_ref s ind =
   match CString.Map.find s !table with
-  | GlobRef.IndRef r -> Ind.CanOrd.equal r ind
+  | GlobRef.IndRef r -> Ind.UserOrd.equal r ind
   | _ -> false
   | exception Not_found -> false
 

plugins/btauto/refl_btauto.ml

@@ -93,7 +93,7 @@ module Bool = struct
   | Negb of t
   | Ifb of t * t * t
 
-  let quote (env : Env.t) sigma (c : Constr.t) : t =
+  let quote (env : Env.t) genv sigma (c : Constr.t) : t =
     let trueb = Lazy.force trueb in
     let falseb = Lazy.force falseb in
     let andb = Lazy.force andb in
@@ -115,7 +115,7 @@ module Bool = struct
     | Case (info, _, _, _, _, arg, pats) ->
       let is_bool =
         let i = info.ci_ind in
-        Names.Ind.CanOrd.equal i (Lazy.force ind)
+        Environ.QInd.equal genv i (Lazy.force ind)
       in
       if is_bool then
         Ifb ((aux arg), (aux (snd pats.(0))), (aux (snd pats.(1))))
@@ -239,8 +239,8 @@ module Btauto = struct
       | App (c, [|typ; tl; tr|])
           when typ === bool && c === eq ->
           let env = Env.empty () in
-          let fl = Bool.quote env sigma tl in
-          let fr = Bool.quote env sigma tr in
+          let fl = Bool.quote env (Tacmach.pf_env gl) sigma tl in
+          let fr = Bool.quote env (Tacmach.pf_env gl) sigma tr in
           let env = Env.to_list env in
           let fl = reify env fl in
           let fr = reify env fr in

plugins/cc/ccalgo.ml

@@ -139,7 +139,7 @@ sig
   val mkProduct : (Sorts.t * Sorts.t) -> t
   val mkEps : Id.t -> t
   val mkAppli : (t * t) -> t
-  val mkConstructor : cinfo -> t
+  val mkConstructor : Environ.env -> cinfo -> t
 
   val equal : t -> t -> bool
   val constr : t -> constr
@@ -162,7 +162,7 @@ struct
       | Appli (t1', u1'), Appli (t2', u2') -> term_equal t1'.term t2'.term && term_equal u1'.term u2'.term
       | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1},
         Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} ->
-          Int.equal i1 i2 && Int.equal j1 j2 && Construct.CanOrd.equal c1 c2 (* FIXME check eq? *)
+          Int.equal i1 i2 && Int.equal j1 j2 && Construct.UserOrd.equal c1 c2
       | _ -> false
 
   let equal t1 t2 = term_equal t1.term t2.term
@@ -175,7 +175,7 @@ struct
     | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
     | Eps i -> combine 3 (Id.hash i)
     | Appli (t1', t2') -> combine3 4 (t1'.hash) (t2'.hash)
-    | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (Construct.CanOrd.hash c) i j
+    | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (Construct.UserOrd.hash c) i j
 
   let hash t = t.hash
 
@@ -223,7 +223,10 @@ struct
 
   let mkAppli (t1', t2') = make (Appli (t1', t2'))
 
-  let mkConstructor info = make (Constructor info)
+  let mkConstructor env info =
+    let canon i = Environ.QConstruct.canonize env i in
+    let info = { info with ci_constr = on_fst canon info.ci_constr } in
+    make (Constructor info)
 
   let rec nth_arg t n =
     match t.term with

plugins/cc/ccalgo.mli

@@ -29,7 +29,7 @@ sig
   val mkSymb : constr -> t
   val mkProduct : (Sorts.t * Sorts.t) -> t
   val mkAppli : (t * t) -> t
-  val mkConstructor : cinfo -> t
+  val mkConstructor : Environ.env -> cinfo -> t
   val constr : t -> constr
   val nth_arg : t -> int -> t
 end

plugins/cc/cctac.ml

@@ -64,14 +64,11 @@ let rec decompose_term env sigma t =
         ATerm.mkAppli (ATerm.mkAppli (ATerm.mkProduct (sort_a,sort_b),
                     decompose_term env sigma a),
               decompose_term env sigma b)
-    | Construct c ->
-        let (((mind,i_ind),i_con),u)= c in
+    | Construct ((ind, _ as cstr), u) ->
         let u = EInstance.kind sigma u in
-        let canon_mind = MutInd.make1 (MutInd.canonical mind) in
-        let canon_ind = canon_mind,i_ind in
-        let (oib,_)=Global.lookup_inductive (canon_ind) in
-        let nargs=constructor_nallargs env (canon_ind,i_con) in
-          ATerm.mkConstructor {ci_constr= ((canon_ind,i_con),u);
+        let oib = Environ.lookup_mind (fst ind) env in
+        let nargs = constructor_nallargs env cstr in
+        ATerm.mkConstructor env {ci_constr = (cstr, u);
                        ci_arity=nargs;
                        ci_nhyps=nargs-oib.mind_nparams}
     | Ind c ->

plugins/firstorder/formula.ml

@@ -217,6 +217,9 @@ type _ identifier =
 | GoalId : [ `Goal ] identifier
 | FormulaId : GlobRef.t -> [ `Hyp ] identifier
 
+let goal_id = GoalId
+let formula_id env gr = FormulaId (Environ.QGlobRef.canonize env gr)
+
 type _ pattern =
 | LeftPattern : left_pattern -> [ `Hyp ] pattern
 | RightPattern : right_pattern -> [ `Goal ] pattern

plugins/firstorder/formula.mli

@@ -67,10 +67,13 @@ type left_pattern=
   | Lexists of pinductive
   | LA of constr*left_arrow_pattern
 
-type _ identifier =
+type _ identifier = private
 | GoalId : [ `Goal ] identifier
 | FormulaId : GlobRef.t -> [ `Hyp ] identifier
 
+val goal_id : [ `Goal ] identifier
+val formula_id : Environ.env -> GlobRef.t -> [ `Hyp ] identifier
+
 type _ pattern =
 | LeftPattern : left_pattern -> [ `Hyp ] pattern
 | RightPattern : right_pattern -> [ `Goal ] pattern