[m-dev.] Successful test of Mercury solver types

[Ralph Becket]

I've got a version of the compiler running that compiles the attached
`church.m' module, an implementation and demonstration of a Church
numerals solver type using the new solver types facility.

Output from the demo:

$ ./church
Before...
A = *
B = succ(succ(succ(*)))
C = succ(succ(succ(succ(succ(zero)))))

After B = C...
A = succ(succ(zero))
B = succ(succ(succ(succ(succ(zero)))))
C = succ(succ(succ(succ(succ(zero)))))

Today, solver types; tomorrow, the world.

TODO: there are a few loose ends to tie up in the compiler and various
documentation jobs left to do.

-- Ralph
-------------- next part --------------
%-----------------------------------------------------------------------------%
% church.m
% Ralph Becket <rafe at cs.mu.oz.au>
% Fri Apr  2 14:31:57 EST 2004
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%
%-----------------------------------------------------------------------------%

:- module church.

:- interface.

:- import_module io.



:- semipure pred main(io :: di, io :: uo) is cc_multi.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- implementation.

:- import_module anyvar.
:- import_module bool.
:- import_module int.
:- import_module list.
:- import_module std_util.
:- import_module string.

%-----------------------------------------------------------------------------%

main(!IO) :-

    A = church_var,
    B = church_plus_n(A, 3),
    C = church_plus_n(church_zero, 5),

    io.format("Before...\n", [], !IO),
    io.format("A = ", [], !IO), semipure print_church(A, !IO), io.nl(!IO),
    io.format("B = ", [], !IO), semipure print_church(B, !IO), io.nl(!IO),
    io.format("C = ", [], !IO), semipure print_church(C, !IO), io.nl(!IO),

    io.format("\nAfter B = C...\n", [], !IO),
    ( if B = C then
        io.format("A = ", [], !IO), semipure print_church(A, !IO), io.nl(!IO),
        io.format("B = ", [], !IO), semipure print_church(B, !IO), io.nl(!IO),
        io.format("C = ", [], !IO), semipure print_church(C, !IO), io.nl(!IO)
      else
        io.format("* unification failed!\n", [], !IO)
    ).

%-----------------------------------------------------------------------------%

:- semipure pred print_church(church::in(any), io::di, io::uo) is cc_multi.
:- pragma promise_semipure(print_church/3).

print_church(A0, !IO) :-
    impure deref(A0, A1),
    impure 'inst cast church/0'(A1, A),
    (
        A = zero,
        io.write_string("zero", !IO)
    ;
        A = succ(A2),
        io.write_string("succ(", !IO),
        semipure print_church(A2, !IO),
        io.write_string(")", !IO)
    ;
        A = var(_),
        io.write_string("*", !IO)
    ).

%-----------------------------------------------------------------------------%

:- func church_zero = (church::out(any)) is det.
:- pragma promise_pure(church_zero/0).

church_zero = A :-
    impure 'inst cast church/0'(A, zero).


:- func church_var = (church::in(any)) is det.

church_var = _.


:- func church_plus_n(church::in(any), int::in) = (church::out(any)) is det.
:- pragma promise_pure(church_plus_n/2).

church_plus_n(A0, N) = A :-
    ( if N = 0 then
        A = A0
      else
        impure 'inst cast church/0'(A1, succ(A0)),
        A = church_plus_n(A1, N - 1)
    ).

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- solver type church
    --->    zero
    ;       succ(church `with_inst` any)
    ;       var(church_var)
    where   initialisation  is  init_church,
            equality        is  eq_church.

:- type church_var == anyvar(maybe(church)).

%-----------------------------------------------------------------------------%

:- pred init_church(church::out(any)) is det.
:- pragma promise_pure(init_church/1).

init_church(A) :-
    impure anyvar.new(no, RefMaybe),
    impure 'inst cast church/0'(A, var(RefMaybe)).

%-----------------------------------------------------------------------------%

:- pred eq_church(church::in(any), church::in(any)) is semidet.

eq_church(A, B) :-
    promise_only_solution(eq_church_2(A, B)) = yes.


:- pred eq_church_2(church::in(any), church::in(any), bool::out) is cc_multi.
:- pragma promise_pure(eq_church_2/3).

eq_church_2(A0, B0, Eq) :-
    impure deref(A0, A1),
    impure deref(B0, B1),
    impure 'inst cast church/0'(A1, A),
    impure 'inst cast church/0'(B1, B),
    (   A = zero,       B = zero,              Eq = yes
    ;   A = zero,       B = succ(_),           Eq = no
    ;   A = zero,       B = var(V),     impure set_church_var_1(V, A, Eq)
    ;   A = succ(_),    B = zero,              Eq = no
    ;   A = succ(A2),   B = succ(B2),          eq_church_2(A2, B2, Eq)
    ;   A = succ(_),    B = var(V),     impure set_church_var_1(V, A, Eq)
    ;   A = var(V),     B = zero,       impure set_church_var_1(V, B, Eq)
    ;   A = var(V),     B = succ(_),    impure set_church_var_1(V, B, Eq)
    ;   A = var(VA),    B = var(VB),    impure set_church_var_2(VA, VB, B, Eq)
    ).


:- impure pred deref(church::in(any), church::out(any)) is cc_multi.

deref(A0, A) :-
    impure 'inst cast church/0'(A0, A1),
    (   A1 = zero,          A = A0
    ;   A1 = succ(_),       A = A0
    ;   A1 = var(V),        impure anyvar.get(V, MaybeA2),
                            (
                                MaybeA2 = no,
                                A       = A0
                            ;
                                MaybeA2 = yes(A2),
                                impure deref(A2, A)
                            )
    ).


:- impure pred set_church_var_1(church_var::in, church::in(any), bool::out)
                    is det.

set_church_var_1(V, A, yes) :-
    impure anyvar.set(V, yes(A)).


:- impure pred set_church_var_2(church_var::in, church_var::in,
                    church::in(any), bool::out) is det.

set_church_var_2(VA, VB, B, yes) :-
    ( if   VA = VB
      then true
      else impure anyvar.set(VA, yes(B))
    ).

%-----------------------------------------------------------------------------%

:- semipure pred is_var(church::in(any)) is semidet.
:- pragma promise_semipure(is_var/1).

is_var(A) :-
    promise_only_solution(is_var_2(A)) = yes.


:- pred is_var_2(church::in(any), bool::out) is cc_multi.
:- pragma promise_pure(is_var_2/2).

is_var_2(A0, IsV) :-
    impure deref(A0, A1),
    impure 'inst cast church/0'(A1, A),
    (   A = zero,       IsV = no
    ;   A = succ(_),    IsV = no
    ;   A = var(_),     IsV = yes
    ).

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%
-------------- next part --------------
%-----------------------------------------------------------------------------%
% anyvar.m
% Ralph Becket <rafe at cs.mu.oz.au>
% Mon Apr 19 11:19:23 EST 2004
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%
% Trailed variables for inst any arguments.
%
%-----------------------------------------------------------------------------%

:- module anyvar.

:- interface.



    % Equality between anyvars is by identity, rather than structural
    % equality.  That is, two anyvars may contain equal values, but
    % not compare equal.  This is unfortunate, but necessary.
    %
:- type anyvar(T).



:- impure pred new(T::in(any), anyvar(T)::out) is det.

    % This is impure, rather than semipure, because we may obtain a
    % non-ground value from a ground anyvar.
    %
:- impure pred get(anyvar(T)::in, T::out(any)) is det.

:- impure pred set(anyvar(T)::in, T::in(any)) is det.

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%

:- implementation.



:- pragma foreign_decl("C", "typedef MR_Word *c_anyvar;").

:- pragma foreign_type("C", anyvar(T), "c_anyvar") where equality is eq.

%-----------------------------------------------------------------------------%

:- pred eq(anyvar(T)::in, anyvar(T)::in) is semidet.
:- pragma promise_pure(eq/2).

:- pragma foreign_proc("C", eq(AnyVarA::in, AnyVarB::in),
    [thread_safe, will_not_call_mercury],
    "
        SUCCESS_INDICATOR = (*AnyVarA == *AnyVarB);
    ").

%-----------------------------------------------------------------------------%

:- pragma foreign_proc("C", new(X::in(any), AnyVar::out),
    [thread_safe, will_not_call_mercury],
    "
        AnyVar = (c_anyvar) MR_GC_NEW(c_anyvar);
        *AnyVar = (MR_Word) X;
    ").

%-----------------------------------------------------------------------------%

:- pragma foreign_proc("C", get(AnyVar::in, X::out(any)),
    [thread_safe, will_not_call_mercury],
    "
        (MR_Word) X = *AnyVar;
    ").

%-----------------------------------------------------------------------------%

    % XXX Is trailing thread_safe?  Or, rather, is threading trail safe :-) ?
    %
:- pragma foreign_proc("C", set(AnyVar::in, X::in(any)),
    [/*thread_safe, */will_not_call_mercury],
    "
        MR_trail_current_value(AnyVar);
        *AnyVar = (MR_Word) X;
    ").

%-----------------------------------------------------------------------------%
%-----------------------------------------------------------------------------%