Hard-coded left injection

[matthewhammer]

hazel/src/semantics.v

Line 802 in a04ae65

(ZExp.RightAsc (HExp.Inj side (HExp.EmptyHole u')) (ZTyp.LeftSum (ZTyp.CursorT HTyp.Hole) HTyp.Hole)),

Seems like there's a bug where injection construction always creates a Left injection, even when the user asks for a right injection.

[cyrus-]

Don't think this is broken? The "side" variable determines which injection it is. The "LeftSum" is the Z-expression direction, not the side of the injection.

…

On Wed, Dec 20, 2017 at 10:58 PM Matthew Hammer ***@***.***> wrote: https://github.com/hazelgrove/hazel/blob/a04ae650aa5f0a7399091a0f03b296c9469fb9c2/src/semantics.v#L802 Seems like there's a bug where injection construction always creates a Left injection, even when the user asks for a right injection. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#28>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AARIPv7Uc1W4q2OUyrlqtkuLUlGgfhGtks5tCeVvgaJpZM4RJWw7> .

[matthewhammer]

Yeah, I just realized that's the wrong line (the line I quoted is fine), but there is an issue elsewhere. It's just more subtle than that.

To recreate the issue:

• Create a right injection
• Fill the value of the injection to be a number constant
• The injection will be rewritten to be a left injection