Implement new rules in the paper

[jstolarek]

TODO:

• [x] #27
• [x] tracing new constructs (Fig. 2)
• [ ] forward slicing (Fig. 3 and. Fig 5)
  • [x] writes (Fig. 4)
  • [ ] new primitive to access forward slicing
• [x] backward slicing (Fig. 3 and Fig. 6)
• [x] lub for new language constructs
• [x] use pslice for trace slicing
• [ ] put all of this together

Cleanup

• [x] rename pslice to bwdslice. Also rename the primitive
• [ ] does pslice require extracting stars from the result and the environment? I think VStar can only be introduced in an environment

This is a note-to-self ticket.

[jstolarek]

It seems that with exceptions tracing has just become a major pain. On paper we need a new tracing construct for let (because exception can be raised in a binding) but in reality this means we need a new tracing construct for every expression that consists of more than one unconditional subexpression. This includes: assignment, sequencing, pairs and application. I'm also having trouble figuring out how to handle operators. Say I have raise "foo" + 2 represented as EOp OpPlus [ERaise "foo", EInt 2]. What should a trace look like for this? My guess would be TOp OpPlus [TRaise "foo"] but this means I now have OpPlus applied to incorrect number of arguments.

Looking at the rules I think that instead of creating new constructs I could just insert holes as traces of expressions that weren't executed. So let_F T_1 from the paper would be encoded as TLet t1 x THole. Does that sound reasonable?

[jamescheney]

Yes, I think putting holes in for subtraces that do not execute is reasonable. Alternatively we could make the potentially-missing subtraces Maybe, but this would be more verbose and I'm not sure whether this distinction matters. Alternatively one could add a trace form "Missing" for such subtrace components if we want to distinguish them from holes.