Elimination with a motive should simplify more equations

[GoogleCodeExporter]

The simplification code in elimination gets rid of some flex-rigid
equations, but leaves others present, and doesn't do anything with
rigid-rigid equations. It would be nice if more of these were simplified
automatically (try defining vector append interactively, using elimination!).

Example coming up...

Original issue reported on code.google.com by adamgundry on 12 May 2010 at 4:25

[GoogleCodeExporter]

I don't know who flex-rigid is, but I think that what you want is to replace the
"case p of ..." in "simplify", by "matchRef" commented under "simplify", further
extending "matchRef" to deal with that rigid-rigid person.

Original comment by pedag...@gmail.com on 13 May 2010 at 6:16

[GoogleCodeExporter]

That's the idea. Sorry for the slight misuse of unification terminology. A 
flex-rigid
problem is one with a variable on one side and a non-variable term on the 
other, and
I think these are usually dealt with by the current code, no?

I am about to push ./test/LetVec.pig which contains an example of equations 
that are
not simplified. As we start working more with IDesc, I think these are more 
likely to
arise.

Original comment by adamgundry on 13 May 2010 at 7:29

[GoogleCodeExporter]

I've refactored the simplification code, and it now splits pairs in the 
generated
constraints, so working with vectors is much nicer. Remaining constraints 
generally
arise from IDesc rather than elimination, and will need to be dealt with by 
problem
simplification.

Original comment by adamgundry on 25 May 2010 at 10:00

• Changed state: Fixed