223 lines
5.4 KiB
Prolog
223 lines
5.4 KiB
Prolog
/**
|
|
* @file coinduction.yap
|
|
* @author VITOR SANTOS COSTA <vsc@VITORs-MBP.lan>, Arvin Bansal,
|
|
*
|
|
*
|
|
* @date Tue Nov 17 14:55:02 2015
|
|
*
|
|
* @brief Co-inductive execution
|
|
*
|
|
*
|
|
*/
|
|
|
|
|
|
/*************************************************************************
|
|
* *
|
|
* YAP Prolog *
|
|
* *
|
|
* Yap Prolog was developed at NCCUP - Universidade do Porto *
|
|
* *
|
|
* Copyright L.Damas, V.S.Costa and Universidade do Porto 1985-1997 *
|
|
* *
|
|
**************************************************************************
|
|
* *
|
|
* File: coinduction.yap *
|
|
* Last rev: 8/2/88 *
|
|
* mods: *
|
|
* comments: coinduction support for Prolog *
|
|
* *
|
|
*************************************************************************/
|
|
|
|
% :- yap_flag(unknown,error).
|
|
% :- style_check(all).
|
|
|
|
%
|
|
% Code originally written by Arvin Bansal and Vitor Santos Costa
|
|
% Includes nice extensions from Jan Wielemaker (from the SWI version).
|
|
%
|
|
|
|
:- module(coinduction,
|
|
[ (coinductive)/1,
|
|
op(1150, fx, (coinductive))
|
|
]).
|
|
|
|
:- use_module(library(error)).
|
|
|
|
/** <module> coinduction Co-Logic Programming
|
|
@ingroup library
|
|
|
|
This simple module implements the directive coinductive/1 as described
|
|
in "Co-Logic Programming: Extending Logic Programming with Coinduction"
|
|
by Luke Somin et al. The idea behind coinduction is that a goal succeeds
|
|
if it unifies to a parent goal. This enables some interesting programs,
|
|
notably on infinite trees (cyclic terms).
|
|
|
|
~~~~
|
|
:- use_module(library(coinduction)).
|
|
|
|
:- coinductive stream/1.
|
|
stream([H|T]) :- i(H), stream(T).
|
|
|
|
% inductive
|
|
i(0).
|
|
i(s(N)) :- i(N).
|
|
|
|
?- X=[s(s(A))|X], stream(X).
|
|
X= [s(s(A))|X], stream(X).
|
|
A = 0,
|
|
X = [s(s(0)),**]
|
|
~~~~
|
|
|
|
This predicate is true for any cyclic list containing only 1-s,
|
|
regardless of the cycle-length.
|
|
|
|
@bug Programs mixing normal predicates and coinductive predicates must
|
|
be _stratified_. The theory does not apply to normal Prolog calling
|
|
coinductive predicates, calling normal Prolog predicates, etc.
|
|
|
|
Stratification is not checked or enforced in any other way and thus
|
|
left as a responsibility to the user.
|
|
@see "Co-Logic Programming: Extending Logic Programming with Coinduction"
|
|
by Luke Somin et al.
|
|
|
|
@addtogroup coinduction Co-induction
|
|
@ingroup library
|
|
@{
|
|
|
|
*/
|
|
|
|
:- meta_predicate coinductive(:).
|
|
|
|
:- dynamic coinductive/3.
|
|
|
|
|
|
%-----------------------------------------------------
|
|
|
|
coinductive(Spec) :-
|
|
var(Spec),
|
|
!,
|
|
throw(error(instantiation_error,coinductive(Spec))).
|
|
coinductive(Module:Spec) :-
|
|
coinductive_declaration(Spec, Module, coinductive(Module:Spec)).
|
|
coinductive(Spec) :-
|
|
prolog_load_context(module, Module),
|
|
coinductive_declaration(Spec, Module, coinductive(Spec)).
|
|
|
|
coinductive_declaration(Spec, _M, G) :-
|
|
var(Spec),
|
|
!,
|
|
throw(error(instantiation_error,G)).
|
|
coinductive_declaration((A,B), M, G) :- !,
|
|
coinductive_declaration(A, M, G),
|
|
coinductive_declaration(B, M, G).
|
|
coinductive_declaration(M:Spec, _, G) :- !,
|
|
coinductive_declaration(Spec, M, G).
|
|
coinductive_declaration(Spec, M, _G) :-
|
|
valid_pi(Spec, F, N),
|
|
functor(S,F,N),
|
|
atomic_concat(['__coinductive__',F,'/',N],NF),
|
|
functor(NS,NF,N),
|
|
match_args(N,S,NS),
|
|
atomic_concat(['__stack_',M,':',F,'/',N],SF),
|
|
nb_setval(SF, _),
|
|
assert((M:S :-
|
|
b_getval(SF,L),
|
|
coinduction:in_stack(S, L, End),
|
|
(
|
|
nonvar(End)
|
|
->
|
|
true
|
|
;
|
|
End = [S|_],
|
|
M:NS)
|
|
)
|
|
),
|
|
assert(coinduction:coinductive(S,M,NS)).
|
|
|
|
valid_pi(Name/Arity, Name, Arity) :-
|
|
must_be(atom, Name),
|
|
must_be(integer, Arity).
|
|
|
|
match_args(0,_,_) :- !.
|
|
match_args(I,S1,S2) :-
|
|
arg(I,S1,A),
|
|
arg(I,S2,A),
|
|
I1 is I-1,
|
|
match_args(I1,S1,S2).
|
|
|
|
%-----------------------------------------------------
|
|
|
|
co_term_expansion((M:H :- B), _, (M:NH :- B)) :- !,
|
|
co_term_expansion((H :- B), M, (NH :- B)).
|
|
co_term_expansion((H :- B), M, (NH :- B)) :- !,
|
|
coinductive(H, M, NH), !.
|
|
co_term_expansion(H, M, NH) :-
|
|
coinductive(H, M, NH), !.
|
|
|
|
/** user:term_expansion(+M:Cl,-M:NCl )
|
|
|
|
rule preprocessor
|
|
*/
|
|
user:term_expansion(M:Cl,M:NCl ) :- !,
|
|
co_term_expansion(Cl, M, NCl).
|
|
|
|
user:term_expansion(G, NG) :-
|
|
prolog_load_context(module, Module),
|
|
co_term_expansion(G, Module, NG).
|
|
|
|
|
|
%-----------------------------------------------------
|
|
|
|
in_stack(_, V, V) :- var(V), !.
|
|
in_stack(G, [G|_], [G|_]) :- !.
|
|
in_stack(G, [_|T], End) :- in_stack(G, T, End).
|
|
|
|
writeG_val(G_var) :-
|
|
b_getval(G_var, G_val),
|
|
write(G_var), write(' ==> '), write(G_val), nl.
|
|
|
|
%-----------------------------------------------------
|
|
|
|
/**
|
|
|
|
Some examples from Coinductive Logic Programming and its Applications by Gopal Gupta et al, ICLP 97
|
|
|
|
~~~~
|
|
:- coinductive stream/1.
|
|
stream([H|T]) :- i(H), stream(T).
|
|
|
|
% inductive
|
|
i(0).
|
|
i(s(N)) :- i(N).
|
|
|
|
% Are there infinitely many "occurrences" of arg1 in arg2?
|
|
:- coinductive comember/2.
|
|
|
|
comember(X, L) :-
|
|
drop(X, L, L1),
|
|
comember(X, L1).
|
|
|
|
% Drop some prefix of arg2 upto an "occurrence" of arg1 from arg2,
|
|
% yielding arg3.
|
|
% ("Occurrence" of X = something unifiable with X.)
|
|
%:- table(drop/3). % not working; needs tabling supporting cyclic terms!
|
|
drop(H, [H| T], T).
|
|
drop(H, [_| T], T1) :-
|
|
drop(H, T, T1).
|
|
|
|
|
|
% X = [1, 2, 3| X], comember(E, X).
|
|
|
|
user:p(E) :-
|
|
X = [1, 2, 3| X],
|
|
comember(E, X),
|
|
format('~w~n',[E]),
|
|
get_code(_),
|
|
fail.
|
|
|
|
~~~~
|
|
|
|
@}
|
|
*/
|
|
|