Merge PR #10049: [elaboration] Bidirectionality hints

Ack-by: RalfJung
Reviewed-by: SkySkimmer
Reviewed-by: gares
Ack-by: maximedenes

4 files changed, 82 insertions, 15 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 7c8c2b10ab..5eec8aed1e 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -752,6 +752,7 @@ GRAMMAR EXTEND Gram
         mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
          { let mods = match mods with None -> [] | Some l -> List.flatten l in
          let slash_position = ref None in
+         let ampersand_position = ref None in
          let rec parse_args i = function
            | [] -> []
            | `Id x :: args -> x :: parse_args (i+1) args
@@ -760,10 +761,15 @@ GRAMMAR EXTEND Gram
                 (slash_position := Some i; parse_args i args)
               else
                 user_err Pp.(str "The \"/\" modifier can occur only once")
+           | `Ampersand :: args ->
+             if Option.is_empty !ampersand_position then
+               (ampersand_position := Some i; parse_args i args)
+             else
+               user_err Pp.(str "The \"&\" modifier can occur only once")
          in
          let args = parse_args 0 (List.flatten args) in
          let more_implicits = Option.default [] more_implicits in
-         VernacArguments (qid, args, more_implicits, !slash_position, mods) }
+         VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) }
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
 	   { VernacReserve bl }
@@ -785,6 +791,7 @@ GRAMMAR EXTEND Gram
       | IDENT "default"; IDENT "implicits" -> { [`DefaultImplicits] }
       | IDENT "clear"; IDENT "implicits" -> { [`ClearImplicits] }
       | IDENT "clear"; IDENT "scopes" -> { [`ClearScopes] }
+      | IDENT "clear"; IDENT "bidirectionality"; IDENT "hint" -> { [`ClearBidiHint] }
       | IDENT "rename" -> { [`Rename] }
       | IDENT "assert" -> { [`Assert] }
       | IDENT "extra"; IDENT "scopes" -> { [`ExtraScopes] }
@@ -810,6 +817,7 @@ GRAMMAR EXTEND Gram
              notation_scope=notation_scope;
              implicit_status = NotImplicit}] }
     | "/" -> { [`Slash] }
+    | "&" -> { [`Ampersand] }
     | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 2e97a169cc..e307c0c268 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1047,7 +1047,7 @@ open Pputils
                 | Some Flags.Current -> [SetOnlyParsing]
                 | Some v -> [SetCompatVersion v]))
         )
-      | VernacArguments (q, args, more_implicits, nargs, mods) ->
+      | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) ->
         return (
           hov 2 (
             keyword "Arguments" ++ spc() ++
@@ -1058,22 +1058,23 @@ open Pputils
                 | Impargs.Implicit -> str "[" ++ x ++ str "]"
                 | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
                 | Impargs.NotImplicit -> x in
-              let rec print_arguments n l =
-                match n, l with
-                  | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
-                  | _, [] -> mt()
-                  | n, { name = id; recarg_like = k;
+              let rec print_arguments n nbidi l =
+                match n, nbidi, l with
+                  | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l
+                  | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l
+                  | _, _, [] -> mt()
+                  | n, nbidi, { name = id; recarg_like = k;
                          notation_scope = s;
                          implicit_status = imp } :: tl ->
                     spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
-                      print_arguments (Option.map pred n) tl
+                    print_arguments (Option.map pred n) (Option.map pred nbidi) tl
               in
               let rec print_implicits = function
                 | [] -> mt ()
                 | (name, impl) :: rest ->
                    spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
               in
-              print_arguments nargs args ++
+              print_arguments nargs nargs_before_bidi args ++
                 if not (List.is_empty more_implicits) then
                   prlist (fun l -> str"," ++ print_implicits l) more_implicits
                 else (mt ()) ++
@@ -1086,7 +1087,8 @@ open Pputils
                     | `Assert -> keyword "assert"
                     | `ExtraScopes -> keyword "extra scopes"
                     | `ClearImplicits -> keyword "clear implicits"
-                    | `ClearScopes -> keyword "clear scopes")
+                    | `ClearScopes -> keyword "clear scopes"
+                    | `ClearBidiHint -> keyword "clear bidirectionality hint")
                   mods)
         )
       | VernacReserve bl ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5ae572541e..22427621e6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1204,6 +1204,36 @@ let vernac_syntactic_definition ~module_local lid x y =
   Dumpglob.dump_definition lid false "syndef";
   Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
 
+let cache_bidi_hints (_name, (gr, ohint)) =
+  match ohint with
+  | None -> Pretyping.clear_bidirectionality_hint gr
+  | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs
+
+let load_bidi_hints _ r =
+  cache_bidi_hints r
+
+let subst_bidi_hints (subst, (gr, ohint as orig)) =
+  let gr' = subst_global_reference subst gr in
+  if gr == gr' then orig else (gr', ohint)
+
+let discharge_bidi_hints (_name, (gr, ohint)) =
+  if isVarRef gr && Lib.is_in_section gr then None
+  else
+    let vars = Lib.variable_section_segment_of_reference gr in
+    let n = List.length vars in
+    Some (gr, Option.map ((+) n) ohint)
+
+let inBidiHints =
+  let open Libobject in
+  declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with
+                   load_function = load_bidi_hints;
+                   cache_function = cache_bidi_hints;
+                   classify_function = (fun o -> Substitute o);
+                   subst_function = subst_bidi_hints;
+                   discharge_function = discharge_bidi_hints;
+                 }
+
+
 let warn_arguments_assert =
   CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
          (fun sr ->
@@ -1216,7 +1246,7 @@ let warn_arguments_assert =
 (* [nargs_for_red] is the number of arguments required to trigger reduction,
    [args] is the main list of arguments statuses,
    [more_implicits] is a list of extra lists of implicit statuses  *)
-let vernac_arguments ~section_local reference args more_implicits nargs_for_red flags =
+let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let assert_flag = List.mem `Assert flags in
@@ -1227,6 +1257,7 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   let default_implicits_flag = List.mem `DefaultImplicits flags in
   let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
   let nomatch_flag = List.mem `ReductionDontExposeCase flags in
+  let clear_bidi_hint = List.mem `ClearBidiHint flags in
 
   let err_incompat x y =
     user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
@@ -1285,6 +1316,9 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   if Option.cata (fun n -> n > num_args) false nargs_for_red then
     user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
 
+  if Option.cata (fun n -> n > num_args) false nargs_before_bidi then
+    user_err Pp.(str "The \"&\" modifier should be put before any extra scope.");
+
   let scopes_specified = List.exists Option.has_some scopes in
   
   if scopes_specified && clear_scopes_flag then
@@ -1396,6 +1430,12 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
 
   let red_modifiers_specified = Option.has_some red_behavior in
 
+  let bidi_hint_specified = Option.has_some nargs_before_bidi in
+
+  if bidi_hint_specified && clear_bidi_hint then
+    err_incompat "clear bidirectionality hint" "&";
+
+
   (* Actions *)
 
   if renaming_specified then begin
@@ -1428,10 +1468,26 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
               strbrk "are relevant for constants only.")
   end;
 
+  if bidi_hint_specified then begin
+    let n = Option.get nargs_before_bidi in
+    if section_local then
+      Pretyping.add_bidirectionality_hint sr n
+    else
+      Lib.add_anonymous_leaf (inBidiHints (sr, Some n))
+    end;
+
+  if clear_bidi_hint then begin
+    if section_local then
+      Pretyping.clear_bidirectionality_hint sr
+    else
+      Lib.add_anonymous_leaf (inBidiHints (sr, None))
+  end;
+
  if not (renaming_specified ||
          implicits_specified ||
          scopes_specified ||
-         red_modifiers_specified) && (List.is_empty flags) then
+         red_modifiers_specified ||
+         bidi_hint_specified) && (List.is_empty flags) then
     warn_arguments_assert sr
 
 let default_env () = {
@@ -2437,8 +2493,8 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
   | VernacSyntacticDefinition (id,c,b) ->
     with_module_locality ~atts vernac_syntactic_definition id c b;
     pstate
-  | VernacArguments (qid, args, more_implicits, nargs, flags) ->
-    with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags;
+  | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) ->
+    with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags;
     pstate
   | VernacReserve bl ->
     unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index f946e0596e..df1d08ad0f 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -362,8 +362,9 @@ type nonrec vernac_expr =
       vernac_argument_status list (* Main arguments status list *) *
         (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
       int option (* Number of args to trigger reduction *) *
+      int option (* Number of args before bidirectional typing *) *
         [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename |
-          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes |
+          `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint |
           `DefaultImplicits ] list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of (lident list) option