search

ToposInstitute / polytt

A type theory with native support for Polynomial Functors.
37 stars 3 forks source link

Engineering Pride #21

Open MonoidMusician opened 1 year ago

MonoidMusician commented 1 year ago

Checklist of things I want to clean up in the code that aren't going to be visible to users, just devs:

  1. [ ] (style) Use consistent names for variables across the codebase, e.g. we should decide to always write Pi (nm, a, b) instead of Pi (name, tm1, tm2) or whatever
  2. [x] (docs) Related: document what each of those constructors look like in syntax,
  3. [ ] (docs) Document what effects each module uses and how they interact, e.g. how Eff.Locals feeds all the other environments (semantics, quoting, and pretty-printing)
  4. [ ] (docs) How to add stuff to the syntax (tokens, grammar, elaboration, and data/syntax/semantics, if applicable)
  5. [ ] (code) Remove duplication between rules/Hom.ml and rules/Prog.hml
  6. [ ] (code) Remove duplication of common constructions, like calculating the underlying type of HomLam (currently in the conversion checker, elaborator, quoter, and do_hom_elim), and D.Neu (tp, { hd = D.Borrow lvl; spine = Emp }))
  7. [ ] (code) Remove extraneous Debug.print statements
solomon-b commented 1 year ago

@MonoidMusician where would you say we are at on this issue?

MonoidMusician commented 1 year ago

I'm going to keep adding things as they come up, I don't think we're going to close it any time soon.