Artifact for "An Exploration of First-Class Constrained Types: Semantics, Soundness, Principal Type Inference, and a Characterization of Termination"

# FCCT^I+ Demo ## Simple Evaluation with Docker 1. Run `run.sh`. This automatically imports the prebuilt docker image, starts the container, run the build, and copy the web-demo code out to the `web-demo` directory. The build will produce many warnings, but they are unrelated to FCCT^I+. The build should take a few minutes.2. `cd web-demo`, and use a simple http server to preview the page, e.g., `python -m http.server`. In the webpage, you will see the following screen, where the panel on the right is initially empty.You can click the `Type Check` button to run type inference and generate the typer output.You can try different examples and edit them.The final resolved type is in the `Resolved Weak Types` section.  One can uncomment line 3 and comment out line 4 in `run.sh` to build the docker image from source. ## Without Docker > Warning: Windows Subsystem for Linux (WSL) may encounter issues when running without docker1. Install sbt2. Unzip `mlscript.zip` to `mlscript` and `cd mlscript`.3. `mkdir web-demo`, since we will be writing the web-demo code to here.4. Run `sbt`, inside it run `hkmc2JS/fullLinkJS; hkmc2AllTests/test`. This builds the code and place the web-demo code in `web-demo` directory.5. See step 2 in the docker section. ## Code The core logic for the demo is in `hkmc2/shared/src/main/scala/hkmc2/typing/supremef/SupremeF.scala`.The most important parts are `Typer` and `CtxSolver`. - `CoreTerm`: AST for the terms, note that this is an extended version that supports: - Integer constants (used as literal types) - Let, which is just a syntax sugar.- `Type`: A trait for all types.- `QuantType`, `PosType`, `NegType`, `TypeVar`, `Constraint`, `Mark`: Corresponds to the constructs in the type. Note that we have `PosType.Const(int)` for literal types.- `Typer`: Construct `CoreTerm` from mlscript terms, and runs type inference on the `CoreTerm` to give a type and context.- `unify`: Corresponds to the `U(ty1, ty2)` function used to generate constraints for C-Forall2.- `CtxSolver`: Performs constraint solving step-by-step.- `InferenceCtx` and `NamingCtx`: Helpers. Notes:- Canonicalize is for renaming bound variables to canonical names, so we can directly compare for structural equality.- Refresh is for updating bound variable names, to avoid name conflicts. ## Claims in the paper We mentioned that we have an anonymous web demo of FCCT^I+.This artifact is the source code for the web demo.The code should resemble the FCCT^I+ formalization.