From 86685e9ec5e8d7ce1d6cec79e1e6160a8699ccc8 Mon Sep 17 00:00:00 2001 From: "Serge S. Gulin" Date: Wed, 4 Mar 2026 18:25:48 +0300 Subject: [PATCH 1/3] [ docs ] Use perl for cross-platform capitalization in typecheck script Replace sed-based capitalization with perl for cross-platform compatibility. BSD sed on macOS doesn't support `\u` escape sequences, causing the script to produce literal 'u' prefixes instead of capitalized directory names. Changes: - Use perl for case conversion with sed fallback - Replace echo -n with printf for POSIX shell compliance - Use heredoc for docs.ipkg generation for reliable newline handling --- tests/docs/typecheck/run | 35 +++++++++++++++++++++++++++-------- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/tests/docs/typecheck/run b/tests/docs/typecheck/run index 06e8b74f2..80befb361 100755 --- a/tests/docs/typecheck/run +++ b/tests/docs/typecheck/run @@ -9,28 +9,47 @@ DOCSDIR=../../../docs/source/ # Generate `src` dir and symlinks to all `*.md` files (upper-case renamed) all_modules=$( find "$DOCSDIR" -type f -name '*.md' -print | sort | while read r; do - # capitalization idea taken from https://stackoverflow.com/questions/27703739/capitalize-words-in-a-bash-variable-using-sed - capname=$(echo "${r#$DOCSDIR}" | sed 's/^./\u&/; s|/\(.\)|/\u\1|g; s/-\(.\)/\u\1/g') + # Use perl for cross-platform compatibility (MacOS BSD sed doesn't support \u) + # Convert explanation/derivation/design/closure-of-gens.md -> Explanation/Derivation/Design/ClosureOfGens.md + if command -v perl >/dev/null 2>&1; then + # Perl command explanation: + # s/(^|\/)(.)/\1\u\2/g - Capitalize letter at start (^) or after slash (/) + # s/-(.)/\u\1/g - Remove dash and capitalize following letter + capname=$(echo "${r#$DOCSDIR}" | perl -pe 's/(^|\/)(.)/\1\u\2/g; s/-(.)/\u\1/g') + else + # Sed command explanation (POSIX): + # s/^./\u&/ - Capitalize first character of string + # s|/\(.\)|/\u\1|g - Capitalize character after each slash + # s/-\(.\)/\u\1/g - Capitalize character after each dash + # On BSD/macOS sed, \u is literal 'u', producing uexplanation.uderivation... + # capitalization idea taken from https://stackoverflow.com/questions/27703739/capitalize-words-in-a-bash-variable-using-sed + capname=$(echo "${r#$DOCSDIR}" | sed 's/^./\u&/; s|/\(.\)|/\u\1|g; s/-\(.\)/\u\1/g') + fi localname="src/$capname" localdir=$(dirname "$localname")/ mkdir -p "$localdir" + # sed 's|[^/]*/|\.\./|g' replaces each directory component with ../ + # Example: src/Explanation/Derivation/Design/ -> ../../../../ ln -s "$(echo "$localdir" | sed 's|[^/]*/|\.\./|g')$r" "$localname" + # Convert path to module name: remove .md extension, replace / with . + # Example: Explanation/Derivation/Design/ClosureOfGens.md -> Explanation.Derivation.Design.ClosureOfGens modulename=$(echo "${capname%.md}" | sed 's|/|\.|g') - echo -n ", $modulename" + # Use printf instead of echo -n for POSIX compliance and consistent behavior across shells + # printf outputs format string with variables, no trailing newline + printf ", %s" "$modulename" # Accumulate module names for docs.ipkg done ) -# Generate `docs.ipkg` containing all `*.md` files (upper-case renamed) -[ -n "$all_modules" ] && echo \ -" +# Use cat with heredoc instead of echo for reliable newline handling and escape sequences +[ -n "$all_modules" ] && cat > docs.ipkg < docs.ipkg +sourcedir = "src" +EOF # Build the docs if [ -e docs.ipkg ]; then From 2b805690367b3240196c80c22b46f83e7663c0cf Mon Sep 17 00:00:00 2001 From: "Serge S. Gulin" Date: Fri, 24 Oct 2025 08:48:30 +0400 Subject: [PATCH 2/3] [ docs ] Add `Tutorials` with AI-generated content according to https://diataxis.fr/tutorials/ --- .editorconfig | 15 + .github/workflows/ci-super-linter.yml | 19 +- .linters/super-linter-fix.ipkg | 3 + .linters/super-linter-local.env | 2 + .linters/super-linter-run.ipkg | 3 + .linters/super-linter.env | 17 + .linters/super-linter.sh | 13 + docs/source/tutorials.rst | 14 +- docs/source/tutorials/derivation.md | 1 - docs/source/tutorials/generators.md | 1 - .../tutorials/t00-installation-and-setup.md | 186 ++++++++++ docs/source/tutorials/t01-generator-monad.md | 308 ++++++++++++++++ .../tutorials/t02-handling-emptiness.md | 187 ++++++++++ .../tutorials/t03-measuring-test-coverage.md | 176 +++++++++ .../t04-automatic-generator-derivation.md | 275 ++++++++++++++ .../tutorials/t05-derivegen-signatures.md | 202 +++++++++++ .../t06-mixing-manual-and-automatic.md | 170 +++++++++ docs/source/tutorials/t07-beyond-fuel.md | 236 ++++++++++++ .../t08-generating-gadts-with-proofs.md | 240 ++++++++++++ docs/source/tutorials/t09-toy-example.md | 341 ++++++++++++++++++ .../source/tutorials/t10-derivation-tuning.md | 211 +++++++++++ docs/source/tutorials/test-function.md | 1 - pack.toml | 17 +- tests/docs/typecheck/expected | 46 ++- 24 files changed, 2645 insertions(+), 39 deletions(-) create mode 100644 .linters/super-linter-fix.ipkg create mode 100644 .linters/super-linter-local.env create mode 100644 .linters/super-linter-run.ipkg create mode 100644 .linters/super-linter.env create mode 100755 .linters/super-linter.sh delete mode 100644 docs/source/tutorials/derivation.md delete mode 100644 docs/source/tutorials/generators.md create mode 100644 docs/source/tutorials/t00-installation-and-setup.md create mode 100644 docs/source/tutorials/t01-generator-monad.md create mode 100644 docs/source/tutorials/t02-handling-emptiness.md create mode 100644 docs/source/tutorials/t03-measuring-test-coverage.md create mode 100644 docs/source/tutorials/t04-automatic-generator-derivation.md create mode 100644 docs/source/tutorials/t05-derivegen-signatures.md create mode 100644 docs/source/tutorials/t06-mixing-manual-and-automatic.md create mode 100644 docs/source/tutorials/t07-beyond-fuel.md create mode 100644 docs/source/tutorials/t08-generating-gadts-with-proofs.md create mode 100644 docs/source/tutorials/t09-toy-example.md create mode 100644 docs/source/tutorials/t10-derivation-tuning.md delete mode 100644 docs/source/tutorials/test-function.md diff --git a/.editorconfig b/.editorconfig index 569258485..0f2df35fc 100644 --- a/.editorconfig +++ b/.editorconfig @@ -48,3 +48,18 @@ max_line_length = off [*.py] indent_size = 4 + +# See: https://stackoverflow.com/a/40348831/2572373 +[**{.build,docs/build,linters/build}**] +charset = unset +end_of_line = unset +insert_final_newline = unset +trim_trailing_whitespace = unset +indent_style = unset +indent_size = unset +max_line_length = unset + +# Auto-generated file +[.idrisCommit] +insert_final_newline = unset + diff --git a/.github/workflows/ci-super-linter.yml b/.github/workflows/ci-super-linter.yml index 988b6d15e..070d6f9b5 100644 --- a/.github/workflows/ci-super-linter.yml +++ b/.github/workflows/ci-super-linter.yml @@ -42,20 +42,13 @@ jobs: fetch-depth: 0 persist-credentials: false # https://docs.zizmor.sh/audits/#artipacked + - name: Load super-linter configuration + # Use grep inverse matching to exclude eventual comments in the .env file + # because the GitHub Actions command to set environment variables doesn't + # support comments. + run: grep -v '^#' .github/linters/super-linter.env >> "$GITHUB_ENV" + - name: Lint Code Base uses: super-linter/super-linter/slim@v8 env: - DEFAULT_BRANCH: master GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} - IGNORE_GENERATED_FILES: true - SAVE_SUPER_LINTER_SUMMARY: true # Required for generating linting reports in PR - - VALIDATE_PYTHON_BLACK: false # Avoid conflict: Ruff is preferred - VALIDATE_GIT_COMMITLINT: false - - VALIDATE_MARKDOWN_PRETTIER: false # We use markdownlint - VALIDATE_YAML_PRETTIER: false # We use yamllint - - # Disable Biome - VALIDATE_BIOME_FORMAT: false - VALIDATE_BIOME_LINT: false diff --git a/.linters/super-linter-fix.ipkg b/.linters/super-linter-fix.ipkg new file mode 100644 index 000000000..c60283e3f --- /dev/null +++ b/.linters/super-linter-fix.ipkg @@ -0,0 +1,3 @@ +package super-linter-fix + +prebuild = "FIX_MARKDOWN=true FIX_NATURAL_LANGUAGE=true FIX_SPELL_CODESPELL=true ./super-linter.sh" diff --git a/.linters/super-linter-local.env b/.linters/super-linter-local.env new file mode 100644 index 000000000..b23a2a02a --- /dev/null +++ b/.linters/super-linter-local.env @@ -0,0 +1,2 @@ +# Disable stuff which may not work for local run +VALIDATE_CHECKOV=false diff --git a/.linters/super-linter-run.ipkg b/.linters/super-linter-run.ipkg new file mode 100644 index 000000000..10b181c4a --- /dev/null +++ b/.linters/super-linter-run.ipkg @@ -0,0 +1,3 @@ +package super-linter-run + +prebuild = "./super-linter.sh" diff --git a/.linters/super-linter.env b/.linters/super-linter.env new file mode 100644 index 000000000..ba32c1a01 --- /dev/null +++ b/.linters/super-linter.env @@ -0,0 +1,17 @@ +DEFAULT_BRANCH=master +IGNORE_GENERATED_FILES=true +# Required for generating linting reports in PR +SAVE_SUPER_LINTER_SUMMARY=true + +# Avoid conflict: Ruff is preferred +VALIDATE_GIT_COMMITLINT=false +VALIDATE_PYTHON_BLACK=false + +# We use markdownlint +VALIDATE_MARKDOWN_PRETTIER=false +# We use yamllint +VALIDATE_YAML_PRETTIER=false + +# Disable Biome +VALIDATE_BIOME_FORMAT=false +VALIDATE_BIOME_LINT=false diff --git a/.linters/super-linter.sh b/.linters/super-linter.sh new file mode 100755 index 000000000..6601cdbdb --- /dev/null +++ b/.linters/super-linter.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +# See: https://github.com/super-linter/super-linter/blob/dd82ec5c927bff0fecc98865b0be8aa6ef849001/docs/run-linter-locally.md +docker run --platform linux/amd64 \ + --env-file "$(pwd)/../.github/linters/super-linter.env" \ + --env-file "$(pwd)/../.github/linters/super-linter-local.env" \ + -e LOG_LEVEL=NOTICE \ + -e RUN_LOCAL=true \ + -e FIX_MARKDOWN="${FIX_MARKDOWN:-false}" \ + -e FIX_NATURAL_LANGUAGE="${FIX_NATURAL_LANGUAGE:-false}" \ + -e FIX_SPELL_CODESPELL="${FIX_SPELL_CODESPELL:-false}" \ + -v "$(pwd)/../":/tmp/lint \ + ghcr.io/super-linter/super-linter:latest diff --git a/docs/source/tutorials.rst b/docs/source/tutorials.rst index fc8be5383..d4855c012 100644 --- a/docs/source/tutorials.rst +++ b/docs/source/tutorials.rst @@ -14,6 +14,14 @@ You can read more in the `original framework `_ :maxdepth: 1 :caption: Choose what to learn - tutorials/test-function - tutorials/generators - tutorials/derivation + tutorials/t00-installation-and-setup + tutorials/t01-generator-monad + tutorials/t02-handling-emptiness + tutorials/t03-measuring-test-coverage + tutorials/t04-automatic-generator-derivation + tutorials/t05-derivegen-signatures + tutorials/t06-mixing-manual-and-automatic + tutorials/t07-beyond-fuel + tutorials/t08-generating-gadts-with-proofs + tutorials/t09-toy-example + tutorials/t10-derivation-tuning diff --git a/docs/source/tutorials/derivation.md b/docs/source/tutorials/derivation.md deleted file mode 100644 index 14eaabc00..000000000 --- a/docs/source/tutorials/derivation.md +++ /dev/null @@ -1 +0,0 @@ -# Automatic derivation of generators diff --git a/docs/source/tutorials/generators.md b/docs/source/tutorials/generators.md deleted file mode 100644 index eb61ce7b6..000000000 --- a/docs/source/tutorials/generators.md +++ /dev/null @@ -1 +0,0 @@ -# Hand-written generators diff --git a/docs/source/tutorials/t00-installation-and-setup.md b/docs/source/tutorials/t00-installation-and-setup.md new file mode 100644 index 000000000..e30181872 --- /dev/null +++ b/docs/source/tutorials/t00-installation-and-setup.md @@ -0,0 +1,186 @@ +# Installation and First Steps + +Welcome to DepTyCheck! This tutorial will guide you through installing Idris 2 and DepTyCheck, creating your first project, and running a simple +generator. + +## Our Goal + +In this tutorial, you will: + +1. Install Idris 2 and the DepTyCheck library +2. Create a project configured with DepTyCheck +3. Write and run a generator that produces random `TrafficLight` values + +By the end, you will see output like: + +```text +Red : TrafficLight +``` + +--- + +## Step 1: Install Idris 2 + +First, you need to install Idris 2. We recommend using [`pack`](https://github.com/stefan-hoeck/idris2-pack/), which manages both the compiler +and library dependencies. + +Follow its [installation script](https://github.com/stefan-hoeck/idris2-pack/?tab=readme-ov-file#quick-installation). + +**Verify your installation:** + +```bash +idris2 --version +``` + +Sample output: + +```text +Idris 2, version 0.8.0-80fd5e4d7 +``` + +```{note} +You need Idris 2 version **0.8.0 or newer** for DepTyCheck to work. +``` + +--- + +## Step 2: Create Your First Project + +### Create a project directory + +```bash +mkdir deptycheck-tutorial +cd deptycheck-tutorial +``` + +### Create a project file named `tutorial.ipkg` + +```text +package tutorial + +version = 0.0.1 +langversion >= 0.8.0 + +sourcedir = "." +builddir = ".build" + +modules = Main +main = Main +executable = tutorial + +depends = deptycheck +``` + +```{note} +The `depends = deptycheck` line tells Idris to use the DepTyCheck library. +``` + +--- + +## Step 3: Write Your First Generator + +### Create a file `Main.idr` with the following code + +```idris +import Deriving.DepTyCheck.Gen +import System.Random.Pure.StdGen + +data TrafficLight = Red | Yellow | Green + +Show TrafficLight where + show Red = "Red" + show Yellow = "Yellow" + show Green = "Green" + +genTrafficLight : Fuel -> Gen MaybeEmpty TrafficLight +genTrafficLight = deriveGen + +main : IO () +main = do + Just light <- pick (genTrafficLight (limit 0)) + | Nothing => putStrLn "Generation failed" + printLn light +``` + +```{note} +- `%language ElabReflection` enables the metaprogramming features needed for `deriveGen` +- `deriveGen` automatically creates a generator for `TrafficLight` +- `pick` runs the generator and extracts one value +``` + +--- + +## Step 4: Build and Run + +### Build the project + +```bash +pack build +``` + +`pack` will download and build all dependencies automatically along with source code of the module. + +### Run the executable + +```bash +pack run tutorial.ipkg +``` + +Expected output (your result will vary): + +```text +Yellow +``` + +```{note} +Run the command multiple times to see different results (Yellow, Green, Red). +``` + +--- + +## Step 4: Try It in the REPL (Optional) + +You can also test your generator interactively. + +### Start the REPL + +Pass the Main module name to preload it: + +```bash +rlwrap pack repl ./Main.idr +``` + +```{note} +- `%language ElabReflection` enables the metaprogramming features needed for `deriveGen` +- `deriveGen` automatically creates a generator for `TrafficLight` +- `pick` runs the generator and extracts one value +``` + +### Run the generator + +```text +:exec printLn =<< pick (genTrafficLight (limit 0)) +``` + +Expected output: + +```text +Just Green +``` + +### Run it multiple times to see different colors + +### Exit the REPL + +```text +:quit +``` + +--- + +## Next Steps + +Now that you have a working setup, you are ready to learn the fundamentals of generator creation: + +- **Continue to Tutorial 1:** [The Generator Monad](t01-generator-monad.md) to learn how to create generators manually using `pure`, `elements`, + `choose`, and other combinators. diff --git a/docs/source/tutorials/t01-generator-monad.md b/docs/source/tutorials/t01-generator-monad.md new file mode 100644 index 000000000..4019aceb7 --- /dev/null +++ b/docs/source/tutorials/t01-generator-monad.md @@ -0,0 +1,308 @@ +# 1. The Generator Monad: Your First Generator + +Welcome to `DepTyCheck`! This tutorial is a hands-on guide that will help you learn the most important skill in property-based testing: generating +random test data. + +We will keep things practical and focus on what you need to get started. You'll write code, run it, and see the results immediately. + +## Our Goal + +In this tutorial, we will guide you step by step to create a generator for the following `UserProfile` data type: + +```text +data UserProfile = MkProfile String Nat +``` + +By the end, you will have a working program that produces random user profiles, like this: + +```text +MkProfile "Alice" 37 : UserProfile +``` + +## Prerequisites + +This tutorial assumes you have completed [Installation and First Steps](t00-installation-and-setup.md) and have a working Idris 2 installation with +DepTyCheck +configured for your `tutorial.ipkg`. + +--- + +## Step 1: Your First Generator + +Let's start by creating a generator that always produces the _same_ value. This will confirm our setup is working. + +### Create a new file named `Tutorial.idr` + +```idris +import Test.DepTyCheck.Gen +import Data.Vect + +%language ElabReflection +``` + +### Add the following code to it. We'll define our data type and import the necessary `DepTyCheck` modules + +```idris +data UserProfile = MkProfile String Nat + +Show UserProfile where + show (MkProfile s y) = "MkProfile " ++ show s ++ " " ++ show y + +-- A generator that always produces the same, constant user profile +genConstantUser : Gen1 UserProfile +genConstantUser = pure (MkProfile "Alice" 30) +``` + +```{note} +The `pure` function creates the simplest possible "recipe": one that always returns the exact value you give it. The type `Gen1` means this generator +is guaranteed to produce a value. +``` + +### Run your generator + +To test your first generator lets do the following: + +```bash +echo -e ':exec printLn =<< pick1 genConstantUser' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +Here we do: + +| | | +| --- | ---------- | +| `echo -e` and `\|` | We are going to run Idris2 in REPL mode, pass the input, wait for the output and close | +| `:exec` | It is actually the Idris2 REPL command to run something in `IO` monad. For `:exec ?wat` the `?wat` is `IO _`. | +| `printLn =<<` | Runs generator and prints output. `:exec` alone drops results; this shows them. | +| `pick1 genConstantUser` | _We are very close, that's what is needed._ | +| `rlwrap` | Not strictly needed for single runs, but reminds that Idris2 REPL lacks readline support | +| `pack` | DepTyCheck depends on a set of libraries, so, `pack` launches `idris2` with the full set of required things | +| `--extra-args="--no-banner"` | Reduces REPL output noise. Passes flag to hide Idris2 welcome banner | +| `repl` | It actually instructs `pack` to run `idris2` in REPL mode | + +You will see an output, similar to the following: + +```text +MkProfile "Alice" 30 +``` + +You've just created and run your first generator! Now, let's make it more interesting by adding some randomness. + +--- + +## Step 2: Adding Randomness + +Instead of a fixed age, let's generate a random one. We'll use the `choose` function for this. + +### Modify your file to create a new generator + +```idris +-- A generator for a user with a random age between 18 and 99 +genRandomAgeUser : Gen1 UserProfile +genRandomAgeUser = MkProfile "Alice" <$> choose (18, 99) +``` + +Here's what's new: + +- `choose (18, 99)` creates a recipe for picking a random number in that range. + +```{note} +The `choose` function randomly picks between two generators with equal probability (50/50). This gives you a simple way to add variation to your +generators. +``` + +- The `<$>` operator takes the result from the recipe on the right (our random number) and feeds it into the function on the left (`MkProfile "Alice"`). + +### Run it multiple times + +```bash +echo -e ':exec printLn =<< pick1 genRandomAgeUser' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +```bash +echo -e ':exec printLn =<< pick1 genRandomAgeUser' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +This time, you'll see a different result with each run: + +```text +MkProfile "Alice" 22 +MkProfile "Alice" 35 +``` + +Success! You've introduced randomness into your data. + +--- + +## Step 3: Combining Two Random Generators + +Now, let's make the name random too. We need to combine two different random recipes. + +### Add a new generator that combines a random name and a random age + +```idris +-- A generator for a user with a random name and a random age +genUserProfile : Gen1 UserProfile +genUserProfile = MkProfile <$> elements ["Alice", "Bob", "Charlie"] <*> choose (18, 99) +``` + +Here's the change: + +- `elements ["Alice", "Bob", "Charlie"]` creates a recipe for picking a random name from a list. +- The `<*>` operator is the key: it lets us combine two recipes. It runs the name recipe and the age recipe, then feeds _both_ results into `MkProfile`. + +### Run your new generator a few times + +```bash +echo -e ':exec printLn =<< pick1 genUserProfile' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +```bash +echo -e ':exec printLn =<< pick1 genUserProfile' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +You'll now see completely random user profiles! + +```text +MkProfile "Alice" 33 +MkProfile "Bob" 47 +``` + +--- + +## Step 4: Choosing Between Generators + +What if you want to generate more varied data? For example, maybe you want to generate a user who is either an "Admin" or a "Guest", with "Guest" being +more common. + +`DepTyCheck` provides `oneOf` for equal choices and `frequency` for weighted choices. + +### Add these new generators to your file + +```idris +-- A generator for a user role, with each role having an equal chance +genRole : Gen1 String +genRole = oneOf [pure "Admin", pure "User", pure "Guest"] + +-- A generator for a user type, where "Standard" is 4x more likely than "Premium" +genUserType : Gen1 String +genUserType = frequency [ (4, pure "Standard"), (1, pure "Premium") ] +``` + +- `oneOf` takes a list of generators and chooses one of them with equal probability. +- `frequency` takes a list of `(weight, generator)` pairs. The weights determine the probability. Here, there are 5 total "parts" (4+1), so "Standard" +has a 4/5 chance and "Premium" has a 1/5 chance. + +### Run them in the REPL + +```bash +echo -e ':exec printLn =<< pick1 genRole' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +```bash +echo -e ':exec printLn =<< pick1 genUserType' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +Sample output: + +```text +"Guest" +"Standard" +``` + +If you run `pick1 genUserType` many times, you will notice that `"Standard"` appears much more often than `"Premium"`. + +--- + +## Step 5: Dependent Generation + +So far, the random values we've generated (name, age) have been independent of each other. But what if the **type** of one value needs to depend on the +_value_ of another? + +This is the core challenge of generating dependent types. For example, let's generate a pair containing a random length `n` and a `Vect` that has +exactly `n` elements. The type `Vect n Bool` depends directly on the value `n`. + +This is called **dependent generation**. We must first generate `n`, and _then_ use that value to create a generator for a vector of that specific type. +We use `do` notation for this. + +### Add this generator to `Tutorial.idr`. It will create a dependent pair `(n ** Vect n Bool)` + +```idris +-- A generator for a dependent pair: a random length `n` and a vector of that length +genDependentVect : Gen1 (n ** Vect n Bool) +genDependentVect = do + n <- choose (1, 5) -- Step 1: Generate a random length `n` + vec <- vectOf {n} (elements [True, False]) -- Step 2: Generate a vector of that exact length + pure (n ** vec) -- Step 3: Package them into a dependent pair with (**) +``` + +This `do` block is a sequence of dependent instructions: + +1. `n <- choose (1, 5)`: A random `Nat` is generated. Let's say the result is `3`. +2. `vec <- vectOf {n} ...`: _Because_ `n` has the value `3`, this line creates and runs a generator for the type `Vect 3 Bool`. We have to pass it as a +named argument because it is used at the type definition of `vectOf`. +3. `pure (n ** vec)`: The value `3` and the generated vector (e.g., `[True, False, True]`) are bundled into a dependent pair using the `**` constructor. + +Run it in the REPL: + +```bash +echo -e ':exec printLn =<< pick1 genDependentVect' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +For multiple times the output might be: + +```text +(3 ** [False, False, False]) +(5 ** [True, True, True, True, True]) +(2 ** [True, False]) +``` + +Notice that the length of the vector in the output always matches the number next to it. This powerful technique is what allows `DepTyCheck` to generate +valid data for complex, dependent types. + +--- + +## Step 6: Generating a Collection + +Finally, let's generate a list of test users. You can use the `listOf` combinator to run your generator multiple times and collect the results. + +### Add one last generator to your `Tutorial.idr` file + +```idris +-- A generator that produces a list of 5 random user profiles +genFiveUsers : Gen1 (List UserProfile) +genFiveUsers = listOf {length=pure 5} genUserProfile +``` + +The `listOf` function takes a `length` generator (which we provide as a constant `5`), and creates a new recipe that runs the generator how a provided +`length` generator generated times. + +Run it in the REPL: + +```bash +echo -e ':exec printLn =<< pick1 genFiveUsers' | + rlwrap pack --extra-args="--no-banner" repl ./Tutorial.idr +``` + +The output will be a list of five unique, randomly-generated users: + +```text +[MkProfile "Alice" 84, MkProfile "Charlie" 30, MkProfile "Bob" 41, MkProfile "Bob" 59, MkProfile "Bob" 67] +``` + +--- + +## Next Steps + +You've mastered the basics. Where you go next depends on your needs: + +- **Want to handle types that might be empty?** Continue to [Handling Emptiness](t02-handling-emptiness.md) to learn about `Gen0`, `empty`, and `pick`. +- **Ready to have `DepTyCheck` do the work for you?** Continue to [Automatic Generator Derivation](t04-automatic-generator-derivation.md) to learn about +`deriveGen`. diff --git a/docs/source/tutorials/t02-handling-emptiness.md b/docs/source/tutorials/t02-handling-emptiness.md new file mode 100644 index 000000000..77fee1626 --- /dev/null +++ b/docs/source/tutorials/t02-handling-emptiness.md @@ -0,0 +1,187 @@ +# 2. Handling Emptiness: When a Type Has No Values + +In the [first tutorial](t01-generator-monad.md), we used `Gen1`, which is a guarantee—a promise—that a value can always be generated. This works +perfectly for types like `Nat` or `String` that always have inhabitants. + +But what happens when a type might be **uninhabited** (have no values at all) under certain conditions? + +This is a common scenario in dependently-typed programming. A perfect example is `Fin n`, the type of natural numbers from `0` up to `n-1`. + +- `Fin 3` has three inhabitants: `0`, `1`, and `2`. +- `Fin 1` has one inhabitant: `0`. +- But what about `Fin 0`? It asks for a number in the range `0` to `-1`. There are no such numbers. This type is **uninhabited**. + +It is impossible to write a generator that produces a value of type `Fin 0`, because none exist. Our testing library must be able to handle this +gracefully. In this tutorial, you will learn how to write safe generators for types that might be empty. You will build a correct generator for `Fin n` +and see how to handle its results safely. + +## Prerequisites + +This tutorial assumes you have completed [Installation and First Steps](t00-installation-and-setup.md) and the first tutorial, ["The Generator +Monad"](t01-generator-monad.md). + +--- + +## Step 1: Discovering the Problem + +Let's start by trying to write a generator for `Fin n` using only the tools we know from the first tutorial. + +### Create a new file named `EmptyTutorial.idr` + +### Add the following code to it. We need to import `Data.Fin` along with our usual testing modules + +```idris +import Test.DepTyCheck.Gen +import Data.Fin +import System.Random.Pure.StdGen +``` + +Now, **try to write a `Gen1` generator** for `Fin n`. We can handle the case where `n` is greater than zero, but the `Z` (zero) case presents a major +problem. + +```idris +-- This is an INTENTIONALLY INCORRECT generator to show the problem +genFinIncorrect : (n : Nat) -> Gen1 (Fin n) +genFinIncorrect (S k) = FS <$> genFinIncorrect k +genFinIncorrect Z = ?wat -- What could we possibly write here? +``` + +We have a problem. In the `(S k)` case, we can walk all possible values of `Fin (S k)` and convert them to `Fin` to create a generator. But in the `Z` +case, what can we do? + +The type is `Gen1 (Fin 0)`, but `Fin 0` has no values. We can't use `pure` because we don't have a value to give it. We're stuck. + +```{note} +The `Gen0` emptiness flag indicates this generator might fail to produce a value. Use it for types that may not have inhabitants (like `Fin 0`). +This is the problem `DepTyCheck` is designed to solve. We need a way to tell the system that a generator is _intentionally_ empty. +``` + +--- + +## Step 2: Introducing `Gen0` and `empty` + +`DepTyCheck` provides two new tools to solve this exact problem: + +- **`Gen0 a`**: A type for a generator that _might_ produce a value of type `a`. Think of it as a "possibly empty" recipe. +- **`empty`**: A specific generator of type `Gen0 a` that is _guaranteed_ to produce nothing. It's the recipe for an empty set. + +Let's use these to fix our incorrect generator. + +### Add the correct `genFin` generator to your `EmptyTutorial.idr` file + +```idris +-- A correct, safe generator for Fin n +genFin : (n : Nat) -> Gen0 (Fin n) +genFin Z = empty +genFin (S k) = FS <$> elements' (allFins k) +``` + +The changes are small but critical: + +- The return type is now `Gen0 (Fin n)`, which signals that the result may be empty. + +```{note} +The `empty` generator fails immediately. Combined with `pick`, it lets you express "try A, and if it fails, try B" logic without explicit branching. +``` + +- In the `Z` case, we can now simply return `empty`. This correctly tells `DepTyCheck` that the recipe for `Fin 0` produces nothing. + +--- + +## Step 3: Running a `Gen0` Generator + +Because a `Gen0` generator might not produce a value, we can't use `pick1` (which promises to return one value). Instead, we must use `pick`, which +safely handles the possibility of emptiness. + +- `pick1 gen` returns `a` +- `pick gen` returns `Maybe a` + +Let's see this in action. + +### Run `genFin` for both an inhabited case (`Fin 3`) and an empty case (`Fin 0`) + +```idris +run : IO () +run = do + printLn !(pick (genFin 3)) + printLn !(pick (genFin 0)) +``` + +Run it + +```bash +echo -e ':exec run' | rlwrap pack repl ./src/CustomGen.idr +``` + +You will see something like that: + +```text +Just 2 +Nothing +``` + +First result will be a `Fin 3` value wrapped in a `Just`, because a value could be generated. But for the second we used `empty` in our definition for +`genFin Z`, `DepTyCheck` knows this generator can't produce a value, and `pick` safely returns `Nothing` + +This is the core of safe, dependently-typed testing. The type system allows us to model that some generations are impossible, and the runner (`pick`) +allows us to handle those cases gracefully at runtime without any crashes. + +## Step 4: Filtering with `suchThat` + +A type can also be effectively "empty" if we filter its values so much that none remain. `DepTyCheck` provides `suchThat` for this. + +I.e. `g` suchThat `p` takes a generator `g` and a predicate (a function that returns a `Bool`) `p`. It runs the generator `g`, and if the value it +produces satisfies `p`, it returns it. If not, the generation fails for that attempt. + +Because the condition might never be met, `suchThat` always returns a `Gen0`. + +### Add these two generators to your `EmptyTutorial.idr` file + +```idris +isEven : Nat -> Bool +isEven n = n `mod` 2 == 0 + +-- A generator that tries to find an even number between 0 and 10. +-- This will sometimes succeed and sometimes fail (if `choose` picks an odd number). +genEven : Gen0 Nat +genEven = choose (0, 10) `suchThat` isEven + +-- A generator that tries to find a number greater than 10 in a range where none exist. +-- This recipe is impossible and will always be empty. +genImpossible : Gen0 Int +genImpossible = choose (1, 10) `suchThat` (> 10) +``` + +### Run them both + +```idris +runSuchThat : IO () +runSuchThat = do + printLn !(pick genEven) + printLn !(pick genImpossible) +``` + +Run it + +```bash +echo -e ':exec runSuchThat' | rlwrap pack repl ./src/CustomGen.idr +``` + +You will see something like that: + +```text +Just 2 +Nothing +``` + +This demonstrates another critical aspect of `Gen0`: it allows for speculative generation that might fail, giving you a powerful way to define complex +properties. + +--- + +## Next Steps + +Now that you've mastered manual generation for both simple and complex types, it's time to see how `DepTyCheck` can do this work for you automatically. + +- **Next Tutorial:** Continue to **[Measuring Your Test Coverage](t03-measuring-test-coverage.md)** to learn how to analyze the quality of your +generated data. diff --git a/docs/source/tutorials/t03-measuring-test-coverage.md b/docs/source/tutorials/t03-measuring-test-coverage.md new file mode 100644 index 000000000..cbb014b10 --- /dev/null +++ b/docs/source/tutorials/t03-measuring-test-coverage.md @@ -0,0 +1,176 @@ +# 3. Measuring Your Test Coverage + +In the last tutorials, we learned how to write generators for random data. But how do we know if our random data is _good_? Are we testing all the +important cases, or is our generator accidentally biased, leaving critical parts of our code untested? + +If a generator only ever produces one kind of value, our tests won't find bugs that only appear in other cases. We need a way to measure the quality of +our random data. + +## Our Goal + +In this tutorial, you will learn how to add **labels** to your generators to measure your test coverage. You will build a generator for a `TrafficLight` +data type, add labels to track each color, and run a test that produces a coverage report, like this: + +```text +TrafficLight covered fully (1000 times) + - Red: covered (332 times) + - Green: covered (334 times) + - Amber: covered (334 times) +``` + +## Prerequisites + +This tutorial assumes you have completed [Installation and First Steps](t00-installation-and-setup.md) and the first two tutorials on [basic +generation](t01-generator-monad.md) and [emptiness handling](t02-handling-emptiness.md). + +--- + +## Step 1: Creating a Generator to Test + +First, let's create a simple data type and a generator for it. This will be the subject of our coverage analysis. + +### Create a new file named `CoverageTutorial.idr` + +```idris +import Data.List +import Data.List.Lazy +import Test.DepTyCheck.Gen +import Test.DepTyCheck.Gen.Coverage +import System.Random.Pure.StdGen + +import Control.Monad.Maybe +import Control.Monad.Random +import Control.Monad.State +``` + +### Add the following code to it + +```idris +data TrafficLight = Red | Amber | Green + +Show TrafficLight where + show Red = "Red" + show Amber = "Amber" + show Green = "Green" + +-- A generator that produces a traffic light color +genTrafficLight : Gen1 TrafficLight +genTrafficLight = oneOf [pure Red, pure Amber, pure Green] +``` + +This generator works, but we have no way of knowing if it's distributing its results evenly. To see that, we need to add labels. + +--- + +## Step 2: Generating the Coverage Report + +To get a full, aggregated coverage report, we need to run the generator many times and combine the results. This is a three-step process: + +1. Initialize Report: Create an empty `CoverageGenInfo` report. This serves as a template that knows about all the types and constructors in our +generator. +2. Collect Data: Run the generator many times and collect the raw `ModelCoverage` (the label counts) from each individual run. +3. Analyze Results: Fold the collected raw data into the report template to produce the final, printable `CoverageGenInfo`. + +```{note} +Coverage measurement happens in three phases: + +1. Generate many samples with different random seeds +2. Track which constructors appear +3. Report how much every constructor had been called +``` + +Here is how to implement this in a `main` function. + +### Add a `main` function to your `CoverageTutorial.idr` file + +```idris +runReportWithCoverage : IO () +runReportWithCoverage = do + -- Step 1: Initialize the report template. + let reportTemplate = initCoverageInfo genTrafficLight + + -- Step 2: Run the generator 1000 times to collect raw coverage data. + -- `withCoverage` is needed here because our generator is written by hand. + let rawCoverageRuns = unGenTryND 1000 someStdGen (withCoverage genTrafficLight) + let allRawCoverage = concatMap fst rawCoverageRuns + + -- Step 3: Fold the raw data into the template to get the final report. + let finalReport = registerCoverage allRawCoverage reportTemplate + + -- 4. Print the final report. + putStrLn $ show finalReport +``` + +### Compile and run your file + +```bash +idris2 --build CoverageTutorial.idr +./build/exec/CoverageTutorial +``` + +### Check the output + +You will see the aggregated coverage report printed to your console. Because we used `oneOf`, the distribution should be very even: + +```text +TrafficLight covered fully (1000 times) + - Red: covered (332 times) + - Green: covered (334 times) + - Amber: covered (334 times) +``` + +This gives us high confidence that our generator is testing all three `TrafficLight` cases equally. + +--- + +## Step 3: Debugging with Labels + +Besides aggregated reports, labels are also an invaluable tool for debugging. You can instruct the generator runner to print every label as it's +activated. This allows you to trace the execution of a single, complex generation. + +`DepTyCheck` uses the `CanManageLabels` interface to handle this. By default, the `pick` function we've used before uses the `IgnoreLabels` +implementation. But we can provide a different one, `PrintAllLabels`, to change its behavior. + +### Add a new `runDebug` function to your file + +This new function will use `pick` and provide the `PrintAllLabels` implementation via the `@{}` syntax. + +```idris +runDebug : IO () +runDebug = do + Just v <- runMaybeT {m=IO} + $ evalRandomT someStdGen + $ evalStateT Z $ unGen {labels = PrintAllLabels} (withCoverage genTrafficLight) + | Nothing => putStrLn "couldn't produce a value" + putStrLn $ "Generated withCoverage: " ++ show v + + val <- pick genTrafficLight + putStrLn $ "Generated via pick: " ++ show val +``` + +### Compile and run the file again + +```bash + idris2 --build CoverageTutorial.idr + ./build/exec/CoverageTutorial +``` + +### Analyze the output. You will see a clear difference + +```text +Main.TrafficLight[?] +Main.Amber (user-defined) +Generated withCoverage: Amber +Generated via pick: Just Green +``` + +In the first run, the label was printed to the console the moment the corresponding generator was executed. In second run, no label were printed. For a +deeply nested generator, this trace allows you to understand exactly which path was taken to produce a specific problematic value. + +--- + +## Next Steps + +Now that you can write, run, and measure generators manually, it's time to learn how `DepTyCheck` can do all of this for you automatically. + +- **Next Tutorial:** Continue to **[Automatic Generator Derivation](t04-automatic-generator-derivation.md)** to learn how to use `deriveGen`. diff --git a/docs/source/tutorials/t04-automatic-generator-derivation.md b/docs/source/tutorials/t04-automatic-generator-derivation.md new file mode 100644 index 000000000..a207db40b --- /dev/null +++ b/docs/source/tutorials/t04-automatic-generator-derivation.md @@ -0,0 +1,275 @@ +# 4. Automatic Generator Derivation + +In the previous tutorials, we showed how to write generators by hand. This is fine for simple types, but quickly becomes tedious and error-prone for +complex, recursive data structures. + +This is where `DepTyCheck` shines. It comes with a powerful macro, `deriveGen`, that inspects your data type at compile-time and automatically writes a +high-quality generator for it, handling recursion and constraints for you. + +## Our Goal + +In this tutorial, we will use a single, running example—a file system `Entry`—to demonstrate the power of `deriveGen`. We will: + +1. Show how complex a manual generator for `Entry` would be. +2. Replace it with a single `deriveGen` call. +3. Learn how to provide an **external generator** to produce meaningful filenames. +4. Learn how to **pass arguments** to the generator to make it context-aware. + +## Prerequisites + +- Completion of [Installation and First Steps](t00-installation-and-setup.md) and the tutorials on [manual generation](t01-generator-monad.md), +[emptiness](t02-handling-emptiness.md), and [coverage analysis](t03-measuring-test-coverage.md). + +### Create a new file named `DeriveTutorial.idr` + +```idris +import Deriving.DepTyCheck.Gen -- For the deriveGen macro +import Data.Fuel + +import Test.DepTyCheck.Gen +import System.Random.Pure.StdGen +``` + +We need the `%language ElabReflection` pragma to enable compile-time elaboration which will automatically write code for defined generators by their +types. + +```idris +%language ElabReflection +``` + +--- + +## Step 1: The Burden of Manual Derivation + +Let's start with a recursive data type for a file system entry. + +```idris +data EntryManual = FileManual String | DirectoryManual (List EntryManual) + +Show EntryManual where + show (FileManual s) = "FileManual " ++ show s + show (DirectoryManual l) = "DirectoryManual " ++ (assert_total $ show l) +``` + +How would we write a generator for this by hand? It would be complex: + +- We would need to accept a `Fuel` parameter to stop recursion. +- In the `DirectoryManual` case, we'd need to call ourself with less fuel. +- We'd have to balance the choice between `FileManual` and `DirectoryManual` to get a good distribution. +- We would need a separate generator for the `String` in `FileManual`. + +A sketch might look like this: + +```idris +-- A complex, manual generator (conceptual) +genEntryManual : Fuel -> Gen MaybeEmpty EntryManual +genEntryManual Dry = pure (FileManual "default.txt") -- Base case when out of fuel +genEntryManual (More recFuel) = + frequency + [ (1, FileManual <$> elements ["file1", "file2"]) -- some string generator + , (1, DirectoryManual <$> (listOf (genEntryManual recFuel)) ) -- recursive call + ] + where +``` + +Prepare a test for it: + +```idris +runEntryManual : IO () +runEntryManual = do + printLn "limit = 1" + for_ (the (List Int) [1..5]) $ \_ => do + Just e <- pick (genEntryManual (limit 1)) + | Nothing => printLn "Generation failed" + printLn e + + printLn "limit = 2" + for_ (the (List Int) [1..5]) $ \_ => do + Just e <- pick (genEntryManual (limit 2)) + | Nothing => printLn "Generation failed" + printLn e + + printLn "limit = 3" + for_ (the (List Int) [1..5]) $ \_ => do + Just e <- pick (genEntryManual (limit 3)) + | Nothing => printLn "Generation failed" + printLn e +``` + +This is a lot of work to get right. Now, let's do it the easy way. + +--- + +## Step 2: Automatic Derivation with `deriveGen` + +We can replace the manual logic with a single line. But it has some limitations. To make the automagic generation works we need to drop off polymorphic +parameters: + +```idris +mutual + data EntryList : Type where + Nil : EntryList + (::) : Entry -> EntryList -> EntryList + + data Entry = File String | Directory EntryList + +mutual + Show Entry where + show (File s) = "File " ++ show s + show (Directory l) = "Directory " ++ (assert_total $ show l) + + Show EntryList where + show xs = "[" ++ show' xs ++ "]" where + show' : EntryList -> String + show' Nil = "" + show' (x :: Nil) = show x + show' (x :: xs) = show x ++ ", " ++ show' xs +``` + +```{note} +The latest version of DepTyCheck supports polymorphic specialization for automatically derived generators, but its support is still experimental. Also +automagic generator deriving supports only `Gen MaybeEmpty` for now. If you need stricter `Gen NonEmpty`, you still need to do it by your hands. +``` + +### Define the generator + +Our first naive attempt to use `deriveGen` might be the following: + +```idris +failing "No constructors found for the type `^prim^.String`" + genEntry : Fuel -> Gen MaybeEmpty Entry + genEntry = deriveGen +``` + +But honestly DepTyCheck is would decline our example because we need also to pass a generator for strings. It does not present out of the box, so, we +need some to add some special stuff around which will be uncovered by further tutorials. + +```idris +%hint +genStr : Gen MaybeEmpty String +genStr = elements ["a", "b", "c", "d", "f", "g", "h"] + +genEntry : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty Entry +genEntry = deriveGen +``` + +That's it. The `deriveGen` macro will now inspect the `Entry` type and write a generator that handles recursion, fuel, choices, and even attaches a +generator for `String` from the context. It might also automatically add the coverage labels we learned about in further tutorials! + +You can immediately generate a random file system structure. + +Prepare a test for it: + +```idris +runEntryDefault : IO () +runEntryDefault = do + Just e <- pick (genEntry (limit 10)) + | Nothing => printLn "Generation failed" + printLn e +``` + +Running this might produce output like: `Directory [File "a", Directory [File "b"]]`. + +--- + +## Step 3: Providing an External Generator + +The default generator is powerful, but the `String`s it produces are random nonsense. To generate meaningful data, we can provide `deriveGen` with a +"hint" in the form of an external generator. + +### Write a custom `String` generator + +This generator will produce realistic filenames. + +```idris +genFilename : Fuel -> Gen MaybeEmpty String +genFilename _ = elements ["config.yml", "main.idr", "README.md"] +``` + +### Call the new generator + +When we call `genEntry`, we can use the `@{...}` syntax to pass our `genFilename` function to satisfy the constraint. + +```idris +runEntryWithHint : IO () +runEntryWithHint = do + putStrLn "--- Generating Entries with a custom String generator ---" + for_ (the (List Int) [1..5]) $ \_ => do + Just e <- pick (genEntry @{genFilename} (limit 5)) + | Nothing => printLn "Generation failed" + printLn e +``` + +You will see that `deriveGen` still handles the `Directory` and `List` logic automatically, but every `File` now contains one of your hand-picked +filenames. + +```text +--- Generating Entries with a custom String generator --- +Directory [File "main.idr"] +File "config.yml" +Directory [] +File "README.md" +Directory [Directory [File "config.yml"]] +``` + +--- + +## Step 4: Passing Runtime Arguments + +Sometimes, a generator needs more context than `Fuel`. For example, what if we want to generate files with names that are context-dependent, based on +their parent directory? + +Any arguments that appear in the signature _before_ the `Fuel` parameter are treated as regular inputs. `deriveGen` is smart enough to thread these +arguments through its recursive calls. + +### Write a context-aware `String` generator + +This generator takes a `path` prefix as an argument and changes its output accordingly. + +```idris +genContextAwareFilename : String -> Fuel -> Gen MaybeEmpty String +genContextAwareFilename path _ = + if path == "src" + then elements ["main.idr", "lib.idr"] + else if path == "doc" + then elements ["tutorial.md", "README.md"] + else elements ["file.txt"] +``` + +To call `genCtxEntry`, we provide the initial path, and our context-aware generator. The `deriveGen` engine will handle passing the `path` argument down +to `genContextAwareFilename` during any recursive calls. + +Prepare a test for it: + +```idris +runCtxEntry : IO () +runCtxEntry = do + putStrLn "--- Generating files in `src` directory ---" + -- We pass the initial path "src" and the context-aware generator + Just e <- pick (genEntry @{genContextAwareFilename "src"} (limit 5)) + | Nothing => printLn "Generation Failed" + printLn e +``` + +You will see that files generated have names appropriate for the `src` directory, because our custom generator was called with `path = "src"`. + +```text +--- Generating files in `src` directory --- +Directory [Directory [], Directory [], File "main.idr", File "lib.idr"] +``` + +This powerful pattern allows you to create highly flexible generators that adapt their behavior based on runtime context. + +--- + +## Next Steps + +Now that you know how to automatically generate data and provide hints, you are ready for more advanced topics: + +- **Want to learn how to control what gets generated?** Continue to **[DeriveGen Signatures](t05-derivegen-signatures.md)** to learn how to use given vs +generated parameters and dependent pairs in signatures. +- **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel](t07-beyond-fuel.md)** to learn about `SpendingFuel` vs +`StructurallyDecreasing` recursion. +- **How do I fix a biased generator or control generation order?** The default derivation strategy is smart, but sometimes needs more specific guidance. +Continue to **[Derivation Tuning](t10-derivation-tuning.md)** to learn how to use `instance` declarations to control constructor probabilities and +argument generation order. diff --git a/docs/source/tutorials/t05-derivegen-signatures.md b/docs/source/tutorials/t05-derivegen-signatures.md new file mode 100644 index 000000000..b9499e04a --- /dev/null +++ b/docs/source/tutorials/t05-derivegen-signatures.md @@ -0,0 +1,202 @@ +# 5. DeriveGen Signatures: Controlling What Gets Generated + +In the previous tutorial, we saw how `deriveGen` can automatically create generators. But how do we tell it _what kind_ of data we want? For example, +should the length of a `Vect` be given as an argument, or should it be randomly generated? + +The answer is the function signature. The signature is not just a type; it is a blueprint of your intent that tells `deriveGen` exactly what to do. + +## Our Goal + +In this tutorial, we will learn to command `deriveGen` by writing three different function signatures for the `Vect` type. By the end of this tutorial, +you will have built: + +1. A generator for a `Vect` of a **specific, given** length. +2. A generator that produces a `Vect` of a **random, generated** length. +3. A flexible generator that takes both a **given** length and an **external generator** for its elements. + +This will give you a deep understanding of how to use signatures to control `deriveGen`. + +## Prerequisites + +- All previous tutorials, especially [Measuring Your Test Coverage](t03-measuring-test-coverage.md). + +--- + +## Step 1: The Setup + +First, let's create our file and add the necessary imports. We will be using `Vect` throughout this tutorial. + +### Create a new file named `DeriveTutorial.idr` + +### Add the following boilerplate + +This includes the `ElabReflection` pragma and all the modules we will need. + +```idris +import Deriving.DepTyCheck.Gen +import Data.Vect +import Data.Fuel + +import Test.DepTyCheck.Gen +import System.Random.Pure.StdGen + +%language ElabReflection + +%hint +genStr : Fuel -> Gen MaybeEmpty String +genStr _ = elements ["a", "b", "c", "d", "f", "g", "h"] + +public export +data VectString : (len : Nat) -> Type where + Nil : VectString Z + (::) : (x : String) -> (xs : VectString len) -> VectString (S len) + +Show (VectString n) where + show xs = "[" ++ show' xs ++ "]" where + show' : forall n . VectString n -> String + show' Nil = "" + show' (x :: Nil) = show x + show' (x :: xs) = show x ++ ", " ++ show' xs +``` + +--- + +_Note: For the following steps, you can put all the code in the same `DeriveTutorial.idr` file and temporarily rename the `main` function you want to +run as `main` before compiling._ + +## Step 2: Scenario A - Generating a `Vect` of a Given Length + +Our first goal is to create a generator that produces a `Vect` of a specific length that we provide as an argument. To do this, we simply place the +argument _before_ the `Fuel` parameter in the signature. + +The signature `(n : Nat) -> Fuel -> Gen MaybeEmpty (Vect n String)` tells `deriveGen`: "You will be _given_ a `Nat` named `n`. Your job is to produce a +`Vect` of that exact length." + +Define the generator: + +```idris +genVectOfLen : Fuel -> (n : Nat) -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (VectString n) +genVectOfLen = deriveGen +``` + +Let's write a `main` function to call our generator, providing `5` as the length. + +```idris +runVect : IO () +runVect = do + putStrLn "--- Generating a Vect of a given length (5) ---" + Just v <- pick (genVectOfLen (limit 10) 5) + | Nothing => printLn "Generation failed" + printLn v +``` + +The output will show a `Vect` that always has exactly 5 elements, filled with random strings from the default `String` generator. + +Compile and run: + +```text +--- Generating a Vect of a given length (5) --- +["a", "b", "c", "d", "e"] +The length is: 5 +``` + +By placing `n` before `Fuel`, you have successfully commanded `deriveGen` to use it as a fixed input. + +--- + +## Step 3: Scenario B - Generating a `Vect` of a Random Length + +What if we don't want to provide a specific length? What if we want the generator itself to invent a random length? To do this, we use a **dependent +pair** in the return type. + +The signature `Fuel -> Gen MaybeEmpty (n ** Vect n String)` tells `deriveGen`: "Your job is to first generate a random `Nat` (which you will call `n`), +and then generate a `Vect` of that length. When you are done, give me back both `n` and the `Vect`." + +Define the generator: + +```idris +genRandomVect : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (n ** VectString n) +genRandomVect = deriveGen +``` + +This time, when we call the generator, we don't provide a length. The generator will produce a pair containing the length it chose and the vector it +created. + +Prepare a test for it: + +```idris +runRandomVect : IO () +runRandomVect = do + putStrLn "--- Generating a Vect of a random length ---" + for_ (the (List Int) [1..3]) $ \_ => do + Just (n ** v) <- pick (genRandomVect (limit 10)) + | Nothing => printLn "Generation failed" + printLn n + printLn v +``` + +You will see vectors of different, random lengths each time you run it. + +Compile and run: + +```text +--- Generating a Vect of a random length --- +3 +["a", "b", "c"] +0 +[] +5 +["d", "e", "f", "g", "h"] +``` + +By moving the parameter `n` from an input to a **generated** part of the output using the `**` syntax, you have completely changed `deriveGen`'s +behavior. + +--- + +## Step 4: The Flexible Generator - Combining Patterns + +Let's combine the patterns we've learned. Our first generator is flexible enough: it is taking a `Nat` as a _given_ input, but it is also taking an +_external generator_ hint for the element type using the `=>` syntax which will be overridden by the following exapmple. + +To call this generator, we must provide both the length `n` and an element generator via the `@` syntax. + +Prepare a test for it: + +```idris +runFlexi : IO () +runFlexi = do + putStrLn "--- Generating a Vect of length 7 with overridden Str generator ---" + let myStrGen = \fuel => elements ["A", "B", "C"] -- Our custom generator for the elements + -- It is created manually, so no need to use `fuel`. + + Just v <- pick (genVectOfLen (limit 10) 7 @{myStrGen}) + | Nothing => printLn "Generation failed" + printLn v + + Just v' <- pick (genVectOfLen (limit 10) 7 @{genStr}) + | Nothing => printLn "Generation failed" + printLn v' +``` + +### Compile, run, and observe + +You will see a `Vect` of length 7, filled with numbers between 100 and 200, proving that `deriveGen` correctly used both your given length and your +external generator. + +```text +--- Generating a Vect of length 7 with overridden Str generator --- +["A", "C", "B", "A", "A", "A", "C"] +["b", "c", "f", "a", "b", "b", "h"] +``` + +--- + +## Next Steps + +Now that you know how to control `deriveGen` through signatures, you are ready for more advanced topics: + +- **Want to understand how recursion affects generation?** Continue to **[Beyond Fuel: Structural Recursion](t07-beyond-fuel.md)** to learn about +`SpendingFuel` vs `StructurallyDecreasing` recursion. +- **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md)** to see how +`deriveGen` handles types like `SortedList`. diff --git a/docs/source/tutorials/t06-mixing-manual-and-automatic.md b/docs/source/tutorials/t06-mixing-manual-and-automatic.md new file mode 100644 index 000000000..f41685f4a --- /dev/null +++ b/docs/source/tutorials/t06-mixing-manual-and-automatic.md @@ -0,0 +1,170 @@ +# 6. Mixing Manual and Automatic Generation + +In the [previous tutorial](t05-derivegen-signatures.md), we saw how to control what `deriveGen` generates by crafting function signatures. We also saw +how to give it "hints" for primitive types like `String` using the `=>` syntax. + +But what if you have a custom data type that needs a special, handwritten generator? `DepTyCheck` provides a powerful, "magic" feature: if you define a +generator for a type, `deriveGen` will automatically find it and use it. + +## Our Goal + +In this tutorial, you will: + +1. Define a custom type with a handwritten generator +2. Mark that generator with `%hint` for automatic discovery +3. See `deriveGen` automatically find and use your generator without explicit passing +4. Compare implicit (`%hint`) vs explicit (`@{...}`) generator passing + +You will see output like: + +```text +--- Testing mixed generation --- +MkUser (MkSpecialString "root") 5 +``` + +--- + +## Prerequisites + +- Completion of [Tutorial 5: DeriveGen Signatures](t05-derivegen-signatures.md) +- Understanding of the `=>` syntax for explicit generator constraints +- Idris2 source file `./src/Mixed.idr` with the header: + +```idris +import Test.DepTyCheck.Gen +import Data.Fuel +import Deriving.DepTyCheck.Gen +import System.Random.Pure.StdGen + +%language ElabReflection +``` + +--- + +## Step 1: Define Types and a Handwritten Generator + +Imagine we have a `SpecialString` type that should only ever contain specific, predefined values (e.g., usernames with special privileges). A fully +random `String` generator is not appropriate here. + +### Create a new file named `Mixed.idr` + +### Define the `SpecialString` type with a `%hint` generator + +```idris +-- A type that needs special generation +data SpecialString = MkSpecialString String + +Show SpecialString where + show (MkSpecialString s) = "MkSpecialString " ++ show s + +-- A handwritten generator for SpecialString +%hint +genSpecialString : Gen MaybeEmpty SpecialString +genSpecialString = map MkSpecialString (elements ["admin", "root", "system"]) +``` + +### Define the `User` type that contains `SpecialString` + +```idris +-- Standard domain types +data User = MkUser SpecialString Nat + +Show User where + show (MkUser s i) = "MkUser (" ++ show s ++ ") " ++ show i +``` + +- Signature `Gen MaybeEmpty SpecialString` (no `Fuel ->`) is used for manually defined generators +- The `%hint` pragma marks `genSpecialString` for **auto-implicit search** in Idris 2. It makes this function a candidate for automatic insertion - no +explicit `@{genSpecialString}` required! + +```{note} +From Idris 2 docs: `%hint` marks functions for auto search, similar to unnamed type class instances. The compiler prioritizes these hints during +unification when explicit arguments are absent. +``` + +--- + +## Step 2: Create the Derived Generator + +Now, let's define a generator for `User` using `deriveGen`. A `User` contains a `SpecialString` and a `Nat`. `deriveGen` knows how to generate a `Nat` +by default. What will it do for `SpecialString`? + +### Add the derived generator to `Mixed.idr` + +```idris +-- Add deriveGen for the User +genUser : Fuel -> (Fuel -> Gen MaybeEmpty SpecialString) => Gen MaybeEmpty User +genUser = deriveGen +``` + +- Automatic derivation by `deriveGen` requires `Fuel ->` +- The constraint `(Fuel -> Gen MaybeEmpty SpecialString) =>` tells `deriveGen` it needs a generator for `SpecialString` + +```{note} +Normally, you'd pass it explicitly: `genUser @{genSpecialString} fuel`. But `%hint` enables automatic resolution - Idris finds and inserts +`genSpecialString` automatically! +``` + +--- + +## Step 3: Test the Generator + +Let's create a main function to see our automatic discovery in action. + +### Add a test function to `Mixed.idr` + +```idris +main : IO () +main = do + putStrLn "--- Testing mixed generation ---" + Just u <- pick (genUser (limit 10)) + | Nothing => putStrLn "Generation failed" + printLn u +``` + +### Compile and run + +```bash +pack build Mixed && pack exec Mixed +``` + +Expected output (will vary): + +```text +--- Testing mixed generation --- +MkUser (MkSpecialString "root") 5 +``` + +--- + +## When to Use %hint? + +`Constraint + %hint` approach is recommended for custom types. + +**Pattern:** Mark your generator with `%hint`, add constraint to derived generator: + + ```idris + %hint + genMyType : Gen MaybeEmpty MyType + genMyType = map MkMyType (elements ["a", "b"]) + + genContainer : Fuel -> (Gen MaybeEmpty MyType) => Gen MaybeEmpty Container + genContainer = deriveGen + ``` + +**Call site:** + + ```idris + pick (genContainer fuel) -- No @{...} needed! + ``` + +**Best for:** Custom types where you want automatic discovery with explicit dependencies in the signature. + +--- + +## Next Steps + +- **Continue to the next tutorial:** [Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md) to see how these techniques apply to even more +advanced types with proof constraints. +- **Experiment:** Try creating your own custom type with a `%hint` generator and see if `deriveGen` finds it automatically. +- **Read more:** Check out the Idris 2 documentation on `%hint` for advanced auto-implicit search patterns. diff --git a/docs/source/tutorials/t07-beyond-fuel.md b/docs/source/tutorials/t07-beyond-fuel.md new file mode 100644 index 000000000..0faff4116 --- /dev/null +++ b/docs/source/tutorials/t07-beyond-fuel.md @@ -0,0 +1,236 @@ +# 7. Beyond Fuel: A Tutorial on Structural Recursion + +In our previous tutorials, we learned that `Fuel` is a crucial safety mechanism. It provides a "generation budget" that prevents `deriveGen` from +getting stuck in an infinite loop when generating recursive data. + +For a simple type like `List`, the rule is easy to understand: every `Cons` call is a recursive step, so it must spend one unit of fuel. But is this +always the case? Is every recursive call equally "expensive"? + +## Our Goal + +In this tutorial, you will discover that `deriveGen` is smart enough to identify two different kinds of recursion, with very different performance +characteristics. You will write two generators: + +1. A generator for a Peano `Nat` type that strictly obeys the fuel budget. +2. A generator for the indexed `Fin` type that appears to get "free" recursion, defying the budget. + +You will learn why this happens, how to recognize the difference between **`SpendingFuel`** and **`StructurallyDecreasing`** recursion, and how you can +design your own types to take advantage of this powerful optimization. + +## Prerequisites + +- All previous tutorials, especially [Automatic Generator Derivation](t04-automatic-generator-derivation.md). + +--- + +## Step 1: The Standard Case - `SpendingFuel` Recursion + +Let's start by examining the type of recursion we are already familiar with. We will create a simple Peano number type, where `deriveGen` must spend +fuel on every recursive call to guarantee termination. + +### Create a new file named `RecursionTutorial.idr` + +```idris +import Deriving.DepTyCheck.Gen +import Data.Fuel +import Data.Fin + +import Test.DepTyCheck.Gen +import System.Random.Pure.StdGen + +%language ElabReflection +``` + +### Add the following code + +This defines our `PNat` (Peano Natural) type and a standard derived generator for it. + +```idris +data PNat = PZ | PS PNat + +Show PNat where + show n = show (the Integer (pnatToInteger n)) + where + pnatToInteger : PNat -> Integer + pnatToInteger PZ = 0 + pnatToInteger (PS k) = 1 + pnatToInteger k + +genPNat : Fuel -> Gen MaybeEmpty PNat +genPNat = deriveGen +``` + +### The Experiment + +Now, let's write a `main` function to call this generator twice: once with a generous fuel budget (`limit 10`) and once with a very small one (`limit +3`). + +```idris +runPeano : IO () +runPeano = do + putStrLn "--- Generating with a large fuel budget (10) ---" + Just p_large <- pick (genPNat (limit 10)) + | Nothing => printLn "Generation failed" + printLn p_large + + putStrLn "--- Generating with a small fuel budget (3) ---" + Just p_small <- pick (genPNat (limit 3)) + | Nothing => printLn "Generation failed" + printLn p_small +``` + +### Compile, run, and observe + +```bash +idris2 --build RecursionTutorial.idr +./build/exec/RecursionTutorial +``` + +Your output will be random, but it will follow a strict pattern: + +```text +--- Generating with a large fuel budget (10) --- +PS (PS (PS (PS (PS PZ)))) +--- Generating with a small fuel budget (3) --- +PS (PS PZ) +``` + +Notice that the generator with more fuel produced a larger number. The number of `PS` constructors is strictly limited by the fuel you provide. This is +because `deriveGen` identifies the `PS` constructor as `SpendingFuel`. For each `PS` it generates, it must consume one unit of fuel from the budget. +This is the default, safe behavior for simple recursive types. + +--- + +## Step 2: StructurallyDecreasing Recursion + +Must `deriveGen` _always_ spend fuel on recursion? No. If it can prove that a recursive call is guaranteed to terminate by its structure alone, it can +perform a powerful optimization. + +A perfect example is `Fin n`, the type of numbers from `0` to `n-1`. + +### Add the `Fin` generator to your `RecursionTutorial.idr` file + +```idris +genFin : Fuel -> (n : Nat) -> Gen MaybeEmpty (Fin n) +genFin = deriveGen +``` + +### The Counter-Intuitive Experiment + +Now, let's try to generate a `Fin 100`. This would require 100 recursive calls to `FS`. According to our last experiment, this should require at least +`limit 100` fuel. But what happens if we only give it `limit 3`? + +```idris +runFin : IO () +runFin = do + putStrLn "--- Generating a large Fin with a tiny fuel budget (3) ---" + -- We ask for a Fin up to 100, but only provide fuel for 3 steps! + Just fin <- pick (genFin (limit 3) 100) + | Nothing => printLn "Generation failed" + printLn fin +``` + +### Run the experiment and observe the surprising result + +```text + --- Generating a large Fin with a tiny fuel budget (3) --- + 97 +``` + +It works! Even with a tiny fuel budget, it successfully generated a very large `Fin` value. It did not fail or run out of fuel. + +### The Explanation + +This is not magic. `deriveGen` is smart enough to analyze the `Fin` type and its `FS` constructor + +`FS : Fin k -> Fin (S k)` + +It sees that the input `Fin k` is for a type whose index `k` is provably, _structurally smaller_ than the output's index `S k`. Because the `Nat` index +itself guarantees that the recursion will eventually terminate when it hits `Fin 0`, `deriveGen` does not need to use the `Fuel` parameter as a safety +budget. It classifies this kind of recursion as `StructurallyDecreasing`. + +This optimization allows `deriveGen` to generate values for indexed, recursive data types like `Fin` and `Vect` much more efficiently than it can for +simple recursive types like `PNat` or `List`. + +--- + +## Under the Hood: How deriveGen Uses Fuel + +### The Mental Model + +`deriveGen` generates code that follows a simple pattern: a `case` split on the `Fuel` parameter. + +```text +genSomething : Fuel -> Gen MaybeEmpty Something +genSomething Dry = -- Base case: no fuel, choose non-recursive constructors +genSomething (More f) = -- Recursive case: spend fuel or use optimization +``` + +- When `Fuel` is `Dry`, the generator **must** choose non-recursive constructors (like `PZ`, `Leaf`, `Nil`) +- When `Fuel` is `More f`, the generator **can** choose recursive constructors (like `PS`, `Node`, `Cons`) +- Each recursive call consumes one unit of `Fuel` (calls with `f` instead of `More f`) +- This guarantees termination: eventually `Fuel` reaches `Dry` and recursion stops + +This is why higher `Fuel` values produce larger structures — more recursive steps are allowed before hitting the `Dry` base case. + +But the key insight is: **deriveGen doesn't always spend fuel on recursion**. It depends on the type of recursion. + +### SpendingFuel: Manual Implementation + +For a type like `PNat`, the generated code looks like this: + +```idris +genPNat' : Fuel -> Gen MaybeEmpty PNat +genPNat' Dry = pure PZ -- Must choose non-recursive constructor +genPNat' (More f) = frequency + [ (1, pure PZ) -- Non-recursive option + , (1, PS <$> genPNat' f) -- Recursive: spends fuel (calls with f, not More f) + ] +``` + +```{note} +When generating `PS`, we call `genPNat' f` — we pass the **smaller** fuel value. Each recursive step consumes one unit of fuel. +``` + +### StructurallyDecreasing: Manual Implementation + +For `Fin`, the generated code would be different: + +```idris +genFin' : (n : Nat) -> Fuel -> Gen MaybeEmpty (Fin n) +genFin' Z _ = empty -- No values for Fin 0 +genFin' (S k) fuel = frequency + [ (1, pure FZ) -- Base constructor + , (1, FS <$> genFin' k fuel) ] -- Recursive: SAME fuel! +``` + +```{note} +When generating `FS`, we call `genFin' k fuel` — with the **same** fuel value! +``` + +Why is this safe? Because the **type index** decreases (`S k` → `k`), guaranteeing termination even without +spending fuel. The index itself acts as the termination measure. + +### The Key Difference + +| Aspect | SpendingFuel | StructurallyDecreasing | +| -------- | -------------- | ------------------------ | +| **Fuel in recursive call** | `gen f` (less fuel) | `gen fuel` (same fuel) | +| **Termination proof** | Fuel budget decreases | Type index decreases | +| **Max generated size** | Limited by fuel | Limited by index | +| **Examples** | `PNat`, `List a`, `Tree` | `Fin n`, `Vect n a` | + +This is the core optimization: when the type system guarantees termination through decreasing indices, `deriveGen` doesn't need to spend fuel. This +makes generation of indexed types both faster and capable of producing larger values. + +--- + +## Next Steps + +Now that you understand how `deriveGen` handles recursion, you are ready for more advanced topics: + +- **Want to fix biased generators?** Continue to **[Derivation Tuning](t10-derivation-tuning.md)** to learn how to use `ProbabilityTuning` and +`GenOrderTuning` instances. +- **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t06-mixing-manual-and-automatic.md)** to see how +`deriveGen` discovers and uses your custom generators. +- **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md)** to see how +`deriveGen` handles auto-implicit proof arguments. diff --git a/docs/source/tutorials/t08-generating-gadts-with-proofs.md b/docs/source/tutorials/t08-generating-gadts-with-proofs.md new file mode 100644 index 000000000..ecf0accd0 --- /dev/null +++ b/docs/source/tutorials/t08-generating-gadts-with-proofs.md @@ -0,0 +1,240 @@ +# 8. Generating GADTs with Proof Constraints + +In previous tutorials, we used `deriveGen` for regular data types and indexed types like `Vect`. But what about types that carry **proofs** as +constructors arguments? Can `deriveGen` handle those? + +Yes! `deriveGen` is smart enough to automatically satisfy proof constraints during generation. + +## Our Goal + +In this tutorial, you will build a generator for a `SortedList` type that is **always sorted by construction**. The type itself carries a proof of +sortedness, and `deriveGen` will automatically find valid values that satisfy the proof constraints. + +By the end, you will: + +1. Define a GADT with a proof argument (`{auto prf : isSorted ...}`) +2. Derive a generator with a single `deriveGen` call +3. Run the generator and verify that all output is sorted + +## Prerequisites + +- Completion of [Tutorial 5: DeriveGen Signatures](t05-derivegen-signatures.md) +- Understanding of dependent pairs and indexed types +- Idris2 source file `./src/Playground.idr` with the header: + +```idris +import Deriving.DepTyCheck.Gen +import System.Random.Pure.StdGen +``` + +## Step 1: Define a SortedList Type + +First, let's define a list type that is guaranteed to be sorted. The key is that the `SCons` constructor requires a proof that adding a new element +maintains sortedness. + +```idris +isSorted : List Nat -> Bool +isSorted [] = True +isSorted [_] = True +isSorted (x :: y :: xs) = x <= y && isSorted (y :: xs) + +mutual + data SortedList : Type where + SNil : SortedList + SCons : (x : Nat) -> (xs : SortedList) -> {auto prf : So $ isSorted (x :: toList xs)} -> SortedList + + toList : SortedList -> List Nat + toList SNil = [] + toList (SCons x xs) = x :: toList xs +``` + +The `SCons` constructor has an **auto-implicit** argument `{auto prf : isSorted (x :: toList xs)}`. This means: + +- To construct an `SCons`, Idris must find a proof that the list is sorted. +- The `auto` keyword tells Idris to search for this proof automatically. + +```{note} +The `{auto prf : isSorted ...}` constraint ensures only sorted lists are generated. The `auto` keyword makes Idris search for proof automatically +during generation. +``` + +--- + +## Step 2: Derive the Generator + +Now comes the magic. We derive a generator for `SortedList` with a single line. + +### Add the derived generator + +```idris +genSortedList : Fuel -> Gen MaybeEmpty SortedList +genSortedList = deriveGen +``` + +That's it! No manual logic, no special handling for the proof argument. `deriveGen` will: + +1. Generate a candidate `x : Nat` +2. Recursively generate `xs : SortedList` +3. Check if `isSorted (x :: toList xs)` can be proven +4. If yes, construct the `SCons`; if no, try another `x` + +--- + +## Step 3: Run and Verify + +Let's test the generator and verify that all output is sorted. + +```idris +testList : HasIO io => io () +testList = do + putStrLn "--- Generating 5 sorted lists ---" + for_ (the (List Int) [1..5]) $ \_ => do + Just sl <- pick (genSortedList (limit 5)) + | Nothing => printLn "Generation failed" + let asList = toList sl + putStrLn $ "Generated: " ++ show asList + putStrLn $ "Is sorted: " ++ show (isSorted asList) +``` + +### Compile and run + +```bash +echo -e ':exec testList' | rlwrap pack repl ./src/Playground.idr +``` + +### Analyze the output + +```text +... +Main> --- Generating 5 sorted lists --- +Generated: [2, 3, 3, 4, 4] +Is sorted: True +Generated: [2, 2] +Is sorted: True +Generated: [3, 4] +Is sorted: True +Generated: [2] +Is sorted: True +Generated: [4] +Is sorted: True +``` + +Every generated list is sorted! `deriveGen` automatically found values of `x` that satisfy the `isSorted` constraint. + +--- + +## Step 4: Understanding How It Works + +How does `deriveGen` solve the proof constraint? The key is in the **search order** and **backtracking**. + +When `deriveGen` encounters `{auto prf : So $ isSorted (x :: toList xs)}`, it: + +1. **Generates candidates** for `x` from the default `Nat` generator +2. **Recursively generates** `xs : SortedList` (which is already sorted by construction) +3. **Checks the constraint**: Is `x <= head xs` (or `x` can be anything if `xs` is empty)? +4. **Backtracks if needed**: If the constraint fails, it tries another `x` + +```{note} +The proof argument guarantees sortedness by construction: + +- `SNil` is always sorted (base case) +- `SCons` requires proof that new element maintains order +- Invalid constructions are rejected at compile time +``` + +This is why the generator may be slower for complex constraints — it may need multiple attempts to find valid values. + +The `Fuel` parameter controls how deep the recursion can go, so, with more fuel, `deriveGen` can generate longer sorted lists: + +```idris +-- Add to main: +testFuel : IO () +testFuel = do + putStrLn "\n--- With small fuel (limit 3) ---" + Just sl1 <- pick (genSortedList (limit 3)) + | Nothing => printLn "Generation failed" + printLn $ toList sl1 + + putStrLn "\n--- With large fuel (limit 8) ---" + Just sl2 <- pick (genSortedList (limit 8)) + | Nothing => printLn "Generation failed" + printLn $ toList sl2 +``` + +Run it: + +```bash +echo -e ':exec testFuel' | rlwrap pack repl ./src/Playground.idr +... +Main> --- Generating 5 sorted lists --- +Generated: [2, 3, 3, 4, 4] +Is sorted: True +Generated: [2, 2] +Is sorted: True +Generated: [3, 4] +Is sorted: True +Generated: [2] +Is sorted: True +Generated: [4] +Is sorted: True +``` + +--- + +## Step 5: Another Example — Bounded Values + +Let's see another example of proof-carrying data. Consider a type that represents numbers bounded by a given limit: + +```idris +data BoundedNat : (limit' : Nat) -> Type where + MkBounded : (n : Nat) -> {auto prf : n `LT` limit'} -> BoundedNat limit' + +genBoundedNat : Fuel -> (limit' : Nat) -> Gen MaybeEmpty (BoundedNat limit') +genBoundedNat = deriveGen + +testBounded : IO () +testBounded = do + putStrLn "--- Generating BoundedNat with limit'=5 ---" + for_ (the (List Int) [1..5]) $ \_ => do + Just bn <- pick (genBoundedNat (limit 10) 5) + | Nothing => printLn "Failed" + case bn of + MkBounded n => putStrLn $ "Generated: " ++ show n ++ " (< 5)" +``` + +Run it: + +```bash +echo -e ':exec testBounded' | rlwrap pack repl ./src/Playground.idr +``` + +The output might be varied: + +```text +Main> --- Generating BoundedNat with limit'=5 --- +Generated: 4 (< 5) +Generated: 1 (< 5) +Generated: 1 (< 5) +Generated: 3 (< 5) +Generated: 4 (< 5) +``` + +The `{auto prf : LT n limit}` constraint ensures that only values less than the limit are generated. `deriveGen` will automatically search for valid `n` +values. + +--- + +## Next Steps + +Now that you can generate proof-carrying data, you are ready for more advanced topics: + +- **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t06-mixing-manual-and-automatic.md)** to see how +`deriveGen` automatically discovers and uses your custom generators. + + diff --git a/docs/source/tutorials/t09-toy-example.md b/docs/source/tutorials/t09-toy-example.md new file mode 100644 index 000000000..7dc1274b7 --- /dev/null +++ b/docs/source/tutorials/t09-toy-example.md @@ -0,0 +1,341 @@ +# 9. Toy Example: Generating ASTs for a DSL + +In previous tutorials, we learned how to create generators for simple data types and how to combine manual and automatic derivation. Now, let's apply +these skills to a real-world scenario: generating **Abstract Syntax Trees (ASTs)** for a simple imperative programming language. + +This tutorial is based on **PIL (Primitive Imperative Language)**, a real example from the DepTyCheck repository. + +## Our Goal + +In this tutorial, you will build a complete AST generator for a simple imperative language. By the end, you will have: + +1. Defined expression and statement types for the language +2. Created both automatic (`deriveGen`) and hand-written generators +3. Generated valid random programs with control flow structures + +You will see output like: + +```text +Seq (Assign "x" (Lit 5)) (If (Add (Var "x") (Lit 3)) (Assign "y" (Lit 10)) Skip) +``` + +**Expected time:** 30-40 minutes + +--- + +## Step 1: Define the Expression Language + +Let's start with the foundation: arithmetic and logical expressions. + +### Create a new file named `PILTutorial.idr` + +### Add the basic setup and expression type + +```idris +import Data.Fuel +import Data.List +import Deriving.DepTyCheck.Gen +import Test.DepTyCheck.Gen +import System.Random.Pure.StdGen + +-- Arithmetic and logical expressions +data Expr : Type where + Lit : Nat -> Expr + Var : String -> Expr + Add : Expr -> Expr -> Expr + Mul : Expr -> Expr -> Expr + And : Expr -> Expr -> Expr + Lt : Expr -> Expr -> Expr + +Show Expr where + show (Lit l) = "Lit " ++ show l + show (Var s) = "Var " ++ show s + show (Add e1 e2) = "Add (" ++ show e1 ++ ") (" ++ show e2 ++ ")" + show (Mul e1 e2) = "Mul (" ++ show e1 ++ ") (" ++ show e2 ++ ")" + show (And e1 e2) = "And (" ++ show e1 ++ ") (" ++ show e2 ++ ")" + show (Lt e1 e2) = "Lt (" ++ show e1 ++ ") (" ++ show e2 ++ ")" +``` + +### Create a simple derived generator with a generator-helper for strings + +```idris +genVarName : Fuel -> Gen MaybeEmpty String +genVarName _ = elements ["x", "y", "z", "temp", "result", "counter"] + +genExpr : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty Expr +genExpr = deriveGen +``` + +### Test it + +```idris +main : IO () +main = do + putStrLn "--- Generating random expressions ---" + for_ (the (List Int) [1..5]) $ \_ => do + Just e <- pick (genExpr @{genVarName} (limit 3)) + | Nothing => putStrLn "Generation failed" + printLn e +``` + +### Build and run + +```bash +echo -e ':exec main' | rlwrap pack repl ./PILTutorial.idr +``` + +Expected output (will vary): + +```text +--- Generating random expressions --- +Lt (Mul (Lt (Var "x") (Var "temp")) (Add (Lit 3) (Lit 1))) (Add (Var "temp") (Lt (Var "result") (Lit 0))) +Lt (And (Var "counter") (And (Lit 2) (Var "y"))) (And (Lit 1) (Add (Lit 0) (Var "counter"))) +And (Mul (And (Lit 0) (Lit 0)) (Lit 3)) (Lit 3) +Mul (Lit 2) (Var "z") +Add (Lit 0) (Add (And (Var "y") (Lit 2)) (And (Lit 2) (Var "counter"))) +``` + +```{note} +`deriveGen` automatically handles the recursive structure of expressions. The `limit 3` fuel controls the maximum depth of nested expressions. +``` + +--- + +## Step 2: Add Statements and Control Flow + +Now let's add statements that form complete programs. + +### Add the statement type to your file + +```idris +-- Statements with control flow +data Stmt : Type where + Skip : Stmt + Assign : String -> Expr -> Stmt + Seq : Stmt -> Stmt -> Stmt + If : Expr -> Stmt -> Stmt -> Stmt + While : Expr -> Stmt -> Stmt + +Show Stmt where + show Skip = "Skip" + show (Assign s e) = "Assign " ++ show s ++ " (" ++ show e ++ ")" + show (Seq s1 s2) = "Seq (" ++ show s1 ++ ") (" ++ show s2 ++ ")" + show (If e1 s1 s2) = "If (" ++ show e1 ++ ") (" ++ show s1 ++ ") (" ++ show s2 ++ ")" + show (While e1 s1) = "While (" ++ show e1 ++ ") (" ++ show s1 ++ ")" +``` + +### Create a hand-written generator with explicit fuel control + +```idris +genStmt : Fuel -> Gen MaybeEmpty Stmt +genStmt Dry = pure Skip -- Base case: only non-recursive constructors +genStmt (More f) = frequency + [ (1, pure Skip) + , (5, Assign <$> genVarName (More f) <*> genExpr @{genVarName} (More f)) + , (3, Seq <$> genStmt f <*> genStmt f) + , (2, If <$> genExpr @{genVarName} (More f) <*> genStmt f <*> genStmt f) + , (2, While <$> genExpr @{genVarName} (More f) <*> genStmt f) + ] +``` + +```{note} +- `genStmt Dry = pure Skip` ensures termination when fuel is exhausted +- `genStmt f` (less fuel) in recursive calls controls program size +- `frequency` weights make simple statements more common than complex ones +``` + +### Test the statement generator + +```idris +main_stmt : IO () +main_stmt = do + putStrLn "--- Generating random statements ---" + for_ (the (List Int) [1..5]) $ \_ => do + Just s <- pick (genStmt (limit 4)) + | Nothing => putStrLn "Generation failed" + printLn s +``` + +Try to run `main_stmt` + +```bash +echo -e ':exec main_stmt' | rlwrap pack repl ./PILTutorial.idr +``` + +Expected output: + +```text +--- Generating random statements --- +Assign "counter" (Lt (Lit 0) (Lit 4)) +Assign "x" (Lt (Mul (Lt (Var "temp") (Lit 1)) (Lit 2)) (Lt (Var "counter") (And (Add (Var "y") (Lit 2)) (And (Var "counter") (Lit 2))))) +Assign "y" (And (Add (Mul (Var "x") (Var "temp")) (Var "temp")) (And (Mul (Mul (Var "y") (Lit 3)) (Lt (Var "counter") (Lit 2))) (Var "result"))) +If (Lt (Mul (And (Lt (Lit 4) (Var "z")) (Add (Lit 1) (Var "x"))) + (Mul (Mul (Var "x") (Var "y")) (Add (Lit 0) (Lit 0)))) + (And (Lt (Add (Lit 3) (Lit 0)) (Mul (Lit 0) (Var "counter"))) + (Add (Var "z") (Var "temp"))) + (Assign "counter" (And (Mul (And (Var "z") (Lit 1)) (Var "result")) (Var "result"))) + (If (Lt (Mul (And (Var "z") (Var "counter")) (Lit 0)) + (Add (Lit 0) (Mul (Lit 3) (Lit 3)))) + (If (Mul (Mul (Lit 0) (Var "result")) (And (Lit 1) (Var "temp"))) + (While (Lt (Var "x") (Var "y")) (Skip)) + (While (Lt (Var "result") (Var "temp")) (Skip))) + (Assign "temp" (Lt (Mul (Lit 2) (Lit 1)) (Mul (Lit 0) (Var "counter"))))) +Seq (Assign "result" (Var "z")) + (While (Add (Add (Var "counter") (And (Lit 3) (Lit 2))) + (Lt (And (Var "temp") (Lit 1)) (Var "temp"))) + (Assign "y" (And (Lt (Var "counter") (Lit 1)) + (Lt (Var "counter") (Var "temp"))))) +``` + +--- + +## Step 3: Generate Complete Programs + +Now let's generate complete programs with multiple statements. + +### Define a Program type and generator + +```idris +-- A program is a list of statements +data Program = MkProgram (List Stmt) + +Show Program where + show (MkProgram lst) = "MkProgram " ++ show lst + +genProgram : (n : Nat) -> Fuel -> Gen MaybeEmpty Program +genProgram n fuel = MkProgram <$> listOf {length=pure n} (genStmt fuel) +``` + +### Test program generation + +```idris +main_program : IO () +main_program = do + putStrLn "--- Generating a random program (5 statements) ---" + Just prog <- pick (genProgram 5 (limit 3)) + | Nothing => putStrLn "Generation failed" + printLn prog +``` + +Try to run + +```bash +echo -e ':exec main_program' | rlwrap pack repl ./PILTutorial.idr +``` + +Expected output: + +```text +--- Generating a random program (5 statements) --- +MkProgram [Seq (While (Add (Lit 1) (And (Lit 1) (Var "x"))) (While (Var "x") (Skip))) + (Assign "temp" (And (And (Var "temp") (Var "y")) (Lit 1))), + If (And (Add (Add (Var "x") (Lit 0)) (Lit 1)) (Lit 2)) + (Assign "result" (Lt (Lt (Lit 2) (Var "temp")) (Mul (Var "y") (Var "y")))) + (While (Var "temp") (Seq (Skip) (Skip))), + While (Mul (Var "result") (Mul (Lit 1) (Add (Var "y") (Lit 1)))) + (Assign "counter" (Lt (And (Lit 1) (Var "result")) (Lit 0))), + Seq (If (And (And (Lit 1) (Var "result")) (Mul (Lit 0) (Lit 1))) + (If (Lit 1) (Skip) (Skip)) (While (Lit 0) (Skip))) + (If (Mul (Add (Var "x") (Lit 1)) (And (Lit 1) (Var "counter"))) + (While (Add (Lit 1) (Lit 1)) (Skip)) + (Assign "y" (Add (Lit 1) (Lit 0)))), + Assign "temp" (Add (Add (Lit 1) (And (Var "y") (Var "z"))) (And (Lit 1) (Lit 3)))] +``` + +```{note} +`listOf {length=pure n} gen` runs the generator `n` times and collects results into a list. +``` + +--- + +## Step 4: Test Properties of Generated Programs + +Let's verify that our generated programs have certain properties. + +### Add property checking functions + +```idris +-- Check if a statement contains an assignment +hasAssign : Stmt -> Bool +hasAssign Skip = False +hasAssign (Assign _ _) = True +hasAssign (Seq s1 s2) = hasAssign s1 || hasAssign s2 +hasAssign (If _ s1 s2) = hasAssign s1 || hasAssign s2 +hasAssign (While _ s) = hasAssign s + +-- Count statements in a program +stmtCount : Program -> Nat +stmtCount (MkProgram stmts) = length stmts + +-- Check if program has a loop +hasLoop : Stmt -> Bool +hasLoop Skip = False +hasLoop (Assign _ _) = False +hasLoop (Seq s1 s2) = hasLoop s1 || hasLoop s2 +hasLoop (If _ s1 s2) = hasLoop s1 || hasLoop s2 +hasLoop (While _ _) = True +``` + +### Test properties + +```idris +main_properties : IO () +main_properties = do + putStrLn "--- Checking properties of generated programs ---" + for_ (the (List Int) [1..10]) $ \_ => do + Just prog <- pick (genProgram 3 (limit 3)) + | Nothing => putStrLn "Generation failed" + + let hasAnyAssign = Prelude.any {t=List} hasAssign (case prog of MkProgram stmts => stmts) + let hasAnyLoop = Prelude.any {t=List} hasLoop (case prog of MkProgram stmts => stmts) + let count = stmtCount prog + + putStrLn $ "Program with " ++ show count ++ " statements" + putStrLn $ " Has assignment: " ++ show hasAnyAssign + putStrLn $ " Has loop: " ++ show hasAnyLoop + putStrLn "" +``` + +Try to run + +```bash +echo -e ':exec main_properties' | rlwrap pack repl ./PILTutorial.idr +``` + +A sample of the output: + +```text +--- Checking properties of generated programs --- +Program with 3 statements + Has assignment: True + Has loop: False + +Program with 3 statements + Has assignment: True + Has loop: True + +Program with 3 statements + Has assignment: True + Has loop: False +... +``` + +```{note} +You can use these property checks to ensure your generated programs meet certain criteria for testing compilers or interpreters. +``` + +--- + +## Next Steps + +Now that you can generate complex ASTs, you're ready for many other applications: + +- **Test an interpreter:** Use your generated PIL programs to test a language interpreter with property-based testing. +- **Add more language features:** Extend the language with functions, arrays, or I/O operations. +- **Integrate custom generators:** Continue to **[Mixing Manual and Automatic](t06-mixing-manual-and-automatic.md)** to see how `deriveGen` discovers +and uses your custom generators. +- **Control distribution:** Continue to **[Derivation Tuning](t10-derivation-tuning.md)** to learn how to fine-tune constructor probabilities for more +realistic program distributions. + +The complete `PILTutorial.idr` file is available for reference. You can find it in the DepTyCheck examples or build it step-by-step following this +tutorial. diff --git a/docs/source/tutorials/t10-derivation-tuning.md b/docs/source/tutorials/t10-derivation-tuning.md new file mode 100644 index 000000000..05612fd32 --- /dev/null +++ b/docs/source/tutorials/t10-derivation-tuning.md @@ -0,0 +1,211 @@ +# 10. Advanced Derivation Tuning + +In the last tutorial, we saw how to use `deriveGen` and provide it with custom generators for base types like `String`. However, `DepTyCheck` offers +even deeper, more powerful mechanisms for controlling the derivation process for situations where just providing a generator isn't enough. + +```{warning} +**This is an Advanced Tutorial.** The tuning mechanism uses some of Idris's more powerful features, specifically compile-time reflection +and type class instances. We will walk through it step-by-step, but a full explanation of these concepts is beyond the scope of this tutorial. If you +just want to use `deriveGen` with its default settings and provide external generators, you can safely skip this lesson. +``` + +## Our Goal + +We will tackle two common problems that cannot be solved with external generators alone: + +1. Fixing Bias: We will prove that a default generator is biased and then implement the `ProbabilityTuning` interface to change the frequency of a +specific constructor. +2. Fixing Inefficiency: We will show how a naive generator for a constrained type is inefficient and then implement the `GenOrderTuning` interface to +guide the derivation logic and make it robust. + +## Prerequisites + +- Completion of [Automatic Generator Derivation](t04-automatic-generator-derivation.md). +- A willingness to engage with some advanced Idris concepts! + +--- + +## Step 1: Discovering a Biased Generator + +Let's start by defining a simple, recursive data type where the default `deriveGen` strategy will produce a biased result. + +### Create a new file named `TuningTutorial.idr` + +```idris +import Deriving.DepTyCheck.Gen +import Deriving.DepTyCheck.Gen.Tuning -- For the tuning interfaces +import Data.Fuel +import Data.So + +-- From previous tutorials +import Test.DepTyCheck.Gen +import Test.DepTyCheck.Gen.Coverage +import System.Random.Pure.StdGen + +%language ElabReflection + +%hint +genStr : Gen MaybeEmpty String +genStr = elements ["a", "b", "c", "d", "f", "g", "h"] +``` + +### Add the following code + +```idris +mutual + data EntryList : Type where + Nil : EntryList + (::) : Entry -> EntryList -> EntryList + + data Entry = File String | Directory EntryList + +-- A generator for Entry that takes an external String generator +genEntry : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty Entry +genEntry = deriveGen +``` + +### Add a coverage analysis `main` function + +```idris +main : IO () +main = do + let reportTemplate = initCoverageInfo genEntry + let rawCoverageRuns = unGenTryND 1000 someStdGen (genEntry (limit 10)) + let allRawCoverage = concatMap fst rawCoverageRuns + let finalReport = registerCoverage allRawCoverage reportTemplate + putStrLn $ show finalReport +``` + +### Analyze the report + +The results will be starkly imbalanced because `deriveGen` prefers the non-recursive `File` constructor + +```text + Entry covered fully (1000 times) + - File: covered (909 times) + - Directory: covered (91 times) +``` + +This is the problem we need to solve. + +--- + +## Step 2: Probability Tuning + +To fix the bias, we must implement the `ProbabilityTuning` interface for the `Directory` constructor. This tells `deriveGen` to override its default +weight. + +### Define the implementation + +Place this implementation at the top level of your file. It targets the `Directory` constructor by its name + +```idris +mutual + data EntryListP : Type where + Nil2 : EntryListP + Q2 : EntryP -> EntryListP -> EntryListP + + data EntryP = FileP String | DirectoryP EntryListP + +-- A generator for Entry that takes an external String generator +genEntryP : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty EntryListP +genEntryP = deriveGen + +ProbabilityTuning `{DirectoryP}.dataCon where + isConstructor = itIsConstructor + tuneWeight _ = 1 +``` + +- `ProbabilityTuning ... where`: We define a specific implementation of this interface for a constructor. +- `"Directory".dataCon`: This is a `Name` literal that refers to the `Directory` constructor. Since `Directory` is defined in this same file, we can use +the simple name without a module prefix. +- `isConstructor = itIsConstructor`: This is a required line of reflection boilerplate that confirms we have targeted a valid constructor. +- `tuneWeight _ = 10`: We implement the `tuneWeight` function. It takes the default weight `_` and we ignore it, always returning our new, higher weight +of `10`. + +### Re-run the coverage analysis + +The compiler will now automatically find and apply our implementation. Simply recompile and run. + +```idris +mainP : IO () +mainP = do + let reportTemplate = initCoverageInfo genEntryP + let rawCoverageRuns = unGenTryND 1000 someStdGen (genEntryP (limit 10)) + let allRawCoverage = concatMap fst rawCoverageRuns + let finalReport = registerCoverage allRawCoverage reportTemplate + putStrLn $ show finalReport +``` + +### Analyze the new report + +The distribution will now be much closer to a 50/50 balance, proving we have successfully tuned the probability. + +```text + Entry covered fully (1000 times) + - File: covered (526 times) + - Directory: covered (474 times) +``` + +--- + +## Step 3: Generation Order Tuning + +Probability isn't the only thing we can tune. For some dependent types, the _order_ in which arguments are generated is critical for efficiency. +Consider a pair `(n, m)` where we require `n < m`. + +```idris +data LtPair : Type where + MkLtPair : (n : Nat) -> (m : Nat) -> (prf : So $ n < m) -> LtPair +``` + +`deriveGen`'s default strategy might randomly pick `n=10` and `m=5`, then fail because it can't prove `10 < 5`. This is very inefficient. We can tell it +to generate `m` first, making it much easier to pick a valid `n`. + +### Define the generator and the tuning implementation in your file + +```idris +GenOrderTuning `{MkLtPair}.dataCon where + isConstructor = itIsConstructor + deriveFirst _ _ = [`{m}] + +genLtPair : Fuel -> Gen MaybeEmpty LtPair +genLtPair = deriveGen + +Show LtPair where + show (MkLtPair n m _) = "MkLtPair " ++ show n ++ " " ++ show m ++ " _" +``` + +- `GenOrderTuning ... where`: We implement the ordering interface for the `MkLtPair` constructor. +- `deriveFirst _ _ = [``{m}]`: We implement `deriveFirst` to return a list of arguments that must be generated first. Here, we specify the argument +named `m` using a name literal ```{m}`. + +### Test It + +With this instance in scope, `deriveGen` will now follow our instructions. When generating an `LtPair`, it will generate `m` first, and then be smart +enough to only generate values for `n` that are less than `m`. + +```idris +-- A main function to test the LtPair generator +main_lt : IO () +main_lt = do + let reportTemplate = initCoverageInfo genLtPair + let rawCoverageRuns = unGenTryND 1000 someStdGen (genLtPair (limit 10)) + let allRawCoverage = concatMap fst rawCoverageRuns + let finalReport = registerCoverage allRawCoverage reportTemplate + putStrLn $ show finalReport +``` + +You will see that this generator efficiently produces valid pairs like `MkLtPair 5 10 True` every time, without the wasteful failures of the naive +approach. + +--- + +## Next Steps + +- **Want to integrate handwritten generators?** Continue to **[Mixing Manual and Automatic Generation](t06-mixing-manual-and-automatic.md)** to see how +`deriveGen` automatically discovers and uses your custom generators. +- **Want to generate types with proof constraints?** Continue to **[Generating GADTs with Proofs](t08-generating-gadts-with-proofs.md)** to see how +`deriveGen` handles GADTs with auto-implicit proof arguments. +- **Want to see a complete example?** Continue to **[Toy Example: Generating ASTs for a DSL](t09-toy-example.md)** to build a complete generator for a +simple imperative language. diff --git a/docs/source/tutorials/test-function.md b/docs/source/tutorials/test-function.md deleted file mode 100644 index 5343f3b89..000000000 --- a/docs/source/tutorials/test-function.md +++ /dev/null @@ -1 +0,0 @@ -# Test you first function diff --git a/pack.toml b/pack.toml index 9aab81d2a..17797f273 100644 --- a/pack.toml +++ b/pack.toml @@ -3,7 +3,12 @@ ################ [install] -whitelist = [ "deptycheck-docs", "pil-fun", "pil-dyn" ] +whitelist = [ "deptycheck-docs" + , "pil-fun" + , "pil-dyn" + , "super-linter-run" + , "super-linter-fix" + ] ####################### ### Elab-util-extra ### @@ -30,6 +35,16 @@ type = "local" path = "docs" ipkg = "docs.ipkg" +[custom.all.super-linter-run] +type = "local" +path = ".linters" +ipkg = "super-linter-run.ipkg" + +[custom.all.super-linter-fix] +type = "local" +path = ".linters" +ipkg = "super-linter-fix.ipkg" + ################ ### Examples ### ################ diff --git a/tests/docs/typecheck/expected b/tests/docs/typecheck/expected index fe4f238df..fa24eaf61 100644 --- a/tests/docs/typecheck/expected +++ b/tests/docs/typecheck/expected @@ -1,19 +1,27 @@ - 1/19: Building Tutorials.TestFunction (src/Tutorials/TestFunction.md) - 2/19: Building Tutorials.Generators (src/Tutorials/Generators.md) - 3/19: Building Tutorials.Derivation (src/Tutorials/Derivation.md) - 4/19: Building Reference.Users.Pbt (src/Reference/Users/Pbt.md) - 5/19: Building Reference.Users.GenMonad (src/Reference/Users/GenMonad.md) - 6/19: Building Reference.Users.Derivation (src/Reference/Users/Derivation.md) - 7/19: Building Reference.Contributors.GenMonad (src/Reference/Contributors/GenMonad.md) - 8/19: Building Reference.Contributors.Derivation (src/Reference/Contributors/Derivation.md) - 9/19: Building Meta.Test (src/Meta/Test.md) -10/19: Building Explanation.Specifications.Recommendations (src/Explanation/Specifications/Recommendations.md) -11/19: Building Explanation.Specifications.Experiments (src/Explanation/Specifications/Experiments.md) -12/19: Building Explanation.Generators.Design (src/Explanation/Generators/Design.md) -13/19: Building Explanation.Derivation.Design (src/Explanation/Derivation/Design.md) -14/19: Building Explanation.Derivation.Design.WhenDerivationHappens (src/Explanation/Derivation/Design/WhenDerivationHappens.md) -15/19: Building Explanation.Derivation.Design.TypeParamsAndIndices (src/Explanation/Derivation/Design/TypeParamsAndIndices.md) -16/19: Building Explanation.Derivation.Design.SingleGen (src/Explanation/Derivation/Design/SingleGen.md) -17/19: Building Explanation.Derivation.Design.SingleCon (src/Explanation/Derivation/Design/SingleCon.md) -18/19: Building Explanation.Derivation.Design.DerivationTask (src/Explanation/Derivation/Design/DerivationTask.md) -19/19: Building Explanation.Derivation.Design.ClosureOfGens (src/Explanation/Derivation/Design/ClosureOfGens.md) + 1/27: Building Tutorials.T10DerivationTuning (src/Tutorials/T10DerivationTuning.md) + 2/27: Building Tutorials.T09ToyExample (src/Tutorials/T09ToyExample.md) + 3/27: Building Tutorials.T08GeneratingGadtsWithProofs (src/Tutorials/T08GeneratingGadtsWithProofs.md) + 4/27: Building Tutorials.T07BeyondFuel (src/Tutorials/T07BeyondFuel.md) + 5/27: Building Tutorials.T06MixingManualAndAutomatic (src/Tutorials/T06MixingManualAndAutomatic.md) + 6/27: Building Tutorials.T05DerivegenSignatures (src/Tutorials/T05DerivegenSignatures.md) + 7/27: Building Tutorials.T04AutomaticGeneratorDerivation (src/Tutorials/T04AutomaticGeneratorDerivation.md) + 8/27: Building Tutorials.T03MeasuringTestCoverage (src/Tutorials/T03MeasuringTestCoverage.md) + 9/27: Building Tutorials.T02HandlingEmptiness (src/Tutorials/T02HandlingEmptiness.md) +10/27: Building Tutorials.T01GeneratorMonad (src/Tutorials/T01GeneratorMonad.md) +11/27: Building Tutorials.T00InstallationAndSetup (src/Tutorials/T00InstallationAndSetup.md) +12/27: Building Reference.Users.Pbt (src/Reference/Users/Pbt.md) +13/27: Building Reference.Users.GenMonad (src/Reference/Users/GenMonad.md) +14/27: Building Reference.Users.Derivation (src/Reference/Users/Derivation.md) +15/27: Building Reference.Contributors.GenMonad (src/Reference/Contributors/GenMonad.md) +16/27: Building Reference.Contributors.Derivation (src/Reference/Contributors/Derivation.md) +17/27: Building Meta.Test (src/Meta/Test.md) +18/27: Building Explanation.Specifications.Recommendations (src/Explanation/Specifications/Recommendations.md) +19/27: Building Explanation.Specifications.Experiments (src/Explanation/Specifications/Experiments.md) +20/27: Building Explanation.Generators.Design (src/Explanation/Generators/Design.md) +21/27: Building Explanation.Derivation.Design (src/Explanation/Derivation/Design.md) +22/27: Building Explanation.Derivation.Design.WhenDerivationHappens (src/Explanation/Derivation/Design/WhenDerivationHappens.md) +23/27: Building Explanation.Derivation.Design.TypeParamsAndIndices (src/Explanation/Derivation/Design/TypeParamsAndIndices.md) +24/27: Building Explanation.Derivation.Design.SingleGen (src/Explanation/Derivation/Design/SingleGen.md) +25/27: Building Explanation.Derivation.Design.SingleCon (src/Explanation/Derivation/Design/SingleCon.md) +26/27: Building Explanation.Derivation.Design.DerivationTask (src/Explanation/Derivation/Design/DerivationTask.md) +27/27: Building Explanation.Derivation.Design.ClosureOfGens (src/Explanation/Derivation/Design/ClosureOfGens.md) From 4d67965955616dec86f584216d0a136d21817f74 Mon Sep 17 00:00:00 2001 From: "Serge S. Gulin" Date: Thu, 19 Mar 2026 12:24:50 +0300 Subject: [PATCH 3/3] [ docs ] Fix error message --- docs/source/tutorials/t04-automatic-generator-derivation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/tutorials/t04-automatic-generator-derivation.md b/docs/source/tutorials/t04-automatic-generator-derivation.md index a207db40b..cd20fe491 100644 --- a/docs/source/tutorials/t04-automatic-generator-derivation.md +++ b/docs/source/tutorials/t04-automatic-generator-derivation.md @@ -136,7 +136,7 @@ automagic generator deriving supports only `Gen MaybeEmpty` for now. If you need Our first naive attempt to use `deriveGen` might be the following: ```idris -failing "No constructors found for the type `^prim^.String`" +failing "Cannot derive generator for the primitive type String, use external instead" genEntry : Fuel -> Gen MaybeEmpty Entry genEntry = deriveGen ```