Move the rewrite implementation out of Ltac.

ppedrot · ppedrot · commit 8e7fa4686ad6 · 2022-03-14T19:47:48.000+01:00
It had nothing to do there, actually. Because of dependency chains, the
module was split into two, one defining the setoid_rewrite tactic and its
variants, in tactics, and the other one defining the related vernacular
commands in vernac/.
diff --git a/plugins/ltac/comRewrite.ml b/plugins/ltac/comRewrite.ml
@@ -0,0 +1,258 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Names
+open Nameops
+open Constr
+open Constrexpr
+open EConstr
+open Libnames
+
+let () = CErrors.register_handler begin function
+| Rewrite.RewriteFailure (env, sigma, e) ->
+  let e = Himsg.explain_pretype_error env sigma e in
+  Some Pp.(str"setoid rewrite failed: " ++ e)
+| _ -> None
+end
+
+module TC = Typeclasses
+
+let classes_dirpath =
+  Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"])
+
+let init_setoid () =
+  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
+  else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
+
+type rewrite_attributes = { polymorphic : bool; global : bool }
+
+let rewrite_attributes =
+  let open Attributes.Notations in
+  Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
+  let global = not (Locality.make_section_locality locality) in
+  Attributes.Notations.return { polymorphic; global }
+
+(** Utility functions *)
+
+let find_reference dir s =
+  Coqlib.find_reference "generalized rewriting" dir s
+[@@warning "-3"]
+
+let lazy_find_reference dir s =
+  let gr = lazy (find_reference dir s) in
+  fun () -> Lazy.force gr
+
+module PropGlobal = struct
+
+  let morphisms = ["Coq"; "Classes"; "Morphisms"]
+
+  let respectful_ref = lazy_find_reference morphisms "respectful"
+
+  let proper_class =
+    let r = lazy (find_reference morphisms "Proper") in
+    fun env sigma -> TC.class_info env sigma (Lazy.force r)
+
+  let proper_proj env sigma =
+    mkConst (Option.get (List.hd (proper_class env sigma).TC.cl_projs).TC.meth_const)
+
+
+end
+
+(* By default the strategy for "rewrite_db" is top-down *)
+
+let mkappc s l = CAst.make @@ CAppExpl ((qualid_of_ident (Id.of_string s),None),l)
+
+let declare_an_instance n s args =
+  (((CAst.make @@ Name n),None),
+   CAst.make @@ CAppExpl ((qualid_of_string s,None), args))
+
+let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
+
+let get_locality b = if b then Hints.SuperGlobal else Hints.Local
+
+let anew_instance atts binders (name,t) fields =
+  let locality = get_locality atts.global in
+  let _id = Classes.new_instance ~poly:atts.polymorphic
+      name binders t (true, CAst.make @@ CRecord (fields))
+      ~locality Hints.empty_hint_info
+  in
+  ()
+
+let declare_instance_refl atts binders a aeq n lemma =
+  let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
+  in anew_instance atts binders instance
+       [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
+
+let declare_instance_sym atts binders a aeq n lemma =
+  let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
+  in anew_instance atts binders instance
+       [(qualid_of_ident (Id.of_string "symmetry"),lemma)]
+
+let declare_instance_trans atts binders a aeq n lemma =
+  let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
+  in anew_instance atts binders instance
+       [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
+
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
+  init_setoid ();
+  let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
+  let () = anew_instance atts binders instance [] in
+  match (refl,symm,trans) with
+    (None, None, None) -> ()
+  | (Some lemma1, None, None) ->
+    declare_instance_refl atts binders a aeq n lemma1
+  | (None, Some lemma2, None) ->
+    declare_instance_sym atts binders a aeq n lemma2
+  | (None, None, Some lemma3) ->
+    declare_instance_trans atts binders a aeq n lemma3
+  | (Some lemma1, Some lemma2, None) ->
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    declare_instance_sym atts binders a aeq n lemma2
+  | (Some lemma1, None, Some lemma3) ->
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
+    anew_instance atts binders instance
+      [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
+       (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
+  | (None, Some lemma2, Some lemma3) ->
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
+    anew_instance atts binders instance
+      [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
+       (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
+  | (Some lemma1, Some lemma2, Some lemma3) ->
+    let () = declare_instance_refl atts binders a aeq n lemma1 in
+    let () = declare_instance_sym atts binders a aeq n lemma2 in
+    let () = declare_instance_trans atts binders a aeq n lemma3 in
+    let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
+    anew_instance atts binders instance
+      [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
+       (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
+       (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
+
+let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
+
+let proper_projection env sigma r ty =
+  let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
+  let ctx, inst = decompose_prod_assum sigma ty in
+  let mor, args = destApp sigma inst in
+  let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
+  let app = mkApp (PropGlobal.proper_proj env sigma,
+                  Array.append args [| instarg |]) in
+    it_mkLambda_or_LetIn app ctx
+
+let declare_projection name instance_id r =
+  let env = Global.env () in
+  let poly = Environ.is_polymorphic env r in
+  let sigma = Evd.from_env env in
+  let sigma,c = Evd.fresh_global env sigma r in
+  let ty = Retyping.get_type_of env sigma c in
+  let body = proper_projection env sigma c ty in
+  let sigma, typ = Typing.type_of env sigma body in
+  let ctx, typ = decompose_prod_assum sigma typ in
+  let typ =
+    let n =
+      let rec aux t =
+        match EConstr.kind sigma t with
+        | App (f, [| a ; a' ; rel; rel' |])
+            when isRefX sigma (PropGlobal.respectful_ref ()) f ->
+          succ (aux rel')
+        | _ -> 0
+      in
+      let init =
+        match EConstr.kind sigma typ with
+            App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f  ->
+              mkApp (f, fst (Array.chop (Array.length args - 2) args))
+          | _ -> typ
+      in aux init
+    in
+    let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
+    in it_mkProd_or_LetIn ccl ctx
+  in
+  let types = Some (it_mkProd_or_LetIn typ ctx) in
+  let kind = Decls.(IsDefinition Definition) in
+  let impargs, udecl = [], UState.default_univ_decl in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let info = Declare.Info.make ~kind ~udecl ~poly () in
+  let _r : GlobRef.t =
+    Declare.declare_definition ~cinfo ~info ~opaque:false ~body sigma
+  in ()
+
+let add_setoid atts binders a aeq t n =
+  init_setoid ();
+  let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
+  in
+  anew_instance atts binders instance
+    [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+     (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+     (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
+
+let add_morphism_as_parameter atts m n : unit =
+  init_setoid ();
+  let instance_id = add_suffix n "_Proper" in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let poly = atts.polymorphic in
+  let kind = Decls.(IsAssumption Logical) in
+  let impargs, udecl = [], UState.default_univ_decl in
+  let evd, types = Rewrite.Internal.build_morphism_signature env evd m in
+  let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
+  let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
+  let cst = GlobRef.ConstRef cst in
+  Classes.Internal.add_instance
+    (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst;
+  declare_projection n instance_id cst
+
+let add_morphism_interactive atts ~tactic m n : Declare.Proof.t =
+  init_setoid ();
+  let instance_id = add_suffix n "_Proper" in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let evd, morph = Rewrite.Internal.build_morphism_signature env evd m in
+  let poly = atts.polymorphic in
+  let kind = Decls.(IsDefinition Instance) in
+  let hook { Declare.Hook.S.dref; _ } = dref |> function
+    | GlobRef.ConstRef cst ->
+      Classes.Internal.add_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info
+        atts.global (GlobRef.ConstRef cst);
+      declare_projection n instance_id (GlobRef.ConstRef cst)
+    | _ -> assert false
+  in
+  let hook = Declare.Hook.make hook in
+  Flags.silently
+    (fun () ->
+       let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in
+       let info = Declare.Info.make ~poly ~hook ~kind () in
+       let lemma = Declare.Proof.start ~cinfo ~info evd in
+       fst (Declare.Proof.by tactic lemma)) ()
+
+let add_morphism atts ~tactic binders m s n =
+  init_setoid ();
+  let instance_id = add_suffix n "_Proper" in
+  let instance_name = (CAst.make @@ Name instance_id),None in
+  let instance_t =
+    CAst.make @@ CAppExpl
+      ((Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
+       [cHole; s; m])
+  in
+  let locality = get_locality atts.global in
+  let _id, lemma = Classes.new_instance_interactive
+      ~locality ~poly:atts.polymorphic
+      instance_name binders instance_t
+      ~tac:tactic ~hook:(declare_projection n instance_id)
+      Hints.empty_hint_info None
+  in
+  lemma (* no instance body -> always open proof *)
diff --git a/plugins/ltac/comRewrite.mli b/plugins/ltac/comRewrite.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Constrexpr
+
+type rewrite_attributes
+val rewrite_attributes : rewrite_attributes Attributes.attribute
+
+val declare_relation
+  : rewrite_attributes
+  -> ?binders:local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> constr_expr option
+  -> constr_expr option
+  -> constr_expr option
+  -> unit
+
+val add_setoid
+  : rewrite_attributes
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> unit
+
+val add_morphism_interactive : rewrite_attributes ->
+  tactic:unit Proofview.tactic -> constr_expr -> Id.t -> Declare.Proof.t
+val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
+
+val add_morphism
+  :  rewrite_attributes
+  -> tactic:unit Proofview.tactic
+  -> local_binder_expr list
+  -> constr_expr
+  -> constr_expr
+  -> Id.t
+  -> Declare.Proof.t
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
@@ -20,6 +20,7 @@ open Genintern
 open Geninterp
 open Extraargs
 open Rewrite
+open ComRewrite
 open Stdarg
 open Tactypes
 open Pcoq.Prim
@@ -280,6 +281,13 @@ END
 let add_setoid atts binders a aeq t n =
   add_setoid atts binders a aeq t n.CAst.v
 
+let morphism_tactic =
+  let open Tacexpr in
+  let name = "Coq.Classes.SetoidTactics.add_morphism_tactic" in
+  let tacqid = Libnames.qualid_of_string name in
+  let tac = CAst.make @@ TacArg (TacCall (CAst.make (tacqid, []))) in
+  Tacinterp.interp tac
+
 }
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
@@ -295,17 +303,17 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
     => { VtStartProof(GuaranteesOpacity, [n.CAst.v]) }
     -> { if Lib.is_modtype () then
            CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
-         add_morphism_interactive atts m n.CAst.v }
+         add_morphism_interactive atts ~tactic:morphism_tactic m n.CAst.v }
   | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" identref(n) ]
     => { VtSideff([n.CAst.v], VtLater) }
     -> { add_morphism_as_parameter atts m n.CAst.v }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" identref(n) ]
     => { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
-    -> { add_morphism atts [] m s n.CAst.v }
+    -> { add_morphism atts ~tactic:morphism_tactic [] m s n.CAst.v }
   | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" identref(n) ]
     => { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
-    -> { add_morphism atts binders m s n.CAst.v }
+    -> { add_morphism atts ~tactic:morphism_tactic binders m s n.CAst.v }
 END
 
 TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
@@ -430,18 +430,18 @@ let ring_equality env sigma (r,add,mul,opp,req) =
         let sigma, setoid = setoid_of_relation env sigma r req in
         let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
         let add_m, add_m_lem =
-          try Rewrite.default_morphism signature add
+          try Rewrite.Internal.default_morphism env sigma signature add
           with Not_found ->
             CErrors.user_err (str "Ring addition " ++ pr_econstr_env env sigma add ++ str " should be declared as a morphism.") in
         let mul_m, mul_m_lem =
-          try Rewrite.default_morphism signature mul
+          try Rewrite.Internal.default_morphism env sigma signature mul
           with Not_found ->
             CErrors.user_err (str "Ring multiplication " ++ pr_econstr_env env sigma mul ++ str " should be declared as a morphism.") in
         let op_morph =
           match opp with
             | Some opp ->
                 (let opp_m,opp_m_lem =
-                  try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp
+                  try Rewrite.Internal.default_morphism env sigma ([Some(r,Some req)],Some(r,Some req)) opp
                   with Not_found ->
                     CErrors.user_err (str "Ring opposite " ++ pr_econstr_env env sigma opp ++ str " should be declared as a morphism.") in
                 let op_morph =
@@ -854,7 +854,7 @@ let field_equality env sigma r inv req =
         let _setoid = setoid_of_relation env sigma r req in
         let signature = [Some (r,Some req)],Some(r,Some req) in
         let inv_m, inv_m_lem =
-          try Rewrite.default_morphism signature inv
+          try Rewrite.Internal.default_morphism env sigma signature inv
           with Not_found ->
             error "field inverse should be declared as a morphism" in
           inv_m_lem
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
