From 3902229664376039cacad407554e8732bac34067 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 19 Mar 2025 12:14:52 +0100 Subject: [PATCH] [syntax] Make "lconstr" (parenthesis-free terms) available to Ltac2 notations Co-authored-by: Portegies, Jim Co-authored-by: Otte, P.J. (Pim)" --- src/g_waterproof.mlg | 49 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/src/g_waterproof.mlg b/src/g_waterproof.mlg index 87abab8..0b47faa 100644 --- a/src/g_waterproof.mlg +++ b/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