search

overturetool / overture

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

Type inference is incorrect for nat1 multiplication #153

Closed joey-coleman closed 11 years ago

joey-coleman commented 11 years ago

The following bug was originally reported on Sourceforge by nick_battle, 2012-10-17 11:59:04.731000:

Value definitions that infer the type of a variable rather, than being given it explicitly, incorrectly infer the type as nat1 if the expression is a product with left or right being a nat1. For example:

functions f: () -> nat f() == let N1:nat1 = 1, N0:nat = 0 in let p = N1 * N0 in p;

This fails with Error 4064: Value 0 is not a nat1 in 'DEFAULT' (Test.vdmsl) at line 5:8.

The workaround is to give the explicit type of p as (in this case) p:nat.

joey-coleman commented 11 years ago

Comment by nick_battle, 2012-10-20 07:18:00.296000:

This is now fixed. It should make it into 1.2.3.

joey-coleman commented 11 years ago

Comment by nick_battle, 2012-10-20 07:18:33.052000:

  • status: open --> closed