Map apply expressions can fail with mismatched key types

[nickbattle]

The following spec fails in 3.0.2:

types
    Beat = <Hourly> | <Daily> | <Weekly>
    ord b1 < b2 ==
        let value = { <Hourly> |-> 1, <Daily>  |-> 2, <Weekly> |-> 3 } in
            value(b1) < value(b2);

    SimpleConversion = inmap Beat to real
    inv sc == sc(<Hourly>) >= 1 and sc(<Weekly>) <= 1;

values
    X :  map Beat to real = { <Hourly> |-> 1, <Daily>  |-> 1/24, <Weekly> |-> 1/(7*24) };

functions
    test: () +> bool
    test() == is_SimpleConversion(X);

> p test()
Error 4061: No such key value in map: <Hourly> in 'DEFAULT' (test.vdm) at line 8:15
Stopped in 'DEFAULT' (test.vdm) at line 8:15
8:      inv sc == sc(<Hourly>) >= 1 and sc(<Weekly>) <= 1;
[MainThread-3]> p sc
sc = {<Hourly> |-> 1, <Daily> |-> 0.041666666666666664, <Weekly> |-> 0.005952380952380952}
[MainThread-3]>

The lookup of <Hourly> fails, even though it is clearly in the domain of the map. The problem is that the value in the map is a Beat value, which has an order clause. That is used to store the range value in a particular branch of a Java TreeMap (which backs the VDM map). But the argument passed to the map apply is a literal <Hourly>, which is a raw quote type. This is not ordered (it has a default ordering, based on the toString), and hence Java searches a different part of the TreeMap, and fails to find the key.

[nickbattle]

The issue can be resolved by treating map applies (and sequence applies) the same way as function applies, where the argument is converted to the parameter type (ie. the domain type of the map, or nat1 for sequences) before the evaluation proceeds. In this case, the raw <Hourly> is converted to a Beat type before searching for it in the TreeMap. This then works as expected.

It's interesting to note that this approach is already taken in assignment statements that lookup a map/sequence designator. So I suspect that an equivalent to this problem has already been found in an assignment context.

[nickbattle]

Fix now available in ncb/development.