eyeprolog

Term input and output

Can a program write Prolog terms to a file and read them back intact?

Prolog terms are data that can travel through text. This example writes two terms to a temporary file, then reopens it to read them back in order, recover variable names and singletons, and detect the end of the stream.

Run it in the playground · Source

The question

What does ISO term I/O guarantee when a term makes the round trip through a text file? Does the term come back the same? Do shared variables stay shared? Can the reader report which variable names it saw?

The example writes its file under /tmp, so run it from the command line.

Writing the fixture

:- initialization(write_fixture).

write_fixture :-
  fixture_path(Path),
  open(Path, write, Stream, [type(text)]),
  write_canonical(Stream, event(sensor_7, online)),
  put_char(Stream, '.'),
  nl(Stream),
  write(Stream, rule(X, X, _Y)),
  put_char(Stream, '.'),
  nl(Stream),
  close(Stream).

The initialization goal runs once before any query. Output predicates do not add the final full stop themselves, so the program writes . and a newline after each term to make it readable again.

Reading it back

report(variable_metadata, checked) :-
  fixture_path(Path),
  open(Path, read, Stream, []),
  read(Stream, _),
  read_term(Stream, rule(A, A, B), [
    variables([A, B]),
    variable_names([NameA=A, NameB=B]),
    singletons([NameB=B])
  ]),
  atom(NameA),
  atom(NameB),
  NameA \== NameB,
  close(Stream).

read_term/3 returns the term together with its metadata. The pattern rule(A, A, B) requires the first two arguments to come back as one shared variable. The options report the two distinct variables, their source names, and the one that occurs only once.

The answer

eyeprolog examples/iso-term-io.pl

report(first_term, event(sensor_7, online)).
report(variable_metadata, checked).
report(reached_end, yes).

The first term comes back unchanged. The second keeps its variable sharing and its singleton. With eof_action(eof_code), a read after the last term returns end_of_file.

The reason

eyeprolog --proof examples/iso-term-io.pl

step(fixture_path('/tmp/eyeprolog-iso-term-io-example.pl'), fact(2), [], []).
step(open('/tmp/eyeprolog-iso-term-io-example.pl', read, '$stream'(1), []), builtin, [], []).
step(read('$stream'(1), event(sensor_7, online)), builtin, [], []).

The first report rests on the path fact and three stream operations. Each operation is recorded with the stream handle and the term it returned.

The check

condition('C1', resolution, ok, 4).
condition('C5', re_decision, ok, 3).
obligation(builtin, stateful, read('$stream'(1), event(sensor_7, online))).
verdict(checked_with_obligations).

The rule steps replay against the program. The stream operations cannot: what read/2 returns depends on a file and a stream position that existed only during the run. The checker lists each of those 13 steps as a stateful obligation. The proof is valid on the condition that the file really held those terms.

Try it

Replace write_canonical/2 with writeq/2 for the first term. Does the round trip still work?
Write a term containing an operator, such as a :- b, with write/2, and read it back.
Remove the put_char(Stream, '.') after the second term. What does the reader do with a term that has no full stop?

Learn more in The Art of EyeProlog, Chapter 37.

This site is open source. Improve this page.