Skip to content

Commit f38799d

Browse files
author
Jan-Oliver Kaiser
committed
Add and use helper for predicates producing diagnostics
1 parent 9d9fc51 commit f38799d

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
@@ -3545,13 +3545,9 @@ Universe constraints are put in the constraint store.|})))),
35453545
let state, assignments = set_current_sigma ~depth state sigma in
35463546
state, r, assignments
35473547
with Pretype_errors.PretypeError (env, sigma, err) ->
3548-
match diag with
3549-
| Data B.OK ->
3550-
(* optimization: don't print the error if caller wants OK *)
3551-
raise No_clause
3552-
| _ ->
3553-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3554-
state, ?: None +! B.mkERROR error, [])),
3548+
diag_error_lazy diag @@ fun () ->
3549+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3550+
state, ?: None +! B.mkERROR error, [])),
35553551
DocAbove);
35563552

35573553
MLCode(Pred("coq.typecheck-ty",
@@ -3579,13 +3575,9 @@ Universe constraints are put in the constraint store.|})))),
35793575
let state, assignments = set_current_sigma ~depth state sigma in
35803576
state, r, assignments
35813577
with Pretype_errors.PretypeError (env, sigma, err) ->
3582-
match diag with
3583-
| Data B.OK ->
3584-
(* optimization: don't print the error if caller wants OK *)
3585-
raise No_clause
3586-
| _ ->
3587-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3588-
state, ?: None +! B.mkERROR error, [])),
3578+
diag_error_lazy diag @@ fun () ->
3579+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3580+
state, ?: None +! B.mkERROR error, [])),
35893581
DocAbove);
35903582

35913583
MLCode(Pred("coq.unify-eq",
@@ -3600,13 +3592,9 @@ Universe constraints are put in the constraint store.|})))),
36003592
let state, assignments = set_current_sigma ~depth state sigma in
36013593
state, !: B.mkOK, assignments
36023594
with Pretype_errors.PretypeError (env, sigma, err) ->
3603-
match diag with
3604-
| Data B.OK ->
3605-
(* optimization: don't print the error if caller wants OK *)
3606-
raise No_clause
3607-
| _ ->
3608-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3609-
state, !: (B.mkERROR error), [])),
3595+
diag_error_lazy diag @@ fun () ->
3596+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3597+
state, !: (B.mkERROR error), [])),
36103598
DocAbove);
36113599

36123600
MLCode(Pred("coq.unify-leq",
@@ -3621,13 +3609,9 @@ Universe constraints are put in the constraint store.|})))),
36213609
let state, assignments = set_current_sigma ~depth state sigma in
36223610
state, !: B.mkOK, assignments
36233611
with Pretype_errors.PretypeError (env, sigma, err) ->
3624-
match diag with
3625-
| Data B.OK ->
3626-
(* optimization: don't print the error if caller wants OK *)
3627-
raise No_clause
3628-
| _ ->
3629-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3630-
state, !: (B.mkERROR error), [])),
3612+
diag_error_lazy diag @@ fun () ->
3613+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3614+
state, !: (B.mkERROR error), [])),
36313615
DocAbove);
36323616

36333617
MLCode(Pred("coq.elaborate-skeleton",
@@ -3670,13 +3654,9 @@ Supported attributes:
36703654
let state, assignments = set_current_sigma ~depth state sigma in
36713655
state, ?: None +! uj_val +! B.mkOK, assignments
36723656
with Pretype_errors.PretypeError (env, sigma, err) ->
3673-
match diag with
3674-
| Data B.OK ->
3675-
(* optimization: don't print the error if caller wants OK *)
3676-
raise No_clause
3677-
| _ ->
3678-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3679-
state, ?: None +? None +! B.mkERROR error, [])),
3657+
diag_error_lazy diag @@ fun () ->
3658+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3659+
state, ?: None +? None +! B.mkERROR error, [])),
36803660
DocAbove);
36813661

36823662
MLCode(Pred("coq.elaborate-ty-skeleton",
@@ -3704,13 +3684,9 @@ Supported attributes:
37043684
let state, assignments = set_current_sigma ~depth state sigma in
37053685
state, !: sort +! uj_val +! B.mkOK, assignments
37063686
with Pretype_errors.PretypeError (env, sigma, err) ->
3707-
match diag with
3708-
| Data B.OK ->
3709-
(* optimization: don't print the error if caller wants OK *)
3710-
raise No_clause
3711-
| _ ->
3712-
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3713-
state, ?: None +? None +! B.mkERROR error, [])),
3687+
diag_error_lazy diag @@ fun () ->
3688+
let error = string_of_ppcmds proof_context.options @@ Himsg.explain_pretype_error env sigma err in
3689+
state, ?: None +? None +! B.mkERROR error, [])),
37143690
DocAbove);
37153691

37163692
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)