[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] }
end
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
2
What am I doing wrong? And where can I find some documentation about
this syntactic sugar?
Thanks,
Alan
More information about the Why3-club
mailing list