Maps

As explained above, a map is defined as a ``set'' (built with the associative and commutative operator _,_) of entries. Notice that Entry, whose only constructor is the operator _|->_, is a subsort of Map.

The domain and codomain values of the map come from the parameters of the parameterized data type, both of them satisfying the theory TRIV and thus providing a set of elements.

The module MAP provides a constant undefined of the kind [Y$Elt] corresponding to the sort Y$Elt and representing the undefined result.

  fmod MAP{X :: TRIV, Y :: TRIV} is
    protecting BOOL .
    sorts Entry{X,Y} Map{X,Y} .
    subsort Entry{X,Y} < Map{X,Y} .

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

    var  D : X$Elt .
    vars R R' : Y$Elt .
    var  M : Map{X,Y} .

The operator insert adds a new entry to a map, but when the first argument already appears in the domain of definition of the map, the second argument is used to update the map. Notice the use of matching and of the otherwise attribute to distinguish these two cases in a simple way. Furthermore, in the first case, an auxiliary operation $hasMapping is used to make sure that in the resulting map only one entry is associated with the given value. The operation $hasMapping checks whether a domain value actually has an associated entry in a map.

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

The lookup operator is represented with the notation _[_]. Again, matching and owise are used to distinguish whether or not the second argument appears in the domain of definition of the map provided as first argument. When the answer is affirmative an the map contains exactly one entry associated with such argument (as checked with the auxiliary operation $hasMapping), the result is the value provided in that entry. When the answer is negative or the map is not well defined because there is more than one entry associated with the same argument, the result is the constant undefined in the kind, with the self-explanatory meaning that in those cases the map is undefined on the given argument.

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

We use the predefined views String and Nat (see Section 7.11.1) to define maps from strings to natural numbers, and do some sample reductions.

  fmod STRING-NAT-MAP is
    pr MAP{String, Nat} .
  endfm

  Maude> red in STRING-NAT-MAP :
           insert("one", 1, 
             insert("two", 2, insert("three", 3, empty))) .
  result Map{String,Nat}: "one" |-> 1, "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 [FindResult]: undefined

  Maude> red ("a" |-> 3, "a" |-> 2)["a"] .
  result [FindResult]: undefined

The last reduction shows that the undesired repetition of a domain value in two entries of the same map also produces the undefined constant as result.