Merge PR #11164: [CS] allow Let variable to be canonical

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot

2 files changed, 42 insertions, 26 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 35e182840b..4046419bd5 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -19,7 +19,6 @@ open CErrors
 open Util
 open Pp
 open Names
-open Globnames
 open Constr
 open Mod_subst
 open Reductionops
@@ -80,7 +79,7 @@ let subst_structure subst (id, kl, projs as obj) =
      (Option.Smart.map (subst_constant subst))
     projs
   in
-  let id' = subst_constructor subst id in
+  let id' = Globnames.subst_constructor subst id in
   if projs' == projs && id' == id then obj else
     (id',kl,projs')
 
@@ -190,13 +189,13 @@ let rec cs_pattern_of_constr env t =
     let _, params = Inductive.find_rectype env ty in
     Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
-  | _ -> Const_cs (global_of_constr t) , None, []
+  | _ -> Const_cs (Globnames.global_of_constr t) , None, []
 
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
-         (fun (sign,env,t,con,proji_sp) ->
+         (fun (sign,env,t,ref,proji_sp) ->
           let env = Termops.push_rels_assum sign env in
-          let con_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef con) in
+          let con_pp = Nametab.pr_global_env Id.Set.empty ref in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef proji_sp) in
           let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
@@ -204,11 +203,16 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections env ~warn (con,ind) =
-  let o_CTX = Environ.constant_context env con in
-  let u = Univ.make_abstract_instance o_CTX in
-  let o_DEF = mkConstU (con, u) in
-  let c = Environ.constant_value_in env (con,u) in
+let compute_canonical_projections env ~warn (gref,ind) =
+  let o_CTX = Environ.universes_of_global env gref in
+  let o_DEF, c =
+    match gref with
+    | GlobRef.ConstRef con ->
+        let u = Univ.make_abstract_instance o_CTX in
+        mkConstU (con, u), Environ.constant_value_in env (con,u)
+    | GlobRef.VarRef id ->
+        mkVar id, Option.get (Environ.named_body id env)
+    | GlobRef.ConstructRef _ | GlobRef.IndRef _ -> assert false in
   let sign,t = Reductionops.splay_lam env (Evd.from_env env) (EConstr.of_constr c) in
   let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
@@ -230,7 +234,7 @@ let compute_canonical_projections env ~warn (con,ind) =
                { o_ORIGIN = con ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
               :: acc
             | exception Not_found ->
-              if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp);
+              if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
               acc
           ) acc spopt
       else acc
@@ -266,12 +270,17 @@ let register_canonical_structure ~warn env sigma o =
           warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
       )
 
-let subst_canonical_structure subst (cst,ind as obj) =
+type cs = GlobRef.t * inductive
+
+let subst_canonical_structure subst (gref,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
-  let cst' = subst_constant subst cst in
-  let ind' = subst_ind subst ind in
-  if cst' == cst && ind' == ind then obj else (cst',ind')
+  match gref with
+  | GlobRef.ConstRef cst ->
+      let cst' = subst_constant subst cst in
+      let ind' = subst_ind subst ind in
+      if cst' == cst && ind' == ind then obj else (GlobRef.ConstRef cst',ind')
+  | _ -> assert false
 
 (*s High-level declaration of a canonical structure *)
 
@@ -282,15 +291,20 @@ let error_not_structure ref description =
           description))
 
 let check_and_decompose_canonical_structure env sigma ref =
-  let sp =
+  let vc =
     match ref with
-      GlobRef.ConstRef sp -> sp
-    |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
+    | GlobRef.ConstRef sp ->
+        let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
+        begin match Environ.constant_opt_value_in env (sp, u) with
+        | Some vc -> vc
+        | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+    | GlobRef.VarRef id ->
+        begin match Environ.named_body id env with
+        | Some b -> b
+        | None -> error_not_structure ref (str "Could not find its value in the global environment.") end
+    | GlobRef.IndRef _ | GlobRef.ConstructRef _ ->
+        error_not_structure ref (str "Expected an instance of a record or structure.")
   in
-  let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
-  let vc = match Environ.constant_opt_value_in env (sp, u) with
-    | Some vc -> vc
-    | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
   let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
@@ -308,7 +322,7 @@ let check_and_decompose_canonical_structure env sigma ref =
   let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
-  (sp,indsp)
+  (ref,indsp)
 
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (GlobRef.Map.find proj !object_table)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index aaba7cc3e5..7eac0ddf52 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -87,13 +87,15 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
 
 val pr_cs_pattern : cs_pattern -> Pp.t
 
+type cs = GlobRef.t * inductive
+
 val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
 val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
-  Constant.t * inductive -> unit
-val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive
+  cs -> unit
+val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
 
-val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive
+val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> cs