coq-elpi-checker.elpi

/* coq-elpi: Coq terms as the object language of elpi                        */
/* license: GNU Lesser General Public License Version 2.1 or later           */
/* ------------------------------------------------------------------------- */

% redirect to Coq type checking messages

:before "default-typechecking-error"
error [] _ :- !.
:before "default-typechecking-error"
error [pr L M] tt :- !, coq.error L M.
:before "default-typechecking-error"
error Msgs tt :- !, coq.error "At least one of the following errors holds:" {error-concat Msgs}.

pred error-concat i:list string, o:string.
error-concat [] "\n".
error-concat [pr L X] R :- error-concat XS Rest, term_to_string L LS, R is LS ^ " " ^ X.
error-concat [pr L X|XS] R :- error-concat XS Rest, term_to_string L LS, R is LS ^ " " ^ X ^ "\n" ^ Rest.

:before "default-typechecking-warning"
warning L M :- !, coq.warning "elpi" "elpi.typecheck" L M.