Patches for BbML

[NeilKleistGao]

In this PR:

• Remove unused components in BBCtx and fix related bugs
• Use hint names for type variables if possible instead of using α everywhere
• Fix metaprogramming pattern matching related problems
• Fix predef type annotations and add missing operators
• Update skolem extrusion
• Rename bbml prelude file

[LPTK]

LGTM. Plz address my one comment and I'll merge.

In a follow-up PR, it would be good to generate human-readable type variable names, instead of ones that include counters. For this, I think you can directly reuse the codegen.js.Scope helper. It's not really specific to JS, so we could move it out of this js sub-package. OTOH type pretty-printing could be considered a form of codegen, so Scope can remain in codegen.

[NeilKleistGao]

LGTM. Plz address my one comment and I'll merge.

In a follow-up PR, it would be good to generate human-readable type variable names, instead of ones that include counters. For this, I think you can directly reuse the codegen.js.Scope helper. It's not really specific to JS, so we could move it out of this js sub-package. OTOH type pretty-printing could be considered a form of codegen, so Scope can remain in codegen.

Good suggestions! I will track this in a new issue.