Here's a slightly modified version of the arity-inference algorithm, with
the distinction that we now have a kind "fn" with possible values "call"
and "arg", to make the interpretation of arrow types a bit clearer:
Everything else is as before.
expr(P, var(X), cons(def(X, T), nil), T).
expr(P, nat(X1), nil, nat) :-
nat(X).
expr(P, bool(X), nil, bool) :-
bool(X).
expr(P, pair(X, Y), C3, prod(A, B)) :-
expr(pair, X, C1, A),
expr(pair, Y, C2, B),
append(C1, C2, C3).
expr(app, app(Fun, Arg), Cxt, B) :-
expr(app, Fun, C1, arrow(fn(M), A, B)),
expr(app, Arg, C2, A),
append(C1, C2, Cxt).
expr(P, app(Fun, Arg), Cxt, B) :-
dif(P, app),
expr(app, Fun, C1, arrow(fn(call), A, B)),
expr(app, Arg, C2, A),
append(C1, C2, Cxt).
expr(P, lam(V1, lam(V2, Body)), Cxt, arrow(fn(arg), A, B)) :-
expr(lam, lam(V2, Body), C1, B),
split(V1, C1, Def, Cxt),
unifyall(Def, A).
expr(P, lam(Var, Body), Cxt, arrow(fn(call), A, B)) :-
dif(Body, lam(X, Y)),
expr(lam, Body, C1, B),
split(Var, C1, Def, Cxt),
unifyall(Def, A).
expr(P, let(Var, Body, Rhs), Cxt, T2) :-
expr(let, Body, C1, T1),
expr(let, Rhs, C2, T2),
split(Var, C2, Def, C3),
unifyeach(Def, pair(C1, T1), C4),
append(C3, C4, Cxt).
Keean.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
