Skip to content

Commit e427ff0

Browse files
author
Jan-Oliver Kaiser
committed
Add and use helper for predicates producing diagnostics
1 parent 646dda5 commit e427ff0

File tree

3 files changed

+47
-42
lines changed

3 files changed

+47
-42
lines changed

‎src/rocq_elpi_builtins.ml‎

Lines changed: 18 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -3526,13 +3526,9 @@ Universe constraints are put in the constraint store.|})))),
35263526
let state, assignments = set_current_sigma ~depth state sigma in
35273527
state, r, assignments
35283528
with Pretype_errors.PretypeError (env, sigma, err) ->
3529-
match diag with
3530-
| Data B.OK ->
3531-
(* optimization: don't print the error if caller wants OK *)
3532-
raise No_clause
3533-
| _ ->
3534-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3535-
state, ?: None +! B.mkERROR error, [])),
3529+
diag_error_lazy diag @@ fun () ->
3530+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3531+
state, ?: None +! B.mkERROR error, [])),
35363532
DocAbove);
35373533

35383534
MLCode(Pred("coq.typecheck-ty",
@@ -3560,13 +3556,9 @@ Universe constraints are put in the constraint store.|})))),
35603556
let state, assignments = set_current_sigma ~depth state sigma in
35613557
state, r, assignments
35623558
with Pretype_errors.PretypeError (env, sigma, err) ->
3563-
match diag with
3564-
| Data B.OK ->
3565-
(* optimization: don't print the error if caller wants OK *)
3566-
raise No_clause
3567-
| _ ->
3568-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3569-
state, ?: None +! B.mkERROR error, [])),
3559+
diag_error_lazy diag @@ fun () ->
3560+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3561+
state, ?: None +! B.mkERROR error, [])),
35703562
DocAbove);
35713563

35723564
MLCode(Pred("coq.unify-eq",
@@ -3581,13 +3573,9 @@ Universe constraints are put in the constraint store.|})))),
35813573
let state, assignments = set_current_sigma ~depth state sigma in
35823574
state, !: B.mkOK, assignments
35833575
with Pretype_errors.PretypeError (env, sigma, err) ->
3584-
match diag with
3585-
| Data B.OK ->
3586-
(* optimization: don't print the error if caller wants OK *)
3587-
raise No_clause
3588-
| _ ->
3589-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3590-
state, !: (B.mkERROR error), [])),
3576+
diag_error_lazy diag @@ fun () ->
3577+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3578+
state, !: (B.mkERROR error), [])),
35913579
DocAbove);
35923580

35933581
MLCode(Pred("coq.unify-leq",
@@ -3602,13 +3590,9 @@ Universe constraints are put in the constraint store.|})))),
36023590
let state, assignments = set_current_sigma ~depth state sigma in
36033591
state, !: B.mkOK, assignments
36043592
with Pretype_errors.PretypeError (env, sigma, err) ->
3605-
match diag with
3606-
| Data B.OK ->
3607-
(* optimization: don't print the error if caller wants OK *)
3608-
raise No_clause
3609-
| _ ->
3610-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3611-
state, !: (B.mkERROR error), [])),
3593+
diag_error_lazy diag @@ fun () ->
3594+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3595+
state, !: (B.mkERROR error), [])),
36123596
DocAbove);
36133597

36143598
MLCode(Pred("coq.elaborate-skeleton",
@@ -3651,13 +3635,9 @@ Supported attributes:
36513635
let state, assignments = set_current_sigma ~depth state sigma in
36523636
state, ?: None +! uj_val +! B.mkOK, assignments
36533637
with Pretype_errors.PretypeError (env, sigma, err) ->
3654-
match diag with
3655-
| Data B.OK ->
3656-
(* optimization: don't print the error if caller wants OK *)
3657-
raise No_clause
3658-
| _ ->
3659-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3660-
state, ?: None +? None +! B.mkERROR error, [])),
3638+
diag_error_lazy diag @@ fun () ->
3639+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3640+
state, ?: None +? None +! B.mkERROR error, [])),
36613641
DocAbove);
36623642

36633643
MLCode(Pred("coq.elaborate-ty-skeleton",
@@ -3685,13 +3665,9 @@ Supported attributes:
36853665
let state, assignments = set_current_sigma ~depth state sigma in
36863666
state, !: sort +! uj_val +! B.mkOK, assignments
36873667
with Pretype_errors.PretypeError (env, sigma, err) ->
3688-
match diag with
3689-
| Data B.OK ->
3690-
(* optimization: don't print the error if caller wants OK *)
3691-
raise No_clause
3692-
| _ ->
3693-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3694-
state, ?: None +? None +! B.mkERROR error, [])),
3668+
diag_error_lazy diag @@ fun () ->
3669+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3670+
state, ?: None +? None +! B.mkERROR error, [])),
36953671
DocAbove);
36963672

36973673
LPDoc "-- Coq's reduction flags ------------------------------------";

‎src/rocq_elpi_utils.ml‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -873,3 +873,26 @@ let eta_contract env sigma t =
873873
in
874874
(*Printf.eprintf "------------- %s\n" Pp.(string_of_ppcmds @@ Printer.pr_econstr_env env sigma t);*)
875875
map env t
876+
877+
(* Command argument specifiers *)
878+
type arg_kind =
879+
| Elaborated
880+
| Unelaborated
881+
| Syntactic
882+
let arg_kind_merge ?loc (old : arg_kind option) (k : arg_kind) =
883+
match old with
884+
| None -> k
885+
| Some old when old = k -> k
886+
| _ -> CErrors.user_err ?loc Pp.(str "Syntax error, incompatible values for attribute \"arguments\"")
887+
888+
(* Helper for predicates that produce diagnostics *)
889+
let diag_error_lazy
890+
?(on_ok=fun () -> raise API.BuiltInPredicate.No_clause)
891+
diag_arg
892+
(on_other : unit -> 'a) : 'a =
893+
let open API.BuiltInPredicate in
894+
(* optimization: don't print the error if caller wants OK *)
895+
match diag_arg with
896+
| Data Elpi.Builtin.OK -> on_ok ()
897+
| _ -> on_other ()
898+

‎src/rocq_elpi_utils.mli‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,3 +89,9 @@ val mp2path: Names.ModPath.t -> string list
8989
val gr2path: Names.GlobRef.t -> string list
9090

9191
val eta_contract : Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t
92+
93+
(* Diagnostics *)
94+
val diag_error_lazy : ?on_ok:(unit -> 'a) -> (* defaults to [raise No_clause] *)
95+
Elpi.Builtin.diagnostic Elpi.API.BuiltInPredicate.ioarg ->
96+
(unit -> 'a) ->
97+
'a

0 commit comments

Comments
 (0)