From ad8859c0e2e6f925b56c776b6a39f1329ec2cd30 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Mon, 20 Jan 2025 17:49:16 +0100 Subject: [PATCH] reformat code and upgrade dhall --- .github/workflows/build-and-test.yml | 2 +- github-scala-build-and-test.dhall | 2 +- .../chymyst/nanodhall/NanoDhallGrammar.scala | 156 ++++++------------ .../chymyst/nanodhall/NanoDhallParser.scala | 2 +- .../scala/io/chymyst/nanodhall/NanoExpr.scala | 10 +- .../nanodhall/unit/NanoDhallGrammarTest.scala | 33 +++- 6 files changed, 88 insertions(+), 117 deletions(-) diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml index c701e738..e252515f 100644 --- 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 index 98088a74..911bb8c6 100644 --- 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 index aba69469..36c45852 100644 --- 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 index e0e9cf5a..e491bd4b 100644 --- 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 index 41b162c8..b69b4e35 100644 --- 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 index d8291f0d..190410f4 100644 --- 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") {