CiaoPP Quick Tutorial

Author(s): Isabel Garcia-Contreras.

Quick guide to using CiaoPP.

In this tutorial we assume that CiaoPP has been installed (see Installation for more information).

For more information see the Advanced Tutorial on Program Development and Optimization using the Ciao Preprocessor.

In this tutorial we want to quickly illustrate the kind of static processing that CiaoPP can perform.

Analyzing

Let us analyze this implementation of the append predicate:

:- module(app, [app/3], [assertions]).

:- entry app(A,B,C) : (list(A), list(B)).
app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
        app(Xs,Ys,Zs).

Automatic analysis can be performed by using the direct acces button in the emacs interface .

By default, CiaoPP analyzes programs with a type domain (eterms) and a sharing/freeness domain (shfr):

The inferred information is expressed with (true) assertions (for a more extensive tutorial of the assertion language see Using assertions for preprocessing programs).

true represents abstractions of the behavior of the program inferred by the analyzer. In this case it was inferred:

:- true pred app(A,B,C) % (1)
         : ( list(A), list(B), term(C) )
        => ( list(A), list(B), list(C) ).

:- true pred app(A,B,C) % (2)
         : mshare([[A],[A,B],[A,B,C],[A,C],[B],[B,C],[C]])
        => mshare([[A,B,C],[A,C],[B,C]]).

Assertion (1) contains types information and encodes predicate app/3 is called with A and B as lists and if it succeeds, C will be a list.

Assertion (2) contains information about how variables are shared. It was inferred that when app(A,B,C) is called arguments A, B, and C may be shared and if it succeeds they also will be shared, sice C is the concatenation of A and B.

Assertion Checking

Let us add an assertion with properties that we want to prove about the execution of the program.

:- module(_, [app/3], [assertions]).

:- entry app(A,B,C) : (list(A), list(B)).
:- pred app(A,B,C) : (list(A), list(B)) => var(C).
app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
        app(Xs,Ys,Zs).

This assertion is stating that if the predicate is called with a A and B list, if it succeeds C will be a free variable. We can check this assertion by clicking the icon in the emacs interface:

Of course this assertion does not hold and we get a message saying so.

Assertion checking can also be reported within the source code by typing "output." in the CiaoPP top-level and open the file (C-c C-v). This feature is experimental:

This assertion was wrong so we correct it with:

:- pred app(A,B,C) : (list(A), list(B)) => list(C).

and run the analysis again. In this case we get no error messages and, as before, results can also be reported in the source file:

Program Optimization

The following program naively implements a predicate that duplicates the first element of a list.

:- module(_, [dup_first/2], []).

dup_first([X|Xs], Zs) :-
        app([X], [X|Xs], Zs).

app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
        app(Xs,Ys,Zs).

CiaoPP can automatically optimize sources by using the button:

Advanced Preprocessing

CiaoPP has several parameters for each of the main actions. For more information, see the Advanced Tutorial on Program Development and Optimization using the Ciao Preprocessor.