From afb875fe827fb4217f08318afe53cef386d9003c Mon Sep 17 00:00:00 2001 From: Raphael Fromentin Date: Wed, 13 Sep 2023 22:14:53 +0200 Subject: [PATCH] dev: Add snippet checking to reference pages --- docs/_docs/reference/constraint.md | 2 + docs/_docs/reference/implication.md | 49 +++++++++- docs/_docs/reference/iron-type.md | 10 +++ docs/_docs/reference/newtypes.md | 133 +++++++++++++++++++++++++++- docs/_docs/reference/refinement.md | 55 +++++++++--- 5 files changed, 232 insertions(+), 17 deletions(-) diff --git a/docs/_docs/reference/constraint.md b/docs/_docs/reference/constraint.md index 5e0e2d25..1bd5bc5a 100644 --- a/docs/_docs/reference/constraint.md +++ b/docs/_docs/reference/constraint.md @@ -66,6 +66,7 @@ Here is how it looks: ```scala sc:nocompile sc-name:PositiveAndConstraint.scala sc-compile-with:Positive.scala //{ import io.github.iltotore.iron.* + //} given Constraint[Int, Positive] with @@ -80,6 +81,7 @@ you can use a trait to reduce boilerplate: ```scala sc:nocompile sc-compile-with:Positive.scala //{ import io.github.iltotore.iron.* + //} trait PositiveConstraint[A] extends Constraint[A, Positive]: override inline def message: String = "Should be strictly positive" diff --git a/docs/_docs/reference/implication.md b/docs/_docs/reference/implication.md index fb9f7f80..2f4a50bb 100644 --- a/docs/_docs/reference/implication.md +++ b/docs/_docs/reference/implication.md @@ -16,8 +16,8 @@ For example, the following code compiles due to [transitivity](https://en.wikipe //{ import io.github.iltotore.iron.* import io.github.iltotore.iron.constraint.numeric.Greater -//} +//} val x: Int :| Greater[5] = ??? val y: Int :| Greater[0] = x ``` @@ -36,12 +36,25 @@ Note: implications are a purely compile-time mechanism. For example, the following implication: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Not + +//} given [C1]: (C1 ==> Not[Not[C1]]) = Implication() ``` allows us (if imported) to compile this code: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Not +import io.github.iltotore.iron.constraint.numeric.Greater + +given [C1]: (C1 ==> Not[Not[C1]]) = Implication() + +//} val x: Int :| Greater[0] = ??? val y: Int :| Not[Not[Greater[0]]] = x //C1 implies Not[Not[C1]]: `x` can be safely casted. ``` @@ -51,7 +64,13 @@ val y: Int :| Not[Not[Greater[0]]] = x //C1 implies Not[Not[C1]]: `x` can be saf Almost every implication has a dependency. For example, our previous "double negation" implication doesn't work in the following case: -```scala +```scala sc:nocompile +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Not +import io.github.iltotore.iron.constraint.numeric.Greater + +//} val x: Int :| Greater[1] = ??? //Assuming that Greater[1] ==> Greater[0] @@ -61,6 +80,11 @@ val y: Int :| Not[Not[Greater[0]]] = x But it should. This can be fixed by using two different constraints linked by an implication: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Not + +//} given [C1, C2](using C1 ==> C2): (C1 ==> Not[Not[C2]]) = Implication() ``` @@ -69,6 +93,14 @@ given [C1, C2](using C1 ==> C2): (C1 ==> Not[Not[C2]]) = Implication() Our implication now depends on another implication: `C1 ==> C2`. With this implementation, our code now compiles: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Not +import io.github.iltotore.iron.constraint.numeric.Greater + +given [C1, C2](using C1 ==> C2): (C1 ==> Not[Not[C2]]) = Implication() + +//} val x: Int :| Greater[1] = ??? //Assuming that Greater[1] ==> Greater[0] @@ -86,6 +118,11 @@ This can be combined with [[iron.ops|io.github.iltotore.iron.ops]] to create log For example, we can implement the [transitive relation](https://en.wikipedia.org/wiki/Transitive_relation): ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Greater + +//} import io.github.iltotore.iron.compileTime.* given [V1, V2](using V1 > V2 =:= true): (Greater[V1] ==> Greater[V2]) = Implication() @@ -96,6 +133,14 @@ given [V1, V2](using V1 > V2 =:= true): (Greater[V1] ==> Greater[V2]) = Implicat Now, the following code compiles: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.compileTime.* +import io.github.iltotore.iron.constraint.numeric.Greater + +given [V1, V2](using V1 > V2 =:= true): (Greater[V1] ==> Greater[V2]) = Implication() + +//} val x: Int :| Greater[1] = ??? val y: Int :| Greater[0] = x //x > 1 and 1 > 0, so x > 0. ``` diff --git a/docs/_docs/reference/iron-type.md b/docs/_docs/reference/iron-type.md index b3e70a37..72a48ea0 100644 --- a/docs/_docs/reference/iron-type.md +++ b/docs/_docs/reference/iron-type.md @@ -20,6 +20,11 @@ used in set builders. Refined types are subtypes of their unrefined form. For instance, `Int :| Greater[0]` is a subtype of `Int`. ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Greater + +//} val x: Int :| Greater[0] = ??? val y: Int = x //Compiles ``` @@ -28,6 +33,11 @@ val y: Int = x //Compiles types overheadless. ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Greater + +//} val x: Int :| Greater[0] = ??? ``` diff --git a/docs/_docs/reference/newtypes.md b/docs/_docs/reference/newtypes.md index c44bff50..83200e52 100644 --- a/docs/_docs/reference/newtypes.md +++ b/docs/_docs/reference/newtypes.md @@ -11,15 +11,28 @@ You can create no-overhead new types like [scala-newtype](https://github.com/est Iron provides a convenient trait called `RefinedTypeOps` to easily add smart constructors to your type: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} type Temperature = Double :| Positive object Temperature extends RefinedTypeOps[Temperature] ``` ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +type Temperature = Double :| Positive +object Temperature extends RefinedTypeOps[Temperature] + +//} val temperature = Temperature(15) //Compiles println(temperature) //15 -val positive: Int :| Positive = 15 +val positive: Double :| Positive = 15 val tempFromIron = Temperature(positive) //Compiles too ``` @@ -28,6 +41,14 @@ val tempFromIron = Temperature(positive) //Compiles too `RefinedTypeOps` supports [all refinement methods](refinement.md) provided by Iron: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +type Temperature = Double :| Positive +object Temperature extends RefinedTypeOps[Temperature] + +//} val unsafeRuntime: Temperature = Temperature.applyUnsafe(15) val option: Option[Temperature] = Temperature.option(15) val either: Either[String, Temperature] = Temperature.either(15) @@ -36,13 +57,34 @@ val either: Either[String, Temperature] = Temperature.either(15) Constructors for other modules exist: ```scala -val zioValidation: Temperature = Temperature.validation(15) +//{ +import zio.prelude.Validation + +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive +import io.github.iltotore.iron.zio.* + +type Temperature = Double :| Positive +object Temperature extends RefinedTypeOps[Temperature] + +//} +val zioValidation: Validation[String, Temperature] = Temperature.validation(15) ``` Note: all these constructors are inline. They don't bring any overhead: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +type Temperature = Double :| Positive +object Temperature extends RefinedTypeOps[Temperature] + +//} val temperature: Temperature = Temperature(15) + +val runtimeValue: Double = ??? val unsafeRuntime: Temperature = Temperature.applyUnsafe(runtimeValue) ``` @@ -50,6 +92,8 @@ compiles to ```scala val temperature: Double = 15 + +val runtimeValue: Double = ??? val unsafeRuntime: Double = if runtimeValue > 0 then runtimeValue else throw new IllegalArgumentException("...") @@ -62,10 +106,23 @@ constraint. [[Pure|io.github.iltotore.iron.constraint.any.Pure]] is an alias for [[True|io.github.iltotore.iron.constraint.any.True]], a constraint that is always satisfied. ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Pure + +//} type FirstName = String :| Pure object FirstName extends RefinedTypeOps[FirstName] ``` ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.any.Pure + +type FirstName = String :| Pure +object FirstName extends RefinedTypeOps[FirstName] + +//} val firstName = FirstName("whatever") ``` @@ -74,10 +131,22 @@ val firstName = FirstName("whatever") The aliased type of an [opaque type](https://docs.scala-lang.org/scala3/book/types-opaque-types.html) is only known in its definition file. It is not considered like a type alias outside of it: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} opaque type Temperature = Double :| Positive ``` -```scala +```scala sc:nocompile +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +opaque type Temperature = Double :| Positive + +//} val x: Double :| Positive = 5 val temperature: Temperature = x //Error: Temperature expected, got Double :| Positive ``` @@ -85,11 +154,24 @@ val temperature: Temperature = x //Error: Temperature expected, got Double :| Po Such encapsulation is especially useful to avoid mixing different domain types with the same refinement: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} opaque type Temperature = Double :| Positive opaque type Moisture = Double :| Positive ``` ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +opaque type Temperature = Double :| Positive +opaque type Moisture = Double :| Positive + +//} case class Info(temperature: Temperature, moisture: Moisture) val temperature: Temperature = ??? @@ -102,11 +184,24 @@ Therefore, it also forces the user to convert the value explicitly, for example `RefinedTypeOps`: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} opaque type Temperature = Double :| Positive object Temperature extends RefinedTypeOps[Temperature] ``` ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +opaque type Temperature = Double :| Positive +object Temperature extends RefinedTypeOps[Temperature] + +//} val value: Double :| Positive = ??? val a: Temperature = value //Compile-time error @@ -141,6 +236,12 @@ object Foo: def apply(value: String): Foo = value ``` ```scala +//{ +opaque type Foo <: String = String +object Foo: + def apply(value: String): Foo = value + +//} val x = Foo("abcd") x.toUpperCase //"ABCD" ``` @@ -148,10 +249,24 @@ x.toUpperCase //"ABCD" Therefore, you can combine it with `RefinedTypeOps`: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.all.* + +//} opaque type FirstName <: String :| ForAll[Letter] = String :| ForAll[Letter] object FirstName extends RefinedTypeOps[FirstName] ``` -```scala + +```scala sc:nocompile +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.all.* + +opaque type FirstName <: String :| ForAll[Letter] = String :| ForAll[Letter] +object FirstName extends RefinedTypeOps[FirstName] + +//} val x = FirstName("Raphael") x.toUpperCase //"RAPHAEL" ``` @@ -162,6 +277,11 @@ Usually, transparent type aliases do not need a special handling for typeclass d instances for `IronType`. However, this is not the case for opaque type aliases, for instance: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} opaque type Temperature = Double :| Positive object Temperature extends RefinedTypeOps[Temperature] ``` @@ -172,6 +292,11 @@ each `RefinedTypeOps`. It works the same as from the [ZIO JSON module](https://iltotore.github.io/iron/docs/modules/zio-json.html): ```scala +//{ +import zio.json.* +import io.github.iltotore.iron.* + +//} inline given[T](using mirror: RefinedTypeOps.Mirror[T], ev: JsonDecoder[mirror.IronType]): JsonDecoder[T] = ev.asInstanceOf[JsonDecoder[T]] ``` diff --git a/docs/_docs/reference/refinement.md b/docs/_docs/reference/refinement.md index 81ff8b31..58de4ecf 100644 --- a/docs/_docs/reference/refinement.md +++ b/docs/_docs/reference/refinement.md @@ -11,8 +11,6 @@ Iron provides multiple ways at compile time or runtime to refine a type dependin Unconstrained values are automatically cast to their refined form if they satisfy the constraint at compile time: ```scala -//This import will be assumed in next examples. - import io.github.iltotore.iron.* import io.github.iltotore.iron.constraint.numeric.* @@ -22,10 +20,15 @@ val x: Int :| Greater[0] = 5 If they don't, a compile-time error is thrown: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.* + +//} val y: Int :| Greater[0] = -1 ``` -```scala +```scala sc:nocompile -- Constraint Error -------------------------------------------------------- Could not satisfy a constraint for type scala.Int. @@ -37,11 +40,16 @@ Message: Should be strictly greater than 0 If the value (or the constraint itself) cannot be evaluated at compile time, then the compilation also fails: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.* + +//} val runtimeValue: Int = ??? val x: Int :| Greater[0] = runtimeValue ``` -```scala +```scala sc:nocompile -- Constraint Error -------------------------------------------------------- Cannot refine non full inlined input at compile-time. To test a constraint at runtime, use the `refine` extension method. @@ -58,6 +66,11 @@ By default, all fully inlined literals (including AnyVals, String, Option and Ei Note that the constraint condition also needs to be fully inlined. ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.* + +//} inline val value = 2 val x: Int :| Greater[0] = value //OK ``` @@ -66,7 +79,7 @@ val x: Int :| Greater[0] = value //OK Sometimes, you want to refine a value that is not available at compile time. For example in the case of form validation. -```scala +```scala sc:nocompile import io.github.iltotore.iron.* import io.github.iltotore.iron.constraint.string.* @@ -81,7 +94,12 @@ Fortunately, Iron supports explicit runtime checking using extension methods You can imperatively refine a value at runtime (much like an assertion) using the `refine[C]` method: -```scala +```scala sc:nocompile +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.string.* + +//} val runtimeString: String = ??? val username: String :| Alphanumeric = runtimeString.refine //or more explicitly, refine[LowerCase]. ``` @@ -94,7 +112,7 @@ does not pass the assertion. Iron also provides methods similar to `refine` but returning an `Option` (`refineOption`) or an `Either` (`refineEither`), useful for data validation: -```scala +```scala sc:nocompile import io.github.iltotore.iron.* import io.github.iltotore.iron.constraint.all.* @@ -116,7 +134,7 @@ createUser("Iltotore", 18) //Right(User("Iltotore", 18)) You can accumulate refinement errors using the [Cats](../modules/cats.md) or [ZIO](../modules/zio.md) module. Here is an example with the latter: -```scala +```scala sc:nocompile import zio.prelude.Validation import io.github.iltotore.iron.* @@ -150,7 +168,7 @@ Check the [Cats module](../modules/cats.md) or [ZIO module](../modules/zio.md) p Sometimes you want to refine the same value multiple times with different constraints. This is especially useful when you want fine-grained refinement errors. Let's take the last example but with passwords: -```scala +```scala sc:nocompile import io.github.iltotore.iron.* import io.github.iltotore.iron.constraint.all.* @@ -178,7 +196,7 @@ However, it's not clear which constraint is not satisfied: is my password to sho Using `refineFurther`/`refineFurtherEither`/... enables more detailed messages: -```scala +```scala sc:nocompile type Username = DescribedAs[Alphanumeric, "Username should be alphanumeric"] type Password = DescribedAs[ Alphanumeric & MinLength[5] & Exists[Letter] & Exists[Digit], @@ -205,7 +223,7 @@ createUser("Iltotore", "abc123 ") //Left("Should be alphanumeric") Or with custom error messages: -```scala +```scala sc:nocompile type Username = DescribedAs[Alphanumeric, "Username should be alphanumeric"] type Password = DescribedAs[ Alphanumeric & MinLength[5] & Exists[Letter] & Exists[Digit], @@ -237,6 +255,11 @@ Note: Accumulative versions exist for [Cats](../modules/cats.md) and [ZIO](../mo Sometimes, you know that your value always passes (possibly at runtime) a constraint. For example: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} val random = scala.util.Random.nextInt(9)+1 val x: Int :| Positive = random ``` @@ -246,6 +269,11 @@ We could use `refine` but we don't actually need to apply the constraint to `ran Instead, we can can use `assume[C]`. It simply acts like a safer cast. ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} val random = scala.util.Random.nextInt(9)+1 val x: Int :| Positive = random.assume ``` @@ -253,6 +281,11 @@ val x: Int :| Positive = random.assume This code will compile to: ```scala +//{ +import io.github.iltotore.iron.* +import io.github.iltotore.iron.constraint.numeric.Positive + +//} val random: Int = scala.util.Random.nextInt(9)+1 val x: Int = random ```