[Builtins] Allow casing on booleans and integers

plutus-benchmark/common/PlutusBenchmark/Common.hs

@@ -33,6 +33,7 @@ import PlutusBenchmark.ProtocolParameters as PP
 import PlutusLedgerApi.Common qualified as LedgerApi
 
 import PlutusCore qualified as PLC
+import PlutusCore.Builtin qualified as PLC
 import PlutusCore.Default
 import PlutusCore.Evaluation.Machine.ExBudget (ExBudget (..))
 import PlutusCore.Evaluation.Machine.ExBudgetingDefaults qualified as PLC
@@ -97,6 +98,7 @@ mkEvalCtx ll semvar =
             let errOrCtx =
                     LedgerApi.mkDynEvaluationContext
                         ll
+                        (\_ -> PLC.CaserBuiltin PLC.caseBuiltin)
                         [semvar]
                         (const semvar)
                         p

plutus-conformance/haskell-steppable/Spec.hs

@@ -4,6 +4,7 @@
 module Main (main) where
 
 import PlutusConformance.Common
+import PlutusCore.Evaluation.Machine.MachineParameters qualified as UPLC
 import PlutusCore.Evaluation.Machine.MachineParameters.Default
 import PlutusPrelude
 import UntypedPlutusCore as UPLC
@@ -31,9 +32,9 @@ failingBudgetTests = []
 evalSteppableUplcProg :: UplcEvaluator
 evalSteppableUplcProg = UplcEvaluatorWithCosting $
   \modelParams (UPLC.Program a v t) -> do
-    params <- case mkMachineParametersFor [def] modelParams of
+    params <- case mkMachineVariantParametersFor [def] modelParams of
       Left _               -> Nothing
-      Right machParamsList -> lookup def machParamsList
+      Right machParamsList -> UPLC.MachineParameters def <$> lookup def machParamsList
     -- runCek-like functions (e.g. evaluateCekNoEmit) are partial on term's with
     -- free variables, that is why we manually check first for any free vars
     case UPLC.deBruijnTerm t of

plutus-conformance/haskell/Spec.hs

@@ -4,6 +4,7 @@
 module Main (main) where
 
 import PlutusConformance.Common (UplcEvaluator (..), runUplcEvalTests)
+import PlutusCore.Evaluation.Machine.MachineParameters qualified as UPLC
 import PlutusCore.Evaluation.Machine.MachineParameters.Default
 import PlutusPrelude (def)
 import UntypedPlutusCore qualified as UPLC
@@ -13,9 +14,9 @@ import UntypedPlutusCore.Evaluation.Machine.Cek (CountingSt (..), counting, runC
 evalUplcProg :: UplcEvaluator
 evalUplcProg = UplcEvaluatorWithCosting $ \modelParams (UPLC.Program a v t) ->
   do
-    params <- case mkMachineParametersFor [def] modelParams of
+    params <- case mkMachineVariantParametersFor [def] modelParams of
       Left _               -> Nothing
-      Right machParamsList -> lookup def machParamsList
+      Right machParamsList -> UPLC.MachineParameters def <$> lookup def machParamsList
     -- runCek-like functions (e.g. evaluateCekNoEmit) are partial on term's with
     -- free variables, that is why we manually check first for any free vars
     case UPLC.deBruijnTerm t of

plutus-conformance/test-cases/uplc/evaluation/term/case/case-5/case-5.uplc

@@ -1,4 +1,4 @@
 -- case of non-constr
 (program 1.1.0
-    (case (con integer 1) (lam x x) (lam x x))
+    (case (lam x x) (lam x x) (lam x x))
 )

plutus-core/cost-model/budgeting-bench/Benchmarks/Nops.hs

@@ -122,7 +122,7 @@ nopCostModel =
 
 nopCostParameters :: MachineParameters CekMachineCosts NopFun (CekValue DefaultUni NopFun ())
 nopCostParameters =
-    mkMachineParameters def $
+    MachineParameters def . mkMachineVariantParameters def $
         CostModel defaultCekMachineCostsForTesting nopCostModel
 
 -- This is just to avoid some deeply nested case expressions for the NopNc

plutus-core/plutus-core.cabal

@@ -233,6 +233,7 @@ library
     Data.Aeson.Flatten
     Data.Functor.Foldable.Monadic
     Data.Vector.Orphans
+    PlutusCore.Builtin.Case
     PlutusCore.Builtin.HasConstant
     PlutusCore.Builtin.KnownKind
     PlutusCore.Builtin.KnownType

plutus-core/plutus-core/src/PlutusCore/Builtin.hs

@@ -4,6 +4,7 @@ module PlutusCore.Builtin
     ( module Export
     ) where
 
+import PlutusCore.Builtin.Case as Export
 import PlutusCore.Builtin.HasConstant as Export
 import PlutusCore.Builtin.KnownKind as Export
 import PlutusCore.Builtin.KnownType as Export

plutus-core/plutus-core/src/PlutusCore/Builtin/Case.hs

@@ -0,0 +1,51 @@
+{-# LANGUAGE DataKinds         #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes        #-}
+{-# LANGUAGE TypeOperators     #-}
+
+module PlutusCore.Builtin.Case where
+
+import PlutusCore.Core.Type (Type, UniOf)
+import PlutusCore.Name.Unique
+
+import Control.DeepSeq (NFData (..), rwhnf)
+import Data.Default.Class (Default (..))
+import Data.Text (Text)
+import Data.Vector (Vector)
+import NoThunks.Class
+import Text.PrettyBy (display)
+import Universe
+
+class AnnotateCaseBuiltin uni where
+    -- | Given a tag for a built-in type and a list of branches, annotate each of the branches with
+    -- its expected argument types or fail if casing on values of the built-in type isn't supported.
+    annotateCaseBuiltin
+        :: UniOf term ~ uni
+        => SomeTypeIn uni
+        -> [term]
+        -> Either Text [(term, [Type TyName uni ann])]
+
+class CaseBuiltin uni where
+    -- | Given a constant with its type tag and a vector of branches, choose the appropriate branch
+    -- or fail if the constant doesn't correspond to any of the branches (or casing on constants of
+    -- this type isn't supported at all).
+    caseBuiltin :: UniOf term ~ uni => Some (ValueOf uni) -> Vector term -> Either Text term
+
+data CaserBuiltin uni = CaserBuiltin
+    { unCaserBuiltin
+        :: !(forall term. UniOf term ~ uni => Some (ValueOf uni) -> Vector term -> Either Text term)
+    }
+
+instance NFData (CaserBuiltin uni) where
+    rnf = rwhnf
+
+deriving via OnlyCheckWhnfNamed "PlutusCore.Builtin.Case.CaserBuiltin" (CaserBuiltin uni)
+    instance NoThunks (CaserBuiltin uni)
+
+instance CaseBuiltin uni => Default (CaserBuiltin uni) where
+    def = CaserBuiltin caseBuiltin
+
+unavailableCaserBuiltin :: Int -> CaserBuiltin uni
+unavailableCaserBuiltin ver =
+    CaserBuiltin $ \_ _ -> Left $
+        "'case' on values of built-in types is not supported in protocol version " <> display ver

plutus-core/plutus-core/src/PlutusCore/Compiler/Types.hs

@@ -2,14 +2,19 @@
 
 module PlutusCore.Compiler.Types where
 
-import Data.Hashable
+import PlutusCore
 import PlutusCore.Builtin
 import PlutusCore.Name.Unique
-import PlutusCore.Quote
+
+import Data.Hashable
 
 type Compiling m uni fun name a =
   ( ToBuiltinMeaning uni fun
   , MonadQuote m
+  , CaseBuiltin uni
+  , GEq uni
+  , Closed uni
+  , Everywhere uni Eq
   , HasUnique name TermUnique
   , Ord name
   , Typeable name

plutus-core/plutus-core/src/PlutusCore/Default/Universe.hs

@@ -6,6 +6,7 @@
 -- to test that some constraints are solvable
 {-# OPTIONS -Wno-redundant-constraints #-}
 
+{-# LANGUAGE BangPatterns             #-}
 {-# LANGUAGE BlockArguments           #-}
 {-# LANGUAGE CPP                      #-}
 {-# LANGUAGE ConstraintKinds          #-}
@@ -20,6 +21,7 @@
 {-# LANGUAGE PolyKinds                #-}
 {-# LANGUAGE RankNTypes               #-}
 {-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TupleSections            #-}
 {-# LANGUAGE TypeApplications         #-}
 {-# LANGUAGE TypeFamilies             #-}
 {-# LANGUAGE TypeOperators            #-}
@@ -58,7 +60,8 @@ import Data.Proxy (Proxy (Proxy))
 import Data.Text (Text)
 import Data.Text qualified as Text
 import Data.Typeable (typeRep)
-import Data.Vector.Strict (Vector)
+import Data.Vector qualified as Vector
+import Data.Vector.Strict qualified as Strict (Vector)
 import Data.Word (Word16, Word32, Word64)
 import GHC.Exts (inline, oneShot)
 import Text.PrettyBy.Fixity (RenderContext, inContextM, juxtPrettyM)
@@ -106,7 +109,7 @@ data DefaultUni a where
     DefaultUniString :: DefaultUni (Esc Text)
     DefaultUniUnit :: DefaultUni (Esc ())
     DefaultUniBool :: DefaultUni (Esc Bool)
-    DefaultUniProtoArray :: DefaultUni (Esc Vector)
+    DefaultUniProtoArray :: DefaultUni (Esc Strict.Vector)
     DefaultUniProtoList :: DefaultUni (Esc [])
     DefaultUniProtoPair :: DefaultUni (Esc (,))
     DefaultUniApply :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a))
@@ -261,7 +264,7 @@ instance DefaultUni `Contains` Bool where
     knownUni = DefaultUniBool
 instance DefaultUni `Contains` [] where
     knownUni = DefaultUniProtoList
-instance DefaultUni `Contains` Vector where
+instance DefaultUni `Contains` Strict.Vector where
     knownUni = DefaultUniProtoArray
 instance DefaultUni `Contains` (,) where
     knownUni = DefaultUniProtoPair
@@ -286,8 +289,8 @@ instance KnownBuiltinTypeAst tyname DefaultUni Bool =>
     KnownTypeAst tyname DefaultUni Bool
 instance KnownBuiltinTypeAst tyname DefaultUni [a] =>
     KnownTypeAst tyname DefaultUni [a]
-instance KnownBuiltinTypeAst tyname DefaultUni (Vector a) =>
-    KnownTypeAst tyname DefaultUni (Vector a)
+instance KnownBuiltinTypeAst tyname DefaultUni (Strict.Vector a) =>
+    KnownTypeAst tyname DefaultUni (Strict.Vector a)
 instance KnownBuiltinTypeAst tyname DefaultUni (a, b) =>
     KnownTypeAst tyname DefaultUni (a, b)
 instance KnownBuiltinTypeAst tyname DefaultUni Data =>
@@ -313,8 +316,8 @@ instance KnownBuiltinTypeIn DefaultUni term Data =>
     ReadKnownIn DefaultUni term Data
 instance KnownBuiltinTypeIn DefaultUni term [a] =>
     ReadKnownIn DefaultUni term [a]
-instance KnownBuiltinTypeIn DefaultUni term (Vector a) =>
-    ReadKnownIn DefaultUni term (Vector a)
+instance KnownBuiltinTypeIn DefaultUni term (Strict.Vector a) =>
+    ReadKnownIn DefaultUni term (Strict.Vector a)
 instance KnownBuiltinTypeIn DefaultUni term (a, b) =>
     ReadKnownIn DefaultUni term (a, b)
 instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element =>
@@ -338,8 +341,8 @@ instance KnownBuiltinTypeIn DefaultUni term Data =>
     MakeKnownIn DefaultUni term Data
 instance KnownBuiltinTypeIn DefaultUni term [a] =>
     MakeKnownIn DefaultUni term [a]
-instance KnownBuiltinTypeIn DefaultUni term (Vector a) =>
-    MakeKnownIn DefaultUni term (Vector a)
+instance KnownBuiltinTypeIn DefaultUni term (Strict.Vector a) =>
+    MakeKnownIn DefaultUni term (Strict.Vector a)
 instance KnownBuiltinTypeIn DefaultUni term (a, b) =>
     MakeKnownIn DefaultUni term (a, b)
 instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element =>
@@ -518,6 +521,37 @@ instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni te
                  ]
     {-# INLINE readKnown #-}
 
+outOfBoundsErr :: Pretty a => a -> Vector.Vector term -> Text
+outOfBoundsErr x branches = fold
+    [ "'case "
+    , display x
+    , "' is out of bounds for the given number of branches: "
+    , display $ Vector.length branches
+    ]
+
+instance AnnotateCaseBuiltin DefaultUni where
+    annotateCaseBuiltin (SomeTypeIn uni) branches = case uni of
+        DefaultUniBool    -> Right $ map (, []) branches
+        DefaultUniInteger -> Right $ map (, []) branches
+        _                 -> Left $ display uni <> " isn't supported in 'case'"
+
+instance CaseBuiltin DefaultUni where
+    caseBuiltin (Some (ValueOf uni x)) branches = case uni of
+        DefaultUniBool -> case x of
+            -- We allow there to be only one branch as long as the scrutinee is 'False'.
+            -- This is strictly to save size by not having the 'True' branch if it was gonna be
+            -- 'Error' anyway.
+            False | len == 1 || len == 2 -> Right $ branches Vector.! 0
+            True  |             len == 2 -> Right $ branches Vector.! 1
+            _                            -> Left  $ outOfBoundsErr x branches
+        DefaultUniInteger
+            | 0 <= x && x < toInteger len -> Right $ branches Vector.! fromInteger x
+            | otherwise                   -> Left  $ outOfBoundsErr x branches
+        _ -> Left $ display uni <> " isn't supported in 'case'"
+      where
+        !len = Vector.length branches
+    {-# INLINE caseBuiltin #-}
+
 {- Note [Stable encoding of tags]
 'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
 universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'
@@ -534,7 +568,7 @@ instance Closed DefaultUni where
         , constr `Permits` ()
         , constr `Permits` Bool
         , constr `Permits` []
-        , constr `Permits` Vector
+        , constr `Permits` Strict.Vector
         , constr `Permits` (,)
         , constr `Permits` Data
         , constr `Permits` BLS12_381.G1.Element

plutus-core/plutus-core/src/PlutusCore/Error.hs

@@ -124,6 +124,7 @@ data TypeError term uni fun ann
     | FreeTypeVariableE !ann !TyName
     | FreeVariableE !ann !Name
     | UnknownBuiltinFunctionE !ann !fun
+    | UnsupportedCaseBuiltin !ann !T.Text
     deriving stock (Show, Eq, Generic, Functor)
     deriving anyclass (NFData)
 
@@ -270,6 +271,11 @@ instance (Pretty term, PrettyUni uni, Pretty fun, Pretty ann) =>
         , pretty $ name1 ^. theUnique
         , "is attempted to be referenced"
         ]
+    prettyBy _ (UnsupportedCaseBuiltin ann err) = hsep
+        [ "Unsupported 'case' of a value of a built-in type at"
+        , pretty ann <> ":"
+        , pretty err
+        ]
 
 instance (PrettyUni uni, Pretty fun, Pretty ann) =>
         PrettyBy PrettyConfigPlc (Error uni fun ann) where

plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/ExBudgetingDefaults.hs

@@ -149,17 +149,20 @@ faster than the used in production. Also see Note [noinline for saving on
 ticks]. -}
 defaultCekParametersA :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersA =
-    noinline mkMachineParameters DefaultFunSemanticsVariantA cekCostModelVariantA
+    MachineParameters def $
+        noinline mkMachineVariantParameters DefaultFunSemanticsVariantA cekCostModelVariantA
 
 -- See Note [No inlining for MachineParameters]
 defaultCekParametersB :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersB =
-    noinline mkMachineParameters DefaultFunSemanticsVariantB cekCostModelVariantB
+    MachineParameters def $
+        noinline mkMachineVariantParameters DefaultFunSemanticsVariantB cekCostModelVariantB
 
 -- See Note [No inlining for MachineParameters]
 defaultCekParametersC :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 defaultCekParametersC =
-    noinline mkMachineParameters DefaultFunSemanticsVariantC cekCostModelVariantC
+    MachineParameters def $
+        noinline mkMachineVariantParameters DefaultFunSemanticsVariantC cekCostModelVariantC
 
 {- Note [noinline for saving on ticks]
 We use 'noinline' purely for saving on simplifier ticks for definitions, whose performance doesn't
@@ -357,5 +360,6 @@ unitCostBuiltinCostModel = BuiltinCostModelBase
 unitCekParameters :: Typeable ann => MachineParameters CekMachineCosts DefaultFun (CekValue DefaultUni DefaultFun ann)
 unitCekParameters =
     -- See Note [noinline for saving on ticks].
-    noinline mkMachineParameters def $
-        CostModel unitCekMachineCosts unitCostBuiltinCostModel
+    MachineParameters def $
+        noinline mkMachineVariantParameters def $
+            CostModel unitCekMachineCosts unitCostBuiltinCostModel