Add plutus-tx tests for compiling to case on built-ins (#7539)

Author: basetunnel

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

@@ -13,10 +13,32 @@ This use of `case` in UPLC was introduced with protocol version 11 and requires
 :::
 
 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:
+`Integer` and `Bool` using `case` syntax, which is also used
+for [sums-of-products](./encoding#sums-of-products). This may improve script performance
+and size, compared to older alternatives that use built-in functions.
+
+This page describes the built-in types that are supported in UPLC and how Plinth
+developers can benefit from the improved performance.
+
+## Usage from Plinth
+
+:::info
+
+The Plinth compiler option will change from `datatypes=BuiltinCasing` to
+`datatypes=SumsOfProducts` in the future.
+
+:::
+
+
+Plinth developers can benefit from the performance of `case` by enabling the
+compiler [option](./plinth-compiler-options) `datatypes=BuiltinCasing`, and
+using standard library functions such as `caseList`, `fstPair`.
+Note that Plinth's `case ... of ...` syntax is not generally compiled to UPLC,
+as it can be more expressive.
+
+## Supported types
+
+The UPLC built-in types that `case` can be used on are:
 
 - `bool`
 - `unit`
@@ -26,144 +48,184 @@ The built-in types that `case` currently supports are:
 
 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` (which in the future be achieved with
-`datatypes=SumsOfProducts), 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:
+The following Plinth code implements a basic assertion:
 
-```uplc
-lam b (case b (con bool True) (con bool False))
+```haskell
+assert :: Bool -> BuiltinUnit
+assert False = error ()
+assert True = unitval
 ```
 
-When only a single branch is provided, script execution will fail when the
-boolean evaluates to `True`.
+With `datatypes=BuiltinCasing`, it is compiled to the new casing on builtins:
 
-Using a single branch is appropriate when the second branch was supposed to fail
-already, saving script size.
+```uplc
+\b -> case b [error, ()]
+```
 
+In UPLC, booleans can be used in `case` with either one or two branches, where
+the first is always the `False` branch. When only a single branch is provided,
+script execution will fail when the boolean evaluates to True.
 
 :::info
 
-When compiling without `datatypes=BuiltinCasing`, Plinth's `ifThenElse` is
-compiled into UPLC's `ifThenElse` built-in function, which usually requires more
-AST nodes since each branch argument needs to be delayed (function application is
-strict), and finally force the chosen branch. This impacts the size and
-execution cost.
+Compare this to the UPLC that would have been generated otherwise:
+
+```uplc
+\b -> force (force ifThenElse b (delay ()) (delay error))
+```
 
+This uses the UPLC builtin function `ifThenElse`, which requires delaying the branch
+arguments, since application in UPLC is strict. The additional forcing and
+delaying impacts the size and execution cost.
 :::
 
 
-### Unit
+### BuiltinUnit
+
+The built-in unit type can be used in a trivial way with `case` in UPLC, which
+takes exactly one branch. With `datatypes=BuiltinCasing`, Plinth will compile
+`chooseUnit` from `PlutusTx.Builtins.Internal` into `case`. For example:
+
+```haskell
+forceUnit :: BuiltinUnit -> Integer
+forceUnit e = chooseUnit e 5
+```
 
-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`.
+Which results in the following UPLC:
 
 ```uplc
-case (con unit ()) (con integer 5)
+\e -> case e [5]
 ```
 
-### Pair
+UPLC's case on built-in unit requires exactly one branch. If the expression
+being cased on evaluates to the unit value, evaluation will continue with the
+expression in that branch.
 
-A built-in pair expects a single branch: a function that takes both components
-of the pair.
+### BuiltinPair
 
-This example sums the two integer constants in a pair.
+To destruct a built-in pair, use `casePair` from `PlutusTx.Builtins`. For example:
 
-```uplc
-lam x (case x (lam a (lam b [(builtin addInteger) a b])))
+```haskell
+addPair :: BuiltinPair Integer Integer -> Integer
+addPair p = casePair p (+)
+```
+
+This compiles into `case` in UPLC, which expects a single branch:
+
+```
+\p -> case p [(\x y -> addInteger x y)]
 ```
 
 :::info
 
 When compiling without `datatypes=BuiltinCasing`, Plinth's `choosePair` is
 compiled into multiple built-in function calls to project out the pair's
-components, impacting size and execution cost.
+components, impacting size and execution cost:
+
+```uplc
+\p -> addInteger (force (force fstPair) p) (force (force sndPair) p)
+```
 
 :::
 
 ### Integer
 
-Casing on integers can be used for non-negative integers only, and a variable
+Casing on integers in UPLC 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.
+`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"`
+In Plinth, use the `caseInteger` function:
 
-```
-case [(builtin addInteger) (con integer 1) (con integer 1)]
-  (con string "a")
-  (con string "b")
-  (con string "c")
+```haskell
+integerABC :: Integer -> BuiltinString
+integerABC i = caseInteger i ["a", "b", "c"]
 ```
 
-If the `i`th branch is not given, or `i` is a negative integer, evaluation will
-fail:
+Applying this function to `2` gives `"c"`, while `10` or `-1` produce an error.
+Note that the second argument must be given as a literal list, otherwise it is a
+Plinth compile error.
 
-```
-case [(builtin addInteger) (con integer 2) (con integer 2)]
-  (con string "a")
-  (con string "b")
-  (con string "c")
-```
 
-Results in
+Plinth generates the following UPLC:
 
 ```
-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
+\i -> case i ["a", "b", "c"]
 ```
 
-Note that there is no way to provide a "catch-all" case for integers.
+In general, if `i`th branch is not given, or `i` is a negative integer, evaluation will
+fail. Note that there is no way to provide a "catch-all" case for integers.
 
 :::info
 
-In Plinth, using `caseInteger` with `datatypes=BuiltinCasing` will be compiled into
-the above `case` construct in PIR, provided the second argument is given as a
-literal list (otherwise this is a compile error).
-
 When not using `datatypes=BuiltinCasing`, Plinth's `caseInteger` is compiled
 into a much less efficient implementation that turns the second argument in a
 list (of which the representation depends on the chosen `datatypes=` flag), and
-does a recursive lookup in that list.
+does a recursive lookup in that list. The above Plinth code is compiled to:
+
 
+```uplc
+(\traceError ->
+       (\go i ->
+          force
+            (force ifThenElse
+               (lessThanInteger i 0)
+               (delay (traceError "PT6"))
+               (delay
+                  (go
+                     i
+                     (constr 1
+                        [ "a"
+                        , (constr 1
+                             ["b", (constr 1 ["c", (constr 0 [])])]) ])))))
+         ((\s -> s s)
+            (\s ds ds ->
+               case
+                 ds
+                 [ (traceError "PT7")
+                 , (\x xs ->
+                      force
+                        (force ifThenElse
+                           (equalsInteger 0 ds)
+                           (delay x)
+                           (delay
+                              ((\x -> s s x) (subtractInteger ds 1) xs)))) ])))
+      (\str -> (\x -> error) (force trace str (constr 0 [])))
+```
 :::
 
 
-### List
+### BuiltinList
 
 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.
+This example implements a `head` function for boolean lists, which fails if the list if empty.
 
 ```uplc
-lam xs (case xs (lam y (lam ys y)))
+head :: BuiltinList Bool -> Bool
+head xs = caseList (\_ -> error ()) (\x _ -> x) xs
 ```
 
 :::info
 
-When compiling without `datatypes=BuiltinCasing`, Plinth's `caseList` is
-compiled into a combination of built-in calls such as `chooseList`, `headList`
-and `tailList`. Similarly to booleans, the branches are also thunked, impacting
-script size and execution cost.
+When compiling without `datatypes=BuiltinCasing`, compilation falls back on
+using multiple built-ins, such as `chooseList`, `headList` and `tailList`.
+Similarly to booleans, the branches are thunked, impacting script size and
+execution cost:
+
+```uplc
+(\xs ->
+      force
+        (force (force chooseList)
+           xs
+           (delay (\ds -> error))
+           (delay ((\x xs ds -> x) (force headList xs) (force tailList xs))))
+        (constr 0 []))
+```
 
 :::

plutus-tx-plugin/plutus-tx-plugin.cabal

@@ -131,6 +131,7 @@ test-suite plutus-tx-plugin-tests
     Budget.Spec
     Budget.WithGHCOptimisations
     Budget.WithoutGHCOptimisations
+    BuiltinCasing.Spec
     BuiltinList.Budget.Spec
     BuiltinList.NoCasing.Spec
     ByteStringLiterals.Lib

plutus-tx-plugin/test/BuiltinCasing/9.6/addPair.golden.uplc

@@ -0,0 +1 @@
+(program 1.1.0 (\p -> case p [(\x y -> addInteger x y)]))

plutus-tx-plugin/test/BuiltinCasing/9.6/assert.golden.uplc

@@ -0,0 +1 @@
+(program 1.1.0 (\ds -> case ds [error, ()]))

plutus-tx-plugin/test/BuiltinCasing/9.6/forceUnit.golden.uplc

@@ -0,0 +1 @@
+(program 1.1.0 (\e -> case e [5]))

plutus-tx-plugin/test/BuiltinCasing/9.6/head.golden.uplc

@@ -0,0 +1 @@
+(program 1.1.0 (\xs -> case xs [(\x xs ds -> x), (\ds -> error)] (constr 0 [])))

plutus-tx-plugin/test/BuiltinCasing/9.6/integerABC.golden.uplc

@@ -0,0 +1 @@
+(program 1.1.0 (\i -> case i ["a", "b", "c"]))

plutus-tx-plugin/test/BuiltinCasing/Spec.hs

@@ -0,0 +1,45 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:datatypes=BuiltinCasing #-}
+
+{-| This module tests compilation of built-in types into UPLC's casing of constants
+the examples also appear in the Plinth guide page about case -}
+module BuiltinCasing.Spec where
+
+import Test.Tasty.Extras
+
+import PlutusTx (compile)
+import PlutusTx.Builtins (caseInteger, caseList, casePair)
+import PlutusTx.Builtins.Internal (chooseUnit, unitval)
+import PlutusTx.Prelude
+import PlutusTx.Test
+
+assert :: Bool -> BuiltinUnit
+assert False = error ()
+assert True = unitval
+
+forceUnit :: BuiltinUnit -> Integer
+forceUnit e = chooseUnit e 5
+
+addPair :: BuiltinPair Integer Integer -> Integer
+addPair p = casePair p (+)
+
+integerABC :: Integer -> BuiltinString
+integerABC i = caseInteger i ["a", "b", "c"]
+
+head :: BuiltinList Bool -> Bool
+head xs = caseList (\_ -> error ()) (\x _ -> x) xs
+
+tests :: TestNested
+tests =
+  testNested "BuiltinCasing"
+    . pure
+    $ testNestedGhc
+      [ goldenUPlcReadable "assert" $$(compile [||assert||])
+      , goldenUPlcReadable "forceUnit" $$(compile [||forceUnit||])
+      , goldenUPlcReadable "addPair" $$(compile [||addPair||])
+      , goldenUPlcReadable "integerABC" $$(compile [||integerABC||])
+      , goldenUPlcReadable "head" $$(compile [||head||])
+      ]

plutus-tx-plugin/test/Spec.hs

@@ -5,6 +5,7 @@ import AsData.Budget.Spec qualified as AsData.Budget
 import AssocMap.Spec qualified as AssocMap
 import Blueprint.Tests qualified
 import Budget.Spec qualified as Budget
+import BuiltinCasing.Spec qualified as BuiltinCasing
 import BuiltinList.Budget.Spec qualified as BuiltinList.Budget
 import BuiltinList.NoCasing.Spec qualified as BuiltinList.NoCasing
 import ByteStringLiterals.Spec qualified as ByteStringLiterals
@@ -64,4 +65,5 @@ tests =
     , embed List.propertyTests
     , Array.smokeTests
     , CallTrace.tests
+    , BuiltinCasing.tests
     ]