Arrays

As explained above, arrays work like maps, with the difference that an attempt to look up an unmapped value always returns the default value, i.e., arrays have a sparse array behavior (hence the name). In the same spirit, mappings to the default value are never inserted.

The main difference between maps and arrays is already made explicit in the parameters of the parameterized data type: while the first one satisfies the theory TRIV, the second one satisfies the theory DEFAULT that in addition to a set of data provides a default value 0 (see Section 7.11.2).

The constructor for entries is named _|->_, as for maps, while the set constructor is denoted here _;_.

  fmod ARRAY{X :: TRIV, Y :: DEFAULT} is
    protecting BOOL .
    sorts Entry{X,Y} Array{X,Y} .
    subsort Entry{X,Y} < Array{X,Y} .

    op _|->_ : X$Elt Y$Elt -> Entry{X,Y} [ctor] .
    op empty : -> Array{X,Y} [ctor] .
    op _;_ : Array{X,Y} Array{X,Y} -> Array{X,Y}
         [ctor assoc comm id: empty prec 71 format (d r os d)] .

    var  D : X$Elt .
    vars R R' : Y$Elt .
    var  A : Array{X,Y} .

The definition of the operator insert for arrays adds a check to the definition of the same operator for maps so that, as mentioned above, entries whose second value is the default value 0 are never inserted. Note, however, that mappings to the default value 0 that are created with the constructors _|->_ and _;_, rather than the insert operator, are not removed as doing this check each time a new array is formed would be excessively inefficient. Furthermore, as we have already seen for maps, in the first case, an auxiliary operation $hasMapping is used to make sure that in the resulting array only one entry is associated with the given value.

    op insert : X$Elt Y$Elt Array{X,Y} -> Array{X,Y} .
    eq insert(D, R, (A ; D |-> R')) 
      = if $hasMapping(A, D) 
        then insert(D, R, A)
        else if R == 0 then A else (A ; D |-> R) fi
        fi .
    eq insert(D, R, A) 
      = if R == 0 then A else (A ; D |-> R) fi [owise] .
    
    op $hasMapping : Array{X,Y} X$Elt -> Bool .
    eq $hasMapping((A ; D |-> R), D) = true .
    eq $hasMapping(A, D) = false [owise] .

The definition of the lookup operator for arrays only differs from the one for maps in the occurrence of the default value 0 instead of the constant undefined. Now, if an argument has more than one associated entry (as checked with the auxiliar operation $hasMapping), it is considered to be ``unmapped'' and the result is also the default value.

    op _[_] : Array{X,Y} X$Elt -> Y$Elt [prec 23] .
    eq (A ; D |-> R)[D] 
      = if $hasMapping(A, D) then 0 else R fi .
    eq A[D] = 0 [owise] .
  endfm

We do the same instantiation for arrays as for maps, with the predefined views String from Section 7.11.1 and Nat0 from Section 7.11.2).

  fmod STRING-NAT-ARRAY is
    pr ARRAY{String, Nat0} .
  endfm

  Maude> red in STRING-NAT-ARRAY :
           insert("one", 1, 
             insert("two", 2, insert("three", 3, empty))) .
  result Array{String,Nat0}: "one" |-> 1 ; "three" |-> 3 ; "two" |-> 2

  Maude> red insert("one", 0, 
               insert("two", 2, insert("three", 3, empty))) .
  result Array{String,Nat0}: "three" |-> 3 ; "two" |-> 2

  Maude> red insert("one", 1, 
               insert("two", 2, 
                 insert("three", 3, empty)))["two"] .
  result NzNat: 2

  Maude> red insert("one", 1, 
               insert("two", 2, 
                 insert("three", 3, empty)))["four"] .
  result Zero: 0