MITTutorialApril2009: ListExercise.fss

component ListExercise
export Executable
import List.{...}

(* The example graph in this exercise is cribbed from
   "Fast Decision Procedures Based on Congruence Closure",
   by G. Nelson and D. C. Oppen.  They give a *far* more efficient
   algorithm for solving the same problem!

The initial graph looks like this:

  f
  |
  f
  |
  f    g
  |   / \
  f  g   |
  | / \  |
  f  g | |
  | / \|/
  a    b

Initially we assert that the following nodes are equivalent:
a = f(f(f(a)))
a = f(f(f(f(f(a)))))
a = g(a, b)

We end up discovering that all the nodes except b are equivalent!
*)

(* EXERCISE 1: samePairs *)

(* Fill in the function samePairs that checks that its two input lists
   contain the same pairs of values (either list may contain
   duplicates, and order doesn't matter).

   You will find BIG AND, BIG OR, and IN operators useful here.
   Also, note that AND: and OR: yield short-circuit evaluation.
 *)
samePairs(a: List[\ (Node,Node) \], b: List[\ (Node,Node) \]): Boolean =
    fail("Ex 1, samePairs, not yet started; "
         "the other exercises won't check without it!")

(* EXERCISE 2: uniq *)

(* Fill in the function uniq that is passed a list of Nodes, and removes elements of the
   list that are equal to preceding elements.

   There are many ways to do this; a particularly nice (parallel) one
   makes use of the split() method on lists.  Another possibility is to use
   |xs| and indexing to extract sublists: x[0], x[1:], and so forth. *)
uniq(xs: List[\(Node,Node)\]) =
   fail("Ex 2, uniq, not yet started.")

(* EXERCISE 3: symmetricTransitiveClosure *)

(* Fill in the function symmetricTransitiveClosure, that given a list
   of pairs computes the symmetric transitive closure of that list.
   The list is symmetrically closed if for each pair (x,y) the list
   also contains (y,x).  The list is transitively closed if, when it
   contains (x,y) and (y,z), it also contains (x,z) when x =/= z.  You
   can decide whether to include reflexive pairs (x,x) as well; this
   exercise is somewhat easier if you do so.

   Note that you'll need to decide when to terminate.  You can use
   samePairs to decide this, or if you're careful you can use list
   equality xs=ys (which is cheaper) or a check for emptiness
   (xs.isEmpty, cheaper still).

   You may find this problem easiest if you symmetrically close a,
   then compute the transitive closure of the result.  We've provided
   an appropriate type signature to help you along.  *)
symmetricTransitiveClosure(a: List[\ (Node,Node) \]): List[\ (Node,Node) \] =
    fail("Ex 3, symmetricTransitiveClosure, not yet started.")

(* Assumption: a is symmetrically closed. *)
transitiveClosure(a: List[\ (Node,Node) \]): List[\ (Node,Node) \] =
    fail("transitiveClosure is used but not implemented.")

(* EXERCISE 4: equivalence by operator *)

(* a list of Nodes, find the symmetric, transitively
   closed list of Nodes with the same operator.  The operator of a
   node n can be obtained by writing n.op (so you'll want to write
   code of the form n.op = m.op)
*)
operatorClosure(nodes: List[\Node\]): List[\(Node,Node)\] =
    fail("Ex 4, operatorClosure, not yet started.")

(* EXERCISE 5: graph equivalence closure *)

(* Given a graph, we define its *equivalence closure*, a
   symmetric, transitively closed list for which the following are true:
       If (a,b) is in initEquivs, it is in the equivalence closure.
       If two nodes a and b have the same operator (they're in the operatorClosure),
           and corresponding pairs of children are equal or in the equivalence closure,
           then (a,b) are also in the equivalence closure.
   For this exercise you'll want to use transitiveClosure, operatorClosure,
       and zip.
      xs.zip[\T\](ys) generates corresponding pairs of elements from xs and ys; for example
        <| x | (x,y) <- <|1,2,3|>.zip[\ZZ32\]<|1,4,3,2|>, x=y |>
      generates the list of elements <1,3>.
   To obtain a list of the children of node n, simply write n.children.
 *)
equivalenceClosure(graph: List[\Node\], initEquivs: List[\(Node,Node)\]): List[\(Node,Node)\] =
    fail("Ex 5, equivalenceClosure, not yet started.")

(************************************************************
 * Built-in utility code down here
 ************************************************************)

value object Node(name: String, op: String, children: List[\Node\]) extends Equality[\Node\]
    getter asString(): String = name
    opr =(self, other:Node): Boolean = name = other.name
end

node(op: String, children: List[\Node\]): Node = do
    name = op "(" (BIG ||[c <- children] (", " c.name))[2:] ")"
    Node(name, op, children)
  end

node(op: String, childNodes: Node...): Node =
    node(op, list[\Node\](childNodes))

leaf(name: String): Node = Node(name, name, <|[\Node\] |>)

showEquiv(eqvs: List[\(Node,Node)\]): String =
    BIG //[(x,y) <- eqvs, |x.name| < |y.name| OR: x.name < y.name] x.name " = " y.name

(************************************************************
 * TESTS
 ************************************************************)

run(): () = do
    a = leaf("a")
    fa = node("f",a)
    ffa = node("f",fa)
    fffa = node("f",ffa)
    ffffa = node("f",fffa)
    fffffa = node("f",ffffa)
    b = leaf("b")
    gab = node("g",a,b)
    gfab = node("g",fa,b)
    ggfab = node("g",gfab,b)
    graph = <|[\Node\] a,fa,ffa,fffa,ffffa,fffffa,b,gab,gfab,ggfab |>
    initEquivs = <|[\(Node,Node)\] (a,fffa), (a,fffffa), (a,gab)|>
    iE = <|[\(Node,Node)\] (a,gab), (a,fffa), (a,fffffa) |>
    eE = <|[\(Node,Node)\] |>
    (* EXERCISE 1: samePairs *)
    assert(samePairs(iE, iE), true, "Ex 1: Should be samePairs",iE,iE)
    assert(samePairs(initEquivs, iE), true, "Ex 1: Should be samePairs",initEquivs,iE)
    assert(samePairs(eE, eE), true, "Ex 1: Should be samePairs",eE,eE)
    iE2 = initEquivs || iE
    assert(samePairs(iE, iE2), true, "Ex 1: Should be samePairs",iE,iE2)
    assert(samePairs(eE, iE), false, "Ex 1: Not samePairs", eE, iE)
    iEr = iE[1:]
    assert(samePairs(iE2, iEr), false, "Ex 1: Not samePairs", iE2, iEr)
    println("EXERCISE 1 Complete")
    (* EXERCISE 2: uniq *)
    assert(initEquivs, uniq(initEquivs), "Ex 2: Uniq is different")
    assert(initEquivs, uniq(initEquivs || iE), "Ex 2: Uniq is different")
    assert(eE, uniq(eE), "Ex 2: Uniq should be empty!")
    println("EXERCISE 2 Complete")
    (* EXERCISE 3: symmetricTransitiveClosure *)
    initEquivs_closed = symmetricTransitiveClosure(initEquivs)
    reflexives = <|[\(Node,Node)\] (a,a), (fffa, fffa), (fffffa, fffffa), (gab, gab) |>
    expected_closure =
        ( initEquivs || reflexives ||
          <|[\(Node,Node)\] (fffa, a), (fffa,fffffa), (fffa, gab),
                        (fffffa, fffa), (fffffa, a), (fffffa, gab),
                        (gab, fffa), (gab, fffffa), (gab, a) |> )
    assert(samePairs(initEquivs_closed || reflexives, expected_closure), true,
           "Ex 3: Closure doesn't have same pairs as expected\n",
           initEquivs_closed, "\n", expected_closure)
    println("EXERCISE 3 Complete")
    (* EXERCISE 4: closure by op *)
    op_closure = operatorClosure(graph)
    reflexive_graph = <|[\(Node,Node)\] (n,n) | n <- graph |>
    expected_op_closure =
        symmetricTransitiveClosure( reflexive_graph ||
          <|[\(Node,Node)\]
            (fa,ffa),(fa,fffa),(fa,ffffa),(fa,fffffa),
            (gab,gfab),(gab,ggfab) |> )
    assert(samePairs(op_closure || reflexive_graph, expected_op_closure), true,
           "Ex 4: Closure by operator doesn't have same pairs as expected\n",
           op_closure, "\n", expected_op_closure)
    println("EXERCISE 4 Complete")
    (* EXERCISE 5: equivalence closure *)
    fullClose = <| (n1,n2) | n1 <- graph, n1.name =/= "b", n2 <- graph, n2.name =/= "b" |>
    equiv_closure = equivalenceClosure(graph, initEquivs)
    println("Initial equivalences:" // showEquiv(initEquivs))
    println("\nFinal equivalences:" // showEquiv(equiv_closure))
    assert(samePairs(fullClose||reflexive_graph, equiv_closure||reflexive_graph), true,
           "Ex 5: Closure by operator is missing some pairs!\n",
           fullClose, "\n", equiv_closure)
    println("EXERCISE 5 Complete")
  end

end