Docs for casing on constants

doc/docusaurus/docs/delve-deeper/casing-constants.md

@@ -0,0 +1,125 @@
+---
+sidebar_position: 26
+---
+
+# Case-splitting on constants
+
+:::info
+
+This use of `case` in UPLC was introduced with protocol version 11 and requires
+[Plutus Core version](../essential-concepts/versions#plutus-core-version)
+`1.1.0`.
+
+:::
+
+In UPLC, it is possible to branch on expressions of certain built-in types, like
+`Integer` and `Bool`. This can be done with `case` syntax, which is also used
+for [sums-of-products](./encoding#sums-of-products). Using `case` on built-in
+values may improve script performance and size. 
+The built-in types that `case` currently supports are:
+
+- `bool`
+- `unit`
+- `integer`
+- `list`
+- `pair`
+
+In the future, support for `data` is also planned.
+
+For each type, the allowed branches and their order differs. See [Supported
+Types](#supported-types) for more detail.
+
+## Compiling to `case` in Plinth
+
+When compiling Plinth code with the [option](./plinth-compiler-options)
+`datatypes=BuiltinCasing`, many standard library functions will be compiled into
+this use of `case`, such as `fstPair`, `ifThenElse` and `caseList`. Note that
+Plinth's `case ... of ...` syntax is not necessarily compiled to UPLC, as it can
+be more expressive.
+
+## Supported types
+
+### Bool
+
+Booleans can be used in `case` with either one or two branches, where the first
+is the `False` branch. Boolean negation can be written for example as:
+
+```uplc
+lam b (case b (con bool True) (con bool False))
+```
+
+When only a single branch is provided, script execution will fail when the
+boolean evaluates to `True`.
+
+Using a single branch is appropriate when the second branch was supposed to fail
+already, saving script size.
+
+### Unit
+
+Needs exactly one branch. If the expression being cased on evaluates to a unit
+value, evaluation will continue with the expression in that branch. For example,
+this expression evaluates to `con integer 5`.
+
+```uplc
+case (con unit ()) (con integer 5)
+```
+
+### Pair
+
+A built-in pair expects a single branch: a function that takes both components
+of the pair.
+
+This example sums the two integer constants in a pair.
+
+```uplc
+lam x (case x (lam a (lam b [(builtin addInteger) a b])))
+```
+
+### Integer
+
+Casing on integers can be used for non-negative integers only, and a variable
+amount of branches may be given. If the expression `e` evaluates to an integer
+`i`, the `i`th branch will be evaluated. If there is no branch, `case` will fail.
+
+For example, the following expression evaluates to `con string "c"`
+
+```
+case [(builtin addInteger) (con integer 1) (con integer 1)]
+  (con string "a")
+  (con string "b")
+  (con string "c")
+```
+
+If the `i`th branch is not given, or `i` is a negative integer, evaluation will
+fail:
+
+```
+case [(builtin addInteger) (con integer 2) (con integer 2)]
+  (con string "a")
+  (con string "b")
+  (con string "c")
+```
+
+Results in
+
+```
+An error has occurred:
+'case' over a value of a built-in type failed with
+'case 4' is out of bounds for the given number of branches: 3
+Caused by: 4
+```
+
+Note that there is no way to provide a "catch-all" case for integers.
+
+### List
+
+A `case` on built-in lists may be given one or two branches (similar to
+booleans), where the first one deals with the cons case, and the second one with
+the empty list. If no second branch is given, execution will fail when the list
+turns out to be empty.
+
+This example implements the `head` function, which fails if the list if empty.
+
+```uplc
+lam xs (case xs (lam y (lam ys y)))
+```

doc/docusaurus/docs/delve-deeper/plinth-compiler-options.md

@@ -26,7 +26,7 @@ For each boolean option, you can add a `no-` prefix to switch it off, such as `n
 |`coverage-all`|Bool|False|Add all available coverage annotations in the trace output|
 |`coverage-boolean`|Bool|False|Add boolean coverage annotations in the trace output|
 |`coverage-location`|Bool|False|Add location coverage annotations in the trace output|
-|`datatypes`|DatatypeCompilationOpts|SumsOfProducts|Set datatype encoding style|
+|`datatypes`|DatatypeCompilationOpts|SumsOfProducts|BuiltinCasing|Set datatype encoding style|
 |`defer-errors`|Bool|False|If a compilation error happens and this option is turned on, the compilation error is suppressed and the original Haskell expression is replaced with a runtime-error expression.|
 |`dump-compilation-trace`|Bool|False|Dump compilation trace for debugging|
 |`dump-pir`|Bool|False|Dump Plutus IR|