Feature/final corrections

roadmap.md

@@ -7,7 +7,7 @@
 - Implement a type-checker that can modify the expression being type checked. The new expression may have some arguments inserted and some type annotations inserted, etc.
 - Implement "one-step" type inference for ∀-spines using that feature. (Not sure whether also λ-spines are required for this to work.) Modify the do-notation by using type inference.
 - Implement some more beta-reducing rules. For example, `Integer/clamp (Integer/clamp x) = Integer/clamp x`, distribute functions such as `List/head` over `if/then/else` when there is opportunity to simplify, or some more rules for `Natural` number operations. I documented some possible new rules in the scall source code. For example, also `(if a then b else c).d` in case `b` and `c` are literal records, or `Integer/negate (Integer/negate x) = x`.
-- At type-checking stage, automatically insert values of the unit type `{}` when needed, similarly to the one-step type inference. Values of the type `{}` will be also inserted when their type was computed depending on previous values. Similarly, insert values of equality types.
+- At type-checking stage, automatically insert values of the unit type `{}` when needed, similarly to the one-step type inference. Values of the type `{}` will be also inserted when their type was computed depending on previous values. Similarly, insert values of equality types. Investigate if we could automatically convert between types `{} → a` and `a` at any usage site.
 - Each expression has a built-in "type annotation" field that may be initially empty. Implement the beta-reducer that can use the type information. If type information is not present, certain "type-sensitive" beta-reductions will not be performed (but others will be). For example, implement the reduction `{ a = x.a } = x` when `x` is a record containing the single field `a`, and similarly with `merge`. Make sure we can symbolically validate monoid laws, state monad laws, etc., which we can't do without such reduction rules. This is low priority because those kinds of reductions are only seen under lambda and not when evaluating concrete literal values.
 - Revisit the standard library's `List` module and implement a better choice of a `List` index built-in. Maybe slicing or direct indexing? Try avoiding the explosion of normal forms.
 - Implement more features for dependent type checking. Add a "value context" to the typechecker and to the beta reducer. (See below.)

tutorial/Makefile

@@ -10,7 +10,7 @@ programming_dhall.pdf: generated.tex programming_dhall.tex
 	( makeindex programming_dhall.idx || true ; pdflatex --interaction=batchmode programming_dhall.tex || true) >& /dev/null
 	fgrep "Output written on programming_dhall.pdf" programming_dhall.log
 
-generated.tex: programming_dhall.md convertMd.sh convertMd.scala
+generated.tex: programming_dhall.md titleback.tex convertMd.sh convertMd.scala
 	bash convertMd.sh tex ../dhall-lang/Prelude
 
 generated.dhall: programming_dhall.md convertMd.sh convertMd.scala

tutorial/convertMd.scala

@@ -260,12 +260,40 @@ def toLatex: Markdown => String = {
   case Markdown.BlankLine => "\n"
 }
 
+val hardcodedReplacements : String => String = { (source : String) =>
+  Seq(
+    "\\$x0\\$" -> "\\$x_0\\$",
+    "(\\\\log)\\{(.*)\\} " -> "$1 _{$2} ",
+    "[tT]he +chapter +\"([^\"]+)\"" -> "Chapter \\\\ref{$1}",
+    "[cC]hapter +\"([^\"]+)\"" -> "Chapter \\\\ref{$1}",
+    "[tT]he [Aa]ppendix +\"([^\"]+)\"" -> "Appendix \\\\ref{$1}",
+    "[Aa]ppendix +\"([^\"]+)\"" -> "Appendix \\\\ref{$1}",
+    "[sS]ection \"([^\"]+)\"" -> "Section \\\\ref{$1}",
+    "[tT]he +section \"([^\"]+)\"" -> "Section \\\\ref{$1}",
+    "[tT]he +subsection \"([^\"]+)\"" -> "Subsection \\\\ref{$1}",
+    "(\\\\label\\{)Appendix: " -> "$1",
+   // "'s" -> "\\\\textsf{'}s", // Leads to junk before page 0 of the book.
+   // "O'" -> "O\\\\textsf{'}",
+   // "s'" -> "s\\\\textsf{'}",
+    //"``" -> "\\\\textsf{``}",
+    "“" -> "\\textsf{``}",
+    //"''" -> "\\\\textsf{''}",
+    "”" -> "\\\\textsf{''}",
+    //"\\\\textsf\\{'\\}'" -> "\\\\textsf{''}",
+    //"\"([a-zA-Z])" -> "\\\\textsf{``}$1",
+    // "([a-zA-Z])\"" -> "$\\\\textsf{``}",
+  ).foldLeft(source) { case (prev, (from, to)) => prev.replaceAll(from, to) }
+}
+
+
+
+
 @main
 def main(code: Boolean, preludePath: String): Unit =
   val result: Seq[Markdown] = parse(System.in, markdown(using _)).get.value
   // The syntax `using _` was suggested as a workaround in https://github.com/scala/scala3/issues/19872
 
-  val convert = if code then toDhall(preludePath) else toLatex
+  val convert = if code then toDhall(preludePath) else (toLatex andThen hardcodedReplacements)
   val sep = if code then "" else "\n"
 
   println(result.map(convert).mkString(sep))