This simple module implements the directive coinductive/1 as described in "Co-Logic Programming: Extending Logic Programming with Coinduction" by Luke Simon 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 p/1. p([1|T]) :- p(T).
This predicate is true for any cyclic list containing only 1-s, regardless of the cycle-length.
- head(+Term, -QHead) is semidet[private]
- Must be first to allow reloading!
- The declaration :- coinductive name/arity, ... defines predicates as coinductive. The predicate definition is wrapped such that goals unify with their ancestors. This directive must precede all clauses of the predicate.
- wrap_coinductive(+Head, +Term, -Clauses) is det[private]
- Create a wrapper. The first clause deal with the case where we already created the wrapper. The second creates the wrapper and the first clause.
- rename_clause(+Clause, +Prefix, -Renamed) is det[private]
- Rename a clause by prefixing its old name wit h Prefix.