Add a type of format strings to Ltac2.

It provides an abstract type of well-typed format strings, a scope to parse
them and a minimal printf-like API.

9 files changed, 258 insertions, 0 deletions

diff --git a/user-contrib/Ltac2/Init.v b/user-contrib/Ltac2/Init.v
index a4f6d497df..097a0ca25f 100644
--- a/user-contrib/Ltac2/Init.v
+++ b/user-contrib/Ltac2/Init.v
@@ -35,6 +35,7 @@ Ltac2 Type preterm.
 Ltac2 Type binder.
 
 Ltac2 Type message.
+Ltac2 Type ('a, 'b, 'c, 'd) format.
 Ltac2 Type exn := [ .. ].
 Ltac2 Type 'a array.
 
diff --git a/user-contrib/Ltac2/Ltac2.v b/user-contrib/Ltac2/Ltac2.v
index d3bf3c10ea..ccfc7e4a70 100644
--- a/user-contrib/Ltac2/Ltac2.v
+++ b/user-contrib/Ltac2/Ltac2.v
@@ -22,5 +22,6 @@ Require Ltac2.Fresh.
 Require Ltac2.Pattern.
 Require Ltac2.Std.
 Require Ltac2.Env.
+Require Ltac2.Printf.
 Require Ltac2.Ltac1.
 Require Export Ltac2.Notations.
diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v
index 4a4d1d815c..39d39562cf 100644
--- a/user-contrib/Ltac2/Message.v
+++ b/user-contrib/Ltac2/Message.v
@@ -25,3 +25,32 @@ Ltac2 @ external of_exn : exn -> message := "ltac2" "message_of_exn".
 (** Panics if there is more than one goal under focus. *)
 
 Ltac2 @ external concat : message -> message -> message := "ltac2" "message_concat".
+
+Module Format.
+
+(** Only for internal use. *)
+
+Ltac2 @ external stop : unit -> ('a, 'b, 'c, 'a) format := "ltac2" "format_stop".
+
+Ltac2 @ external string : ('a, 'b, 'c, 'd) format ->
+  (string -> 'a, 'b, 'c, 'd) format := "ltac2" "format_string".
+
+Ltac2 @ external int : ('a, 'b, 'c, 'd) format ->
+  (int -> 'a, 'b, 'c, 'd) format := "ltac2" "format_int".
+
+Ltac2 @ external constr : ('a, 'b, 'c, 'd) format ->
+  (constr -> 'a, 'b, 'c, 'd) format := "ltac2" "format_constr".
+
+Ltac2 @ external ident : ('a, 'b, 'c, 'd) format ->
+  (ident -> 'a, 'b, 'c, 'd) format := "ltac2" "format_ident".
+
+Ltac2 @ external literal : string -> ('a, 'b, 'c, 'd) format ->
+  ('a, 'b, 'c, 'd) format := "ltac2" "format_literal".
+
+Ltac2 @ external alpha : ('a, 'b, 'c, 'd) format ->
+  (('b -> 'r -> 'c) -> 'r -> 'a, 'b, 'c, 'd) format := "ltac2" "format_alpha".
+
+Ltac2 @ external kfprintf : (message -> 'r) -> ('a, unit, message, 'r) format -> 'a :=
+  "ltac2" "format_kfprintf".
+
+End Format.
diff --git a/user-contrib/Ltac2/Printf.v b/user-contrib/Ltac2/Printf.v
new file mode 100644
index 0000000000..e2470ed1c3
--- /dev/null
+++ b/user-contrib/Ltac2/Printf.v
@@ -0,0 +1,56 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+Require Import Ltac2.Message.
+
+(** This file defines a printf notation for easiness of writing messages *)
+
+(**
+
+  The built-in "format" notation scope can be used to create well-typed variadic
+  printing commands following a printf-like syntax. The "format" scope parses
+  quoted strings which contain either raw string data or printing
+  specifications. Raw strings will be output verbatim as if they were passed
+  to Ltac2.Message.of_string.
+
+  Printing specifications are of the form
+
+  << '%' type >>
+
+  where the type value defines which kind of arguments will be accepted and
+  how they will be printed. They can take the following values.
+
+  - << i >>: takes an argument of type int and behaves as Message.of_int
+  - << I >>: takes an argument of type ident and behaves as Message.of_ident
+  - << s >>: takes an argument of type string and behaves as Message.of_string
+  - << t >>: takes an argument of type constr and behaves as Message.of_constr
+  - << a >>: takes two arguments << f >> of type << (unit -> 'a -> message) >>
+             and << x >> of type << 'a >> and behaves as << f () x >>
+  - << % >>: outputs << % >> verbatim
+
+  TODO: add printing modifiers.
+
+*)
+
+Ltac2 printf fmt := Format.kfprintf print fmt.
+Ltac2 fprintf fmt := Format.kfprintf (fun x => x) fmt.
+
+(** The two following notations are made available when this module is imported.
+
+    - printf will parse a format and generate a function taking the
+      corresponding arguments ant printing the resulting message as per
+      Message.print. In particular when fully applied it has type unit.
+    - fprintf behaves similarly but return the message as a value instead of
+      printing it.
+
+*)
+
+Ltac2 Notation "printf" fmt(format) := printf fmt.
+Ltac2 Notation "fprintf" fmt(format) := fprintf fmt.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 241ca7ad66..948a359124 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -44,6 +44,9 @@ let open_constr_no_classes_flags =
 module Value = Tac2ffi
 open Value
 
+let val_format = Tac2print.val_format
+let format = repr_ext val_format
+
 let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n))
 
 let std_core n = core_prefix Tac2env.std_prefix n
@@ -250,6 +253,79 @@ let () = define2 "message_concat" pp pp begin fun m1 m2 ->
   return (Value.of_pp (Pp.app m1 m2))
 end
 
+let () = define0 "format_stop" begin
+  return (Value.of_ext val_format [])
+end
+
+let () = define1 "format_string" format begin fun s ->
+  return (Value.of_ext val_format (Tac2print.FmtString :: s))
+end
+
+let () = define1 "format_int" format begin fun s ->
+  return (Value.of_ext val_format (Tac2print.FmtInt :: s))
+end
+
+let () = define1 "format_constr" format begin fun s ->
+  return (Value.of_ext val_format (Tac2print.FmtConstr :: s))
+end
+
+let () = define1 "format_ident" format begin fun s ->
+  return (Value.of_ext val_format (Tac2print.FmtIdent :: s))
+end
+
+let () = define2 "format_literal" string format begin fun lit s ->
+  return (Value.of_ext val_format (Tac2print.FmtLiteral (Bytes.to_string lit) :: s))
+end
+
+let () = define1 "format_alpha" format begin fun s ->
+  return (Value.of_ext val_format (Tac2print.FmtAlpha :: s))
+end
+
+let () = define2 "format_kfprintf" closure format begin fun k fmt ->
+  let open Tac2print in
+  let fold accu = function
+  | FmtLiteral _ -> accu
+  | FmtString | FmtInt | FmtConstr | FmtIdent -> 1 + accu
+  | FmtAlpha -> 2 + accu
+  in
+  let pop1 l = match l with [] -> assert false | x :: l -> (x, l) in
+  let pop2 l = match l with [] | [_] -> assert false | x :: y :: l -> (x, y, l) in
+  let arity = List.fold_left fold 0 fmt in
+  let rec eval accu args fmt = match fmt with
+  | [] -> apply k [of_pp accu]
+  | tag :: fmt ->
+    match tag with
+    | FmtLiteral s ->
+      eval (Pp.app accu (Pp.str s)) args fmt
+    | FmtString ->
+      let (s, args) = pop1 args in
+      let pp = Pp.str (Bytes.to_string (to_string s)) in
+      eval (Pp.app accu pp) args fmt
+    | FmtInt ->
+      let (i, args) = pop1 args in
+      let pp = Pp.int (to_int i) in
+      eval (Pp.app accu pp) args fmt
+    | FmtConstr ->
+      let (c, args) = pop1 args in
+      let c = to_constr c in
+      pf_apply begin fun env sigma ->
+        let pp = Printer.pr_econstr_env env sigma c in
+        eval (Pp.app accu pp) args fmt
+      end
+    | FmtIdent ->
+      let (i, args) = pop1 args in
+      let pp = Id.print (to_ident i) in
+      eval (Pp.app accu pp) args fmt
+    | FmtAlpha ->
+      let (f, x, args) = pop2 args in
+      Tac2ffi.apply (to_closure f) [of_unit (); x] >>= fun pp ->
+      eval (Pp.app accu (to_pp pp)) args fmt
+  in
+  let eval v = eval (Pp.mt ()) v fmt in
+  if Int.equal arity 0 then eval []
+  else return (Tac2ffi.of_closure (Tac2ffi.abstract arity eval))
+end
+
 (** Array *)
 
 let () = define0 "array_empty" begin
@@ -1629,6 +1705,7 @@ let () = add_expr_scope "pose" q_pose Tac2quote.of_pose
 let () = add_expr_scope "assert" q_assert Tac2quote.of_assertion
 let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_matching
 let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching
+let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format
 
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr
 let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern
diff --git a/user-contrib/Ltac2/tac2print.ml b/user-contrib/Ltac2/tac2print.ml
index a54eb45f61..7a53b577b6 100644
--- a/user-contrib/Ltac2/tac2print.ml
+++ b/user-contrib/Ltac2/tac2print.ml
@@ -489,3 +489,51 @@ let () =
   | _ -> assert false
   in
   register_val_printer kn { val_printer }
+
+(** {5 Ltac2 primitive} *)
+
+type format =
+| FmtString
+| FmtInt
+| FmtConstr
+| FmtIdent
+| FmtLiteral of string
+| FmtAlpha
+
+let val_format = Tac2dyn.Val.create "format"
+
+exception InvalidFormat
+
+let parse_format (s : string) : format list =
+  let len = String.length s in
+  let buf = Buffer.create len in
+  let rec parse i accu =
+    if len <= i then accu
+    else match s.[i] with
+    | '%' -> parse_argument (i + 1) accu
+    | _ ->
+      let i' = parse_literal i in
+      if Int.equal i i' then parse i' accu
+      else
+        let lit = Buffer.contents buf in
+        let () = Buffer.clear buf in
+        parse i' (FmtLiteral lit :: accu)
+  and parse_literal i =
+    if len <= i then i
+    else match s.[i] with
+    | '%' -> i
+    | c ->
+      let () = Buffer.add_char buf c in
+      parse_literal (i + 1)
+  and parse_argument i accu =
+    if len <= i then raise InvalidFormat
+    else match s.[i] with
+    | '%' -> parse (i + 1) (FmtLiteral "%" :: accu)
+    | 's' -> parse (i + 1) (FmtString :: accu)
+    | 'i' -> parse (i + 1) (FmtInt :: accu)
+    | 'I' -> parse (i + 1) (FmtIdent :: accu)
+    | 't' -> parse (i + 1) (FmtConstr :: accu)
+    | 'a' -> parse (i + 1) (FmtAlpha :: accu)
+    | _ -> raise InvalidFormat
+  in
+  parse 0 []
diff --git a/user-contrib/Ltac2/tac2print.mli b/user-contrib/Ltac2/tac2print.mli
index df5b03f82a..6bb4884666 100644
--- a/user-contrib/Ltac2/tac2print.mli
+++ b/user-contrib/Ltac2/tac2print.mli
@@ -46,3 +46,19 @@ val pr_valexpr : Environ.env -> Evd.evar_map -> valexpr -> 'a glb_typexpr -> Pp.
 val int_name : unit -> (int -> string)
 (** Create a function that give names to integers. The names are generated on
     the fly, in the order they are encountered. *)
+
+(** {5 Ltac2 primitives}*)
+
+type format =
+| FmtString
+| FmtInt
+| FmtConstr
+| FmtIdent
+| FmtLiteral of string
+| FmtAlpha
+
+val val_format : format list Tac2dyn.Val.tag
+
+exception InvalidFormat
+
+val parse_format : string -> format list
diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index 90f8008dc2..d1a72fcfd1 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -35,6 +35,7 @@ let prefix_gen n =
 let control_prefix = prefix_gen "Control"
 let pattern_prefix = prefix_gen "Pattern"
 let array_prefix = prefix_gen "Array"
+let format_prefix = MPdot (prefix_gen "Message", Label.make "Format")
 
 let kername prefix n = KerName.make prefix (Label.of_id (Id.of_string_soft n))
 let std_core n = kername Tac2env.std_prefix n
@@ -75,6 +76,9 @@ let of_tuple ?loc el = match el with
   let len = List.length el in
   CAst.make ?loc @@ CTacApp (CAst.make ?loc @@ CTacCst (AbsKn (Tuple len)), el)
 
+let of_string {loc;v=n} =
+  CAst.make ?loc @@ CTacAtm (AtmStr n)
+
 let of_int {loc;v=n} =
   CAst.make ?loc @@ CTacAtm (AtmInt n)
 
@@ -489,3 +493,27 @@ let of_assertion {loc;v=ast} = match ast with
   let id = of_anti of_ident id in
   let c = of_constr c in
   std_constructor ?loc "AssertValue" [id; c]
+
+let of_format accu = function
+| Tac2print.FmtString ->
+  CAst.make @@ CTacApp (global_ref (kername format_prefix "string"), [accu])
+| Tac2print.FmtInt ->
+  CAst.make @@ CTacApp (global_ref (kername format_prefix "int"), [accu])
+| Tac2print.FmtConstr ->
+  CAst.make @@ CTacApp (global_ref (kername format_prefix "constr"), [accu])
+| Tac2print.FmtIdent ->
+  CAst.make @@ CTacApp (global_ref (kername format_prefix "ident"), [accu])
+| Tac2print.FmtLiteral lit ->
+  let s = of_string (CAst.make lit) in
+  CAst.make @@ CTacApp (global_ref (kername format_prefix "literal"), [s; accu])
+| Tac2print.FmtAlpha ->
+  CAst.make @@ CTacApp (global_ref (kername format_prefix "alpha"), [accu])
+
+let of_format { v = fmt; loc } =
+  let fmt =
+    try Tac2print.parse_format fmt
+    with Tac2print.InvalidFormat ->
+      CErrors.user_err ?loc (str "Invalid format")
+  in
+  let stop = CAst.make @@ CTacApp (global_ref (kername format_prefix "stop"), [of_tuple []]) in
+  List.fold_left of_format stop fmt
diff --git a/user-contrib/Ltac2/tac2quote.mli b/user-contrib/Ltac2/tac2quote.mli
index f9c41b57dc..fcd1339cd7 100644
--- a/user-contrib/Ltac2/tac2quote.mli
+++ b/user-contrib/Ltac2/tac2quote.mli
@@ -85,6 +85,8 @@ val of_constr_matching : constr_matching -> raw_tacexpr
 
 val of_goal_matching : goal_matching -> raw_tacexpr
 
+val of_format : lstring -> raw_tacexpr
+
 (** {5 Generic arguments} *)
 
 val wit_pattern : (Constrexpr.constr_expr, Pattern.constr_pattern) Arg.tag