search

overturetool / overture

The Overture Tool
http://overturetool.org
GNU General Public License v3.0
49 stars 25 forks source link

Record patterns in function parameters are not correctly checked #762

Closed nickbattle closed 3 years ago

nickbattle commented 3 years ago

This came up because of records with "ord" clauses, which produce ord_T functions that are passed record values. If you use a record pattern to match these values, the types are not checked correctly. For example:

types
    T ::
        x: nat
        y: nat;

    R ::
        x: nat
        s: set of nat
    ord mk_R(x, -) < mk_T(a, -) == x < a;

Note that the second pattern in the ord clause uses T rather than R. This is not producing type errors (and fails at runtime).

nickbattle commented 3 years ago

Fix is now available in ncb/development. The spec above produces:

Error 3201: Matching expression is not a compatible record type in 'DEFAULT' (test.vdm) at line 9:22
Pattern type: DEFAULT`T
Expression type: DEFAULT`R