Converting between implicit and explicit parameters

When declaring a type family or constant, the STELF programmer often has a choice between implicit and explicit parameters for some arguments. There is no reason to fret over this choice, for there is an easy technique for converting between implicit and explicit parameters.

Suppose we have a language defined as follows:

%sort exp %.
%sort typ %.
%sort of {_ exp} {_ typ} %.
%term 0 exp %.
%term 1 exp %.
%term bit typ %.
%term void typ %.
%term of1 of 1 bit %.
%term of0 of 0 bit %.

We wish to define a translation between type derivations in this language, as a part of a source to source translation. The implicit and explicit versions are as follows:

%; %% implicit version
%sort translate-i {_ of M A} {_ of M' A} %.
%mode translate-i %in %out %.
%; %% explicit version
%sort translate-e {m exp} {a typ} {m' exp} {_ of m a} {_ of m' a} %.
%mode translate-e %in %in %out %in %out %.

Defining explicit in terms of implicit

Suppose we choose the implicit version and implement it, but later decide we prefer the explicit version. We can then define the explicit version in terms of the implicit one by simply leaving out arguments:

% implicit version
%sort translate-i {_ of M A} {_ of M' A} %.
%mode translate-i %in %out %.
%term translate-i1 translate-i of1 of0 %.
%term translate-i0 translate-i of0 of1 %.
% explicit version
%sort translate-e {m exp} {a typ} {m' exp} {_ of m a} {_ of m' a} %.
%mode translate-e %in %in %out %in %out %.
%term translate-e/i %pi (translate-e M A M' D D') %<- (translate-i D D') %.
%worlds () (translate-i _ _) (translate-e _ _ _ _ _) %.
%total D (translate-i D _) %.
%total D (translate-e _ _ _ D _) %.

Defining implicit in terms of explicit

Suppose we define the explicit version, and then choose to define the implicit version in terms of the explicit:

% explicit version
%sort translate2-e {m exp} {a typ} {m' exp} {_ of m a} {_ of m' a} %.
%mode translate2-e %in %in %out %in %out %.
%term translate2-e1 translate2-e 1 bit 0 of1 of0 %.
%term translate2-e1 translate2-e 0 bit 1 of0 of1 %.
% implicit version
%sort translate2-i {_ of M A} {_ of M' A} %.
%mode translate2-i %in %out %.
%term translate2-i/e %pi (translate2-i D D') %<- (translate2-e _ _ _ D D') %.
%worlds () (translate2-i _ _) (translate2-e _ _ _ _ _) %.
%total D (translate2-e _ _ _ D _) %.
%total D (translate2-i D _) %.