reformat code and upgrade dhall

winitzki · Jan 20, 2025 · ad8859c · ad8859c
1 parent 0961bde
commit ad8859c
Show file tree

Hide file tree

Showing 6 changed files with 88 additions and 117 deletions.
diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml
@@ -97,7 +97,7 @@ jobs:
       - name: Setup dhall executable
         uses: "dhall-lang/setup-dhall@v4"
         with:
-          version: '1.42.0'
+          version: '1.42.2'
       - name: Setup latex
         uses: "zauguin/install-texlive@v3"
         with:

diff --git a/github-scala-build-and-test.dhall b/github-scala-build-and-test.dhall
@@ -49,7 +49,7 @@ in  GithubActions.Workflow::{
                 , GithubActions.Step::{
                   , name = Some "Setup dhall executable"
                   , uses = Some "dhall-lang/setup-dhall@v4"
-                  , `with` = Some (toMap { version = "1.42.0" })
+                  , `with` = Some (toMap { version = "1.42.2" })
                   }
                 , GithubActions.Step::{
                   , name = Some "Setup latex"

diff --git a/nano-dhall/src/main/scala/io/chymyst/nanodhall/NanoDhallGrammar.scala b/nano-dhall/src/main/scala/io/chymyst/nanodhall/NanoDhallGrammar.scala
@@ -24,28 +24,17 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
     " "
       | tab
       | end_of_line
-  )
-    .memoize
+  ).memoize
 
-  def whsp[$: P]: P[Unit] = P(
-    NoCut(whitespace_chunk.rep)
-  )
+  def whsp[$: P]: P[Unit] = P(NoCut(whitespace_chunk.rep))
 
-  def whsp1[$: P]: P[Unit] = P(
-    NoCut(whitespace_chunk.rep(1))
-  )
+  def whsp1[$: P]: P[Unit] = P(NoCut(whitespace_chunk.rep(1)))
 
-  def ALPHANUM[$: P] = P(
-    ALPHA | DIGIT
-  )
+  def ALPHANUM[$: P] = P(ALPHA | DIGIT)
 
-  def simple_label_first_char[$: P] = P(
-    ALPHA | "_"
-  ).memoize
+  def simple_label_first_char[$: P] = P(ALPHA | "_").memoize
 
-  def simple_label_next_char[$: P] = P(
-    ALPHANUM | "-" | "/" | "_"
-  ).memoize
+  def simple_label_next_char[$: P] = P(ALPHANUM | "-" | "/" | "_").memoize
 
   /*
    ; A simple label cannot be one of the reserved keywords
@@ -55,7 +44,7 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
    ; simple-label =
    ;       keyword 1*simple-label-next-char
    ;     / !keyword (simple-label-first-char *simple-label-next-char)
-    */
+   */
   def simple_label[$: P]: P[String] = P(
     (keyword.map(_ => ()) ~ simple_label_next_char.rep(1)) // Do not insert a cut after keyword.
       | (!keyword ~ simple_label_first_char ~ simple_label_next_char.rep)
@@ -67,55 +56,41 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
     // %x60 = '`'
   )
 
-  def quoted_label[$: P] = P(
-    quoted_label_char.rep
-  ).!
+  def quoted_label[$: P] = P(quoted_label_char.rep).!
 
   // Note: identifiers in backquotes may contain arbitrary text, including the name of a Dhall keyword.
   // Example: "let `in` = 1 in `in`" evaluates to "1".
   // A successfully parsed `label` is guaranteed to be either quoted or not a keyword.
-  def label[$: P]: P[String] = P(
-    ("`" ~ quoted_label ~ "`") | simple_label
-  )
+  def label[$: P]: P[String] = P(("`" ~ quoted_label ~ "`") | simple_label)
 
   // A successfully parsed `nonreserved_label` is guaranteed to be either quoted or not a builtin.
-  def nonreserved_label[$: P] = P(
-    (builtin ~ simple_label_next_char.rep(1)).! | (!builtin ~ label)
-  ).map(VarName.apply)
+  def nonreserved_label[$: P] = P((builtin ~ simple_label_next_char.rep(1)).! | (!builtin ~ label)).map(VarName.apply)
 
-  def any_label[$: P]: P[String] = P(
-    label
-  )
+  def any_label[$: P]: P[String] = P(label)
 
   def forall_symbol[$: P] = P(
     "\u2200" // Unicode FOR ALL
   )
 
-  def forall[$: P] = P(
-    forall_symbol | requireKeyword("forall")
-  )
+  def forall[$: P] = P(forall_symbol | requireKeyword("forall"))
 
   private def concatKeywords[$: P](keywords: Seq[String]): P[String] = {
     keywords
       .sorted(Ordering[String].reverse) // Reversing the order will disambiguate parsing of keywords that are substrings of another keyword.
-      .map {
-        k => implicit ctx: P[_] => P(k)
-      }.reduce {
-        (p1, p2) => implicit ctx: P[_] => P(p1(ctx) | p2(ctx))
+      .map { k => implicit ctx: P[_] =>
+        P(k)
+      }.reduce { (p1, p2) => implicit ctx: P[_] =>
+        P(p1(ctx) | p2(ctx))
       }(implicitly[P[$]]).!
   }
   //    .memoize  // Do not memoize: breaks parsing!
 
-
-  def keyword[$: P]: P[String] = concatKeywords(simpleKeywords)
-    .memoize
+  def keyword[$: P]: P[String] = concatKeywords(simpleKeywords).memoize
 
   def builtin[$: P]: P[R] = {
-    (concatKeywords(constantSymbolNames).map(NanoConstant.withName).map(create.Constant)
-      )
+    (concatKeywords(constantSymbolNames).map(NanoConstant.withName).map(create.Constant))
   }.memoize
 
-
   // Helpers to make sure we are using valid keyword and operator names.
   def requireKeyword[$: P](name: String): P[Unit] = {
     assert(simpleKeywordsSet contains name, s"Keyword $name must be one of the supported Dhall keywords")
@@ -124,25 +99,15 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
 
   val constantSymbolNames = NanoConstant.namesToValuesMap.keySet.toIndexedSeq
 
-  val simpleKeywords = Seq(
-    "let",
-    "in",
-    "forall",
-  )
+  val simpleKeywords = Seq("let", "in", "forall")
 
   val simpleKeywordsSet = simpleKeywords.toSet
 
-  def lambda[$: P] = P(
-    "\u03BB" | "\\"
-  )
+  def lambda[$: P] = P("\u03BB" | "\\")
 
-  def arrow[$: P] = P(
-    "\u2192" | "->"
-  )
+  def arrow[$: P] = P("\u2192" | "->")
 
-  def identifier[$: P]: P[R] = P(
-    variable | builtin
-  )
+  def identifier[$: P]: P[R] = P(variable | builtin)
 
   /*
     If the identifier matches one of the names in the `builtin` rule, then it is a
@@ -152,37 +117,38 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
     Otherwise, this is a variable with name and index matching the label and index.
 
     This is guaranteed because `nonreserved_label` does not match any keyword or builtin, and we match builtins separately without a de Bruijn index.
-     */
-  def variable[$: P]: P[R] = P(
-    nonreserved_label ~ (whsp ~ "@" ~/ whsp ~ natural_literal).?
-  ).map { case (name, index) => create.Variable(name, index.map(_.value).getOrElse(BigInt(0))) }
-
-  def expression_lambda[$: P]: P[R] = P(lambda ~ whsp ~/ "(" ~ whsp ~/ nonreserved_label ~ whsp ~ ":" ~ whsp1 ~/ expression ~ whsp ~ ")" ~ whsp ~/ arrow ~/
-    whsp ~ expression)
-    .map { case (name, tipe, body) => create.Lambda(name, tipe, body) }
+   */
+  def variable[$: P]: P[R] = P(nonreserved_label ~ (whsp ~ "@" ~/ whsp ~ natural_literal).?).map { case (name, index) =>
+    create.Variable(name, index.map(_.value).getOrElse(BigInt(0)))
+  }
 
+  def expression_lambda[$: P]: P[R] = P(
+    lambda ~ whsp ~/ "(" ~ whsp ~/ nonreserved_label ~ whsp ~ ":" ~ whsp1 ~/ expression ~ whsp ~ ")" ~ whsp ~/ arrow ~/
+      whsp ~ expression
+  ).map { case (name, tipe, body) => create.Lambda(name, tipe, body) }
 
-  def expression_let_binding[$: P]: P[R] = P(let_binding.rep(1) ~ requireKeyword("in") ~ whsp1 ~/ expression)
-    .map { case (letBindings, expr) =>
-      letBindings.foldRight(expr) { case ((varName, body), prev) => create.Let(varName, body, prev) }
-    }
+  def expression_let_binding[$: P]: P[R] = P(let_binding.rep(1) ~ requireKeyword("in") ~ whsp1 ~/ expression).map { case (letBindings, expr) =>
+    letBindings.foldRight(expr) { case ((varName, body), prev) => create.Let(varName, body, prev) }
+  }
 
-  def expression_forall[$: P]: P[R] = P(forall ~ whsp ~/ "(" ~ whsp ~ nonreserved_label ~ whsp ~/ ":" ~ whsp1 ~/ expression ~ whsp ~ ")" ~ whsp ~ arrow ~/
-    whsp ~ expression)
-    .map { case (varName, tipe, body) => create.Forall(varName, tipe, body) }
+  def expression_forall[$: P]: P[R] = P(
+    forall ~ whsp ~/ "(" ~ whsp ~ nonreserved_label ~ whsp ~/ ":" ~ whsp1 ~/ expression ~ whsp ~ ")" ~ whsp ~ arrow ~/
+      whsp ~ expression
+  ).map { case (varName, tipe, body) => create.Forall(varName, tipe, body) }
 
   // (`A → B` is short-hand for `∀(_ : A) → B`)
-  def expression_arrow[$: P]: P[R] = P(operator_expression ~ whsp ~ arrow ~/ whsp ~ expression)
-    .map { case (head, body) => create.Forall(underscore, head, body) }
+  def expression_arrow[$: P]: P[R] = P(operator_expression ~ whsp ~ arrow ~/ whsp ~ expression).map { case (head, body) =>
+    create.Forall(underscore, head, body)
+  }
 
   def expression[$: P]: P[R] = P(
     //  "\(x : a) -> b"
     expression_lambda./
-      //
-      //  "let x     = e1 in e2"
-      //  We allow dropping the `in` between adjacent let_expressions; the following are equivalent:
-      //  "let x = e1 let y = e2 in e3"
-      //  "let x = e1 in let y = e2 in e3"
+    //
+    //  "let x     = e1 in e2"
+    //  We allow dropping the `in` between adjacent let_expressions; the following are equivalent:
+    //  "let x = e1 let y = e2 in e3"
+    //  "let x = e1 in let y = e2 in e3"
       | expression_let_binding./
       //
       //  "forall (x : a) -> b"
@@ -195,15 +161,12 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
       //
       //  "x : t"
       | annotated_expression./
-  )
-    .memoize
+  ).memoize
 
-  def annotated_expression[$: P]: P[R] = P(
-    operator_expression ~ (whsp ~ ":" ~ whsp1 ~/ expression).?
-  ).map { case (expr, tipe) =>
+  def annotated_expression[$: P]: P[R] = P(operator_expression ~ (whsp ~ ":" ~ whsp1 ~/ expression).?).map { case (expr, tipe) =>
     tipe match {
       case Some(t) => create.Annotation(expr, t)
-      case None => expr
+      case None    => expr
     }
   }
 
@@ -215,14 +178,12 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
     primitive_expression ~ (whsp1 ~ primitive_expression).rep // Do not insert a cut after whsp1 here.
   ).map { case (head, tail) => tail.foldLeft(head)((prev, expr) => create.Application(prev, expr)) }
 
-  def operator_expression[$: P]: P[R] = P(
-    plus_expression
-  )
+  def operator_expression[$: P]: P[R] = P(plus_expression)
 
   def natural_literal[$: P]: P[R with HasBigInt] = P(
     // Decimal; leading 0 digits are not allowed
     (CharIn("1-9") ~ DIGIT.rep).!.map(digits => BigInt(digits, 10))
-      // ... except for 0 itself
+    // ... except for 0 itself
       | P("0").map(_ => BigInt(0))
   ).map(create.NaturalLiteral)
 
@@ -233,26 +194,19 @@ final case class NanoDhallGrammar[R <: NanoExpr[R]](create: NanoExpr[R]) {
 
   def opPlus[$: P] = P("+")
 
-  def plus_expression[$: P]: P[R] = P(
-    application_expression ~ (whsp ~ opPlus ~ whsp1 ~/ application_expression).rep
-  ).withOperator(NanoOperator.Plus)
-    .memoize
+  def plus_expression[$: P]: P[R] = P(application_expression ~ (whsp ~ opPlus ~ whsp1 ~/ application_expression).rep).withOperator(NanoOperator.Plus).memoize
 
-  def complete_expression[$: P] = P(
-    whsp ~ expression ~ whsp
-  )
-    .memoize
+  def complete_expression[$: P] = P(whsp ~ expression ~ whsp).memoize
 
   def primitive_expression[$: P]: P[R] = P(
     //
     //  "2"
     natural_literal
-      //  "x"
-      //  "x@2"
+    //  "x"
+    //  "x@2"
       | identifier
       //
       //  "( e )"
       | P("(" ~/ complete_expression ~/ ")")
-  )
-    .memoize
+  ).memoize
 }
diff --git a/nano-dhall/src/main/scala/io/chymyst/nanodhall/NanoDhallParser.scala b/nano-dhall/src/main/scala/io/chymyst/nanodhall/NanoDhallParser.scala
@@ -7,7 +7,7 @@ final case class NanoDhallParser[R <: NanoExpr[R]](create: NanoExpr[R]) {
 
   def parse(input: String): R = parseToResult(input) match {
     case Parsed.Success(value: R, index) => value
-    case failure: Parsed.Failure =>
+    case failure: Parsed.Failure         =>
       Memoize.clearAll() // Parser will be re-run on trace(). So, the parser cache needs to be cleared.
       throw new Exception(s"Dhall parser error: ${failure.extra.trace().longMsg}")
   }

diff --git a/nano-dhall/src/main/scala/io/chymyst/nanodhall/NanoExpr.scala b/nano-dhall/src/main/scala/io/chymyst/nanodhall/NanoExpr.scala
@@ -26,7 +26,6 @@ trait NanoExpr[R <: NanoExpr[R]] {
   def Operator(l: R, op: NanoOperator, r: R): R
 }
 
-
 final case class VarName(name: String) extends AnyVal
 
 object VarName {
@@ -86,10 +85,7 @@ object NanoExprADT {
   final case class Operator(l: NanoExprADT, op: NanoOperator, r: NanoExprADT) extends NanoExprADT
 }
 
-
-sealed abstract class NanoConstant(override val entryName: String) extends EnumEntry {
-
-}
+sealed abstract class NanoConstant(override val entryName: String) extends EnumEntry {}
 
 object NanoConstant extends Enum[NanoConstant] {
 
@@ -104,11 +100,9 @@ object NanoConstant extends Enum[NanoConstant] {
   case object NaturalIsZero extends NanoConstant("Natural/isZero")
 
   case object NaturalSubtract extends NanoConstant("Natural/subtract")
-  case object Type extends NanoConstant("Type")
+  case object Type            extends NanoConstant("Type")
 }
 
-
-
 sealed abstract class NanoOperator(val name: String) extends EnumEntry
 
 object NanoOperator extends Enum[NanoOperator] {

diff --git a/nano-dhall/src/test/scala/io/chymyst/nanodhall/unit/NanoDhallGrammarTest.scala b/nano-dhall/src/test/scala/io/chymyst/nanodhall/unit/NanoDhallGrammarTest.scala
@@ -12,7 +12,11 @@ class NanoDhallGrammarTest extends FunSuite {
   test("parse natural number") {
     expect(parser1.parse("0") == NaturalLiteral(BigInt(0)))
     expect(parser1.parse("123") == NaturalLiteral(BigInt(123)))
-    expect(parser1.parse("123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890") == NaturalLiteral(BigInt("123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890")))
+    expect(
+      parser1.parse("123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890") == NaturalLiteral(
+        BigInt("123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890")
+      )
+    )
   }
 
   test("parse variable") {
@@ -26,17 +30,36 @@ class NanoDhallGrammarTest extends FunSuite {
   }
 
   test("parse lambda") {
-    expect(parser1.parse("\\(x : Natural) -> x + 1") == Lambda(VarName("x"), Constant(NanoConstant.Natural), Operator(Variable(VarName("x"), BigInt(0)), NanoOperator.Plus, NaturalLiteral(BigInt(1)))))
+    expect(
+      parser1.parse("\\(x : Natural) -> x + 1") == Lambda(
+        VarName("x"),
+        Constant(NanoConstant.Natural),
+        Operator(Variable(VarName("x"), BigInt(0)), NanoOperator.Plus, NaturalLiteral(BigInt(1))),
+      )
+    )
   }
 
-
   test("parse lambda and applications") {
     expect(NaturalLiteral(0) == NaturalLiteral(BigInt(0)))
-    expect(parser1.parse("(\\(x : Natural) -> f x + 1) 2") == Application(Lambda(VarName("x"), Constant(NanoConstant.Natural), Operator(Application(Variable(VarName("f"), BigInt(0)), Variable(VarName("x"), BigInt(0))), NanoOperator.Plus, NaturalLiteral(BigInt(1)))), NaturalLiteral(BigInt(2))))
+    expect(
+      parser1.parse("(\\(x : Natural) -> f x + 1) 2") == Application(
+        Lambda(
+          VarName("x"),
+          Constant(NanoConstant.Natural),
+          Operator(Application(Variable(VarName("f"), BigInt(0)), Variable(VarName("x"), BigInt(0))), NanoOperator.Plus, NaturalLiteral(BigInt(1))),
+        ),
+        NaturalLiteral(BigInt(2)),
+      )
+    )
   }
 
   test("parse forall") {
-    expect(parser1.parse("(\\(x : Natural) -> x + 1) : forall (x : Natural) -> Natural") == Annotation(Lambda(VarName("x"), Constant(NanoConstant.Natural), Operator(Variable(VarName("x"), BigInt(0)), NanoOperator.Plus, NaturalLiteral(BigInt(1)))), Forall(VarName("x"), Constant(NanoConstant.Natural), Constant(NanoConstant.Natural))))
+    expect(
+      parser1.parse("(\\(x : Natural) -> x + 1) : forall (x : Natural) -> Natural") == Annotation(
+        Lambda(VarName("x"), Constant(NanoConstant.Natural), Operator(Variable(VarName("x"), BigInt(0)), NanoOperator.Plus, NaturalLiteral(BigInt(1)))),
+        Forall(VarName("x"), Constant(NanoConstant.Natural), Constant(NanoConstant.Natural)),
+      )
+    )
   }
 
   test("parse let-bindings") {