Merge DHExp and UExp

[Negabinary]

Motivation:

Implements #878,

The advantages of merging DHExp and UExp are:

• Removing duplication of code, making it easier & quicker to add new features to the Hazel language
• Consistency between evaluation results and written code - making easier to copy outputs into code, or to edit outputs, etc.
• Creating a consistency between the way static and dynamic code are pretty-printed, hopefully eventually replacing the pretty printer
• Tracing of ids through code allows us to correspond each construct from an output with the construct in the input

This pr replaces #931 which replaced #857. I have started again (using the previous iterations as inspiration) because the codebase has changed too much since those prs.

Implementation Strategy

My implementation strategy is to slowly get the two data structures to be as similar as possible, and then work on sharing code between them.

Progress

Chapter 1: Matching up the data structures

• Make DHExp match UExp
  • Rename types that just need renaming (Triv, Match, Var, constant literals, BinOp, Seq, If)
  • Combine forward and reverse application
  • Add ids to DHExp
    • Switch stepper render to be id-based
    • Create new ids on copy / evaluation steps
  • Come up with a consistent approach to moving errors through the code
  • Add closures to UExp
  • Add filters to UExp
  • Parentheses
  • Add type aliasing to DHExp
  • Surface Fix
• Make DHPat match UPat
  • Add Ids to DHPat
  • Rename DHPat constructors
  • Add TypeAnn(_) to DHPat
  • Come up with a consistent approach to moving errors through the code
• Merge UTyp and Typ
  • Add rec keyword to UTyp (I think polymorphism branch has already done this)
  • Fix Persist unbound type variables into Typ.t and show #1150 (will be part of Use Editor code to show outputs as well as inputs #1297)
• Merge Deferred Application
• Merge Polymorphism

Chapter 2: Removing footguns post-elaboration

• Ensure that all helper functions are well documented so they are easy to add cases to
• Make the elaborator more explicit
  • Add type assignment to Pat, and have it add casts correctly.
• Make unboxing more explicit
• Make pattern matching more explicit
• Make expected properties of static expressions and dynamic expressions explicit.
• Static error changes
• Take all static errors out of the evaluator, the evaluator should be able to work out itself whether there's an error

Known bugs to fix

• Fixpoint binders sometimes show static errors (will be fixed separately with Fixpoints in SynFun position create static errors #1299)
• Hidden steps are always showing
• Big performance regression (web workers are being sent strings that are ~300 times as long, this is taking a very long time to deserialize.)
• Let "expects" the correct type when there's nothing to expect #1246 causes invalid boxed errors in this pr
• The stepper doesn't step on casts any more (magically fixed itself, not sure how)
• If a pattern is annotated with a function type in a let-binding, the result will be cast to unknown
• Fixpoint printing appears to have regressed
• Elaboration and type checking are spending a lot of time generating Ids
• Make cast printing nicer
• InvalidBoxedFun at 5(?)
  Fix failed casts on:
  • type T = +A in A
  • let f = typfun t -> fun x:t -> x in f@<Int>(5)
• test check marks have moved
• let (x,y):(+X, +Y) = (X, Y) in gives static error
• let x : +X(Int) = X(3) in has bad cast
• shouldn't allow arrow constructors in patterns (This is an independent problem on dev)

Work for future PRs

• Converting expressions that have come out of evaluation into things we can print using the static editor (Use Editor code to show outputs as well as inputs #1297 )
  • Also re-run statics on outputs, and then we can get rid of failed casts, invalid operation errors
• Surfacing Casts & Closures

Notes

At the moment (2024-03-11), in order to add a new construct to the language, you need to:

1. Add a constructor to signature and implementation of Exp in TermBase .
2. Add a cls, and converters cls_of_term show_cls
3. Add cases to the static helpers is_tuple_of_functions append_exp
4. Add cases to the dynamic helpers repair_ids strip_casts fast_equals filter_matcher matches
5. Add a case to the type checker in uexp_to_info_map
6. Add a case to the elaborator and to the cast routine in the elaborator
7. Add a case to DHDocExp printing
8. Add small-step transition rules, and for each transition rule, add a name and string for that rule
9. Add cases to syntax tests var_mention var_applied find_fn tail_check

[disconcision]

I've gone over everything except I only skimmed dynamics. In general this feels pretty solid. Does some much-needed cleanup and generally avoids complecting things. There are some requests for clarifications in the comments but no major changes. I did some basic functional tests, the only issue I've found is the test checkmark thing.

Some general questions:

1. Why are we calling TypeAnns casts now? Not against it just curious as to the exact rationale
2. What exactly is the role of the layout/DH* modules now? And the DH terminology more broadly? It looks like we're still using the old view layer, except now we convert Exps to DHLayouts? Are we waiting to fully deprecate DH?
3. The proliferation of Typ.fresh, fast, etc makes me somewhat question the elimination of the internal Typ.t. We do so much syntax-irrelevant logic on types. Not asking that you roll back this part of the change, just noting that this feels debatable to me.

[disconcision]

this doesn't feel obviously consistent with the way prev_synswitch is described in its type definition

[Negabinary]

in what way?

[Negabinary]

To your general questions, @disconcision

1. I've called TypeAnns casts because that data structure is both used for type annotation and pattern casts. The dream is to also eventually have expression annotations which pare the parallel for expressions using the cast data structure. When used for annotations, one of the arguments to a cast is always ignored.
   

2. Yes, DH is fully deprecated in Use Editor code to show outputs as well as inputs #1297 - the only reason we would keep the terminology is to make a distinction between expressions that have all their casts and expressions that have implicit recursion.

3. Yeah I think that's a valid observation, we possibly could have had a separate data structure just for the statics, but it might make it harder to share code between casting logic and statics code (not that I'm sure we do that much?). I also think I could have come up with some more consistent story for how ids flow through type checking, but I was lazy and just made them all new because I had no use for the type ids yet.

[cyrus-]

• Needs some conflicts resolved
• The polymorphism casting seems to have some issues (see Polymorphism under documentation):

[Crazycolorz5]

The casting in the documentation page seems to be an issue with -> associativity -- adding parens like so removes that:

However, after doing so, I do get an "InvalidBoxedIntLit" error, which I am now investigating.

[Crazycolorz5]

The current branch also seems to not inherit bound names in stepped code / function output. E.g. in Cyrus's comment above you can see several . Additionally, see the screenshot:

See (c119777) also for how this was extended to type functions.

[Crazycolorz5]

Seems to be not a polymorphism in particular. This is a minimal reproducible example. It seems to be an error in the term_of -- somehow the internal variable binding isn't being looked up?

[Negabinary]

Ah yeah thanks @Crazycolorz5 - it was an issue with the transition rules for builtin application not using the evaluated version of the argument.

[cyrus-]

@Negabinary couple of conflicts to resolve here