#import "@preview/cetz:0.2.2": canvas, draw, tree
#import "@preview/codly:0.2.0": *

#set raw(syntaxes: ("syntaxes/MLscript.sublime-syntax"))

#show: codly-init.with()
#codly(
  enable-numbers: false,
  display-icon: false,
  zebra-color: white,
  languages: (
    mls: (name: "MLscript", icon: (), color: blue.lighten(75%)),
  )
)

#set page(paper: "a4", numbering: "1")
#set text(font:"Newsreader", size: 12pt)
#show raw.where(block: false): it => box(
  fill: luma(95%), // blue.desaturate(50%).lighten(90%),
  inset: (left: 0.1em, right: 0.1em),
  outset: (top: 0.25em, bottom: 0.3em),
  radius: 2pt,
  it)
#set par(justify: true, leading: 0.8em)
#set heading(numbering: "1.")
#show heading: it => [
  #it
  #v(0.25em)
]
#show link: set text(fill: blue.saturate(25%).darken(25%))
#show link: it => underline(offset: 4pt, it)
#show ref: set text(fill: teal.saturate(25%).darken(50%))
// #show ref: it => underline(offset: 4pt, it)
#let cell = (it) => table.cell(align: left + horizon)[
  #set par(justify: false)
  #it
]

#let callout-note = (it) => block(
  width: 100%,
  fill: blue.lighten(95%),
  stroke: 0.75pt + blue.lighten(75%),
  inset: (left: 0em, right: 0em, top: 0.75em, bottom: 0.75em),
  outset: (left: 1em, right: 1em, top: 0.25em, bottom: 0.25em),
  radius: 5pt
)[
  #text(fill: blue.darken(50%), weight: "semibold")[Note]
  #set text(fill: blue.darken(35%))
  #it
]

#v(1fr)

#align(center)[
  #text(size: 24pt, weight: "semibold")[
    #set par(justify: false, leading: 0.5em)
    Artifact Documentation for \
    _The Ultimate Conditional Syntax_
  ]

  #text(size: 18pt)[
    For OOPSLA 2024 Artifact Evaluation
  ]

  #text(size: 12pt)[
    <NAME>, Hong Kong University of Science and Technology, China

    September 2024
  ]
]

#v(1fr)

#pagebreak()

#outline(title: [Table of Contents], indent: true)

#pagebreak()

= Overview of the Artifact

Our paper introduces a new expressive conditional syntax called _Ultimate Conditional Syntax_ (hereinafter referred to as UCS). In the paper, we propose an algorithm to translate this syntax to traditional pattern matching and prove its correctness.

Our artifact implements this syntax and its translation algorithm on the MLscript compiler. The artifacts consists of two parts:

1. _The main project_ is a Scala project, which is a complete MLscript compiler, and includes the implementation and tests of UCS;
2. _The web demo_ provides a user-friendly interface, allowing people to compile and run MLscript (with UCS) programs directly in the browser, and view the results of each stage of the algorithm described in the paper.

The main project is the paper's main contribution, which fully implements the algorithm specified by the paper. The web demo illustrates the reusability of our main project: it can be reused by other programs (even in different programming languages).


This document contains the evaluation instructions for these two parts (@getting-started), explains how the algorithm proposed in the paper was implemented (@main-project), and provides usage instructions for the web demo (@web-demo).

== List of Claims

#let list-head = it =>[
  #set text(weight: "semibold", fill: luma(20%))
  #it
]

Most claims in the paper can be verified by reproducing particular examples in the test suite. You can test the examples by modifying them directly in the test suite or just trying them out individually in the web, which comes with a syntax reference.

1. #list-head[The translation algorithm can handle examples from the paper, and the translated program works correctly after being compiled.] The web demo includes most examples in the paper. You can load them and view the translation intermediate results. See @web-demo for a guide to the web demo.
2. #list-head[The translation algorithm's coverage checking stage can identify the three types of redundant branches mentioned in Section 3.5.1 of the paper.] The test files for this claim are located at `shared/src/test/diff/pretyper/ucs/coverage`.
   The warnings and errors in the output (lines starting with `//│`) after each test block#footnote[Check @test-files-explained for more information about test files used in the main project.] are generated by the translation algorithm.
3. #list-head[The translation algorithm's post-processing stage can sort out branches according to Section 3.6 of the paper.] Check the output of following test files:
   - `shared/src/test/diff/pretyper/ucs/stages/PostProcessing.mls`;
   - `shared/src/test/diff/pretyper/ucs/DualOption.mls` since line 172.
// 4. #list-head[]
   

== Hardware Requirements

This artifact does not require advanced hardware to run. Any computer connected to the internet and capable of running Java, Node.js, and modern browsers released in recent two years, can complete the artifact evaluation.

== Reusability Guide

The entire main project can be reused in following ways.

1. The main project can be extended directly. One can refer to @main-project to understand the overall structure of the project. Each stage of the translation in the paper has corresponding source files (as in @correspondence). People only need to make changes to the relevant parts to extend the translation algorithm as well as other parts of the compiler.
2. The web demo illustrates the other aspect of reusing the main project. In `build.sbt`, we derived a subproject named `npmBuild` from the main project, compiled it to JavaScript via #link("https://www.scala-js.org")[Scala.js], and generated a reusable npm package. This package is referenced in the web demo, thus the main project's compiler can be invoked, and the intermediate results of the UCS translation part are output.
   @web-demo:scratch exercises the process above.

#pagebreak()

= Getting Started <getting-started>

This section gives instructions for setup and basic testing. There are several ways of running the artifacts on your computer. We provide a detailed step-by-step guide for each approach. If you encounter any problems at any step, please contact us on the review platform, and we will provide the most timely assistance.

== Running the Main Project

This section introduces two methods to test running the main project. Please refer @running-tests to learn how the tests are organized and performed.

=== Using Docker <using-docker>

We have built Docker images containing all necessary dependencies
compiled for both `amd64` and `arm64` platforms and published them on #link("https://hub.docker.com/r/mlscript/ucs-docker/tags")[Docker Hub].

1. Run command `docker run -it --rm mlscript/ucs-docker`#footnote[This docker image already includes both `amd64` and `arm64` platforms. Docker will automatically select the image based on your computer's architecture.], which will pull the Docker image, launch a temporary container, run sbt's interactive shell inside the container, and immediately attach to the shell.
2. Run command `mlscriptJVM / test` in the shell, which will run _all_ the tests.
3. All tests are expected to be passed.
4. After the test is completed, you can enter `exit` to terminate the sbt shell, and the container just created will be destroyed afterwards.

=== Starting from Scratch <main-project:start-from-scratch>

Before the installation, please make sure that you have the following toolchains installed on your computer. 

1. First, you should install *#link("https://get-coursier.io")[Coursier]*, which sets up a Scala development environment. Please follow its #link("https://get-coursier.io/docs/cli-installation")[instructions] according to your operating system. You may need to install Java manually on some platforms.
2. Then, please install *sbt* and *Scala* compiler with Coursier: `cs install sbt scala`.
3. *#link("https://nodejs.org")[Node.js] 22*. It will also install npm (node package manager), which is also required.
   If you already have Node.js on your computer but don't want to overwrite the default one, you can consider using #link("https://github.com/nvm-sh/nvm")[nvm (node version manager)].
   
   #callout-note[Please ensure the `node` executable is in the `PATH`, otherwise all tests will fail.]

Next, download and unpack the artifact, and then enter the directory. Suppose the artifact is unpacked at location `artifact/`. Follow the steps below.

1. Run `sbt` at `artifact/`. This will start an interactive shell of sbt.
2. Run command `mlscriptJVM / test` in sbt shell, which will run _all_ the tests.
3. All tests are expected to be passed.
4. After the test is completed, you can enter `exit` to terminate the sbt shell

== Running the Web Demo

This section only describes how to run the web demo. Please refer to @web-demo for a guidance to the web demo.

=== Direct Access

The easiest way to start the web demo is to access #link("https://ucs.mlscript.dev")[https://ucs.mlscript.dev] in browsers. The web demo is designed to work on desktop computers and laptops. Also, you have to enable JavaScript to use the web demo normally.

Additionally, the web demo is supposed to to work on a modern browser, if you encountered any problems, please first read @web-demo-compatibility for compatible browsers.

#callout-note[
  The website is hosted via #link("https://pages.cloudflare.com")[Cloudflare Pages] statically and does not contain any trackers. Therefore, any access to the web demo will be purely anonymous.
  Alternatively, you also choose the methods in @web-demo:docker and @web-demo:scratch.
]

=== Using Docker <web-demo:docker>

We have built a Docker image specially for running the web demo locally.

1. Run `docker run -d --name web-demo -p 8080:3000 mlscript/ucs-web-demo`.
2. Access #link("http://localhost:8080")[http://localhost:8080] with your browser.
3. Remember to delete the container named `web-demo`.

#callout-note[You can replace `8080` in the command above with other available ports.]

=== Building from Scratch <web-demo:scratch>

If you want to verify that the web demo does use code from the main project, you can build the web demo from scratch by following the steps below. You are supposed to install toolchains mentioned in @main-project:start-from-scratch.

1. Assume the artifact has been downloaded and unpacked to the `artifact/`.
2. Run command `sbt "npmBuildJS / Compile / fullLinkJS"` at `artifact/`. This will emit a npm package at `artifact/npm/dist`.
3. Change the directory to `artifact/web-demo/` and run `npm install`. This will install dependencies of the web demo project.
4. Run command `npm run dev`, which will starts a development server. This command will usually have the following output.
   #block(breakable: false)[  
     ```
     VITE v5.3.1  ready in 256 ms
   
     ➜  Local:   http://localhost:5173/
     ➜  Network: use --host to expose
     ➜  press h + enter to show help
     ```
   ]
   At this point, you can see the web demo by visiting the suggested URL (usually #link("http://localhost:5173/")[`http://localhost:5173/`]). If you make changes to the source code of the web demo at this time, this development server will automatically update the webpage opened in the browser.

#pagebreak()
   
= Introduction to the Main Project <main-project>

== Project Structure <project-structure>

The implementation of the main project is based on MLscript. @main-project-structure shows the file structure in the project and which source files and tests are related to UCS.

#let framed-node = (it) => rect(
  stroke: 0.75pt,
  radius: 2pt,
  align(center, it)
)

#let shaded-node = (it) => rect(
  stroke: (thickness: 0.75pt, dash: "dashed"),
  radius: 2pt,
  align(center, it)
)

#let centered-node = (it) => align(center, it)

#let data = ([`shared/src/`],
  (centered-node[`main/scala/mlscript/` \ Source code files],
    framed-node[`ucs/` \ UCS implementation],
    centered-node[other \ sources files]
  ),
  (centered-node[`test/diff/` \ Test files],
    shaded-node[`ucs/` and `pretyper/ucs/` \ UCS test files],
    centered-node[other \ test files]
  ),
)

#figure(caption: [The main project's structure.])[
  #canvas(length: 1cm, {
    import draw: *
  
    set-style(content: (padding: .2),
      fill: gray.lighten(25%),
      stroke: gray.lighten(25%))
  
    tree.tree(data, spread: 4, grow: 2.25, draw-node: (node, ..) => {
      // circle((), radius: .5, stroke: none)
      content((), node.content)
    }, draw-edge: (from, to, ..) => {
      line((a: from, number: 1, b: to),
           (a: to, number: 1.1, b: from), mark: (end: ">"))
    }, name: "tree")
  
    // Draw a "custom" connection between two nodes
    // let (a, b) = ("tree.0-0-1", "tree.0-1-0",)
    // line((a, .6, b), (b, .6, a), mark: (end: ">", start: ">"))
  })
] <main-project-structure>

The files from #box(inset: (x: 3pt), outset: (x: 0pt, y: 4pt), stroke: black + 0.75pt, radius: 2pt)[framed part] is the implementation of the algorithm
and the #box(inset: (x: 3pt), outset: (x: 0pt, y: 4pt), stroke: (paint: black, thickness: 0.75pt, dash: "dashed"), radius: 2pt)[dashed framed part] contains the related test files.
@correspondence describes how these source files correspond to the algorithm in the paper. 
The purposes of the remaining source files and test files will be described in @other-parts.

== Correspondence between Paper and Code <correspondence>

The implementation of algorithm and its definition from the paper are implemented in this folder of the artifact: `shared/src/main/scala/mlscript/ucs/`. For brevity, the path names in the following description are relative to this path.

=== Syntax Definitions

#[
  #set text(size: 0.875em)
  #table(stroke: 0.75pt, columns: (1fr, 1fr, 1.4fr),
    [*Definition*], [*Location in the Paper*], [*Source Code Files*],
    cell[Source abstract syntax], cell[Fig. 2 in Section 3.1], [`syntax/source.scala`],
    cell[Core abstract syntax], cell[Fig. 3 in Section 3.2], [`syntax/core.scala`],
  )
]

=== Translation Algorithm

#[
  #set text(size: 0.875em)
  #table(stroke: 0.75pt, columns: (1fr, 1.2fr, 1.6fr),
    [*Stage*], [*Location in the Paper*], [*Source Code Files*],
    cell[Desugaring], cell[Section 3.3 and Appendix A.1 (Fig. 14 and Fig. 15)], cell[`stages/Desugaring.scala`],
    cell[Normalization], cell[Section 3.4 and Fig. 8], cell[`stages/Normalization.scala`],
    cell[Coverage checking], cell[Section 3.5 and Fig. 10], cell[`stages/CoverageChecking.scala`],
    cell[Post-processing], cell[Section 3.6], cell[`stages/PostProcessing.scala`],
  )
]

Besides the specific stages mentioned above, the class `Desugarer` 
// #footnote[At `shared/src/main/scala/mlscript/ucs/Desugarer.scala`.]
is responsible for connecting these stages together and integrating them into the entire compiler pipeline.

One may notice that there is a stage `stages/Transformation.scala`
that is not introduced in the paper.
This is because the parser was implemented before we wrote the paper,
therefore the definition of the syntax tree nodes used by the parser is quite
different.
This stage is designed to convert the old syntax tree nodes to the source abstract syntax nodes described in the paper.

== Running Tests <running-tests>

=== Test Files Explained <test-files-explained>

The suffix of the test file is `.mls`. Each file contains several _test blocks_ separated by empty lines. For example, the test file in @example-test-file contains three test blocks.

Test output is inserted in place in the test file after each corresponding block, as comments beginning with `//│`. This makes it very easy and convenient to see the test results for each code block. For this reason, we recommend using an editor that automatically reloads open files on changes. VSCode#footnote[We recommend to install #link("https://marketplace.visualstudio.com/items?itemName=chengluyu.mlscript-syntax-highlight")[mlscript-syntax-highlight] extension if using VSCode.] and Sublime Text work well for this.

#figure(
  caption: [An example of test files.]
)[
```mls
abstract class List[out T]: Cons[T] | Nil
class Cons[out T](head: T, tail: List[T]) extends List[T]
module Nil extends List[nothing]
fun (::) cons(x, xs) = Cons(x, xs)
//│ abstract class List[T]: Cons[T] | Nil
//│ class Cons[T](head: T, tail: List[T]) extends List
//│ module Nil extends List
//│ fun (::) cons: forall 'T. ('T, List['T]) -> Cons['T]

fun sum(acc, xs) = 
  if xs is
    Cons(x, xs) then sum(acc + x, xs)
    Nil then acc
//│ fun sum: (Int, Cons[Int] | Nil) -> Int

sum(0, 1 :: 2 :: 3 :: Nil)
//│ Int
//│ res
//│     = 6
```
] <example-test-file>

The output of each test block includes inferred types, evaluation results (by executing transpiled JavaScript programs), and possibly debugging information if debug flags are provided.

=== Test in Real-Time with Watch Mode

Using sbt's watch mode, we can modify test files, run tests, and view the test results in real-time. Assume the main project is located at `artifact/`

1. Run sbt at `artifact/`. This starts an interactive shell.
2. Run command `~mlscriptJVM / test`. The leading `~` indicates that the tests will rerun when any test file changes.
3. Open the project with code editor, for example, VSCode. Then, open a UCS test file, for example, `shared/src/test/diff/pretyper/ucs/examples/ListFold.mls`.
4. Make some changes. For example, update line 36 to
   ```mls
   join(", ")(1 :: 2 :: 3 :: 4 :: Nil)
   ```
   You will see its output at line 40 is updated to
   ```mls
   //│     = '1, 2, 3, 4'
   ```

=== Running Tests Individually

The command given above runs all the tests. Individual tests can be run with option `-z`.
```
~mlscriptJVM/testOnly mlscript.DiffTests -- -z List
```
The command above will watch for file changes and continuously run all `List` tests (those that have "List" in their names).
Please note that we have limited the tests to run only those related to UCS, as specified in @project-structure.

== Other Parts of the Main Project <other-parts>

This section explains the other parts of the main project. The main project has all the basic components of a static-typed programming language compiler: lexer, parser, pretyper, typer, and code generator.

=== Lexing and Parsing

The lexer accepts source strings and returns tokens to be parsed.
`Lexer.scala` contains the lexer class and `Token.scala` contains the token data types.

The parser accepts tokens generated by the lexer and
returns an abstract syntax tree of the input program in the surface syntax. `Parser.scala` contains the parser class and `syntax.scala` contains the _surface_ syntax data types of the language.

=== Pre-Typing

The pre-typing stage is used for name resolution and desugaring of high-level syntaxes (such as UCS) into MLscript's core syntax.
The translation algorithm described by the paper is implemented in this stage.

When we packaged this artifact, the pre-typing stage had just been completed, and its name resolution information had not yet been utilized by the typer or the subsequent code generation stage. As a result, some information can only be displayed with test flag `:ShowPreTyperErrors`.

=== Type Inference

The `Typer` class accepts an abstract syntax tree of a program
and performs type checking. MLscript supports principal type inference with subtyping. Please refer to #link("https://dl.acm.org/doi/abs/10.1145/3563304")[MLstruct] for more information.

`Typer.scala` contains the `Typer` class. `TypeSimplifier.scala` contains type simplification algorithms to simplify inferred types.
`TypeDefs.scala` and `NuTypeDefs.scala` contain classes and methods for type declarations.
`ConstraitSolver.scala` contains class `ConstraintSolver` which solves subtyping constraints.
`NormalForms.scala` the infrastructure to solve tricky subtyping constraints with disjunct normal forms (DNF) on the left and conjunct normal forms (CNF) on the right.
`TyperDatatypes.scala` includes data types for internal representation of types with mutable states to support type inference with subtyping.
`TyperHelpers.scala` provides helper methods for the typer.

=== Code Generation

The code generator translates MLscript AST into JavaScript AST and generates the corresponding JavaScript code. Those corresponding files are:

- `codegen/Codegen.scala` contains definitions of JavaScript AST nodes and methods for JavaScript code generation;
- `codegen/Scope.scala` and `codegen/Symbol.scala` provides symbol management and provides hygienic runtime name generation; and
- `JSBackend.scala` contains class `JSBackend` that translates an MLscript AST into a JavaScript AST.

== Compatibility Check

We have tested two methods on the following operating systems. The version of Docker is also annotated. Any similar platform with a proper setup should work as well.

#[
  #set text(size: 0.875em)
  #set par(justify: false)
  #table(stroke: 0.75pt, columns: (1fr, 1.1fr, 0.9fr),
    [],
      cell[*Using Docker* (@using-docker)],
      [*Starting from Scratch* (@main-project:start-from-scratch)],
    [*macOS 14.5 (Apple Silicon)*],
      [Test passed with Docker 26.1.3],
      [Test passed],
    // [macOS 13.6 (Apple Silicon)], [], [],
    // [Windows 11 23H2 (ARM64)], [], [],
    [*Windows 11 (x64)*],
      [Test passed with Docker 24.0.2],
      [Test passed],
    // [Windows 10 (x64)], [], [],
    [*Ubuntu 24.04 (x64)*],
      [Did Not Test],
      [Test passed],
    [*Fedora 40 (x64)*],
      [Test passed with Docker 27.0.3],
      [Did Not Test]
  )
]

If you encounter a situation where the project cannot be run, please contact us through the review platform.

#pagebreak()

= Guide to the Web Demo <web-demo>

This section provides a hands-on guide for the web demo and illustrates various features of the web demo through screenshots. Most importantly, we have visualized the results of different stages in the paper through the web demo and provided an interactive place to test our translation.

== User Interface

#figure(caption: [The user interface of the web demo.])[
  #image("screenshots/user-interface.png")
] <user-interface>

As shown in @user-interface, the interface is divided into three parts: _the navigation bar_, _the editor area_, and _the result display area_. Through the navigation bar, we can load existing examples to the editor and view the MLscript tutorials and artifact's README. The code in the editor area is editable, and the "Compile & Run" button at the top will compile the code in the editor into JavaScript and execute it directly in the browser when clicked. The result display area on the right has four tabs, which function as follows.

- The _UCS Translation_ tab displays how each UCS expression in the code in the left editor is translated. The paper introduces that the translation of UCS expressions includes three stages: desugaring, normalization, and post-processing. We can see the syntax tree of the expression output at each stage here. Note that these syntax trees are also interactive.
- In the _Type Inference_ tab, the results of type inference on the code on the left are displayed, and the panel below shows possible type errors, warnings, and other diagnostic information.
- The _Code Generation_ tab displays the JavaScript code transpiled from the MLscript code on the left side.
- The last _Execution_ tab shows all the values corresponding to expressions and statements after running the transpiled JavaScript.

We strongly recommend that you check out a few examples and look at the output of each stage of the UCS Translation on the right. We also suggest you read the MLscript guide (on the right side of the navigation bar) and then write some programs using UCS yourself and run them to see the results.

== Built-in Examples

=== Loading Built-in Examples

The web demo provides many examples from the paper. By hovering the mouse cursor to the navigation buttons "Basic Examples" and "Advanced Examples", a pop-up menu containing examples will appear (@example-menus).

Click on an example, and it will be loaded into the editor, automatically compiled and executed. Note that the source of each example from the original paper is marked in the lower right corner.

#figure(caption: [Screenshots of built-in examples in the web demo.])[
  #image("screenshots/example-menus.png", width: 75%)
] <example-menus>

=== Viewing UCS Translation Results

After an example is loaded, compiled, and executed, you can see the intermediate results of each stage of the UCS translation in the result display area on the right (@translation-results).

#figure(caption: [The UCS translation results.], placement: auto)[
  #image("screenshots/translation-results.png", width: 75%)
] <translation-results>

The UCS Translation tab displays the intermediate syntax trees from stages of the translation of a UCS expression at a time. Please note that these syntax trees are interactive; for example, users can click on the braces on either side to open/collapse the nested split structures.

From top to bottom, they are:

- the source code in plain text excerpted from the source code;
- the syntax tree obtained after parsing (corresponding to _the source abstract syntax_ in the paper), in which we indicate the type of "split" structures;
- the syntax tree obtained after desugaring (corresponding to _the core abstract syntax_ in the paper);
- the syntax tree obtained after normalization (corresponding to _the restricted core abstract syntax_ in the paper);
- the syntax tree of the final result obtained after post-processing; and
- the coverage checking results.

Since only one UCS expression can be displayed at a time, users can select other UCS expressions from the source code through _the expression selector_ (indicated by the blue frame in @translation-results). Users can also click the "Previous" and "Next" buttons on either side to quickly switch expressions.

== Compatibility Check <web-demo-compatibility>

Generally speaking, people do not need to check their browser version to use the web demo. Since most modern browsers update automatically, any personal computer with a stable internet connection are supposed to run the web demo without issues.

In case you encounter compatibility issues, you can refer to @web-demo-compatibility-table, which lists the versions of browsers available for the web demo that we have tested on various common operating systems.

#figure(caption: [Versions of various browsers that run the web demo across various operating systems which we have tested. They are not the minimum version requirements.])[
  #set text(size: 0.875em)
  #table(stroke: 0.75pt, columns: (1fr, 1fr, 1fr, 1fr, 1fr),
    [],
      [*macOS 14*],
      [*Windows 11*],
      [*Ubuntu 24.04*],
      [*Fedora 40*],
    [*Apple Safari*], [17.5], [N/A], [N/A], [N/A],
    [*Google Chrome*],
      [126.0.6478.127],
      [126.0.6478.127],
      [Did Not Test],
      [126.0.6478.126],
    [*Microsoft Edge*],
      [126.0.2592.87],
      [126.0.2592.87],
      [Did Not Test],
      [126.0.2592.87],
    [*Mozilla Firefox*],
      [127.0.2],
      [127.0.2],
      [119.0],
      [124.0.1],
  )
] <web-demo-compatibility-table>

In old browsers (for example, browsers from two years ago), the layout of the web demo may change, and some components may also not display properly. Please forgive us for not being able to support older browsers, and be sure to use the latest browser to access the web demo.