[Why3-club] Strange type error message on a ref array

David MENTRE dmentre at linux-france.org
Wed Nov 28 15:25:22 CET 2012


Hello,

Using Why3 0.80, I can write this kind of code:
"""
module Test
  use import ref.Ref

  val c : ref int
  function update : int

  let do_update () : () =
   c := update
end
"""

However, when I apply this pattern to a data structure with an array,
it fails with a type error message I don't understand:
"""
module Test2
  use import ref.Ref
  use import array.Array

  type t = array int
  val c : ref t
  function update : t

  let do_update () : () =
   c := update
end
"""

"""
$ PATH=/usr/local/stow/why3-0.80/bin/:/usr/local/bin why3 -C why3.conf
-I . test.mlw
File "test.mlw", line 20, characters 3-4:
This expression has type ref <rho:array <rho1:map int int> int> (array
<rho1:map int int> int), but is expected to have type ref <rho2:array int>
(array int)
"""

Could somebody explain to me what I am doing wrong?

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.mlw
Type: application/octet-stream
Size: 287 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20121128/0b73a0a2/attachment.obj>


More information about the Why3-club mailing list