Check modes of predicate arguments at runtime

[hurufu]

Hello,
Recently I have written a lot of Prolog code (mostly to interface with operating system) and I have found myself writing a lot of checks like var(X) -> throw(...). There is a nice library si, but it is too primitive (like assembly language) to my taste; also there is must_be/2 from SWI-Prolog, but it isn't available universally either, so I wrote my own:

:- op(200, fy, '?').

% Micro-language to specify argument modes and check them at runtime
%
% Examples:
%
%     let(((?A, -B);(+B, +A))).
%     let((-A -> +B);(-B -> +A)).
%
let(Expr) :- phrase(letd(Expr), []), !.
let(Expr) :- phrase(letd(Expr), [H|_]), !, throw(error(H, _)).
let(Expr) :- throw(error(syntax_error(Expr), _)).

letd(+A)             --> {rc(instantiation_error,      ground(A), R)}, R.
letd(-A)             --> {rc(uninstantiation_error(A), var(A),    R)}, R.
letd(?A)             --> {rc(instantiation_error,      nonvar(A), R)}, R.
letd((A,B))          --> letd(A), letd(B).
letd((A;_))          --> letd(A).
letd((_;B))          --> letd(B).
letd((A->B))         --> letd((not(A);B)).
letd(not((A->B)))    --> letd((A,not(B))).
letd(not((A,B)))     --> letd((not(A);not(B))).
letd(not((A;B)))     --> letd((not(A),not(B))).
letd(not(not(A)))    --> letd(A).
letd(not(+A))        --> letd(-A).
letd(not(+A))        --> letd(?A).
letd(not(-A))        --> letd(?A).
letd(not(?A))        --> letd(-A).

% Runtime check
rc(Error, Check, Result) :- call(Check) -> [] = Result; Result = [Error].

Writing mode specification in the comments isn't validated in any way and also in many realistic cases simple % mypred(?A,?B) doesn't capture actual requirements well enough. Additional bonus: in release version I can just redefine: let(_). if speed is important. What to you think? Does it have any obvious shortcomings?

[triska]

Very interesting! Thank you a lot for sharing this!

I have two small syntax comments:

1. there is no need to quote the atom ?
2. maybe you would like to turn rc/3 into a DCG non-terminal rc//3 so that only one use of {}//1 is needed in the entire snippet?

[hurufu]

Thanks, for taking a look.

1. I quoted, because I still can't believe that Prolog parser can handle this, I subconsciously try to "help" the parser :)
2. It's an easy fix, thanks for a remark. I'm still trying to internalize what is considered "good" Prolog code.

Indeed letd(+A) --> rc(ground(A), instantiation_error). does look much cleaner.

[UWN]

library(si)

[hurufu]

Thanks, I'm aware of that library. Actually after second look into it I found when_si/2 predicate, it does what I wanted to achieve. It looks like either I have an old installation of Scryer prolog or I missed it somehow. It would've save me couple of hours ;)

[UWN]

Please note that library(si) is work in progress. So maybe you can identify further additions. Think of sort_si/2 where the ultimate definition might still wait to be discovered.