Update documentation based on review comments

Author: twitu

hmloc-codebase-doc.md

@@ -44,7 +44,7 @@ The typer accepts the abstract syntax tree of a program
 and performs type inference. It tracks source locations of the program terms.
 It wraps the inferred type with the provenance that contains the source location
 of the corresponding terms.
-For more information about the type system, see the paper.
+For more information about the type system, see section 3 of the paper.
 
 The corresponding files are:
 - `Typer.scala` contains the main typer class.
@@ -98,7 +98,7 @@ adds them to the `Ctx`.
 
 `UnificationSolver.scala` defines the `UnificationSolver` class which unifies types.
 Unification is particularly interesting because it tracks the data flow through
-source code locations. As described in the corresponding paper, it uses
+source code locations. As described in section 4 of the corresponding paper, it uses
 the provenance of types, which contains the source code locations,
 to track the data flow.
 

oopsla23-artifact-overview.md

@@ -39,7 +39,8 @@ HMloc. Type errors for programs show detailed data flow information. The artifac
 includes a test suite and many example programs and their reported errors.
 
 The `shared/src/test/diff/ocaml` directory contains tests. Some notable ones are:
-  - `Survey*.mls` are the example programs used in user survey described in the paper
+  - `OriginalDraftIntro.mls` has the introductory examples covered in the paper in section 1 and 2
+  - `Survey*.mls` are the example programs used in user survey described in the paper. The exact user survey program and errors are in the appendix and the results are discussed in section 5 of the paper. Note: that the extra wordings/format might have changed since the user survey however the core data flow information and visualization is retained.
   - `OcamlPresentation.mls` - demonstrates a variety of errors
   - `LetPoly.mls` - shows errors in code that uses let polymorphism
   - `Realistic.mls` - shows examples that might occur in an actual codebase
@@ -86,8 +87,7 @@ docker build --tag 'hmloc-oopsla23' .
 docker run -it --rm 'hmloc-oopsla23'
 ```
 
-The user will be attached to the shell of the container after the image gets pulled and the container is launched.
-Please `cd` to `hmloc/` and launch the SBT shell by typing `sbt`.
+The user will be attached to the shell of the container after the image gets pulled and the container is launched. Launch the SBT shell by typing `sbt`.
 
 ### Setting up from Scratch
 
@@ -98,7 +98,7 @@ Please `cd` to `hmloc/` and launch the SBT shell by typing `sbt`.
 
 ## Experimenting with HMloc
 
-We provide two ways of experimenting with HMloc. A test suite that runs example files and a web demo where the user can type their programs and see the results live.
+We provide two ways of experimenting with HMloc. A test suite that runs example files and a web demo where the user can type their programs and see the results live. The error messages can sometimes can get quite verbose. This is currently a limitation of this approach as is discussed in section 5.4 of the paper.
 
 We recommend using the the test suite.
 
@@ -135,3 +135,5 @@ then open the `local_testing.html` file in a browser.
 | **Top level declarations** | | |
 | definition | val foo: T | def foo x = t |
 | algebraic data type | `type 'a list = Cons of ('a, 'a list) \| Nil` | Cons(1, Nil) |
+
+The syntax for HMloc is a derived from a reduced subset of OCaml. The parser implementation is custom and does not handle all the corner cases expected of a full parser implementation. We encourage users to reference existing examples for specific nuances concerning the syntax.

shared/src/main/scala/hmloc/Typer.scala

@@ -10,6 +10,8 @@ import scala.collection.mutable.{Map => MutMap}
 /** A class encapsulating type inference state.
  *  It uses its own internal representation of types and type variables, using mutable data structures.
  *  Inferred SimpleType values are then turned into CompactType values for simplification.
+ * 
+ * The typing logic and state closely corresponds to the typing rule and explanations given in section 3 of the paper.
  */
 class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool)
     extends TypeDefs with TypeSimplifier {
@@ -301,7 +303,11 @@ class Typer(var dbg: Boolean, var verbose: Bool, var explainErrors: Bool)
     */
   def hintProv(p: TP): TP = noProv
 
-  /** Infer the type of a term. */
+  /** Infer the type of a term.
+   * 
+   * This implementation is closely related to the typing rules described in
+   * section 3 of the paper.
+   */
   def typeTerm(term: Term, desc: String = "")(implicit ctx: Ctx, raise: Raise, vars: Map[Str, SimpleType] = Map.empty): SimpleType
         = trace(s"$lvl. Typing ${if (ctx.inPattern) "pattern" else "term"} $term ${term.getClass.getSimpleName}") {
     // implicit val prov: TypeProvenance = ttp(term)

shared/src/main/scala/hmloc/UnificationSolver.scala

@@ -8,6 +8,11 @@ import scala.collection.immutable.Queue
 import scala.collection.mutable
 import scala.collection.mutable.{Queue => MutQueue, Set => MutSet, Map => MutMap}
 
+/* Unification solver creates data flows from sub-typing constraints. It also formats
+ * reports for incorrect data flows.
+ * 
+ * The unification algorithm is formally described in the section 4 of the paper.
+ */
 trait UnificationSolver extends TyperDatatypes {
   self: Typer =>