Fix equality on external aequiv for symbols

[charlesyuan314]

When we generate equivalence functions for ABTs that utilize symbols, the internal comparison works as expected since symbols are internally unit Abt.t which can be compared using Abt.aequiv.

However, generated external aequiv fails to compile because it still uses Abt.aequiv to compare Temp.t when it should use Temp.equal. This patch remedies the bug, which seems to have been introduced in 02b8f27.

In the following example, we have:

  datatype typ
    = Nat
    | Arrow of typ * typ
    | Prod of (Label.t * typ) list
    | Sum of (Label.t * typ) list

Before patch:

    | ((Prod list'5), (Prod list'6)) =>
      (ListPair.allEq (fn ((label'1, typ'3), (label'2, typ'4)) =>
        ((Abt.aequiv (fn _ =>
          true
        ) (label'1, label'2)) andalso (typ_aequiv (typ'3, typ'4)))
      ) (list'5, list'6))

After:

    | ((Prod list'5), (Prod list'6)) =>
      (ListPair.allEq (fn ((label'1, typ'3), (label'2, typ'4)) =>
        ((Label.equal (label'1, label'2)) andalso (typ_aequiv (typ'3, typ'4)))
      ) (list'5, list'6))

[robsimmons]

I've not fully followed the development of this stuff, but this seems like a reasonable and stylistically appropriate addition - unless @billduff wants to jump in I'll merge this tomorrow. Thank you!

[billduff]

Seems fine to me, but I should let you know that symbols are probably broken in more ways that just that one.

[charlesyuan314]

Yeah, I've been trying to regenerate some structures for 312. At some point it looks like symbols could be compared by custom equality functions, but they're all plain Temps now? I gave up going down that branch.

[billduff]

I’m going try to do a bunch if cleanup work in the next few days. I sent you an email, assuming the email I grabbed off the 312 site is correct.