Moduli di sistema

I moduli di sistema list_util e maps



%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modulo ListUtil %%%%%%%%%%%%%%%%%%%%%%%%%%%%



%% list_util.mod                                                        %%



%% Copyright (c) 1991,1994,1995 by Carnegie Mellon University           %%

%% Copyright (c) 1994,1995 by AT&T Bell Laboratories                    %%

%% Copyright (c) 1995,1996 by the University of Pennsylvania            %%



%% For information about the distributaion, copying, and modification   %%

%% of this software, please read the file COPYING located in the root   %%

%% directory of this distribnutaion. If you did not receive the file    %%

%% COPYING write to Philip Wickline at the address below.               %%



%% This program is distributed in the hope that it will be useful but   %%

%% WITHOUT ANY WARRANTY; without even the implied warranty of           %%

%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the file    %%

%% COPYING for more details.                                            %%



%% For information about the structure of the Terzo lambdaProlog        %%

%% implementation, see the file src/README in this distribution. Please %%

%% address any questions about this code or the Terzo lambdaProlog      %%

%% implementation to Philip Wickline at 
        philipw@saul.cis.upenn.edu.   %%



%% Authors:                                                             %%

%%      Amy Felty felty@bell-labs.com>                                 %%

%%      Frank Pfenning fp@cs.cmu.edu                                  %%

%%      Philip Wickline philipw@saul.cis.upenn.edu                    %%



module ListUtil.

accumulate List.

%% Nota: il modulo List e' caricato automaticamente dall'interprete Terzo



        type memb               A -> list A -> o.

        % memb X L

        %  Succeeds if X is a member of L.  In contrast to member,

        %  this will succeed as often as X unifies with members of L.



        memb X (X :: L).

        memb X (Y :: L) :- memb X L.





        type member             A -> list A -> o.

        % member X L

        %  succeeds if X is a member of L.  In contrast to memb,

        %  this will succeed only once: for the first unifier of

        %  X with a member of L.



        member X (X :: L) :- !.

        member X (Y :: L) :- member X L.



        type append             list A -> list A -> list A -> o.

        % append L K M

        %  Succeeds if M is the result of appending K to L.



        append nil K K.

        append (X :: L) K (X :: M) :- append L K M.





        type join               list A -> list A -> list A -> o.

        % join L K M

        %  Join is similar to append except that members of L that

        %  already appear in K are not appended to form M.  Note

        %  that this `check' will do unification!



        join nil K K.

        join (X :: L) K M :- memb X K, !, join L K M.

        join (X :: L) K (X :: M) :- join L K M.





        type    memb_and_rest   A -> list A -> list A -> o.

        % memb_and_rest X L M

        %  Succeeds for every occurrence of X in L, where M is the

        %  result of removing that occurrence from L.



        memb_and_rest A (A :: Rest) Rest.

        memb_and_rest A (B :: Tail) (B :: Rest) :- memb_and_rest A Tail Rest.





        type    nth_item        int -> A -> list A -> o.

        % nth_item N X L

        %  Succeeds if the Nth item of L is X, where counting starts

        %  at 1.  For N = 0 it behaves like memb.



        nth_item 0 A List :- !, memb A List.

        nth_item 1 A (B::Rest) :- !, A = B.

        nth_item N A (B::Tail) :- M is (N - 1), nth_item M A Tail.





        type    nth_and_rest    int -> A -> list A -> list A -> o.

        % nth_and_rest N X L Rest

        %  Succeeds if the Nth item of L is X, and Rest is the rest

        %  of L.  Counting starts at 1.  For N = 0, it behaves like

        %  memb_and_rest.



        nth_and_rest 0 A List Rest :- !, memb_and_rest A List Rest.

        nth_and_rest 1 A (B::Rest) Rest :- !, A = B.

        nth_and_rest N A (B::Tail) (B::Rest) :-

          M is (N - 1), nth_and_rest M A Tail Rest.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modulo maps %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%   Predicates in Lambda Prolog that define some of the `higher-order'

%   mapping operations



module  maps.

import List.



        type    mapfun          (A -> B) -> (list A) -> (list B) -> o.

        % mapfun F (X1::X2::...::Xn) ((F X1)::(F X2)::...::(F Xn))



        mapfun F nil nil.

        mapfun F (X :: L) ((F X) :: K) :- mapfun F L K.



        type    mappred         (A -> B -> o) -> (list A) -> (list B) -> o.

        % mappred P (X1::X2::...::Xn) (Y1::Y2::...::Yn)

        %       Succeeds if the predicate P relates Xi to Yi.



        mappred P nil nil.

        mappred P (X :: L) (Y :: K) :- P X Y, mappred P L K.



        type    reduce          (A -> B -> B) -> (list A) -> B -> B -> o.

        % reduce F (X1::X2::...::Xn) Init (F X1 (F X2 (... (F Xn Init)))).



        reduce F nil X X.

        reduce F (W :: L) X (F W Y) :-  reduce F L X Y.



        type    forevery        (A -> o) -> (list A) -> o.

        % forevery P (X1::X2::...::Xn)

        %       Succeeds if P holds for every Xi.



        forevery P nil.

        forevery P (X :: L) :- P X, forevery P L.



        type    forsome         (A -> o) -> (list A) -> o.

        % forsome P (X1::X2::...::Xn).

        %       Succeeds if P holds for some Xi.



        forsome P (X :: L) :- P X.

        forsome P (X :: L) :- forsome P L.