from pda vs adt article

gistfile1.txt

adt IntList
representation
    list = NIL | CELL of integer * list
operations
    nil = NIL
    adjoin(x : integer, l : list) =
        CELL(x, l)
    null?(l : list) = case l of
        NIL ⇒ true
        CELL(x, l) ⇒ false
    head(l : list) = case l of
        NIL ⇒ error
        CELL(x, l ′) ⇒ x
    tail(l : list) = case l of
        NIL ⇒ error
        CELL(x, l′) ⇒ l′
    equal(l : list, m : list) = case l of
        NIL ⇒ null?(m)
        CELL(x, l ′) ⇒ not null?(m)
            and x = head(m)
            and equal(l ′, tail(m))

//ADT client
var l : list = adjoin(adjoin(nil, 4), 7);
if equal(nil, l) then ...

// PDA implementation
Nil = recursive self = record
  null? = true
  head = error;
  tail = error;
  cons = fun(y) Cell(y, self);
  equal = fun(m) m.null?
  end
Cell(x, l) = recursive self = record
  null? = false
  head = x;
  tail = l;
  cons = fun(y) Cell(y, self);
  equal = fun(m) (not m.null?)
      and (x = m.head)
      and l.equal(m.tail) end

// PDA client
var l = Nil.adjoin(4).adjoin(7);
if Nil.adjoin(8).equal(l) then ...