1/* Part of SWI-Prolog 2 3 Author: Jan Wielemaker 4 E-mail: J.Wielemaker@vu.nl 5 WWW: http://www.swi-prolog.org 6 Copyright (c) 2010-2011, VU University Amsterdam 7 All rights reserved. 8 9 Redistribution and use in source and binary forms, with or without 10 modification, are permitted provided that the following conditions 11 are met: 12 13 1. Redistributions of source code must retain the above copyright 14 notice, this list of conditions and the following disclaimer. 15 16 2. Redistributions in binary form must reproduce the above copyright 17 notice, this list of conditions and the following disclaimer in 18 the documentation and/or other materials provided with the 19 distribution. 20 21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 32 POSSIBILITY OF SUCH DAMAGE. 33*/ 34 35:- module(coinduction, 36 [ (coinductive)/1, 37 op(1150, fx, (coinductive)) 38 ]). 39:- use_module(library(error)). 40 41/** <module> Co-Logic Programming 42 43This simple module implements the directive coinductive/1 as described 44in "Co-Logic Programming: Extending Logic Programming with Coinduction" 45by Luke Simon et al. The idea behind coinduction is that a goal succeeds 46if it unifies to a parent goal. This enables some interesting programs, 47notably on infinite trees (cyclic terms). 48 49 == 50 :- use_module(library(coinduction)). 51 52 :- coinductive p/1. 53 54 p([1|T]) :- p(T). 55 == 56 57This predicate is true for any cyclic list containing only 1-s, 58regardless of the cycle-length. 59 60@bug Programs mixing normal predicates and coinductive predicates must 61 be _stratified_. The theory does not apply to normal Prolog calling 62 coinductive predicates, calling normal Prolog predicates, etc. 63 64 Stratification is not checked or enforced in any other way and thus 65 left as a responsibility to the user. 66@see "Co-Logic Programming: Extending Logic Programming with Coinduction" 67 by Luke Simon et al. 68*/ 69 70:- multifile 71 system:term_expansion/2, 72 coinductive_declaration/2. % Head, Module 73 74%! head(+Term, -QHead) is semidet. 75% 76% Must be first to allow reloading! 77 78head(Var, _) :- 79 var(Var), !, fail. 80head((H:-_B), Head) :- 81 !, 82 head(H, Head). 83head(H, Head) :- 84 ( H = _:_ 85 -> Head = H 86 ; prolog_load_context(module, M), 87 Head = M:H 88 ). 89 90%! coinductive(:Spec) 91% 92% The declaration :- coinductive name/arity, ... defines 93% predicates as _coinductive_. The predicate definition is wrapped 94% such that goals unify with their ancestors. This directive must 95% preceed all clauses of the predicate. 96 97coinductive(Spec) :- 98 throw(error(context_error(nodirective, coinductive(Spec)), _)). 99 100expand_coinductive_declaration(Spec, Clauses) :- 101 prolog_load_context(module, Module), 102 phrase(expand_specs(Spec, Module), Clauses). 103 104expand_specs(Var, _) --> 105 { var(Var), 106 !, 107 instantiation_error(Var) 108 }. 109expand_specs(M:Spec, _) --> 110 !, 111 expand_specs(Spec, M). 112expand_specs((A,B), Module) --> 113 !, 114 expand_specs(A, Module), 115 expand_specs(B, Module). 116expand_specs(Head, Module) --> 117 { valid_pi(Head, Name, Arity), 118 functor(GenHead, Name, Arity) 119 }, 120 [ coinduction:coinductive_declaration(GenHead, Module) ]. 121 122 123valid_pi(Name/Arity, Name, Arity) :- 124 must_be(atom, Name), 125 must_be(integer, Arity). 126 127 128%! wrap_coinductive(+Head, +Term, -Clauses) is det. 129% 130% Create a wrapper. The first clause deal with the case where we 131% already created the wrapper. The second creates the wrapper and 132% the first clause. 133 134wrap_coinductive(Pred, Term, Clause) :- 135 current_predicate(_, Pred), 136 !, 137 rename_clause(Term, 'coinductive ', Clause). 138wrap_coinductive(Pred, Term, [Wrapper_1,Wrapper_2,FirstClause]) :- 139 Pred = M:Head, 140 functor(Head, Name, Arity), 141 length(Args, Arity), 142 GenHead =.. [Name|Args], 143 atom_concat('coinductive ', Name, WrappedName), 144 WrappedHead =.. [WrappedName|Args], 145 Wrapper_1 = (GenHead :- 146 prolog_current_frame(F), 147 prolog_frame_attribute(F, parent, FP), 148 prolog_frame_attribute(FP, parent_goal, M:GenHead)), 149 Wrapper_2 = (GenHead :- WrappedHead, coinduction:no_lco), 150 rename_clause(Term, 'coinductive ', FirstClause). 151 152:- public no_lco/0. 153 154no_lco. % true, but do not optimize away 155 156%! rename_clause(+Clause, +Prefix, -Renamed) is det. 157% 158% Rename a clause by prefixing its old name wit h Prefix. 159 160rename_clause((Head :- Body), Prefix, (NewHead :- Body)) :- 161 !, 162 rename_clause(Head, Prefix, NewHead). 163rename_clause(M:Head, Prefix, M:NewHead) :- 164 rename_clause(Head, Prefix, NewHead). 165rename_clause(Head, Prefix, NewHead) :- 166 Head =.. [Name|Args], 167 atom_concat(Prefix, Name, WrapName), 168 NewHead =.. [WrapName|Args]. 169 170 171 /******************************* 172 * EXPANSION HOOKS * 173 *******************************/ 174 175systemterm_expansion((:- coinductive(Spec)), Clauses) :- 176 expand_coinductive_declaration(Spec, Clauses). 177systemterm_expansion(Term, Wrapper) :- 178 head(Term, Module:Head), 179 coinductive_declaration(Head, Module), 180 wrap_coinductive(Module:Head, Term, Wrapper)