mercurylang/mercury
1
0
Fork 0
mirror of https://github.com/Mercury-Language/mercury.git synced 2026-04-16 01:43:35 +00:00
Code Issues Projects Releases Wiki Activity

Standardize on one interpreter.m.

Browse Source 
samples/interpreter.m:
    Make this the primary copy of interpreter.m. Incorporate the improvements
    from the other two versions in tests, and generalize them to be suitable
    as a sample program.

tests/debugger/interpreter.m:
tests/general/interpreter.m:
    Make these copies of the primary version.

tests/debugger/Mmakefile:
tests/general/Mmakefile:
    Keep the tests copies of the primary version.

tests/general/interpreter.exp:
    Expect an output now generated for parameter-less invocations.
This commit is contained in:
Zoltan Somogyi
2022-03-04 14:45:01 +11:00
parent cd4d855390
commit 92f60e5c70
6 changed files with 520 additions and 411 deletions
Download Patch File Download Diff File Expand all files Collapse all files

310
samples/interpreter.m
View File

@@ -1,5 +1,5 @@
%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
% vim: ts=4 sw=4 et ft=mercury
%---------------------------------------------------------------------------%
%
% File: interpreter.m.
@@ -9,9 +9,9 @@
% (i.e. pure Prolog with no negation or if-then-else.)
%
% This is just intended as a demonstration of the use of the
% meta-programming library modules term, varset, and term_io.
% meta-programming library modules term, term_io, and varset.
%
% There are many extensions that could be made;
% There are many extensions/improvements that could be made;
% they are left as an exercise for the reader.
%
% For a more efficient version (using backtrackable destructive update),
@@ -20,6 +20,10 @@
% This source file is hereby placed in the public domain. -fjh (the author).
%
%---------------------------------------------------------------------------%
%
% This module is also used as a test case in two test directories, debugger
% and general.
%
%---------------------------------------------------------------------------%
:- module interpreter.
@@ -33,6 +37,7 @@
:- implementation.
:- import_module list.
:- import_module mercury_term_parser.
:- import_module require.
:- import_module solutions.
:- import_module string.
@@ -40,77 +45,54 @@
:- import_module term_io.
:- import_module varset.
%---------------------------------------------------------------------------%
main(!IO) :-
io.write_string("Pure Prolog Interpreter.\n\n", !IO),
io.command_line_arguments(Args, !IO),
database_init(Database0),
(
Args = [],
io.stderr_stream(StdErr, !IO),
io.write_string(StdErr, "Usage: interpreter <filename> ...\n", !IO),
io.set_exit_status(1, !IO)
io.write_string("No files consulted.\n", !IO),
Database = Database0
;
Args = [_ | _],
database_init(Database0),
consult_files(Args, Database0, Database, !IO),
consult_files(Args, Database0, Database, !IO)
),
main_loop(Database, !IO).
:- pred main_loop(database::in, io::di, io::uo) is det.
main_loop(Database, !IO) :-
io.write_string("?- ", !IO),
read_term(ReadTerm, !IO),
(
ReadTerm = eof
;
ReadTerm = error(ErrorMessage, LineNumber),
io.format("Error reading term at line %d of standard input: %s\n",
[i(LineNumber), s(ErrorMessage)], !IO),
main_loop(Database, !IO)
;
ReadTerm = term(VarSet0, Goal),
% Any special commands with side-effects (such as `consult'
% and `listing') could be identified and processed here.
solutions(solve(Database, Goal, VarSet0), Solutions),
(
Solutions = [],
io.write_string("No.\n", !IO)
;
Solutions = [_ | _],
write_solutions(Solutions, Goal, !IO),
io.write_string("Yes.\n", !IO)
),
main_loop(Database, !IO)
).
%---------------------------------------------------------------------------%
:- pred write_solutions(list(varset)::in, term::in, io::di, io::uo) is det.
% We store the database as a list of clauses.
%
% This makes the code simple and readable, but it severely limits its
% performance on anything bigger than toy programs.
%
% It would be more realistic to index the database on the predicate name/arity,
% and subindex on the name/arity of the first argument.
:- type database == list(clause).
:- type clause
---> clause(
clause_vars :: varset,
clause_head :: term,
clause_body :: term
).
:- pred database_init(database::out) is det.
database_init([]).
:- pred database_assert_clause(varset::in, term::in,
database::in, database::out) is det.
database_assert_clause(VarSet, Term, !Database) :-
( if Term = term.functor(term.atom(":-"), [HeadPrime, BodyPrime], _) then
% Term is a rule.
Head = HeadPrime,
Body = BodyPrime
else
% Term is a fact.
Head = Term,
term.context_init(Context),
Body = term.functor(term.atom("true"), [], Context)
),
Clause = clause(VarSet, Head, Body),
!:Database = [Clause | !.Database].
% database_lookup_clause(Database, Goal, VarSet, Head, Body):
%
% For each clause in Database whose head may unify with Goal,
% return the representation of that clause: its varset, head and body.
%
% Since our database has no indexing, we ignore the goal, and return
% *all* clauses.
%
:- pred database_lookup_clause(database::in, term::in, varset::out,
term::out, term::out) is nondet.
database_lookup_clause(Database, _Goal, VarSet, Head, Body) :-
list.member(Clause, Database),
Clause = clause(VarSet, Head, Body).
write_solutions([], _, !IO).
write_solutions([VarSet | VarSets], Goal, !IO) :-
term_io.write_term_nl(VarSet, Goal, !IO),
write_solutions(VarSets, Goal, !IO).
%---------------------------------------------------------------------------%
@@ -118,66 +100,42 @@ database_lookup_clause(Database, _Goal, VarSet, Head, Body) :-
io::di, io::uo) is det.
consult_files([], !Database, !IO).
consult_files([FileName | FileNames], !Database, !IO) :-
consult_file(FileName, !Database, !IO),
consult_files(FileNames, !Database, !IO).
consult_files([File | Files], !Database, !IO) :-
consult_file(File, !Database, !IO),
consult_files(Files, !Database, !IO).
:- pred consult_file(string::in, database::in, database::out,
io::di, io::uo) is det.
consult_file(FileName, !Database, !IO) :-
io.format("Consulting file `%s'...\n", [s(FileName)], !IO),
io.see(FileName, Result, !IO),
consult_file(File, Database0, Database, !IO) :-
io.format("Consulting file `%s'...\n", [s(File)], !IO),
io.open_input(File, OpenResult, !IO),
(
Result = ok,
consult_until_eof(!Database, !IO),
io.seen(!IO)
OpenResult = ok(Stream),
consult_until_eof(Stream, Database0, Database, !IO),
io.close_input(Stream, !IO)
;
Result = error(Error),
io.error_message(Error, ErrorMessage),
io.format("Error opening file `%s' for input: %s\n",
[s(FileName), s(ErrorMessage)], !IO)
OpenResult = error(_),
io.format("Error opening file `%s' for input.\n", [s(File)], !IO),
Database = Database0
).
:- pred consult_until_eof(database::in, database::out, io::di, io::uo) is det.
:- pred consult_until_eof(io.text_input_stream::in,
database::in, database::out, io::di, io::uo) is det.
consult_until_eof(!Database, !IO) :-
term_io.read_term(ReadTerm, !IO),
consult_until_eof(Stream, !Database, !IO) :-
read_term(Stream, ReadTerm, !IO),
(
ReadTerm = eof
;
ReadTerm = error(ErrorMessage, LineNumber),
io.format("Error reading term at line %d of standard input: %s\n",
[i(LineNumber), s(ErrorMessage)], !IO),
consult_until_eof(!Database, !IO)
consult_until_eof(Stream, !Database, !IO)
;
ReadTerm = term(VarSet, Term),
database_assert_clause(VarSet, Term, !Database),
consult_until_eof(!Database, !IO)
).
%---------------------------------------------------------------------------%
:- pred main_loop(database::in, io::di, io::uo) is det.
main_loop(Database, !IO) :-
io.write_string("?- ", !IO),
io.flush_output(!IO),
term_io.read_term(ReadTerm, !IO),
(
ReadTerm = eof
;
ReadTerm = error(ErrorMessage, LineNumber),
io.format("Error reading term at line %d of standard input: %s\n",
[i(LineNumber), s(ErrorMessage)], !IO),
main_loop(Database, !IO)
;
ReadTerm = term(VarSet, Goal),
% Any special queries with side-effects, such as `consult' or
% `listing', should be identified and processed here.
solutions(solve(Database, Goal, VarSet), SolutionVarSets),
write_solutions(SolutionVarSets, Goal, !IO),
main_loop(Database, !IO)
consult_until_eof(Stream, !Database, !IO)
).
%---------------------------------------------------------------------------%
@@ -188,15 +146,15 @@ main_loop(Database, !IO) :-
% producing a new substitution and perhaps introducing some new vars,
% and returns the varset thus updated as the result.
%
% We represent goals simply as terms. We parse (i.e. discover the structure
% of) the body of each clause every time we interpret that clause.
% Definite logic programs do not allow disjunctions in the bodies
% of clauses, but we do, so for us, each clause is a boolean expression
% built up (using the conjunction operator "," and/or the disjunction
% operator ";") from three kinds of primitives: `true', unifications,
% and calls to user-defined predicates.
% We represent goals simply as terms. We parse (i.e. we discover
% the structure of) the body of each clause every time we interpret
% that clause. Definite logic programs do not allow disjunctions
% in the bodies of clauses, but we do, so for us, each clause is
% a boolean expression built up (using the conjunction operator ","
% and/or the disjunction operator ";") from three kinds of primitives:
% `true', unifications, and calls to user-defined predicates.
%
% Parsing each clause just once, before it is put into the database,
% Parsing each clause just once, before we put it into the database,
% would be more efficient.
%
% Not looking up the database of user-defined predicates on goals
@@ -207,7 +165,7 @@ main_loop(Database, !IO) :-
solve(Database, Goal, !VarSet) :-
(
Goal = term.functor(term.atom(","), [SubGoalA, SubGoalB], _),
Goal = term.functor(term.atom(", "), [SubGoalA, SubGoalB], _),
solve(Database, SubGoalA, !VarSet),
solve(Database, SubGoalB, !VarSet)
;
@@ -227,6 +185,8 @@ solve(Database, Goal, !VarSet) :-
solve(Database, Body, !VarSet)
).
%---------------------------------------------------------------------------%
:- pred rename_apart(varset::in, list(term)::in, list(term)::out,
varset::in, varset::out) is det.
@@ -282,8 +242,8 @@ unify_term_pair(TermX, TermY, !VarSet) :-
( if VarX = VarY then
true
else
varset.bind_var(VarX, term.variable(VarY, context_init),
!VarSet)
TermY = term.variable(VarY, term.context_init),
varset.bind_var(VarX, TermY, !VarSet)
)
)
)
@@ -328,38 +288,6 @@ unify_term_pairs([TermX | TermXs], [TermY | TermYs], !VarSet) :-
unify_term_pair(TermX, TermY, !VarSet),
unify_term_pairs(TermXs, TermYs, !VarSet).
%---------------------------------------------------------------------------%
% apply_rec_substitution(VarSet, Term0, Term):
%
% Recursively apply the substitution in VarSet to Term0 until no more
% substitutions can be applied. Return the result as Term.
%
:- pred apply_rec_substitution(varset::in, term::in, term::out) is det.
apply_rec_substitution(VarSet, Term0, Term) :-
(
Term0 = term.variable(Var0, _),
( if varset.search_var(VarSet, Var0, ReplacementTerm1) then
% Recursively apply the substitution to the replacement.
apply_rec_substitution(VarSet, ReplacementTerm1, Term)
else
Term = Term0
)
;
Term0 = term.functor(Functor, ArgTerms0, Context),
apply_rec_substitution_to_list(VarSet, ArgTerms0, ArgTerms),
Term = term.functor(Functor, ArgTerms, Context)
).
:- pred apply_rec_substitution_to_list(varset::in,
list(term)::in, list(term)::out) is det.
apply_rec_substitution_to_list(_VarSet, [], []).
apply_rec_substitution_to_list(VarSet, [Term0 | Terms0], [Term | Terms]) :-
apply_rec_substitution(VarSet, Term0, Term),
apply_rec_substitution_to_list(VarSet, Terms0, Terms).
%---------------------------------------------------------------------------%
% var_occurs_in_term(VarX, TermY, VarSet):
@@ -403,25 +331,85 @@ var_occurs_in_terms(VarX, [TermY | TermsY], VarSet) :-
%---------------------------------------------------------------------------%
:- pred write_solutions(list(varset)::in, term::in, io::di, io::uo) is det.
% apply_rec_substitution(VarSet, Term0, Term):
%
% Recursively apply substitution to Term0 until no more substitions
% can be applied, and then return the result in Term.
%
:- pred apply_rec_substitution(varset::in, term::in, term::out) is det.
write_solutions(VarSets, Goal, !IO) :-
apply_rec_substitution(VarSet, Term0, Term) :-
(
VarSets = [],
io.write_string("No.\n", !IO)
Term0 = term.variable(Var, _),
( if varset.search_var(VarSet, Var, Replacement) then
% Recursively apply the substitution to the replacement.
apply_rec_substitution(VarSet, Replacement, Term)
else
Term = term.variable(Var, context_init)
)
;
VarSets = [_ | _],
write_each_solution(VarSets, Goal, !IO),
io.write_string("Yes.\n", !IO)
Term0 = term.functor(Name, ArgTerms0, Context),
apply_rec_substitution_to_list(VarSet, ArgTerms0, ArgTerms),
Term = term.functor(Name, ArgTerms, Context)
).
:- pred write_each_solution(list(varset)::in, term::in, io::di, io::uo) is det.
:- pred apply_rec_substitution_to_list(varset::in, list(term)::in,
list(term)::out) is det.
write_each_solution([], _, !IO).
write_each_solution([VarSet | VarSets], Goal, !IO) :-
term_io.write_term_nl(VarSet, Goal, !IO),
write_each_solution(VarSets, Goal, !IO).
apply_rec_substitution_to_list(_VarSet, [], []).
apply_rec_substitution_to_list(VarSet, [Term0 | Terms0], [Term | Terms]) :-
apply_rec_substitution(VarSet, Term0, Term),
apply_rec_substitution_to_list(VarSet, Terms0, Terms).
%---------------------------------------------------------------------------%
:- end_module interpreter.
% We store the database just as a list of clauses.
%
% This makes the code simple and readable, but it severely limits its
% performance on anything bigger than toy programs.
%
% It would be more realistic to index the database on the predicate name/arity,
% and subindex on the name/arity of the first argument.
:- type database == list(clause).
:- type clause
---> clause(
clause_vars :: varset,
clause_head :: term,
clause_body :: term
).
:- pred database_init(database::out) is det.
database_init([]).
:- pred database_assert_clause(varset::in, term::in,
database::in, database::out) is det.
database_assert_clause(VarSet, Term, Database, [Clause | Database]) :-
( if Term = term.functor(term.atom(":-"), [H, B], _) then
Head = H,
Body = B
else
Head = Term,
term.context_init(Context),
Body = term.functor(term.atom("true"), [], Context)
),
Clause = clause(VarSet, Head, Body).
% database_lookup_clause(Database, Goal, VarSet, Head, Body):
%
% For each clause in Database whose head may unify with Goal,
% return the representation of that clause: its varset, head and body.
%
% Since our database has no indexing, we ignore the goal, and return
% *all* the clauses.
%
:- pred database_lookup_clause(database::in, term::in,
varset::out, term::out, term::out) is nondet.
database_lookup_clause(Database, _Goal, VarSet, Head, Body) :-
list.member(Clause, Database),
Clause = clause(VarSet, Head, Body).
%---------------------------------------------------------------------------%

5
tests/debugger/Mmakefile
View File

@@ -474,6 +474,11 @@ loopcheck.out: loopcheck loopcheck.$(INP)
true; \
fi
interpreter.m: ../../samples/interpreter.m
chmod u+w interpreter.m
cp ../../samples/interpreter.m .
chmod a-w interpreter.m
interpreter.out: interpreter interpreter.inp
$(MDB_STD) ./interpreter interpreter.m < interpreter.inp \
> interpreter.out 2>&1

305
tests/debugger/interpreter.m
View File

@@ -9,7 +9,7 @@
% (i.e. pure Prolog with no negation or if-then-else.)
%
% This is just intended as a demonstration of the use of the
% meta-programming library modules term, varset, and term_io.
% meta-programming library modules term, term_io, and varset.
%
% There are many extensions/improvements that could be made;
% they are left as an exercise for the reader.
@@ -21,8 +21,8 @@
%
%---------------------------------------------------------------------------%
%
% The .exp file is for XXX.
% The .exp2 file is for asm_fast.gc bootchecks.
% This module is also used as a test case in two test directories, debugger
% and general.
%
%---------------------------------------------------------------------------%
@@ -46,14 +46,17 @@
:- import_module varset.
main(!IO) :-
io.command_line_arguments(Args, !IO),
% We *could* check that Args is non-empty, but the version of this test
% in tests/general is invoked with Args = [], which works because
% queries it is given do not refer to any predicates (they consist
% solely of unifications).
io.write_string("Pure Prolog Interpreter.\n\n", !IO),
io.command_line_arguments(Args, !IO),
database_init(Database0),
consult_files(Args, Database0, Database, !IO),
(
Args = [],
io.write_string("No files consulted.\n", !IO),
Database = Database0
;
Args = [_ | _],
consult_files(Args, Database0, Database, !IO)
),
main_loop(Database, !IO).
:- pred main_loop(database::in, io::di, io::uo) is det.
@@ -137,38 +140,48 @@ consult_until_eof(Stream, !Database, !IO) :-
%---------------------------------------------------------------------------%
% Solve takes a database of rules and facts, a goal to be solved,
% and a varset (which includes a supply of fresh vars, a substitution,
% and names for [some subset of] the variables). It updates the varset,
% producing a new substitution and perhaps introducing some new vars,
% and returns the result.
% Goals are stored just as terms.
% (It might be more efficient to parse them before storing them
% in the database. Currently we do this parsing work every time
% we interpret a clause.)
% Solve takes a database of rules and facts, a goal to be solved,
% and a varset (which includes a supply of fresh vars, a substitution,
% and names for [some subset of] the variables). It updates the varset,
% producing a new substitution and perhaps introducing some new vars,
% and returns the varset thus updated as the result.
%
% We represent goals simply as terms. We parse (i.e. we discover
% the structure of) the body of each clause every time we interpret
% that clause. Definite logic programs do not allow disjunctions
% in the bodies of clauses, but we do, so for us, each clause is
% a boolean expression built up (using the conjunction operator ","
% and/or the disjunction operator ";") from three kinds of primitives:
% `true', unifications, and calls to user-defined predicates.
%
% Parsing each clause just once, before we put it into the database,
% would be more efficient.
%
% Not looking up the database of user-defined predicates on goals
% whose top-level functor is ,/2, ;/2, true/0 or =/2 would also be
% more efficient, as well as semantically cleaner.
%
:- pred solve(database::in, term::in, varset::in, varset::out) is nondet.
solve(Database, Goal, !VarSet) :-
(
Goal = term.functor(term.atom("true"), [], _)
Goal = term.functor(term.atom(", "), [SubGoalA, SubGoalB], _),
solve(Database, SubGoalA, !VarSet),
solve(Database, SubGoalB, !VarSet)
;
Goal = term.functor(term.atom(", "), [A, B], _),
solve(Database, A, !VarSet),
solve(Database, B, !VarSet)
;
Goal = term.functor(term.atom(";"), [A, B], _),
( solve(Database, A, !VarSet)
; solve(Database, B, !VarSet)
Goal = term.functor(term.atom(";"), [SubGoalA, SubGoalB], _),
( solve(Database, SubGoalA, !VarSet)
; solve(Database, SubGoalB, !VarSet)
)
;
Goal = term.functor(term.atom("="), [A, B], _),
unify(A, B, !VarSet)
Goal = term.functor(term.atom("true"), [], _)
;
Goal = term.functor(term.atom("="), [TermA, TermB], _),
unify_term_pair(TermA, TermB, !VarSet)
;
database_lookup_clause(Database, Goal, ClauseVarSet, Head0, Body0),
rename_apart(ClauseVarSet, [Head0, Body0], [Head, Body], !VarSet),
unify(Goal, Head, !VarSet),
unify_term_pair(Goal, Head, !VarSet),
solve(Database, Body, !VarSet)
).
@@ -182,112 +195,138 @@ rename_apart(NewVarSet, Terms0, Terms, VarSet0, VarSet) :-
%---------------------------------------------------------------------------%
% The standard library module `term' contains routines for
% unifying terms based on separate substitutions, but we are
% using the substitutions that are contained in the `varset',
% so we can't use those versions.
:- pred unify(term::in, term::in, varset::in, varset::out) is semidet.
unify(TermX, TermY, !VarSet) :-
(
TermX = term.variable(X, _),
TermY = term.variable(Y, _),
( if varset.search_var(!.VarSet, X, BindingOfX) then
( if varset.search_var(!.VarSet, Y, BindingOfY) then
% Both X and Y already have bindings:
% just unify the terms they are bound to.
unify(BindingOfX, BindingOfY, !VarSet)
else
% Y is an unbound variable.
apply_rec_substitution(!.VarSet,
BindingOfX, SubstBindingOfX),
( if SubstBindingOfX = term.variable(Y, _) then
true
else
not occurs(SubstBindingOfX, Y, !.VarSet),
varset.bind_var(Y, SubstBindingOfX, !VarSet)
)
)
else
( if varset.search_var(!.VarSet, Y, BindingOfY2) then
% X is an unbound variable.
apply_rec_substitution(!.VarSet,
BindingOfY2, SubstBindingOfY2),
( if SubstBindingOfY2 = term.variable(X, _) then
true
else
not occurs(SubstBindingOfY2, X, !.VarSet),
varset.bind_var(X, SubstBindingOfY2, !VarSet)
)
else
% Both X and Y are unbound variables: bind one to the other.
( if X = Y then
true
else
varset.bind_var(X, term.variable(Y, context_init), !VarSet)
)
)
)
;
TermX = term.variable(X, _),
TermY = term.functor(F, As, C),
( if varset.search_var(!.VarSet, X, BindingOfX) then
unify(BindingOfX, term.functor(F, As, C), !VarSet)
else
not occurs_list(As, X, !.VarSet),
varset.bind_var(X, term.functor(F, As, C), !VarSet)
)
;
TermX = term.functor(F, As, C),
TermY = term.variable(X, _),
( if varset.search_var(!.VarSet, X, BindingOfX) then
unify(term.functor(F, As, C), BindingOfX, !VarSet)
else
not occurs_list(As, X, !.VarSet),
varset.bind_var(X, term.functor(F, As, C), !VarSet)
)
;
TermX = term.functor(F, AsX, _),
TermY = term.functor(F, AsY, _),
unify_list(AsX, AsY, !VarSet)
).
:- pred unify_list(list(term)::in, list(term)::in, varset::in, varset::out)
% unify_term_pair(TermX, TermY, !VarSet):
%
% Unify TermX with TermY, updating the varset if the unification succeeds.
%
% The standard library module `term' contains routines for unifying terms
% based on separate substitutions (maps from variables to terms),
% but here we are using substitutions that are contained in the varset
% itself, so we cannot use those versions.
%
:- pred unify_term_pair(term::in, term::in, varset::in, varset::out)
is semidet.
unify_list([], [], !VarSet).
unify_list([X | Xs], [Y | Ys], !VarSet) :-
unify(X, Y, !VarSet),
unify_list(Xs, Ys, !VarSet).
unify_term_pair(TermX, TermY, !VarSet) :-
(
TermX = term.variable(VarX, _ContextX),
TermY = term.variable(VarY, _ContextY),
( if varset.search_var(!.VarSet, VarX, BindingOfX) then
( if varset.search_var(!.VarSet, VarY, BindingOfY) then
% Both X and Y already have bindings;
% unify the terms they are bound to.
unify_term_pair(BindingOfX, BindingOfY, !VarSet)
else
% X is bound, Y is not. Symmetrical with the opposite case.
apply_rec_substitution(!.VarSet, BindingOfX, SubstBindingOfX),
( if SubstBindingOfX = term.variable(VarY, _) then
true
else
not var_occurs_in_term(VarY, SubstBindingOfX, !.VarSet),
varset.bind_var(VarY, SubstBindingOfX, !VarSet)
)
)
else
( if varset.search_var(!.VarSet, VarY, BindingOfY) then
% Y is bound, X is not. Symmetrical with the opposite case.
apply_rec_substitution(!.VarSet, BindingOfY, SubstBindingOfY),
( if SubstBindingOfY = term.variable(VarX, _) then
true
else
not var_occurs_in_term(VarX, SubstBindingOfY, !.VarSet),
varset.bind_var(VarX, SubstBindingOfY, !VarSet)
)
else
% Both X and Y are unbound variables; bind one to the other.
% It does not matter whether we bind X to Y, or Y to X.
( if VarX = VarY then
true
else
TermY = term.variable(VarY, term.context_init),
varset.bind_var(VarX, TermY, !VarSet)
)
)
)
;
TermX = term.variable(VarX, _ContextX),
TermY = term.functor(_FunctorY, _ArgTermsY, _ContextY),
unify_var_functor(VarX, TermY, !VarSet)
;
TermX = term.functor(_FunctorX, _ArgTermsX, _ContextX),
TermY = term.variable(VarY, _ContextY),
unify_var_functor(VarY, TermX, !VarSet)
;
TermX = term.functor(FunctorX, ArgTermsX, _ContextX),
TermY = term.functor(FunctorY, ArgTermsY, _ContextY),
FunctorX = FunctorY,
unify_term_pairs(ArgTermsX, ArgTermsY, !VarSet)
).
:- inst term_functor for term/1
---> functor(ground, ground, ground).
% Unify a variable with a term that is known to be a functor
% applied to some argument terms.
%
:- pred unify_var_functor(term.var::in, term::in(term_functor),
varset::in, varset::out) is semidet.
unify_var_functor(VarX, TermY, !VarSet) :-
( if varset.search_var(!.VarSet, VarX, BindingOfX) then
unify_term_pair(BindingOfX, TermY, !VarSet)
else
TermY = term.functor(_FunctorY, ArgTermsY, _ContextY),
not var_occurs_in_terms(VarX, ArgTermsY, !.VarSet),
varset.bind_var(VarX, TermY, !VarSet)
).
:- pred unify_term_pairs(list(term)::in, list(term)::in,
varset::in, varset::out) is semidet.
unify_term_pairs([], [], !VarSet).
unify_term_pairs([TermX | TermXs], [TermY | TermYs], !VarSet) :-
unify_term_pair(TermX, TermY, !VarSet),
unify_term_pairs(TermXs, TermYs, !VarSet).
%---------------------------------------------------------------------------%
% occurs(Term, Var, VarSet) succeeds if Term contains Var,
% perhaps indirectly via the substitution represented by VarSet.
% (The variable must not be bound by VarSet.)
% var_occurs_in_term(VarX, TermY, VarSet):
%
:- pred occurs(term::in, var::in, varset::in) is semidet.
% Succeed iff VarX occurs in TermY, either as is,
% or after the substitution in VarSet is applied to TermY.
%
% VarX must not be mapped by the substitution in VarSet.
%
:- pred var_occurs_in_term(var::in, term::in, varset::in) is semidet.
occurs(Term, Y, VarSet) :-
var_occurs_in_term(VarX, TermY, VarSet) :-
(
Term = term.variable(X, _),
TermY = term.variable(VarY, _),
(
X = Y
VarX = VarY
;
varset.search_var(VarSet, X, BindingOfX),
occurs(BindingOfX, Y, VarSet)
varset.search_var(VarSet, VarY, BindingOfY),
var_occurs_in_term(VarX, BindingOfY, VarSet)
)
;
Term = term.functor(_F, As, _),
occurs_list(As, Y, VarSet)
TermY = term.functor(_FunctorY, ArgTermsY, _ContextY),
var_occurs_in_terms(VarX, ArgTermsY, VarSet)
).
:- pred occurs_list(list(term)::in, var::in, varset::in) is semidet.
% var_occurs_in_terms(VarX, TermsY, VarSet):
%
% Succeed iff VarX occurs in any of the TermsY, either as is,
% or after the substitution in VarSet is applied to TermsY.
%
% VarX must not be mapped by the substitution in VarSet.
%
:- pred var_occurs_in_terms(var::in, list(term)::in, varset::in) is semidet.
occurs_list([Term | Terms], Y, VarSet) :-
( occurs(Term, Y, VarSet)
; occurs_list(Terms, Y, VarSet)
var_occurs_in_terms(VarX, [TermY | TermsY], VarSet) :-
(
var_occurs_in_term(VarX, TermY, VarSet)
;
var_occurs_in_terms(VarX, TermsY, VarSet)
).
%---------------------------------------------------------------------------%
@@ -325,12 +364,20 @@ apply_rec_substitution_to_list(VarSet, [Term0 | Terms0], [Term | Terms]) :-
%---------------------------------------------------------------------------%
% We store the database just as a list of clauses.
% (It would be more realistic to index this on the predicate name/arity
% and subindex on the name/arity of the first argument.)
%
% This makes the code simple and readable, but it severely limits its
% performance on anything bigger than toy programs.
%
% It would be more realistic to index the database on the predicate name/arity,
% and subindex on the name/arity of the first argument.
:- type database == list(clause).
:- type clause
---> clause(varset, term, term).
---> clause(
clause_vars :: varset,
clause_head :: term,
clause_body :: term
).
:- pred database_init(database::out) is det.
@@ -350,6 +397,14 @@ database_assert_clause(VarSet, Term, Database, [Clause | Database]) :-
),
Clause = clause(VarSet, Head, Body).
% database_lookup_clause(Database, Goal, VarSet, Head, Body):
%
% For each clause in Database whose head may unify with Goal,
% return the representation of that clause: its varset, head and body.
%
% Since our database has no indexing, we ignore the goal, and return
% *all* the clauses.
%
:- pred database_lookup_clause(database::in, term::in,
varset::out, term::out, term::out) is nondet.

5
tests/general/Mmakefile
View File

@@ -111,6 +111,11 @@ include Mercury.options
# Some test cases need special handling.
#
interpreter.m: ../../samples/interpreter.m
chmod u+w interpreter.m
cp ../../samples/interpreter.m .
chmod a-w interpreter.m
# string_format_test_2 and string_format_test_3 are expected to fail
# (string.format should call error/1 for these test cases)
# so we need to ignore the exit status; hence the leading `-'.

1
tests/general/interpreter.exp
View File

@@ -1,5 +1,6 @@
Pure Prolog Interpreter.
No files consulted.
?- a = a.
Yes.
?- X = X.

305
tests/general/interpreter.m
View File

@@ -9,7 +9,7 @@
% (i.e. pure Prolog with no negation or if-then-else.)
%
% This is just intended as a demonstration of the use of the
% meta-programming library modules term, varset, and term_io.
% meta-programming library modules term, term_io, and varset.
%
% There are many extensions/improvements that could be made;
% they are left as an exercise for the reader.
@@ -21,8 +21,8 @@
%
%---------------------------------------------------------------------------%
%
% The .exp file is for XXX.
% The .exp2 file is for asm_fast.gc bootchecks.
% This module is also used as a test case in two test directories, debugger
% and general.
%
%---------------------------------------------------------------------------%
@@ -46,14 +46,17 @@
:- import_module varset.
main(!IO) :-
io.command_line_arguments(Args, !IO),
% We *could* check that Args is non-empty, but the version of this test
% in tests/general is invoked with Args = [], which works because
% queries it is given do not refer to any predicates (they consist
% solely of unifications).
io.write_string("Pure Prolog Interpreter.\n\n", !IO),
io.command_line_arguments(Args, !IO),
database_init(Database0),
consult_files(Args, Database0, Database, !IO),
(
Args = [],
io.write_string("No files consulted.\n", !IO),
Database = Database0
;
Args = [_ | _],
consult_files(Args, Database0, Database, !IO)
),
main_loop(Database, !IO).
:- pred main_loop(database::in, io::di, io::uo) is det.
@@ -137,38 +140,48 @@ consult_until_eof(Stream, !Database, !IO) :-
%---------------------------------------------------------------------------%
% Solve takes a database of rules and facts, a goal to be solved,
% and a varset (which includes a supply of fresh vars, a substitution,
% and names for [some subset of] the variables). It updates the varset,
% producing a new substitution and perhaps introducing some new vars,
% and returns the result.
% Goals are stored just as terms.
% (It might be more efficient to parse them before storing them
% in the database. Currently we do this parsing work every time
% we interpret a clause.)
% Solve takes a database of rules and facts, a goal to be solved,
% and a varset (which includes a supply of fresh vars, a substitution,
% and names for [some subset of] the variables). It updates the varset,
% producing a new substitution and perhaps introducing some new vars,
% and returns the varset thus updated as the result.
%
% We represent goals simply as terms. We parse (i.e. we discover
% the structure of) the body of each clause every time we interpret
% that clause. Definite logic programs do not allow disjunctions
% in the bodies of clauses, but we do, so for us, each clause is
% a boolean expression built up (using the conjunction operator ","
% and/or the disjunction operator ";") from three kinds of primitives:
% `true', unifications, and calls to user-defined predicates.
%
% Parsing each clause just once, before we put it into the database,
% would be more efficient.
%
% Not looking up the database of user-defined predicates on goals
% whose top-level functor is ,/2, ;/2, true/0 or =/2 would also be
% more efficient, as well as semantically cleaner.
%
:- pred solve(database::in, term::in, varset::in, varset::out) is nondet.
solve(Database, Goal, !VarSet) :-
(
Goal = term.functor(term.atom("true"), [], _)
Goal = term.functor(term.atom(", "), [SubGoalA, SubGoalB], _),
solve(Database, SubGoalA, !VarSet),
solve(Database, SubGoalB, !VarSet)
;
Goal = term.functor(term.atom(", "), [A, B], _),
solve(Database, A, !VarSet),
solve(Database, B, !VarSet)
;
Goal = term.functor(term.atom(";"), [A, B], _),
( solve(Database, A, !VarSet)
; solve(Database, B, !VarSet)
Goal = term.functor(term.atom(";"), [SubGoalA, SubGoalB], _),
( solve(Database, SubGoalA, !VarSet)
; solve(Database, SubGoalB, !VarSet)
)
;
Goal = term.functor(term.atom("="), [A, B], _),
unify(A, B, !VarSet)
Goal = term.functor(term.atom("true"), [], _)
;
Goal = term.functor(term.atom("="), [TermA, TermB], _),
unify_term_pair(TermA, TermB, !VarSet)
;
database_lookup_clause(Database, Goal, ClauseVarSet, Head0, Body0),
rename_apart(ClauseVarSet, [Head0, Body0], [Head, Body], !VarSet),
unify(Goal, Head, !VarSet),
unify_term_pair(Goal, Head, !VarSet),
solve(Database, Body, !VarSet)
).
@@ -182,112 +195,138 @@ rename_apart(NewVarSet, Terms0, Terms, VarSet0, VarSet) :-
%---------------------------------------------------------------------------%
% The standard library module `term' contains routines for
% unifying terms based on separate substitutions, but we are
% using the substitutions that are contained in the `varset',
% so we can't use those versions.
:- pred unify(term::in, term::in, varset::in, varset::out) is semidet.
unify(TermX, TermY, !VarSet) :-
(
TermX = term.variable(X, _),
TermY = term.variable(Y, _),
( if varset.search_var(!.VarSet, X, BindingOfX) then
( if varset.search_var(!.VarSet, Y, BindingOfY) then
% Both X and Y already have bindings:
% just unify the terms they are bound to.
unify(BindingOfX, BindingOfY, !VarSet)
else
% Y is an unbound variable.
apply_rec_substitution(!.VarSet,
BindingOfX, SubstBindingOfX),
( if SubstBindingOfX = term.variable(Y, _) then
true
else
not occurs(SubstBindingOfX, Y, !.VarSet),
varset.bind_var(Y, SubstBindingOfX, !VarSet)
)
)
else
( if varset.search_var(!.VarSet, Y, BindingOfY2) then
% X is an unbound variable.
apply_rec_substitution(!.VarSet,
BindingOfY2, SubstBindingOfY2),
( if SubstBindingOfY2 = term.variable(X, _) then
true
else
not occurs(SubstBindingOfY2, X, !.VarSet),
varset.bind_var(X, SubstBindingOfY2, !VarSet)
)
else
% Both X and Y are unbound variables: bind one to the other.
( if X = Y then
true
else
varset.bind_var(X, term.variable(Y, context_init), !VarSet)
)
)
)
;
TermX = term.variable(X, _),
TermY = term.functor(F, As, C),
( if varset.search_var(!.VarSet, X, BindingOfX) then
unify(BindingOfX, term.functor(F, As, C), !VarSet)
else
not occurs_list(As, X, !.VarSet),
varset.bind_var(X, term.functor(F, As, C), !VarSet)
)
;
TermX = term.functor(F, As, C),
TermY = term.variable(X, _),
( if varset.search_var(!.VarSet, X, BindingOfX) then
unify(term.functor(F, As, C), BindingOfX, !VarSet)
else
not occurs_list(As, X, !.VarSet),
varset.bind_var(X, term.functor(F, As, C), !VarSet)
)
;
TermX = term.functor(F, AsX, _),
TermY = term.functor(F, AsY, _),
unify_list(AsX, AsY, !VarSet)
).
:- pred unify_list(list(term)::in, list(term)::in, varset::in, varset::out)
% unify_term_pair(TermX, TermY, !VarSet):
%
% Unify TermX with TermY, updating the varset if the unification succeeds.
%
% The standard library module `term' contains routines for unifying terms
% based on separate substitutions (maps from variables to terms),
% but here we are using substitutions that are contained in the varset
% itself, so we cannot use those versions.
%
:- pred unify_term_pair(term::in, term::in, varset::in, varset::out)
is semidet.
unify_list([], [], !VarSet).
unify_list([X | Xs], [Y | Ys], !VarSet) :-
unify(X, Y, !VarSet),
unify_list(Xs, Ys, !VarSet).
unify_term_pair(TermX, TermY, !VarSet) :-
(
TermX = term.variable(VarX, _ContextX),
TermY = term.variable(VarY, _ContextY),
( if varset.search_var(!.VarSet, VarX, BindingOfX) then
( if varset.search_var(!.VarSet, VarY, BindingOfY) then
% Both X and Y already have bindings;
% unify the terms they are bound to.
unify_term_pair(BindingOfX, BindingOfY, !VarSet)
else
% X is bound, Y is not. Symmetrical with the opposite case.
apply_rec_substitution(!.VarSet, BindingOfX, SubstBindingOfX),
( if SubstBindingOfX = term.variable(VarY, _) then
true
else
not var_occurs_in_term(VarY, SubstBindingOfX, !.VarSet),
varset.bind_var(VarY, SubstBindingOfX, !VarSet)
)
)
else
( if varset.search_var(!.VarSet, VarY, BindingOfY) then
% Y is bound, X is not. Symmetrical with the opposite case.
apply_rec_substitution(!.VarSet, BindingOfY, SubstBindingOfY),
( if SubstBindingOfY = term.variable(VarX, _) then
true
else
not var_occurs_in_term(VarX, SubstBindingOfY, !.VarSet),
varset.bind_var(VarX, SubstBindingOfY, !VarSet)
)
else
% Both X and Y are unbound variables; bind one to the other.
% It does not matter whether we bind X to Y, or Y to X.
( if VarX = VarY then
true
else
TermY = term.variable(VarY, term.context_init),
varset.bind_var(VarX, TermY, !VarSet)
)
)
)
;
TermX = term.variable(VarX, _ContextX),
TermY = term.functor(_FunctorY, _ArgTermsY, _ContextY),
unify_var_functor(VarX, TermY, !VarSet)
;
TermX = term.functor(_FunctorX, _ArgTermsX, _ContextX),
TermY = term.variable(VarY, _ContextY),
unify_var_functor(VarY, TermX, !VarSet)
;
TermX = term.functor(FunctorX, ArgTermsX, _ContextX),
TermY = term.functor(FunctorY, ArgTermsY, _ContextY),
FunctorX = FunctorY,
unify_term_pairs(ArgTermsX, ArgTermsY, !VarSet)
).
:- inst term_functor for term/1
---> functor(ground, ground, ground).
% Unify a variable with a term that is known to be a functor
% applied to some argument terms.
%
:- pred unify_var_functor(term.var::in, term::in(term_functor),
varset::in, varset::out) is semidet.
unify_var_functor(VarX, TermY, !VarSet) :-
( if varset.search_var(!.VarSet, VarX, BindingOfX) then
unify_term_pair(BindingOfX, TermY, !VarSet)
else
TermY = term.functor(_FunctorY, ArgTermsY, _ContextY),
not var_occurs_in_terms(VarX, ArgTermsY, !.VarSet),
varset.bind_var(VarX, TermY, !VarSet)
).
:- pred unify_term_pairs(list(term)::in, list(term)::in,
varset::in, varset::out) is semidet.
unify_term_pairs([], [], !VarSet).
unify_term_pairs([TermX | TermXs], [TermY | TermYs], !VarSet) :-
unify_term_pair(TermX, TermY, !VarSet),
unify_term_pairs(TermXs, TermYs, !VarSet).
%---------------------------------------------------------------------------%
% occurs(Term, Var, VarSet) succeeds if Term contains Var,
% perhaps indirectly via the substitution represented by VarSet.
% (The variable must not be bound by VarSet.)
% var_occurs_in_term(VarX, TermY, VarSet):
%
:- pred occurs(term::in, var::in, varset::in) is semidet.
% Succeed iff VarX occurs in TermY, either as is,
% or after the substitution in VarSet is applied to TermY.
%
% VarX must not be mapped by the substitution in VarSet.
%
:- pred var_occurs_in_term(var::in, term::in, varset::in) is semidet.
occurs(Term, Y, VarSet) :-
var_occurs_in_term(VarX, TermY, VarSet) :-
(
Term = term.variable(X, _),
TermY = term.variable(VarY, _),
(
X = Y
VarX = VarY
;
varset.search_var(VarSet, X, BindingOfX),
occurs(BindingOfX, Y, VarSet)
varset.search_var(VarSet, VarY, BindingOfY),
var_occurs_in_term(VarX, BindingOfY, VarSet)
)
;
Term = term.functor(_F, As, _),
occurs_list(As, Y, VarSet)
TermY = term.functor(_FunctorY, ArgTermsY, _ContextY),
var_occurs_in_terms(VarX, ArgTermsY, VarSet)
).
:- pred occurs_list(list(term)::in, var::in, varset::in) is semidet.
% var_occurs_in_terms(VarX, TermsY, VarSet):
%
% Succeed iff VarX occurs in any of the TermsY, either as is,
% or after the substitution in VarSet is applied to TermsY.
%
% VarX must not be mapped by the substitution in VarSet.
%
:- pred var_occurs_in_terms(var::in, list(term)::in, varset::in) is semidet.
occurs_list([Term | Terms], Y, VarSet) :-
( occurs(Term, Y, VarSet)
; occurs_list(Terms, Y, VarSet)
var_occurs_in_terms(VarX, [TermY | TermsY], VarSet) :-
(
var_occurs_in_term(VarX, TermY, VarSet)
;
var_occurs_in_terms(VarX, TermsY, VarSet)
).
%---------------------------------------------------------------------------%
@@ -325,12 +364,20 @@ apply_rec_substitution_to_list(VarSet, [Term0 | Terms0], [Term | Terms]) :-
%---------------------------------------------------------------------------%
% We store the database just as a list of clauses.
% (It would be more realistic to index this on the predicate name/arity
% and subindex on the name/arity of the first argument.)
%
% This makes the code simple and readable, but it severely limits its
% performance on anything bigger than toy programs.
%
% It would be more realistic to index the database on the predicate name/arity,
% and subindex on the name/arity of the first argument.
:- type database == list(clause).
:- type clause
---> clause(varset, term, term).
---> clause(
clause_vars :: varset,
clause_head :: term,
clause_body :: term
).
:- pred database_init(database::out) is det.
@@ -350,6 +397,14 @@ database_assert_clause(VarSet, Term, Database, [Clause | Database]) :-
),
Clause = clause(VarSet, Head, Body).
% database_lookup_clause(Database, Goal, VarSet, Head, Body):
%
% For each clause in Database whose head may unify with Goal,
% return the representation of that clause: its varset, head and body.
%
% Since our database has no indexing, we ignore the goal, and return
% *all* the clauses.
%
:- pred database_lookup_clause(database::in, term::in,
varset::out, term::out, term::out) is nondet.