Troubleshooting mode checking errors

There are some common pitfalls when you’re dealing with %mode declarations.

Basic mode checking errors

Say we give a definition of the natural numbers with addition:

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%mode plus %in %in %out %.
%term pz plus z N N %.
%term ps %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.

The input of plus is the first and second positions, and the output of plus is the third position, which means that whenever there are ground objects in the first and second positions, that must force a ground object in the third position.

If one of the output arguments is not forced to be a ground, which would be the case if the output of plus no longer matched the output of the subgoal, then we get an error:

px: plus (s N1) N2 (s N)
     <- plus N1 N2 N3.

Another problem occurs when the inputs to a subgoal are not known to be ground, which would happen if we mis-named one of the inputs to the subgoal.

py: plus (s N1) N2 (s N3)
     <- plus N N2 N3.

Ordering subgoals

Mode checking considers subgoals in order, i.e. from top to bottom when the subgoals are written out in the standard style using backwards arrows. The order of subgoals matters very much for mode checking. Say we have an identity function that maps inputs (the first position) to outputs (the second position).

%sort id {_ nat} {_ nat} %.
%mode id %in %out %.
%term id/refl id N N %.

The rule ps' below passes the mode checker, because the call to id takes the ground argument N1 and creates a ground output N1', which is then used in the derivation for plus N1' N2 N3.

ps': plus (s N1) N2 (s N3)
      <- id N1 N1'
      <- plus N1' N2 N3.

However, if we reverse the order of the two subgoals, even though the result is logically equivalent, STELF considers plus N1' N2 N3 before id N1 N1', and so does consider N1' to be ground when it encounters it; thus, complaining accordingly:

ps': plus (s N1) N2 (s N3)
      <- plus N1' N2 N3
      <- id N1 N1'.