Re: More extensive (variable) style checking

Il 03/08/2013 10:33, Jose F. Morales ha scritto:
> On Sat, Aug 3, 2013 at 10:19 AM, Abramo Bagnara
> <[email protected]> wrote:
>> Il 03/08/2013 09:19, Jan Wielemaker ha scritto:
>>> On 08/02/2013 09:15 PM, Michael Hendricks wrote:
>>>> Can this system eliminate the false singleton warning on Query in a
>>>> quasiquote like {|uri||/path?$Query|} ?  Those have become a bit of a
>>>> thorn in my side :-)
>>>
>>> This is an unrelated issue. Yes, I think that is possible by doing QQ
>>> expansion before singleton warnings and walk through the QQ expanded
>>> terms to see whether any of the singletons found so far appear in the QQ
>>> expansion. It it surely planned to look at that at some point. If you
>>> are in a hurry though, you might want to dig into pl-read.c ...
>>>
>>>> Is it possible to warn about unreachable code?  For example,
>>>>
>>>>     t :-
>>>>         ( ground(X) -> unreachable ; do_stuff ).
>>>>
>>>> That makes "failure slice" debugging generate warnings, but I think
>>>> that's acceptable.
>>>
>>> That would be possible. Most likely in the form of "Test always
>>> succeeds: ground(X)", which you would already get if you used nonvar(X).
>>> These warnings from the low level compiler are -at least now- only
>>> generated for inlined tests. ground/1 is not one of them (yet). I don't
>>> know whether we should go for a full-blown mode/type system, the current
>>> limited system or something in between.
>>
>> FWIW in our experience what is most important is a full-blown mode
>> system (types are useful, but a bit less).
>>
>> The nice thing is that a lot of predicates mode annotations might be
>> generated automatically.
>>
>> Internally we use something like that:
>>
>> :- pred(my_predicate(+_Arg1:type1, -_Arg2:type2, \_Arg3:type3),
>>         [semidet]).
>>
>> Where we use + for input arguments, - for output arguments and \ for others.
>>
>> This is currently only used (with huge success) to generate dynamic
>> checks wrapper around predicates in debug build, but our idea is to use
>> them for static analysis like steadfastness checking, det/semidet
>> checking, passing of free variable where non free is expected or
>> viceversa, passing unexpected type, etc.
> 
> Hi Abramo,
> 
> Is there any big difference with the Ciao assertion language? (the

Last time I check it (admittely some time ago) I found it not suitable
for our needs and a bit unnatural.

> problem is really complex when you consider all the different
> possibilities, e.g., what is a type for you?).

Using the example above, we have the following (among others):

- dynamic checking: call(type1, Arg1) should succeed on predicate entry
and call(type2, Arg2) should succeed on predicate exit

- static checking: the predicate must be called with a non free Arg1
having type T where isa(T, type1) succeeds

Our aim was to design a system that might be used for dynamic *and*
static checking with the same annotation.

-- 
Abramo Bagnara

BUGSENG srl - http://bugseng.com
mailto:[email protected]