search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Type check fails for array index expression. #384

Closed gteege closed 4 years ago

gteege commented 4 years ago

Expressions of the form arr@index fail for readonly array arr. In particular, the test case ext-array/pass_array-3.cogent fails with the message

Parsing...
Resolving dependencies...
Typechecking...
Error: Leftover constraint!
Solved A A! [3] [R] () @take (?6)
   in the definition at ("pass_array-3.cogent" (line 2, column 1))
   for the function foo
Error: Leftover constraint!
Solved A A! [3] [R] () @take (?6)
   in the definition at ("pass_array-3.cogent" (line 2, column 1))
   for the function foo
Compilation failed!

I am using Cogent commit cea9dd2d1ee from Sep 25 with flags +builtin-arrays +refinement-types

gteege commented 4 years ago

At least, it fixes this issue and made the test case succeed again.