[syntax] Make "lconstr" (parenthesis-free terms) available to Ltac2 notations

src/g_waterproof.mlg

@@ -23,6 +23,55 @@ open Exceptions
 open Waterprove
 
 let waterproof_version : string = "2.2.0+dev"
+
+module Ltac2Extension = struct
+
+let add_scope s f =
+  let open Ltac2_plugin in
+  Tac2entries.register_scope (Names.Id.of_string s) f
+
+let rec pr_scope =
+  let open Ltac2_plugin in
+  let open Tac2expr in
+  let open CAst in function
+    | SexprStr {v=s} -> Pp.qstring s
+    | SexprInt {v=n} -> Pp.int n
+    | SexprRec (_, {v=na}, args) ->
+      let na = match na with
+        | None -> Pp.str "_"
+        | Some id -> Names.Id.print id
+      in
+      Pp.(na ++ str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")")
+
+let scope_fail s args =
+  let open Pp in
+  let args = str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")" in
+  CErrors.user_err (str "Invalid arguments " ++ args ++ str " in scope " ++ str s)
+
+let () = add_scope "lconstr" (fun arg ->
+  let open Ltac2_plugin in
+  let delimiters = List.map (function
+      | Tac2expr.SexprRec (_, { v = Some s }, []) -> s
+      | _ -> scope_fail "lconstr" arg)
+      arg
+  in
+  let act e = Tac2quote.of_constr ~delimiters e in
+  Tac2entries.ScopeRule (Procq.Symbol.nterm Procq.Constr.lconstr, act)
+  )
+
+let () = add_scope "open_lconstr" (fun arg ->
+  let open Ltac2_plugin in
+  let delimiters = List.map (function
+      | Tac2expr.SexprRec (_, { v = Some s }, []) -> s
+      | _ -> scope_fail "open_.constr" arg)
+      arg
+  in
+  let act e = Tac2quote.of_open_constr ~delimiters e in
+  Tac2entries.ScopeRule (Procq.Symbol.nterm Procq.Constr.lconstr, act)
+  )
+
+end
+
 }
 
 VERNAC COMMAND EXTEND AutomationShieldEnableSideEff CLASSIFIED AS SIDEFF