hazel icon indicating copy to clipboard operation
hazel copied to clipboard

Basic concave grout => n-ary holes

Open disconcision opened this issue 1 year ago • 0 comments

This parses sequences of concave grout to a new kind of term, n-ary holes.

The basic idea here is that a run of subterms saperated by concave grout is treated as if it was a non-empty hole which contains all of those subterms. This is intended to be accomplished in a way such that an empty hole is semantically isomorphic to a 0-ary hole, and a hazel2 non-empty hole is semantically isomorphic to a 1-ary hole.

N-ary hole terms are always regarded as errors. They contain lists of terms of whatever the parent sort is. Otherwise, their semantics is basically: regard the contained subterms as if they were in the place of the n-ary hole; so e.g. expression n-ary holes pass the context to the subterm, etc.

note: this is the first case where the term and tile correspondence is non 1-1. as such, n-ary hole terms also hold a list of ids. this is mostly an implementation detail, to help collate them to make sure that when the caret is on a concave grout it is gets appropriate CI.

Not totally satisfied with the approach here so I'm putting it up for comment. I'm somewhat concerned with how to display these... we frequently get these intermediary states with concave grout... not sure this would feel great if it results in a hole being drawn around the entire segment? Also not totally sure on the treatment of sorts... right now I am just saying that we basically ignore the mold sort on constituents and use the sort expected by the syntactic context. to do otherwise would require some more explicit notion of sort holes, as we'd have to have data structure support for a kind of term that can contain a variably-sorted list....this sounds probably more complicated than its worth.

disconcision avatar Aug 11 '22 21:08 disconcision