Using Latex backend for rendering AL expressions

[jaehyun1ee]

This resolves issue #59.

(1) \textrm is no longer used within inline math blocks

(2) Inline math blocks are now rendered using the Latex backend

Previously, parts that are enclosed in :math: were all AL expressions. Now, an AL-expression-to-EL-expression translation phase is added in backend-prose/render.ml. After translation, the Latex renderer in backend-latex gets to render the portions in math blocks.

Since the Latex renderer already handles display hints, backend-prose/hint.ml which dealt with hints within the prose backend is now removed.

(*) Side-effect: cross-references are no longer inserted

And this also comes with a side-effect that for the most part, cross-references are no longer inserted. Before this change, cross-references were inserted in CaseE (constructor) and CallE expressions. Now that they are all rendered via the Latex backend, which does not support cross-referencing at the moment, the generated PDF does not contain embedded links.

So, I believe it would be ideal for the Latex backend to support cross-referencing. One complication around cross-referencing is that, we need types to distinguish ambiguous names. For instance, both syntax tableinst and syntax meminst contains the TYPE field. So, when we want to insert cross-reference to TYPE in an expression ti.TYPE, we need to know that the type of ti is tableinst, not meminst. To disambiguate such cases in the prose backend, I have translated the types annotated in IL AST to AL on translation. So the prose backend was able to correctly insert a reference to the syntax definition of tableinst from TYPE in expression ti.TYPE.

If we still want cross-references, and in the Latex backend, we need types for disambiguation. For now, I can think of two solutions,

• The frontend generates some typed-version of EL out of the untyped, just-parsed EL, or
• Latex backend renders IL, which is typed, instead of EL, which is untyped

[rossberg]

Excellent, thanks for this! I have few comments that might simplify the translation.

Good point about the cross-refs. I definitely intended the Latex renderer to enable this as well, but your point about needing type information for it is a good one that I hadn't considered. The simplest way to solve this probably is to have the elaborator decorate the EL AST with some extra information on atom nodes, which the renderer then can use. (Rendering from the IL would be difficult, since it loses a lot of information needed for rendering.) I'll think about the best way for doing that.

[rossberg]

Can you add a comment how this can occur? Can it legally happen, or is it indicative of some internal error?

[jaehyun1ee]

I missed out on explaining this, sorry for the confusion. In short, it is legal for this to happen, and not an error.

There are certain AL expressions that must be rendered using plaintext, for example TopLabelE, which should be rendered as “a label is on the top of the stack.” Also, some may contain subexprs, like ContE e, rendered as “the continuation of … some rendered string of e ….”

Considering this, render_expr works as follows:

• First try to translate AL expr to EL exp with al_to_el_exp.
• If the translation succeeds, (indicated by Some), render it using the Latex backend.
  • This translation succeeds if and only if the AL expr and all its subexprs are able to be rendered in :math: blocks.
• Otherwise (indicated by None), it must be the case that the expr itself or one of its subexpr cannot be rendered in :math:. So we fall back to the original prose renderer in render_expr’.

[rossberg]

That makes sense, but even if the whole expressions cannot, shouldn't the subexpressions that can still be rendered with the Latex backend? In particular, I would expect that none of the cases for Var, Num, Bool, names, operators (other than Not), accessors, paths, records, iterators, etc., would ever be rendered here directly.

I would assume there must be an invariant somehow that none of the EL-handled cases can contain a subexpression that cannot be rendered as EL.(*) Or is there a counter-example? If so, shouldn't it be necessary to somehow transform it away, e.g., by introducing an auxiliary variable? For example, consider a record with a nested ContE, wouldn't that produce very jumbled output otherwise?

(*) FWIW, that would also imply that the option monad shouldn't be necessary, since it can only legally fail at the outermost level already.

[jaehyun1ee]

shouldn't the subexpressions that can still be rendered with the Latex backend?

Yes, render_expr' calls render_expr for rendering its subexpressions. For instance,

and render_expr' env expr =
  match expr.it with
  ...
  | Al.Ast.UnE (op, e) ->
        let sop = render_al_unop op in
        let se = render_expr env e in
        sprintf "%s %s" sop se

I would assume there must be an invariant somehow that none of the EL-handled cases can contain a subexpression that cannot be rendered as EL.

There exists a counterexample for AL IterE. For instance, IsDefinedE can be its subexpression, IterE (DefinedE (CallE (default, [ CallE (unpacktype, [ VarE (zt) ]) ])), [zt], *) which should be rendered as for all zt*, $default($unpacktype(zt)) is defined.

FYI, this prose expression is from the execution semantics of STRUCT.NEW_DEFAULT, in a step saying: 5. Assert: Due to validation, for all zt*, $default($unpacktype(zt)) is defined. This is generated from the IL sideconditions.

Other than IterE, the prose being generated now can be distinguished of EL-handled or not at the top level AST. Nevertheless, I am unsure that such invariant (modulo IterE) can persist to hold as the spec evolves, so I left render_expr' as close to the original logic as a foolproof.

[rossberg]

Right, but taking the UnE case as an example, that only makes sense for operators that are themselves in text form. In some of the other cases, the current algorithm would produce math operators outside math, some of that may not even be valid Latex (for example, \cdot is not allowed outside math mode, likewise things like ^?).

In other places, parts of a formula are rendered in a split fashion. For example,

 | Al.Ast.AccE (e, p) ->
       let se = render_expr env e in
       let sp = render_path env p in
       sprintf "%s%s" se sp

This will not type-set correctly, there needs to be a single math wrapper around both, not two separate ones. However, I don't understand how such cases can even legally arise: if one of the two parts cannot be converted to EL, then that supposedly means that it will be rendered as prose, but then concatenating them without space as if they were formulas doesn't seem right.

That's why there needs to be some invariant. There are three classes of expressions:

1. EL-like expressions only containing EL expressions ⇒ rendered by Latex backend
2. AL-only expressions, possibly containing EL expressions ⇒ rendered by prose backend except for inner EL
3. Pseudo EL-like expressions containing AL expressions ⇒ must be rendered by prose backend, as prose

In particular, all expressions in the 3rd category must be rendered as real prose, since they can contain nested prose. It never makes sense to render them as a formula. For example, if the prose renderer were to encounter an expression like ListE [ContE e1, ContE e2], then it would currently generate something like "[the continuation of e1, the continuation of e2]", which is not what we want.

There are only two meaningful possibilities for handling such an example:

• either it's considered illegal, i.e., no AL-specific expressions can ever occur inside a list, but then render_expr' should not handle lists at all

• or it can legally occur, but then render_expr' needs to render the list as proper prose, e.g., something like "the sequence consisting of ..., ..., and ..."

Under no circumstances should render_expr' render any node as a formula-like object. That doesn't compose with nested prose.

Effectively, there are two layers of languages, prose and formula. Ideally the AL AST would separate them as different classes of expressions (possibly duplicating some constructs like iter that can occur on both levels). But short of ensuring the layering by construction, it at least needs to be assumed in the renderer logic.

Does that make sense?

[jaehyun1ee]

Aha, thank you for the detailed description, things got much clearer to my mind with the categorization.

I prefer the or it can legally occur, but then render_expr' needs to render the list as proper prose, e.g., something like "the sequence consisting of ..., ..., and ..." option. So with the latest commit, I have removed all rendering logic in render_expr' that belongs to none of the three category, i.e., the ones that produce math-like output in plaintext.

By the fallback logic from render_expr to render_expr', when rendering UnE in render_expr', it must be that the operator is not a formula. But to make things more clear when reading the code, I added a guard indicating that it is the case. And similarly for BinE and IterE.

(* before *)
| Al.Ast.UnE (op, e) ->
      let sop = render_al_unop op in
      let se = render_expr env e in
      sprintf "%s %s" sop se

(* now *)
| Al.Ast.UnE (op, e) when Option.is_none (al_to_el_unop op) ->
      let sop = render_al_unop op in
      let se = render_expr env e in
      sprintf "%s %s" sop se

Plus, I do believe that the invariant you made is true, but I added this final case to render_expr' since I do not want the renderer to crash on some unexpected, peculiar expression form.

| _ ->
      let s = Al.Print.string_of_expr expr in
      sprintf "warning: %s was not properly handled by prose backend" s |> prerr_endline;
      s

And a final remark, I prefer to keep the option monadic translation of AL-expr-to-EL-exp. First, due to the aforementioned presence of IterE. Second, figuring out if an AL expr is of category 1 and actually carrying out the translation requires one to recurse through all the subexpressions. I prefer to do such in a single function al_to_el_exp, which returns some EL exp if it belongs to category 1, and none otherwise.

[rossberg]

Nice, this looks good. A few more comments.

[rossberg]

Suggested change

	| Al.Ast.UnE (op, e) when Option.is_none (al_to_el_unop op) ->
	| Al.Ast.UnE (op, e) when al_to_el_unop op = None ->

Also, it would be better to change render_al_unop/binop to return options as well, and check the result of that here instead. Some of their cases still produce formulas, and some of those yield malformed Latex in text. You want to guarantee that this cannot happen.

[jaehyun1ee]

I instead enforced render_al_unop and render_al_binop to print out textual (or, not-formula) formats only. For instance, render_al_binop renders Al.Ast.MulOp as "multiplied by" rather than "\cdot".

So we have a guarantee that inside render_expr' (which being their only callsites), they will never print formula as plaintext.

Ditto for render_path mentioned above.

[jaehyun1ee]

Thank you for #62, all keywords in AL are rendered as EL atoms now.

There is one exception though, for the infix operator in AL InfixE (e1, op, 32), which I have hardcoded the type for op when translating it into an EL atom (al_to_el_infixop). Using InfixE in AL is, as far as I know, was a hack to get things done in the AL backends. @f52985 should know the details but he will not be around for a couple of weeks. So I suggest dealing with this InfixE part in another PR.

Plus, I believe bringing the type information from IL to AL would be neater if IL also had atoms annotated with types. Below is the current translation of IL CaseE to AL CaseE. (caseE is just a constructor shorthand) Instead of using the IL exp's type in exp.note, if IL had typed Atoms, the translation would look much more straightforward. This, however, is just a preference and the current implementation is just as great for me :)

(* now *)
| Ast.CaseE (Ast.Atom cons, arg) -> caseE (name2kwd cons exp.note, exp2args arg) ~at:at

(* if IL-Atom is typed *)
| Ast.CaseE ({ it = Ast.Atom cons; note; _ }, arg) -> caseE ((cons, note), exp2args arg) ~at:at

[rossberg]

Great, thanks!

Yeah, the handling of infix operators in the AL indeed looks like a hack. There is too much hard-coding when translating between IL and AL (il2al/translate MixE) and back to EL, and some of that is lossy, too. For example, I'm certain the current code will not show brackets as e.g. in table/memory types correctly.

I suspect that the only reason we are not currently running into that is that we are not yet rendering all validation prose.

To work in all cases, al_to_el_infixop at least needs to implement the inverse of the MixE transformation in il2al/translate, including the string_of_atom function. But a full fix requires changing the AL to reflect all relevant information from the IL, in particular, keep mixops around.

But let's keep cleaning that up for a later change.

I'll think about annotating IL atoms. It'd be a bit annoying to wrap them everywhere, and it caused me a lot of debugging grief for the EL already, because all equality comparisons on atoms silently started misbehaving. (Too bad OCaml's type system doesn't distinguish comparable types. :( )

FWIW, I plan to also annotate symbolic atoms, since we overload some of them as well.

[jaehyun1ee]

Great, happy to see the Latex and prose backends starting to work together 👍