Skip to content

Commit

Permalink
first version of toml export
Browse files Browse the repository at this point in the history
  • Loading branch information
winitzki committed Oct 16, 2024
1 parent 26fc47d commit 4bb41a0
Show file tree
Hide file tree
Showing 6 changed files with 262 additions and 26 deletions.
28 changes: 19 additions & 9 deletions scall-cli/src/main/scala/io/chymyst/dhall/Main.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,15 +14,24 @@ import sourcecode.{File => SourceFile, Line => SourceLine}
object Main {

sealed trait OutputMode

object OutputMode {
case object Dhall extends OutputMode
case object Text extends OutputMode
case object Yaml extends OutputMode
case object Json extends OutputMode
case object Toml extends OutputMode
case object Decode extends OutputMode
case object Encode extends OutputMode
case object Dhall extends OutputMode

case object Text extends OutputMode

case object Yaml extends OutputMode

case object Json extends OutputMode

case object Toml extends OutputMode

case object Decode extends OutputMode

case object Encode extends OutputMode

case object GetType extends OutputMode

case object GetHash extends OutputMode
}

Expand Down Expand Up @@ -60,8 +69,8 @@ object Main {
(tpe.print + "\n").getBytes("UTF-8")
case OutputMode.GetHash =>
("sha256:" + Semantics.semanticHash(expr, Paths.get(".")) + "\n").getBytes("UTF-8")
case OutputMode.Toml =>
(Yaml.toYaml(dhallFile.copy(value = expr), options) match {
case OutputMode.Toml =>
(Toml.toToml(expr) match {
case Left(value) => value + "\n"
case Right(value) => value
}).getBytes("UTF-8")

Check warning on line 76 in scall-cli/src/main/scala/io/chymyst/dhall/Main.scala

View check run for this annotation

Codecov / codecov/patch

scall-cli/src/main/scala/io/chymyst/dhall/Main.scala#L76

Added line #L76 was not covered by tests
Expand Down Expand Up @@ -131,6 +140,7 @@ object Main {
),
)
}

def main(args: Array[String]): Unit = ParserForMethods(this).runOrExit(args)
// $COVERAGE-ON$
}
6 changes: 3 additions & 3 deletions scall-cli/src/test/scala/io/chymyst/dhall/unit/MainSpec.scala
Original file line number Diff line number Diff line change
Expand Up @@ -87,11 +87,11 @@ class MainSpec extends FunSuite with TestTimings with ResourceFiles with ManyFix
}

test("fail to export yaml if Dhall expression contains unsupported types") {
expect(runMain("{ a = Natural, b = 2 }", "yaml") == "Error: Unsupported expression type for Yaml export: Natural of type Type\n")
expect(runMain("{ a = Natural, b = 2 }", "yaml") == "Error: Unsupported expression type for YAML export: Natural of type Type\n")
expect(
runMain("{ a = 1, b = \\(x : Bool) -> x }", "yaml") == "Error: Unsupported expression type for Yaml export: λ(x : Bool) → x of type ∀(x : Bool) → Bool\n"
runMain("{ a = 1, b = \\(x : Bool) -> x }", "yaml") == "Error: Unsupported expression type for YAML export: λ(x : Bool) → x of type ∀(x : Bool) → Bool\n"
)
expect(runMain("{ a = Type }", "yaml") == "Error: Unsupported expression type for Yaml export: Type of type Kind\n")
expect(runMain("{ a = Type }", "yaml") == "Error: Unsupported expression type for YAML export: Type of type Kind\n")
}

test("json main test cases") {
Expand Down
104 changes: 104 additions & 0 deletions scall-core/src/main/scala/io/chymyst/dhall/Toml.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
package io.chymyst.dhall

import io.chymyst.dhall.CBORmodel.CString
import io.chymyst.dhall.Syntax.{DhallFile, Expression, ExpressionScheme}
import io.chymyst.dhall.SyntaxConstants.FieldName

import scala.annotation.tailrec

object Toml {
final case class TomlOptions(indent: Int = 2)

private def errorMessage(expression: Expression): String =
s"Error: Unsupported expression type for TOML export: ${expression.print}, must be a record literal."

def toToml(dhallFile: DhallFile, tomlOptions: TomlOptions): Either[String, String] = toToml(dhallFile.value, tomlOptions)

@tailrec
def toToml(expression: Expression, tomlOptions: TomlOptions = TomlOptions()): Either[String, String] = {
expression.scheme match {
case ExpressionScheme.Annotation(data: Expression, tipe) => toToml(data, tomlOptions)

Check warning on line 20 in scall-core/src/main/scala/io/chymyst/dhall/Toml.scala

View check run for this annotation

Codecov / codecov/patch

scall-core/src/main/scala/io/chymyst/dhall/Toml.scala#L20

Added line #L20 was not covered by tests
case ExpressionScheme.RecordLiteral(defs: Seq[(FieldName, Expression)]) => topLevelRecordToToml(defs)
case ExpressionScheme.KeywordSome(data) => toToml(data, tomlOptions)
case _ => Left(errorMessage(expression))

Check warning on line 23 in scall-core/src/main/scala/io/chymyst/dhall/Toml.scala

View check run for this annotation

Codecov / codecov/patch

scall-core/src/main/scala/io/chymyst/dhall/Toml.scala#L22-L23

Added lines #L22 - L23 were not covered by tests
}
}

private def isRecord(expression: Expression): Boolean = expression.scheme match {
case ExpressionScheme.RecordLiteral(_) => true
case _ => false
}

private def exprToToml(expression: Expression, atTopLevel: Boolean): Either[String, String] = expression.scheme match {

case ExpressionScheme.EmptyList(_) => Right("[]")

Check warning on line 34 in scall-core/src/main/scala/io/chymyst/dhall/Toml.scala

View check run for this annotation

Codecov / codecov/patch

scall-core/src/main/scala/io/chymyst/dhall/Toml.scala#L34

Added line #L34 was not covered by tests
case ExpressionScheme.NonEmptyList(exprs) =>
val converted = exprs.map(exprToToml(_, atTopLevel = false))
val errors = converted.collect { case Left(x) => x }
if (errors.nonEmpty) Left(errors.mkString("; "))
else {
Right(converted.collect { case Right(x) => x }.mkString("[ ", ", ", " ]"))

}
case ExpressionScheme.RecordLiteral(defs) =>
val converted = defs.map { case (fieldName, expr) => tomlKeyValue(fieldName, expr) }
val errors = converted.collect { case Left(x) => x }
if (errors.nonEmpty) Left(errors.mkString("; "))
else {
val convertedValues = converted.collect { case Right(x) => x }
val (prefix, suffix) = if (atTopLevel) ("", "") else ("{\n", "\n}\n")
Right(convertedValues.mkString(prefix, "\n", suffix))
}
case ExpressionScheme.Annotation(data, tipe) => exprToToml(data, atTopLevel)

Check warning on line 52 in scall-core/src/main/scala/io/chymyst/dhall/Toml.scala

View check run for this annotation

Codecov / codecov/patch

scall-core/src/main/scala/io/chymyst/dhall/Toml.scala#L52

Added line #L52 was not covered by tests
case ExpressionScheme.DoubleLiteral(_) | ExpressionScheme.NaturalLiteral(_) | ExpressionScheme.IntegerLiteral(_) | ExpressionScheme.DateLiteral(_, _, _) |
ExpressionScheme.TimeLiteral(_, _, _, _) | ExpressionScheme.TimeZoneLiteral(_) =>
Right(expression.print)
case ExpressionScheme.TextLiteral(Nil, str) => Right(CString(str).toString)

case ExpressionScheme.KeywordSome(data) => exprToToml(data, atTopLevel)

Check warning on line 58 in scall-core/src/main/scala/io/chymyst/dhall/Toml.scala

View check run for this annotation

Codecov / codecov/patch

scall-core/src/main/scala/io/chymyst/dhall/Toml.scala#L58

Added line #L58 was not covered by tests
case ExpressionScheme.ExprConstant(SyntaxConstants.Constant.False) | ExpressionScheme.ExprConstant(SyntaxConstants.Constant.True) =>
Right(expression.print.toLowerCase)
case _ => Left(errorMessage(expression))

Check warning on line 61 in scall-core/src/main/scala/io/chymyst/dhall/Toml.scala

View check run for this annotation

Codecov / codecov/patch

scall-core/src/main/scala/io/chymyst/dhall/Toml.scala#L61

Added line #L61 was not covered by tests
}

private def keyNameToToml(str: String): Either[String, String] = {
// TODO: string escaping and/or errors
Right(str)
}

private def tomlKeyValue(name: FieldName, expression: Expression): Either[String, String] = {
val converted = Seq(keyNameToToml(name.name), exprToToml(expression, atTopLevel = false))

val errors = converted.collect { case Left(x) => x }
if (errors.nonEmpty) Left(errors.mkString("; "))
else {
val Seq(tomlKey, tomlValue) = converted.collect { case Right(x) => x }
Right(s"$tomlKey = $tomlValue")
}
}

def tomlTable(name: FieldName, expression: Expression): Either[String, String] = {
val converted = Seq(keyNameToToml(name.name), exprToToml(expression, atTopLevel = true))

val errors = converted.collect { case Left(x) => x }
if (errors.nonEmpty) Left(errors.mkString("; "))
else {
val Seq(tomlKey, tomlValue) = converted.collect { case Right(x) => x }
Right(s"[$tomlKey]\n$tomlValue")
}
}

private def topLevelRecordToToml(defs: Seq[(FieldName, Expression)]): Either[String, String] = {
// If a record value is not itself a nested record, it is printed as key = value.
// We are at top level. Replace each nested record by a TOML "table".
val converted: Seq[Either[String, String]] = defs.map { case (fieldName, expr) =>
if (isRecord(expr)) {
tomlTable(fieldName, expr)
} else {
tomlKeyValue(fieldName, expr)
}
}
val errors = converted.collect { case Left(x) => x }
if (errors.nonEmpty) Left(errors.mkString("; ")) else Right(converted.collect { case Right(x) => x }.mkString("", "\n", "\n"))
}
}
2 changes: 1 addition & 1 deletion scall-core/src/main/scala/io/chymyst/dhall/Yaml.scala
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ object Yaml {

// This function should ignore options.createDocuments because it is used recursively for sub-document Yaml values.
private def toYamlLines(expr: Expression, options: YamlOptions): Either[String, YamlLines] = {
val format = if (options.jsonFormat) "JSON" else "Yaml"
val format = if (options.jsonFormat) "JSON" else "YAML"
expr.inferType match {
case TypecheckResult.Invalid(errors) => Left(errors.toString)
case TypecheckResult.Valid(tpe) =>
Expand Down
64 changes: 64 additions & 0 deletions scall-core/src/test/scala/io/chymyst/dhall/unit/TomlTest.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
package io.chymyst.dhall.unit

import com.eed3si9n.expecty.Expecty.expect
import io.chymyst.dhall.Parser.StringAsDhallExpression
import io.chymyst.dhall.Syntax.DhallFile
import io.chymyst.dhall.Toml.TomlOptions
import io.chymyst.dhall.{Toml, Yaml}
import io.chymyst.dhall.Yaml.YamlOptions
import munit.FunSuite

class TomlTest extends FunSuite {

test("toml output should ignore comment headers 1") {
val dhallFile = DhallFile(Seq(), "-- comment", """{ a = "True" }""".dhall)
val result = Toml.toToml(dhallFile, TomlOptions()).merge
expect(
result ==
"""a = "True"
|""".stripMargin
)
}

test("toml output for record of lists with indent 4") {
expect(
Toml.toToml("{a = [1, 2, 3], b = [4, 5]}".dhall).merge ==
"""a = [ 1, 2, 3 ]
|b = [ 4, 5 ]
|""".stripMargin
)
}

test("toml output for strings with special characters") {
val result1 = Toml.toToml("{a = \"-\"}".dhall).merge
expect(
result1 ==
"""a = "-"
|""".stripMargin
)
val result2 = Toml.toToml("{a = \"a-b\"}".dhall).merge
expect(
result2 ==
"""a = "a-b"
|""".stripMargin
)
val result3 = Toml.toToml("""{a = "\"abc\""}""".dhall).merge
expect(
result3 ==
"""a = "\"abc\""
|""".stripMargin
)
}

test("toml output with nested records") {
expect(
Toml.toToml("{ a = { b = [1, 2, 3] , c = True } }".dhall).merge
==
"""[a]
|b = [ 1, 2, 3 ]
|c = true
|""".stripMargin
)
}

}
84 changes: 71 additions & 13 deletions tutorial/programming_dhall.md
Original file line number Diff line number Diff line change
Expand Up @@ -2037,7 +2037,7 @@ In addition, Dhall's `assert` feature may be sometimes used to verify the typecl

To see how this works, let us implement some well-known typeclasses in Dhall.

### Show
### The "Show" typeclass

The `Show` typeclass is usually defined in Haskell as:

Expand Down Expand Up @@ -2111,7 +2111,6 @@ class Monoid m where
mempty :: m
mappend :: m -> m -> m
```

The values `mempty` and `mappend` are the **typeclass methods** of the `Monoid` typeclass.

In Scala, a corresponding definition is:
Expand Down Expand Up @@ -2187,7 +2186,9 @@ let foldMap
List/fold a xs m (λ(x : a) λ(y : m) monoid_m.append y (f x)) monoid_m.empty
```

This code shows how to implement typeclass constraints in Dhall.
Typeclass constraints are implemented in Dhall via code similar to this.
Functions with typeclass constraints will have type signatures of the form `∀(t : Type) → SomeTypeclass t → ...`.
When calling those functions, the programmer will have to pass evidence values proving that the type parameters are assigned to types that belong to the specified typeclass.

### Verifying the laws of monoids

Expand All @@ -2208,23 +2209,20 @@ let monoidLaws = λ(m : Type) → λ(monoid_m : Monoid m) → λ(x : m) → λ(y
monoid_assoc_law = plus x (plus y z) === plus (plus x y) z,
}
```
Note that we did not write `assert` expressions here.
If we did, they would have immediately failed because the body of `monoidLaws` cannot yet substitute a specific implementation of `monoid_m` to check whether the laws hold.
For instance, the expressions `plus e x` and `x` are always going to be different _within the body of that function_.
Those expressions will become the same only after we substitute a lawful implementation of a `Monoid` typeclass.
Note that we did not add `assert` expressions here.
If we did, the assertions would have always failed because the body of `monoidLaws` cannot yet substitute a specific implementation of `monoid_m` to check whether the laws hold.
For instance, the expressions `plus e x` and `x` are always going to be different _while type-checking the body of that function_, which happens before that function is ever applied.
Those expressions will become the same only after we apply `monoidLaws` to a type `m` and a lawful implementation of a `Monoid` typeclass for `m`.

So, to check the laws we will need to write `assert` values corresponding to each law and a given typeclass evidence value.
To check the laws, we will write `assert` values corresponding to each law and a given typeclass evidence value.

As an example, here is how we may check that the laws hold for the `Monoid` evidence value `monoidBool` defined above:
As an example, here is how to check the monoid laws for the evidence value `monoidBool` defined above:

```dhall
let check_monoidBool_left_id_law = λ(x : Bool) λ(y : Bool) λ(z : Bool)
assert : (monoidLaws Bool monoidBool x y z).monoid_left_id_law
```

Note: Some of this functionality is non-standard and only available in the [Scala implementation of Dhall](https://github.com/winitzki/scall).
Standard Dhall cannot establish an equivalence between expressions such as `(x + y) + z` and `x + (y + z)` when `x`, `y`, `z` are variables.

### The `Functor` typeclass

In the jargon of the functional programming community, a **functor** is a type constructor `F` with an `fmap` method having the standard type signature and obeying the functor laws.
Expand Down Expand Up @@ -7746,7 +7744,67 @@ let C = λ(a : Type) → LFix (F a)
```
The type signature of `zip` for `C` must be:
```dhall
let zip_C : (a : Type) C a (b : Type) C b C (Pair a b) = ???
let zip_C : (a : Type) C a (b : Type) C b C (Pair a b) = ???
```

It turns out that we can implement an `Applicative` evidence for the functor `C` if the bifunctor `F` supports two functions that we will call `bizip_F1` and `bizip_FC`.
Those functions express a certain kind of applicative-like property for `F`.

The function `bizip_F1` must have the type signature:
```dhall
let bizip_F1 : (r : Type) (a : Type) F a r (b : Type) F b r F (Pair a b) r = ???
```
This type is similar to the `zip` function except it works only with the first type parameter of `F`, keeping the second type parameter (`r`) fixed.
The function `bizip_F1` is not required to satisfy any laws.

The function `bizip_FC` must have the type signature:
```dhall
let bizip_FC : (a : Type) F a (C a) (b : Type) F b (C b) F (Pair a b) (Pair (C a) (C b) = ???
```
The type signature of `bizip_FC` is of the form `F a p → F b q → F (Pair a b) (Pair p q)` if we set `p = C a` and `q = C b`.
So, it is similar to `zip` that works at the same time with both type parameters of `F`.
However, functions with the type `F a r → F b s → F (Pair a b) (Pair r s)` do not exist for certain perfectly ordinary recursion schemes `F`, such as that for non-empty lists (`F a r = Either a (Pair a r)`) and for non-empty binary trees (`F a r = Either a (Pair r r)`).
On the other hand, `bizip_FC` can be implemented for all polynomial bifunctors `F`.

In addition, we require a function for computing the recursion depth of a value of type `C a`.
That function (`depth : ∀(a : Type) → C a → Natural`) can be implemented if we have a function `max : F {} Natural → Natural` that finds the maximum among all `Natural` numbers stored in a given value of type `F {} Natural`.
The function `max` is available for any given polynomial bifunctor `F`.

For illustration, let us implement these functions for `F a r = Either a (Pair r r)`.

The function `bizip_F1` can be implemented in any way whatsoever, as it does not need to satisfy any laws.
For instance, we may discard arguments whenever one of the values of type `F a r` is a `Right`.
```dhall
let F = λ(a : Type) λ(r : Type) Either a (Pair r r)
let bizip_F1
: (r : Type) (a : Type) F a r (b : Type) F b r F (Pair a b) r
= λ(r : Type) λ(a : Type) λ(far: Either a (Pair r r)) λ(b : Type) λ(fbr: Either b (Pair r r))
merge {
Left = λ(x : a) merge {
Left = λ(y : b) (F (Pair a b) r).Left { _1 = x, _2 = y }
, Right = λ(p : Pair r r) (F (Pair a b) r).Right p
} fbr
, Right = λ(p : Pair r r) (F (Pair a b) r).Right p
} far
```

The function `bizip_FC` is implemented similarly to a lawful `zip` method. Arguments are never discarded.
When one argument is a `Left x` and the other is a `Right y` then we use `C`'s `Functor` instance to produce required values of type `Pair (C a) (C b)`.
A `Functor` typeclass evidence for `C` is produced automatically from a `Bifunctor` evidence for `F`:
```dhall
let C = λ(a : Type) LFix (F a)
let bifunctorF : Bifunctor F = ???
let functorC : Functor C = ???
let bizip_FC1
: (r : Type) (a : Type) F a r (b : Type) F b r F (Pair a b) r
= λ(r : Type) λ(a : Type) λ(far: Either a (Pair r r)) λ(b : Type) λ(fbr: Either b (Pair r r))
merge {
Left = λ(x : a) merge {
Left = λ(y : b) (F (Pair a b) r).Left { _1 = x, _2 = y }
, Right = λ(p : Pair r r) (F (Pair a b) r).Right p
} fbr
, Right = λ(p : Pair r r) (F (Pair a b) r).Right p
} far
```


Expand Down

0 comments on commit 4bb41a0

Please sign in to comment.