Merge Turnstile Core

[wilbowma]

Completely rewrites the Curnel to run on Turnstile+. This gives us new extensibility, resugaring, and debugging support. New features include:

• Improved tactics, including an auto tactic and system to managing hints.
• Improved pattern matcher with deep pattern matching and proper totality checking, with a pattern language to support analysis and transformation.
• Fixed termination and positivity checking.

Closes #88

---

• [ ] Remove deprecated and redundant code (mostly in turnstile-impl?)
  • [x] Remove racket-impl
  • [x] Remove ...+bool.rkt
  • [x] Remove ...+data.rkt ~- [ ] (old-)elim~
    ~- [ ] data~ ~- [ ] reflection API? (in favor of turnstile?)
  • can't rely on Turnstile exclusively. Started adding new reflection stuff in both reflection and in cic-saccharata.~ ~- [ ] replace get-match-info~ ~- [ ] Update documentation and examples~ ~- [ ] Remove (or test) output from tests~
• [x] Fix known consistency bugs
  • [x] Universes/Pi
  • [x] define/match/rec see https://github.com/stchang/cur/issues
  • [x] Code review
  • [x] Completely rewrite cause it's garbage (#92, #93, #94 )
  • [x] Closed by #103 #105
  • [x] positivity checking
• [x] Clean up core implementaiton
  • [x] Pi abstracted
  • [x] Type abstracted
  • [x] define-datatype cleaned up Mostly done, but can improve a few things pending work on Turnstile.
• [ ] Update versions
  • [x] Waiting for turnstile rebase.
  • [x] Waiting for turnstile define-internal../new API.
  • [ ] Ensure no dependencies on racket-doc (some of turnstile dependencies, transitively, required this) ~- [ ] Fix fragility of ntac tests?~ Some of these rely on generated names and are fragile. Looks like the problem is in Poly-abbrv mostly.
• [x] All tests passing
• [x] Performance problem with ntac Either fix or move software foundations to a different library to prevent absurd test suite time. Probably a good idea anyway. ~- [ ] Split ntac into separate package?~ ~- [ ] syntax of define/rec/match?~

[wilbowma]

Think I'm going to make my goals for merging this less ambitious and go MVP, since Cur is alpha quality anyway, and we're already once directly someone to install a non-master branch.

[stchang]

Yes, agree!

[wilbowma]

I've finished code review on the totality checker, and cut non-essentials of my checklist. I should be ready to merge this into master this week.

Any chance of getting Cur masters to build on Turnstile master?

[stchang]

Any chance of getting Cur masters to build on Turnstile master?

Yes, definitely. That should be the goal.

To achieve that though, you'll also need to merge in metantac and generic-type-methods (from my fork).

You want me to do the merge?

[wilbowma]

Sure. The turnstile-core branch is stable for now and I won't be making many changes for a bit.

[stchang]

So master is 4 commits ahead for some reason. Do you want those commits? It would make merging a lot easier if I first reset master to match where turnstile-core branched off. (The changes in those commits will be gone anyways bc they are in racket-impl.)

[wilbowma]

If they're all in racket-impl, I would revert them in master during the merge. Not sure if that will cause auto-merge to behave badly.

[stchang]

Yes we might have to ignore the automerge. Or we can revert master first. No one's using it anyways. You want me to do it?

[stchang]

Actually, I dont think i have access to the main repo?

[wilbowma]

Invited.

The only thing I want to avoid is a force push or rebase in master. I might want to revisit that racket-impl

[stchang]

ok sounds good. do you want to keep the commits from the separate branches that get merged in, or squash into one?

[wilbowma]

I think most of them, particularly those related to Turnstile, can be squashed. I want to keep the few that have #closes and such. I've already squashed those as far as I want to. I think there are only 3 of those---auto, termination checking, and totality checking.

[stchang]

sounds good

[stchang]

Question about one of the additions to match-info: https://github.com/wilbowma/cur/commit/9b3dc826660a21fdd14690a18cad0eaf5e301086#r39816834

I think we should keep match-info as small as possible if we can.