Grove: A Bidirectionally typed collaborative structure editor calculus