Simpl tactics: hung Epigram

[GoogleCodeExporter]

* What steps will reproduce the problem?

See test/BugLetDependent.pig

Loading the file simply hungs Epigram. Initially, I was suspecting the Let
machinery to cause the bug. By chance, I tried to "make" the goal and
"simpl" it after, this also causes the problem.

This is a stripped-down version of a much bigger code, so it's rather
contrived, no worry if simpl cannot nail it down.

Some points I've noticed:
 - the fact that there is a proof is key
 - the fact that the equation doesn't compute to refl is key
 - the fact that there is a All in the equation is key
but it's worth double-checking, right :-)

* What is the expected output? What do you see instead?

Well, I'm just expecting an output before the heat death of the universe.
Just give up simplifying man, there is no shame in failing, look at me.

Original issue reported on code.google.com by pedag...@gmail.com on 5 Jun 2010 at 8:22

[GoogleCodeExporter]

Ok, so the reason it loops is rather straightfoward:
  1/ simpl calls into simplifyGoal
  2/ simplifyGoal hits the PI (PRF p) t case, so it runs propSimplify on p
  3/ because p is an ALL s l, it calls into *forceSimplify*
  4/ well, forceSimplify never fails to simplify: if it cannot, it pushes an identity
in front of the term
  5/ so, we are back into simplifyGoal with a simplification which has "succeeded"
  6/ it tries to simplify what it thinks is a subterm (actually, the initial stuff
with an identity at the front)
  7/ GOTO 2 with a bigger ALL-ed term

I don't know how to cleanly fix that, tho. I'm going to hack my repos, waiting 
for
the professionals to solve the problem.

Original comment by pedag...@gmail.com on 5 Jun 2010 at 9:17

[GoogleCodeExporter]

((4) is slightly more involved than "pushing an id" in front, but the effect is 
the same)

My "fix" consists in:

>     thingy refS  (SimplyOne ref (L (HF "id" _)) _) = (|)

before:

>     thingy refS (Simply qs gs h) = do [...]

inside:

> propSimplify gamma delta p@(ALL s l) = [...]

"thingy"... Ha, well. 

Original comment by pedag...@gmail.com on 5 Jun 2010 at 9:59

[GoogleCodeExporter]

Fixed in trunk. This particular test case was easy to fix: just use 
propSimplify rather than forceSimplify for All s t (where s is not a 
proposition). However, a similar problem arose with implications, and that 
required a bit more work.

The PropSimp code is pretty bad (mea maxima culpa) and really could do with 
some heavy refactoring, if not a complete rewrite.

Original comment by adamgundry on 8 Jun 2010 at 8:32

• Changed state: Fixed