rewrite: attributes handle is_univ_poly, is_program_mode

3 files changed, 78 insertions, 70 deletions

diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 7880587366..6a8368d863 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -26,7 +26,6 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
-open Attributes
 
 let wit_hyp = wit_var
 
@@ -183,34 +182,34 @@ END
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) (Some lemma2) None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) (Some lemma2) None }
 
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) None None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) None None }
   | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
-      { declare_relation a aeq n None None None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
   | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
-      { declare_relation a aeq n None (Some lemma2) None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None (Some lemma2) None }
   | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      { declare_relation a aeq n None (Some lemma2) (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) None (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) None (Some lemma3) }
   | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
   | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
-      { declare_relation a aeq n None None (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None None (Some lemma3) }
 END
 
 {
@@ -240,61 +239,61 @@ VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) None None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) None None }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None None None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None (Some lemma2) None }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None (Some lemma2) None }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
   | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None None (Some lemma3) }
+      { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None None (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
   | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
-         add_setoid (not (Locality.make_section_locality (only_locality atts))) [] a aeq t n;
+         add_setoid (Attributes.parse rewrite_attributes atts) [] a aeq t n;
      }
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
-         add_setoid (not (Locality.make_section_locality (only_locality atts))) binders a aeq t n;
+         add_setoid (Attributes.parse rewrite_attributes atts) binders a aeq t n;
      }
   | [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
     -> {
-           add_morphism_infer (not (Locality.make_section_locality (only_locality atts))) m n;
+           add_morphism_infer (Attributes.parse rewrite_attributes atts) m n;
        }
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
     -> {
-           add_morphism (not (Locality.make_section_locality (only_locality atts))) [] m s n;
+           add_morphism (Attributes.parse rewrite_attributes atts) [] m s n;
        }
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
     -> {
-           add_morphism (not (Locality.make_section_locality (only_locality atts))) binders m s n;
+           add_morphism (Attributes.parse rewrite_attributes atts) binders m s n;
        }
 END
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8b2721ae4e..740e955049 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -43,6 +43,16 @@ module NamedDecl = Context.Named.Declaration
 
 (** Typeclass-based generalized rewriting. *)
 
+type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
+
+let rewrite_attributes =
+  let open Attributes.Notations in
+  Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
+  let polymorphic = Option.default (Flags.is_universe_polymorphism()) polymorphic in
+  let program = Option.default (Flags.is_program_mode ()) program in
+  let global = not (Locality.make_section_locality locality) in
+  Attributes.Notations.return { polymorphic; program; global }
+
 (** Constants used by the tactic. *)
 
 let classes_dirpath =
@@ -1776,67 +1786,65 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance global binders instance fields =
-  let program_mode = Flags.is_program_mode () in
-  let poly = Flags.is_universe_polymorphism () in
-  new_instance ~program_mode poly
+let anew_instance atts binders instance fields =
+  let program_mode = atts.program in
+  new_instance ~program_mode atts.polymorphic
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
-    ~global ~generalize:false ~refine:false Hints.empty_hint_info
+    ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
 
-let declare_instance_refl global binders a aeq n lemma =
+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 global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
-let declare_instance_sym global binders a aeq n 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 global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "symmetry"),lemma)]
 
-let declare_instance_trans global binders a aeq n 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 global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
-  let global = not (Locality.make_section_locality locality) in
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
-  in ignore(anew_instance global binders instance []);
+  in ignore(anew_instance atts binders instance []);
   match (refl,symm,trans) with
       (None, None, None) -> ()
     | (Some lemma1, None, None) ->
-	ignore (declare_instance_refl global binders a aeq n lemma1)
+        ignore (declare_instance_refl atts binders a aeq n lemma1)
     | (None, Some lemma2, None) ->
-	ignore (declare_instance_sym global binders a aeq n lemma2)
+        ignore (declare_instance_sym atts binders a aeq n lemma2)
     | (None, None, Some lemma3) ->
-	ignore (declare_instance_trans global binders a aeq n lemma3)
+        ignore (declare_instance_trans atts binders a aeq n lemma3)
     | (Some lemma1, Some lemma2, None) ->
-	ignore (declare_instance_refl global binders a aeq n lemma1);
-	ignore (declare_instance_sym global binders a aeq n lemma2)
+        ignore (declare_instance_refl atts binders a aeq n lemma1);
+        ignore (declare_instance_sym atts binders a aeq n lemma2)
     | (Some lemma1, None, Some lemma3) ->
-	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
-	    anew_instance global binders instance
+            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 _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
-	    anew_instance global binders instance
+            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 _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
-	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
-	  anew_instance global binders instance
+          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)])
@@ -1935,15 +1943,15 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid global binders a aeq t n =
+let add_setoid atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let _lemma_trans = declare_instance_trans global binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let _lemma_trans = 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 ignore(
-    anew_instance global binders instance
+    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])])
@@ -1958,26 +1966,26 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer glob m n =
+let add_morphism_infer atts m n =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
+  (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
-      let uctx = UState.const_univ_entry ~poly uctx in
+      let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
                                  (None,(instance,uctx),None),
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
+                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
-      let kind = Decl_kinds.Global, poly, 
+      let kind = Decl_kinds.Global, atts.polymorphic,
 	Decl_kinds.DefinitionBody Decl_kinds.Instance 
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1985,7 +1993,7 @@ let add_morphism_infer glob m n =
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
-                          glob (ConstRef cst));
+                          atts.global (ConstRef cst));
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
@@ -1995,9 +2003,8 @@ let add_morphism_infer glob m n =
 	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
-let add_morphism glob binders m s n =
+let add_morphism atts binders m s n =
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
@@ -2006,8 +2013,7 @@ let add_morphism glob binders m s n =
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let program_mode = Flags.is_program_mode () in
-  ignore(new_instance ~program_mode ~global:glob poly binders instance
+  ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
            (Some (true, CAst.make @@ CRecord []))
     ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 0d014a0bf3..4f46e78c71 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -19,6 +19,9 @@ open Tacinterp
 
 (** TODO: document and clean me! *)
 
+type rewrite_attributes
+val rewrite_attributes : rewrite_attributes Attributes.attribute
+
 type unary_strategy = 
     Subterms | Subterm | Innermost | Outermost
   | Bottomup | Topdown | Progress | Try | Any | Repeat
@@ -77,18 +80,18 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : ?locality:bool ->
+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 :
-  bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> unit
 
-val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism :
-  bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr