Conversation
|
The subsequent PRs are #959 #960 #961 #962 -- I'm not sure it makes sense merging them separately, but I think splitting them for review may help. (EDIT: my current thoughts are that we should merge them all individually, but sequentially (i.e. add them all to the merge queue in one go), with their current commit structure) Questions for reviewers: I'm not sure what conventional commit prefixes to use on a bunch of these, also I haven't worried about what changes are breaking -- for a dumb openapi frontend they should all be fine, but may break "smarter" clients, (and this PR may well break the DB. I need to document this). |
There was a problem hiding this comment.
Note: this comment was flagged by GitHub as a review, but that wasn't my intention — I just wanted to leave a comment on a particular commit.
Normally I prefer these series of step-by-step incremental changes, but in this particular case, I wonder if it makes more sense to squash the commits starting with this one (620ce7f) until the end of this PR. Is there value in having a history of halfway houses between the old regime and the new one?
edit: ahh, never mind, I see that 620ce7f was effectively the end of the changes in this PR. In that case, if it's helpful to have separate PRs to stage the changes, then that's fine.
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
63dbea1 to
c7abd43
Compare
georgefst
left a comment
georgefst
left a comment
There was a problem hiding this comment.
Looks good! The extent to which these changes have been broken up does lead to some slightly weird temporary code in places as you've said, but I imagine it makes this a lot easier to review than it otherwise could have been.
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
2 times, most recently
from
c3f9ccb to
baeba66
Compare
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
baeba66 to
54c9e8f
Compare
brprice
changed the title
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
54c9e8f to
1fc15f2
Compare
This is a start towards having constructors be fully-saturated. Once constructors are in saturated form (without storing their indices/type applications) as well, there will be much more symmetry between constructions and pattern matches (i.e. the tree structure of creating `C s t` and a pattern match `case e of C x y -> ...` will be the same). This commit changes the data we emit via the OpenAPI endpoints. However, it obeys the same schema (and consumers are expected to not care about the exact data we emit), and is thus not a breaking change.
This is a small step towards having constructors always being fully-saturated. We now have the option for constructors to be partially saturated: they can store some arguments, and receive others by an `App` or `APP`. In the future, the typechecker will enforce full saturation; but before that we need to change all usages to make fully-saturated constructors. (To clarify the terminology, consider a `Cons` constructor, which has one type argument and two term arguments. The following Primer `Expr`s (eliding metadata) are completely unsaturated (i.e. the old status quo): - `Con "Cons" [] []` - `APP (Con "Cons" [] []) _` - `App (APP (Con "Cons" [] []) _) _` - `App (App (APP (Con "Cons" [] []) _) _) _` Note that `Con "Cons" [] []` after this commit corresponds to `Con "Cons"` before this commit. The following is fully saturated (i.e. will be the only valid occurrence in the future) - `Con "Cons" [_] [_,_]` The following are partially-saturated - `Con "Cons" [_] []` - `App (Con "Cons" [_] []) _` - `App (App (Con "Cons" [_] []) _) _` - `Con "Cons" [_] [_]` - `App (Con "Cons" [_] [_]) _` In particular, note that "saturated" refers to how many arguments the constructor is directly applied to, in the sense of being contained in the lists within the `Con` node of `Expr`. Thus we (are starting to) treat the arguments of constructors differently to the arguments of functions.) There are some slightly awkward edges currently, due to not having finished our transition from unsaturated to fully saturated. For partially-saturated constructors (which will be rejected by the typechecker in the future), we have that - `typesInExpr` can focus on all type arguments of constructors - `focusType` will still ignore type arguments of constructors - the new `focusConTypes` will look at type arguments of constructors where necessary (in `Eval.NormalOrder.foldMapExpr`, `Eval.NormalOrder.findRedex` and `Zipper.focusOn`) There are some `TODO` notes documenting some of the work we still have to do, and some of the slight strangeness around this halfway point. These will be dealt with in subsequent commits. BREAKING CHANGE: this commit changes the `Expr` ADT, which will break programs created before this commit (i.e. we cannot load databases created by older versions of primer).
brprice
force-pushed
the
brprice/saturated-constructors-1
branch
from
1fc15f2 to
47b846b
Compare
3 participants
This PR adds the ability for a
Connode to have children: its type and term applications. We try to do the minimal work necessary to support this expanded AST. In particular, we do not enforce full saturation: it is currently perfectly fine to have a mix, à laCon "C" [ty] [tm1] `app` tm2. This will be changed in a subsequent PR.