[Why3-club] syntactic sugar

Alan Schmitt alan.schmitt at polytechnique.org
Mon Sep 24 09:23:43 CEST 2012

Jean-Christophe Filliâtre <Jean-Christophe.Filliatre at lri.fr> writes:

>> I see in array.mlw that it is possible to declare some syntactic sugar
>> to have a[i] be M.get a.elts i.
>> How would I change this to have a[i,j] or a[i][j] (whichever is
>> possible) as syntactic sugar for M.get a.elts (i,j)?
> If you use a map of maps (instead of a map from pairs to values), then
> syntax a[i][j] can be used without any change.

Hi Jean-Christophe,

I'm trying this, but it still fails. Here is what I tried:

module Matrix

  use import int.Int
  use import map.Map as M

  type matrix 'a model {| xlength : int;
                          ylength : int; 
                          mutable elts : map int (map int 'a) |}

  function get (a: matrix 'a) (i: int) (j: int) : 'a = M.get (M.get a.elts i) j

  function ([]) (a: matrix 'a) (i: int) (j: int) : 'a = get a i j

  val ([]) (a: matrix 'a) (i: int) (j:int) :
    { 0 <= i < xlength a /\ 0 <= j < ylength a } 'a reads a { result = a[i][j] }

Using this, I get the error (on the "a[i][j]" syntax):

Bad arity: symbol ([]) must be applied to 3 arguments, but is applied to

What am I doing wrong? And where can I find some documentation about
this syntactic sugar?



More information about the Why3-club mailing list