Non recursive pattern matcher

I was hoping to work more on this. However, I am busy with the matching logic prover so I would like to merge what I have right now.

The speedup of pattern matching gained by eliminating visitor pattern is consistent with the experiment in http://higherlogics.blogspot.com/2008/10/vtable-dispatching-vs-runtime-tests-and.html as well as the paper written by Scala guys http://lampwww.epfl.ch/~emir/written/MatchingObjectsWithPatterns-TR.pdf

@dwightguth @andreistefanescu please review