Re: More extensive (variable) style checking

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
problem is really complex when you consider all the different
possibilities, e.g., what is a type for you?).

Best Regards,

-- 
Jose