Skip to content

Commit 5244c96

Browse files
effectfullyeffectfully
committed
[Builtins] Allow casing on booleans
1 parent f810009 commit 5244c96

File tree

212 files changed

+1659
-1596
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

212 files changed

+1659
-1596
lines changed

‎plutus-core/plutus-core.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -228,6 +228,7 @@ library
228228
Data.Aeson.Flatten
229229
Data.Functor.Foldable.Monadic
230230
Data.Vector.Orphans
231+
PlutusCore.Builtin.Case
231232
PlutusCore.Builtin.HasConstant
232233
PlutusCore.Builtin.KnownKind
233234
PlutusCore.Builtin.KnownType

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ module PlutusCore.Builtin
44
( module Export
55
) where
66

7+
import PlutusCore.Builtin.Case as Export
78
import PlutusCore.Builtin.HasConstant as Export
89
import PlutusCore.Builtin.KnownKind as Export
910
import PlutusCore.Builtin.KnownType as Export

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
{-# LANGUAGE MultiParamTypeClasses #-}
2+
{-# LANGUAGE TypeOperators #-}
3+
4+
module PlutusCore.Builtin.Case where
5+
6+
import PlutusCore.Core.Type (Type, UniOf)
7+
import PlutusCore.Name.Unique
8+
9+
import Data.Vector (Vector)
10+
import Universe
11+
12+
class AnnotateCaseBuiltin uni where
13+
annotateCaseBuiltin
14+
:: UniOf term ~ uni
15+
=> SomeTypeIn uni
16+
-> [term]
17+
-> Either () [(term, [Type TyName uni ann])]
18+
19+
class UniOf term ~ uni => CaseBuiltin term uni where
20+
caseBuiltin :: Some (ValueOf uni) -> Vector term -> Either () term

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

Lines changed: 31 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@
2020
{-# LANGUAGE PolyKinds #-}
2121
{-# LANGUAGE RankNTypes #-}
2222
{-# LANGUAGE StandaloneKindSignatures #-}
23+
{-# LANGUAGE TupleSections #-}
2324
{-# LANGUAGE TypeApplications #-}
2425
{-# LANGUAGE TypeFamilies #-}
2526
{-# LANGUAGE TypeOperators #-}
@@ -43,6 +44,7 @@ module PlutusCore.Default.Universe
4344
import PlutusCore.Builtin
4445
import PlutusPrelude
4546

47+
import PlutusCore.Core.Type (UniOf)
4648
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
4749
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
4850
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
@@ -59,7 +61,8 @@ import Data.Proxy (Proxy (Proxy))
5961
import Data.Text (Text)
6062
import Data.Text qualified as Text
6163
import Data.Typeable (typeRep)
62-
import Data.Vector.Strict (Vector)
64+
import Data.Vector qualified as Vector
65+
import Data.Vector.Strict qualified as Strict (Vector)
6366
import Data.Word (Word16, Word32, Word64)
6467
import GHC.Exts (inline, oneShot)
6568
import Text.PrettyBy.Fixity (RenderContext, inContextM, juxtPrettyM)
@@ -107,7 +110,7 @@ data DefaultUni a where
107110
DefaultUniString :: DefaultUni (Esc Text)
108111
DefaultUniUnit :: DefaultUni (Esc ())
109112
DefaultUniBool :: DefaultUni (Esc Bool)
110-
DefaultUniProtoArray :: DefaultUni (Esc Vector)
113+
DefaultUniProtoArray :: DefaultUni (Esc Strict.Vector)
111114
DefaultUniProtoList :: DefaultUni (Esc [])
112115
DefaultUniProtoPair :: DefaultUni (Esc (,))
113116
DefaultUniApply :: !(DefaultUni (Esc f)) -> !(DefaultUni (Esc a)) -> DefaultUni (Esc (f a))
@@ -262,7 +265,7 @@ instance DefaultUni `Contains` Bool where
262265
knownUni = DefaultUniBool
263266
instance DefaultUni `Contains` [] where
264267
knownUni = DefaultUniProtoList
265-
instance DefaultUni `Contains` Vector where
268+
instance DefaultUni `Contains` Strict.Vector where
266269
knownUni = DefaultUniProtoArray
267270
instance DefaultUni `Contains` (,) where
268271
knownUni = DefaultUniProtoPair
@@ -287,8 +290,8 @@ instance KnownBuiltinTypeAst tyname DefaultUni Bool =>
287290
KnownTypeAst tyname DefaultUni Bool
288291
instance KnownBuiltinTypeAst tyname DefaultUni [a] =>
289292
KnownTypeAst tyname DefaultUni [a]
290-
instance KnownBuiltinTypeAst tyname DefaultUni (Vector a) =>
291-
KnownTypeAst tyname DefaultUni (Vector a)
293+
instance KnownBuiltinTypeAst tyname DefaultUni (Strict.Vector a) =>
294+
KnownTypeAst tyname DefaultUni (Strict.Vector a)
292295
instance KnownBuiltinTypeAst tyname DefaultUni (a, b) =>
293296
KnownTypeAst tyname DefaultUni (a, b)
294297
instance KnownBuiltinTypeAst tyname DefaultUni Data =>
@@ -314,8 +317,8 @@ instance KnownBuiltinTypeIn DefaultUni term Data =>
314317
ReadKnownIn DefaultUni term Data
315318
instance KnownBuiltinTypeIn DefaultUni term [a] =>
316319
ReadKnownIn DefaultUni term [a]
317-
instance KnownBuiltinTypeIn DefaultUni term (Vector a) =>
318-
ReadKnownIn DefaultUni term (Vector a)
320+
instance KnownBuiltinTypeIn DefaultUni term (Strict.Vector a) =>
321+
ReadKnownIn DefaultUni term (Strict.Vector a)
319322
instance KnownBuiltinTypeIn DefaultUni term (a, b) =>
320323
ReadKnownIn DefaultUni term (a, b)
321324
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element =>
@@ -339,8 +342,8 @@ instance KnownBuiltinTypeIn DefaultUni term Data =>
339342
MakeKnownIn DefaultUni term Data
340343
instance KnownBuiltinTypeIn DefaultUni term [a] =>
341344
MakeKnownIn DefaultUni term [a]
342-
instance KnownBuiltinTypeIn DefaultUni term (Vector a) =>
343-
MakeKnownIn DefaultUni term (Vector a)
345+
instance KnownBuiltinTypeIn DefaultUni term (Strict.Vector a) =>
346+
MakeKnownIn DefaultUni term (Strict.Vector a)
344347
instance KnownBuiltinTypeIn DefaultUni term (a, b) =>
345348
MakeKnownIn DefaultUni term (a, b)
346349
instance KnownBuiltinTypeIn DefaultUni term BLS12_381.G1.Element =>
@@ -508,9 +511,9 @@ deriving newtype instance KnownBuiltinTypeIn DefaultUni term [a] =>
508511

509512
deriving newtype instance KnownTypeAst tyname DefaultUni a =>
510513
KnownTypeAst tyname DefaultUni (ArrayCostedByLength a)
511-
deriving newtype instance KnownBuiltinTypeIn DefaultUni term (Vector a) =>
514+
deriving newtype instance KnownBuiltinTypeIn DefaultUni term (Strict.Vector a) =>
512515
MakeKnownIn DefaultUni term (ArrayCostedByLength a)
513-
deriving newtype instance KnownBuiltinTypeIn DefaultUni term (Vector a) =>
516+
deriving newtype instance KnownBuiltinTypeIn DefaultUni term (Strict.Vector a) =>
514517
ReadKnownIn DefaultUni term (ArrayCostedByLength a)
515518

516519
deriving via AsInteger Natural instance
@@ -533,6 +536,22 @@ instance KnownBuiltinTypeIn DefaultUni term Integer => ReadKnownIn DefaultUni te
533536
]
534537
{-# INLINE readKnown #-}
535538

539+
instance UniOf term ~ DefaultUni => CaseBuiltin term DefaultUni where
540+
caseBuiltin (Some (ValueOf uni x)) branches = case uni of
541+
DefaultUniBool
542+
| Vector.length branches == 2 -> Right $ branches Vector.! fromEnum x
543+
| otherwise -> Left ()
544+
DefaultUniInteger
545+
| x < fromIntegral (Vector.length branches) -> Right $ branches Vector.! fromIntegral x
546+
| otherwise -> Left ()
547+
_ -> Left ()
548+
549+
instance AnnotateCaseBuiltin DefaultUni where
550+
annotateCaseBuiltin (SomeTypeIn uni) branches = case uni of
551+
DefaultUniBool -> Right $ map (, []) branches
552+
DefaultUniInteger -> Right $ map (, []) branches
553+
_ -> Left ()
554+
536555
{- Note [Stable encoding of tags]
537556
'encodeUni' and 'decodeUni' are used for serialisation and deserialisation of types from the
538557
universe and we need serialised things to be extremely stable, hence the definitions of 'encodeUni'
@@ -549,7 +568,7 @@ instance Closed DefaultUni where
549568
, constr `Permits` ()
550569
, constr `Permits` Bool
551570
, constr `Permits` []
552-
, constr `Permits` Vector
571+
, constr `Permits` Strict.Vector
553572
, constr `Permits` (,)
554573
, constr `Permits` Data
555574
, constr `Permits` BLS12_381.G1.Element

‎plutus-core/plutus-core/src/PlutusCore/TypeCheck.hs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,8 @@ import PlutusCore.TypeCheck.Internal
4343
-- instantiated and builtins don't. Another reason is that 'Typecheckable' is not required during
4444
-- type checking, since it's only needed for computing 'BuiltinTypes', which is passed as a regular
4545
-- argument to the worker of the type checker.
46-
type Typecheckable uni fun = (ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun)
46+
type Typecheckable uni fun =
47+
(ToKind uni, HasUniApply uni, ToBuiltinMeaning uni fun, AnnotateCaseBuiltin uni)
4748

4849
-- | The default kind checking config.
4950
defKindCheckConfig :: KindCheckConfig

‎plutus-core/plutus-core/src/PlutusCore/TypeCheck/Internal.hs‎

Lines changed: 16 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,8 +18,7 @@ module PlutusCore.TypeCheck.Internal
1818
, MonadNormalizeType
1919
) where
2020

21-
import PlutusCore.Builtin.KnownKind (ToKind, kindOfBuiltinType)
22-
import PlutusCore.Builtin.Result (throwing)
21+
import PlutusCore.Builtin
2322
import PlutusCore.Core.Type (Kind (..), Normalized (..), Term (..), Type (..), toPatFuncKind)
2423
import PlutusCore.Error (AsTypeError (_TypeError), ExpectedShapeOr (ExpectedExact, ExpectedShape),
2524
TypeError (FreeTypeVariableE, FreeVariableE, KindMismatch, NameMismatch, TyNameMismatch, TypeMismatch, UnknownBuiltinFunctionE))
@@ -200,12 +199,13 @@ type MonadKindCheck err term uni fun ann m =
200199

201200
-- | The general constraints that are required for type checking a Plutus AST.
202201
type MonadTypeCheck err term uni fun ann m =
203-
( MonadKindCheck err term uni fun ann m -- Kind checking is run during type checking
204-
-- (this includes the constraint for throwing errors).
202+
( MonadKindCheck err term uni fun ann m -- Kind checking is run during type checking (this
203+
-- includes the constraint for throwing errors).
205204
, Norm.MonadNormalizeType uni m -- Type lambdas open up type computation.
205+
, AnnotateCaseBuiltin uni
206206
, GEq uni -- For checking equality of built-in types.
207-
, Ix fun -- For indexing into the precomputed array of types of
208-
-- built-in functions.
207+
, Ix fun -- For indexing into the precomputed array of
208+
-- types of built-in functions.
209209
)
210210

211211
-- | The constraints that are required for type checking Plutus Core.
@@ -557,22 +557,27 @@ inferTypeM t@(Constr ann resTy i args) = do
557557
-- s_n = [p_n_0 ... p_n_m] [check| G !- c_n : p_n_0 -> ... -> p_n_m -> vResTy]
558558
-- -----------------------------------------------------------------------------
559559
-- [infer| G !- case resTy scrut c_0 ... c_n : vResTy]
560-
inferTypeM (Case ann resTy scrut cases) = do
560+
inferTypeM (Case ann resTy scrut branches) = do
561561
vResTy <- normalizeTypeM $ void resTy
562562
vScrutTy <- inferTypeM scrut
563563

564564
-- We don't know exactly what to expect, we only know that it should
565565
-- be a SOP with the right number of sum alternatives
566-
let prods = map (\j -> "prod_" <> Text.pack (show j)) [0 .. length cases - 1]
566+
let prods = map (\j -> "prod_" <> Text.pack (show j)) [0 .. length branches - 1]
567567
expectedSop = ExpectedShape (Text.intercalate " " $ "sop" : prods) prods
568568
case unNormalized vScrutTy of
569-
TySOP _ sTys -> case zipExact cases sTys of
570-
Just casesAndArgTypes -> for_ casesAndArgTypes $ \(c, argTypes) ->
569+
TySOP _ sTys -> case zipExact branches sTys of
570+
Just branchesAndArgTypes -> for_ branchesAndArgTypes $ \(c, argTypes) ->
571571
-- made of sub-parts of a normalized type, so normalized
572572
checkTypeM ann c (Normalized $ mkIterTyFun () argTypes (unNormalized vResTy))
573573
-- scrutinee does not have a SOP type with the right number of alternatives
574-
-- for the number of cases
574+
-- for the number of branches
575575
Nothing -> throwing _TypeError (TypeMismatch ann (void scrut) expectedSop vScrutTy)
576+
TyBuiltin _ someUni -> case annotateCaseBuiltin someUni branches of
577+
Right branchesAndArgTypes -> for_ branchesAndArgTypes $ \(c, argTypes) ->
578+
-- made of sub-parts of a normalized type, so normalized
579+
checkTypeM ann c (Normalized $ mkIterTyFun () argTypes (unNormalized vResTy))
580+
Left () -> undefined
576581
-- scrutinee does not have a SOP type at all
577582
_ -> throwing _TypeError (TypeMismatch ann (void scrut) expectedSop vScrutTy)
578583

‎plutus-core/plutus-ir/src/PlutusIR/Compiler/Types.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -220,6 +220,7 @@ type Compiling m e uni fun a =
220220
, AsTypeError e (PIR.Term PIR.TyName PIR.Name uni fun ()) uni fun (Provenance a)
221221
, AsTypeErrorExt e uni (Provenance a)
222222
, AsError e uni fun (Provenance a)
223+
, PLC.AnnotateCaseBuiltin uni
223224
, MonadError e m
224225
, MonadQuote m
225226
, Ord a

‎plutus-core/plutus-ir/src/PlutusIR/Pass.hs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ import PlutusIR.Error
99
import PlutusIR.TypeCheck qualified as TC
1010

1111
import PlutusCore qualified as PLC
12+
import PlutusCore.Builtin (AnnotateCaseBuiltin)
1213
import PlutusCore.Name.Unique
1314

1415
import Control.Monad (void, when)
@@ -41,7 +42,7 @@ data BiCondition tyname name uni fun a where
4142
-> BiCondition tyname name uni fun a
4243

4344
checkCondition
44-
:: MonadError (Error uni fun a) m
45+
:: (MonadError (Error uni fun a) m, AnnotateCaseBuiltin uni)
4546
=> Condition tyname name uni fun a
4647
-> Term tyname name uni fun a
4748
-> m ()
@@ -56,7 +57,7 @@ checkCondition c t = case c of
5657
Nothing -> pure ()
5758

5859
checkBiCondition
59-
:: MonadError (Error uni fun a) m
60+
:: (MonadError (Error uni fun a) m, AnnotateCaseBuiltin uni)
6061
=> BiCondition tyname name uni fun a
6162
-> Term tyname name uni fun a
6263
-> Term tyname name uni fun a
@@ -94,7 +95,7 @@ hoistPass f p = case p of
9495
NoOpPass -> NoOpPass
9596

9697
runPass
97-
:: Monad m
98+
:: (Monad m, AnnotateCaseBuiltin uni)
9899
=> (String -> m ())
99100
-> Bool
100101
-> Pass m tyname name uni fun a

‎plutus-core/plutus-ir/src/PlutusIR/TypeCheck/Internal.hs‎

Lines changed: 11 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ import PlutusIR.MkPir qualified as PIR
3434
import PlutusIR.Transform.Rename ()
3535

3636
import PlutusCore (toPatFuncKind, tyVarDeclName, typeAnn)
37+
import PlutusCore.Builtin (annotateCaseBuiltin)
3738
import PlutusCore.Core qualified as PLC
3839
import PlutusCore.Error as PLC
3940
import PlutusCore.MkPlc (mkIterTyFun)
@@ -271,22 +272,27 @@ inferTypeM t@(Constr ann resTy i args) = do
271272
-- s_n = [p_n_0 ... p_n_m] [check| G !- c_n : p_n_0 -> ... -> p_n_m -> vResTy]
272273
-- -----------------------------------------------------------------------------
273274
-- [infer| G !- case resTy scrut c_0 ... c_n : vResTy]
274-
inferTypeM (Case ann resTy scrut cases) = do
275+
inferTypeM (Case ann resTy scrut branches) = do
275276
vResTy <- normalizeTypeM $ void resTy
276277
vScrutTy <- inferTypeM scrut
277278

278279
-- We don't know exactly what to expect, we only know that it should
279280
-- be a SOP with the right number of sum alternatives
280-
let prods = map (\j -> "prod_" <> Text.pack (show j)) [0 .. length cases - 1]
281+
let prods = map (\j -> "prod_" <> Text.pack (show j)) [0 .. length branches - 1]
281282
expectedSop = ExpectedShape (Text.intercalate " " $ "sop" : prods) prods
282283
case unNormalized vScrutTy of
283-
TySOP _ sTys -> case zipExact cases sTys of
284-
Just casesAndArgTypes -> for_ casesAndArgTypes $ \(c, argTypes) ->
284+
TySOP _ sTys -> case zipExact branches sTys of
285+
Just branchesAndArgTypes -> for_ branchesAndArgTypes $ \(c, argTypes) ->
285286
-- made of sub-parts of a normalized type, so normalized
286287
checkTypeM ann c (Normalized $ mkIterTyFun () argTypes (unNormalized vResTy))
287288
-- scrutinee does not have a SOP type with the right number of alternatives
288-
-- for the number of cases
289+
-- for the number of branches
289290
Nothing -> throwing _TypeError (TypeMismatch ann (void scrut) expectedSop vScrutTy)
291+
TyBuiltin _ someUni -> case annotateCaseBuiltin someUni branches of
292+
Right branchesAndArgTypes -> for_ branchesAndArgTypes $ \(c, argTypes) ->
293+
-- made of sub-parts of a normalized type, so normalized
294+
checkTypeM ann c (Normalized $ mkIterTyFun () argTypes (unNormalized vResTy))
295+
Left () -> undefined
290296
-- scrutinee does not have a SOP type at all
291297
_ -> throwing _TypeError (TypeMismatch ann (void scrut) expectedSop vScrutTy)
292298

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Evaluation/Machine/Cek.hs‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ A wrapper around the internal runCek to debruijn input and undebruijn output.
6767
*THIS FUNCTION IS PARTIAL if the input term contains free variables*
6868
-}
6969
runCek
70-
:: ThrowableBuiltins uni fun
70+
:: (ThrowableBuiltins uni fun, CaseBuiltin (NTerm uni fun ann) uni)
7171
=> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
7272
-> ExBudgetMode cost uni fun
7373
-> EmitterMode uni fun
@@ -78,7 +78,7 @@ runCek = Common.runCek runCekDeBruijn
7878
-- | Evaluate a term using the CEK machine with logging disabled and keep track of costing.
7979
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
8080
runCekNoEmit
81-
:: ThrowableBuiltins uni fun
81+
:: (ThrowableBuiltins uni fun, CaseBuiltin (NTerm uni fun ann) uni)
8282
=> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
8383
-> ExBudgetMode cost uni fun
8484
-> Term Name uni fun ann
@@ -88,7 +88,7 @@ runCekNoEmit = Common.runCekNoEmit runCekDeBruijn
8888
-- | Evaluate a term using the CEK machine with logging enabled.
8989
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
9090
evaluateCek
91-
:: ThrowableBuiltins uni fun
91+
:: (ThrowableBuiltins uni fun, CaseBuiltin (NTerm uni fun ann) uni)
9292
=> EmitterMode uni fun
9393
-> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
9494
-> Term Name uni fun ann
@@ -98,7 +98,7 @@ evaluateCek = Common.evaluateCek runCekDeBruijn
9898
-- | Evaluate a term using the CEK machine with logging disabled.
9999
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
100100
evaluateCekNoEmit
101-
:: ThrowableBuiltins uni fun
101+
:: (ThrowableBuiltins uni fun, CaseBuiltin (NTerm uni fun ann) uni)
102102
=> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
103103
-> Term Name uni fun ann
104104
-> Either (CekEvaluationException Name uni fun) (Term Name uni fun ())
@@ -107,7 +107,9 @@ evaluateCekNoEmit = Common.evaluateCekNoEmit runCekDeBruijn
107107
-- | Unlift a value using the CEK machine.
108108
-- *THIS FUNCTION IS PARTIAL if the input term contains free variables*
109109
readKnownCek
110-
:: (ThrowableBuiltins uni fun, ReadKnown (Term Name uni fun ()) a)
110+
:: ( ThrowableBuiltins uni fun, CaseBuiltin (NTerm uni fun ann) uni
111+
, ReadKnown (Term Name uni fun ()) a
112+
)
111113
=> MachineParameters CekMachineCosts fun (CekValue uni fun ann)
112114
-> Term Name uni fun ann
113115
-> Either (CekEvaluationException Name uni fun) a

0 commit comments

Comments
 (0)