%covers

From The Twelf Project
Jump to: navigation, search

A %covers declaration checks input coverage for a type family, which is one of the two kinds of coverage checking that Twelf performs. Running a %total declaration checks input coverage as well as output coverage.

The %covers declaration essentially checks that your type family does an ML-style exhaustive match on its inputs; this does not establish that running your program will succeed, or even terminate!

Example

For this example, we define a type elem with three elements, a, b, c, and a relation rel with three positions. We will then use %covers to check coverage on this relation given a number of different ways of assigning positions as either inputs or outputs.

elem: type.

a: elem.
b: elem.
c: elem.

rel: elem -> elem -> elem -> type.
fail : type.

rel1 : rel a X c.
rel2 : rel b Y b <- fail.
rel3 : rel c c c <- rel c a c.

%worlds () (rel _ _ _) (fail).


The first %covers declaration below checks that rel covers the first position - it does, as there is one case for each of the three possibilities. This is true even though rel b X Y will fail and the query rel c X Y will loop forever. The second declaration checks that rel covers the second position, which happens trivially because the first case, labeled rel1, and the second case rel2, have a metavariable in the second position that matches any possible input.

%covers rel +X1 -X2 -X3.
%covers rel -X1 +X2 -X3.
See Twelf's output


If we try to check coverage on the third position, however, we get an error; the third position does not have a case that handles a.

%covers rel -X1 -X2 +X3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Coverage error --- missing cases: {X1:elem} {X2:elem} |- rel X1 X2 a.

%% ABORT %%


Furthermore, even though we cover the first and second positions individually, if we consider them together we leave out two cases, which is what Twelf's response below explains:

%covers rel +X1 +X2 -X3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Coverage error --- missing cases: {X1:elem} |- rel c a X1, {X1:elem} |- rel c b X1.

%% ABORT %%

Limitations

Coverage checking is a weak test; it only checks that at least one constant will immediately apply during proof search. For example, the following program coverage checks:

bit : type.
0 : bit.
1 : bit.

nope : bit -> type.
%mode nope +B.

not : bit -> bit -> type.
%mode not +B -B'.

n0 : not 0 1.
n1 : not 1 0.

zero : bit -> bit -> type.
%mode zero +B -B'.

cn : zero X 0
  <- nope X.

cz : zero X 0
  <- zero X 1.

cf : zero X 0
  <- not X X.

%worlds () (nope _) (not _ _) (zero _ _).
%covers zero +B -B'.

Although zero passes the coverage check, it always fails. cn matches all inputs, but then appeals to a subgoal (nope) that is empty and immediately fails. cz appeals recursively to zero, but insists that its output be 1, so this also fails. cf appeals to the total relation not, but in a way that constrains the output so that it also always fails (see output freeness). To get all of these tests, you must use the %total declaration. Here, totality fails on the first case as expected:

%total D (zero D _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Termination violation: no order assigned for nope

%% ABORT %%

See also