Re: More extensive (variable) style checking

On Sat, Aug 3, 2013 at 10:54 AM, Abramo Bagnara
<[email protected]> wrote:
> 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.

I admit that the syntax may look unnatural but under the surface there
are not many possibilities. We would be glad to discuss it and even
modify the syntax. I know that there is interest in a common and
portable syntax for assertions among different Prolog systems.

>> 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.

That is also the idea of the Ciao assertion language! :)

Part of it (the runtime checking) was ported to SWI by Edison Mera (I
believe that it will be presented as a technical communication in ICLP
this year).

Bests,

-- 
Jose