Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[AST] Add 'SixList' #5818

Closed
wants to merge 2 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion plutus-core/plutus-core/src/PlutusCore/Compiler/Erase.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ module PlutusCore.Compiler.Erase (eraseTerm, eraseProgram) where
import PlutusCore.Core
import UntypedPlutusCore.Core qualified as UPLC

import GHC.Exts (fromList)

-- | Erase a Typed Plutus Core term to its untyped counterpart.
eraseTerm :: Term tyname name uni fun ann -> UPLC.Term name uni fun ann
eraseTerm (Var ann name) = UPLC.Var ann name
Expand All @@ -16,7 +18,7 @@ eraseTerm (Unwrap _ term) = eraseTerm term
eraseTerm (IWrap _ _ _ term) = eraseTerm term
eraseTerm (Error ann _) = UPLC.Error ann
eraseTerm (Constr ann _ i args) = UPLC.Constr ann i (fmap eraseTerm args)
eraseTerm (Case ann _ arg cs) = UPLC.Case ann (eraseTerm arg) (fmap eraseTerm cs)
eraseTerm (Case ann _ arg cs) = UPLC.Case ann (eraseTerm arg) (fromList $ fmap eraseTerm cs)

eraseProgram :: Program tyname name uni fun ann -> UPLC.Program name uni fun ann
eraseProgram (Program a v t) = UPLC.Program a v $ eraseTerm t
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
Expand Down Expand Up @@ -100,7 +101,7 @@ eqTermM (Constr ann1 i1 args1) (Constr ann2 i2 args2) = do
eqTermM (Case ann1 a1 cs1) (Case ann2 a2 cs2) = do
eqM ann1 ann2
eqTermM a1 a2
case zipExact cs1 cs2 of
case zipExact (toList cs1) (toList cs2) of
Just ps -> for_ ps $ \(t1, t2) -> eqTermM t1 t2
Nothing -> empty
eqTermM Constant{} _ = empty
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ import Data.Word (Word8)
import Flat
import Flat.Decoder
import Flat.Encoder
import GHC.Exts (fromList, toList)
import Prettyprinter
import Universe

Expand Down Expand Up @@ -128,7 +129,7 @@ encodeTerm = \case
Error ann -> encodeTermTag 6 <> encode ann
Builtin ann bn -> encodeTermTag 7 <> encode ann <> encode bn
Constr ann i es -> encodeTermTag 8 <> encode ann <> encode i <> encodeListWith encodeTerm es
Case ann arg cs -> encodeTermTag 9 <> encode ann <> encodeTerm arg <> encodeListWith encodeTerm cs
Case ann arg cs -> encodeTermTag 9 <> encode ann <> encodeTerm arg <> encodeListWith encodeTerm (toList cs)

decodeTerm
:: forall name uni fun ann
Expand Down Expand Up @@ -165,7 +166,7 @@ decodeTerm version builtinPred = go
Constr <$> decode <*> decode <*> decodeListWith go
handleTerm 9 = do
unless (version >= PLC.plcVersion110) $ fail $ "'case' is not allowed before version 1.1.0, this program has version: " ++ (show $ pretty version)
Case <$> decode <*> go <*> decodeListWith go
Case <$> decode <*> go <*> (fromList <$> decodeListWith go)
handleTerm t = fail $ "Unknown term constructor tag: " ++ show t

sizeTerm
Expand Down Expand Up @@ -193,7 +194,7 @@ sizeTerm tm sz =
Error ann -> size ann sz'
Builtin ann bn -> size ann $ size bn sz'
Constr ann i es -> size ann $ size i $ sizeListWith sizeTerm es sz'
Case ann arg cs -> size ann $ sizeTerm arg $ sizeListWith sizeTerm cs sz'
Case ann arg cs -> size ann $ sizeTerm arg $ sizeListWith sizeTerm (toList cs) sz'

-- | An encoder for programs.
--
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,8 @@ instance (PrettyClassicBy configName name, PrettyUni uni, Pretty fun, Pretty ann
Constr ann i es ->
sexp "constr" (consAnnIf config ann (pretty i : fmap (prettyBy config) es))
Case ann arg cs ->
sexp "case" (consAnnIf config ann (prettyBy config arg : fmap (prettyBy config) cs))
sexp "case" . consAnnIf config ann $
prettyBy config arg : fmap (prettyBy config) (toList cs)
where
prettyTypeOf :: Some (ValueOf uni) -> Doc dann
prettyTypeOf (Some (ValueOf uni _ )) = prettyBy juxtRenderContext $ SomeTypeIn uni
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ instance
-- Always rendering the tag on the same line for more compact output, it's just a tiny integer
-- anyway.
Constr _ i es -> iterAppDocM $ \_ prettyArg -> ("constr" <+> prettyArg i) :| [prettyArg es]
Case _ arg cs -> iterAppDocM $ \_ prettyArg -> "case" :| [prettyArg arg, prettyArg cs]
Case _ arg cs -> iterAppDocM $ \_ prettyArg -> "case" :| [prettyArg arg, prettyArg (toList cs)]

instance
(PrettyReadableBy configName (Term name uni fun a)) =>
Expand Down
131 changes: 129 additions & 2 deletions plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Core/Type.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
-- editorconfig-checker-disable-file
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
Expand All @@ -13,6 +15,8 @@ module UntypedPlutusCore.Core.Type
, TPLC.Binder (..)
, Term (..)
, Program (..)
, SixList (..)
, lookupSixList
, progAnn
, progVer
, progTerm
Expand All @@ -28,7 +32,9 @@ module UntypedPlutusCore.Core.Type
import Control.Lens
import PlutusPrelude

import Data.Hashable
import Data.Word
import GHC.Exts as Exts (IsList (..), inline)
import PlutusCore.Builtin qualified as TPLC
import PlutusCore.Core qualified as TPLC
import PlutusCore.MkPlc
Expand Down Expand Up @@ -85,9 +91,130 @@ data Term name uni fun ann
-- TODO: try spine-strict list or strict list or vector
-- See Note [Constr tag type]
| Constr !ann !Word64 ![Term name uni fun ann]
| Case !ann !(Term name uni fun ann) ![Term name uni fun ann]
| Case !ann !(Term name uni fun ann) !(SixList (Term name uni fun ann))
deriving stock (Functor, Generic)

data SixList a
= SixList0
| SixList1 !a
| SixList2 !a !a
| SixList3 !a !a !a
| SixList4 !a !a !a !a
| SixList5 !a !a !a !a !a
| SixList6 !a !a !a !a !a !a
| SixList7 !a !a !a !a !a !a !a
| SixList8 !a !a !a !a !a !a !a !a
| SixList9 !a !a !a !a !a !a !a !a !a
| SixList10 !a !a !a !a !a !a !a !a !a !a
| SixList11 !a !a !a !a !a !a !a !a !a !a !a
| SixList12 !a !a !a !a !a !a !a !a !a !a !a !a
| SixList13 !a !a !a !a !a !a !a !a !a !a !a !a !a
| SixList14 !a !a !a !a !a !a !a !a !a !a !a !a !a !a (SixList a)
deriving stock (Show, Eq, Functor, Foldable, Traversable, Generic)
deriving anyclass (NFData, Hashable)

instance IsList (SixList a) where
type Item (SixList a) = a

fromList [] = SixList0
fromList [x0] = SixList1 x0
fromList [x0, x1] = SixList2 x0 x1
fromList [x0, x1, x2] = SixList3 x0 x1 x2
fromList [x0, x1, x2, x3] = SixList4 x0 x1 x2 x3
fromList [x0, x1, x2, x3, x4] = SixList5 x0 x1 x2 x3 x4
fromList [x0, x1, x2, x3, x4, x5] = SixList6 x0 x1 x2 x3 x4 x5
fromList [x0, x1, x2, x3, x4, x5, x6] = SixList7 x0 x1 x2 x3 x4 x5 x6
fromList [x0, x1, x2, x3, x4, x5, x6, x7] = SixList8 x0 x1 x2 x3 x4 x5 x6 x7
fromList [x0, x1, x2, x3, x4, x5, x6, x7, x8] = SixList9 x0 x1 x2 x3 x4 x5 x6 x7 x8
fromList [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9] = SixList10 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
fromList [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] = SixList11 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10
fromList [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] = SixList12 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11
fromList [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] = SixList13 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
fromList (x0:x1:x2:x3:x4:x5:x6:x7:x8:x9:x10:x11:x12:x13:xs) = SixList14 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 (fromList xs)

toList !xs0 = goStep xs0 where
goStep :: SixList a -> [a]
goStep SixList0 = []
goStep (SixList1 x0) = [x0]
goStep (SixList2 x0 x1) = [x0, x1]
goStep (SixList3 x0 x1 x2) = [x0, x1, x2]
goStep (SixList4 x0 x1 x2 x3) = [x0, x1, x2, x3]
goStep (SixList5 x0 x1 x2 x3 x4) = [x0, x1, x2, x3, x4]
goStep (SixList6 x0 x1 x2 x3 x4 x5) = [x0, x1, x2, x3, x4, x5]
goStep (SixList7 x0 x1 x2 x3 x4 x5 x6) = [x0, x1, x2, x3, x4, x5, x6]
goStep (SixList8 x0 x1 x2 x3 x4 x5 x6 x7) = [x0, x1, x2, x3, x4, x5, x6, x7]
goStep (SixList9 x0 x1 x2 x3 x4 x5 x6 x7 x8) = [x0, x1, x2, x3, x4, x5, x6, x7, x8]
goStep (SixList10 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9) = [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9]
goStep (SixList11 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10) = [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10]
goStep (SixList12 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11) = [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11]
goStep (SixList13 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) = [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12]
goStep (SixList14 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 xs) = x0 : x1 : x2 : x3 : x4 : x5 : x6 : x7 : x8 : x9 : x10 : x11 : x12 : x13 : goRec xs
{-# INLINE goStep #-}

goRec :: SixList a -> [a]
goRec !xs = goStep xs
{-# NOINLINE goRec #-}
{-# INLINE toList #-}

-- >>> import GHC.IsList (fromList)
-- >>> import Data.Maybe
-- >>> mapMaybe (\i -> lookupSixList i $ fromList [0..20 :: Int]) [0..20]
-- [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]
lookupSixList :: Word64 -> SixList a -> Maybe a
lookupSixList !i0 = goStep i0 . inline Exts.toList where
goStep :: Word64 -> [a] -> Maybe a
goStep 0 = \case
x:_ -> Just x
_ -> Nothing
goStep 1 = \case
_:x:_ -> Just x
_ -> Nothing
goStep 2 = \case
_:_:x:_ -> Just x
_ -> Nothing
goStep 3 = \case
_:_:_:x:_ -> Just x
_ -> Nothing
goStep 4 = \case
_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 5 = \case
_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 6 = \case
_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 7 = \case
_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 8 = \case
_:_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 9 = \case
_:_:_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 10 = \case
_:_:_:_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 11 = \case
_:_:_:_:_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 12 = \case
_:_:_:_:_:_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep 13 = \case
_:_:_:_:_:_:_:_:_:_:_:_:_:x:_ -> Just x
_ -> Nothing
goStep i = \case
_:_:_:_:_:_:_:_:_:_:_:_:_:_:xs -> goRec (i - 14) xs
_ -> Nothing
{-# INLINE goStep #-}

goRec :: Word64 -> [a] -> Maybe a
goRec !i = goStep i
{-# NOINLINE goRec #-}
{-# INLINE lookupSixList #-}

deriving stock instance (Show name, GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
=> Show (Term name uni fun ann)

Expand Down Expand Up @@ -123,7 +250,7 @@ instance TermLike (Term name uni fun) TPLC.TyName name uni fun where
iWrap = \_ _ _ -> id
error = \ann _ -> Error ann
constr = \ann _ i es -> Constr ann i es
kase = \ann _ arg cs -> Case ann arg cs
kase = \ann _ arg cs -> Case ann arg $ fromList cs

instance TPLC.HasConstant (Term name uni fun ()) where
asConstant (Constant _ val) = pure val
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,6 @@ import UntypedPlutusCore.Evaluation.Machine.Cek.CekMachineCosts (CekMachineCosts
CekMachineCostsBase (..))
import UntypedPlutusCore.Evaluation.Machine.Cek.StepCounter

import Control.Lens ((^?))
import Control.Lens.Review
import Control.Monad (unless, when)
import Control.Monad.Catch
Expand All @@ -97,7 +96,6 @@ import Data.DList qualified as DList
import Data.Functor.Identity
import Data.Hashable (Hashable)
import Data.Kind qualified as GHC
import Data.List.Extras (wix)
import Data.Proxy
import Data.Semigroup (stimes)
import Data.Text (Text)
Expand Down Expand Up @@ -574,7 +572,7 @@ data Context uni fun ann
-- See Note [Accumulators for terms]
| FrameConstr !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
-- ^ @(constr i V0 ... Vj-1 _ Nj ... Nn)@
| FrameCases !(CekValEnv uni fun ann) ![NTerm uni fun ann] !(Context uni fun ann)
| FrameCases !(CekValEnv uni fun ann) !(SixList (NTerm uni fun ann)) !(Context uni fun ann)
-- ^ @(case _ C0 .. Cn)@
| NoFrame

Expand Down Expand Up @@ -768,7 +766,7 @@ enterComputeCek = computeCek
_ -> returnCek ctx $ VConstr i done'
-- s , case _ (C0 ... CN, ρ) ◅ constr i V1 .. Vm ↦ s , [_ V1 ... Vm] ; ρ ▻ Ci
returnCek (FrameCases env cs ctx) e = case e of
(VConstr i args) -> case cs ^? wix i of
(VConstr i args) -> case lookupSixList i cs of
Just t -> computeCek (transferArgStack args ctx) env t
Nothing -> throwingDischarged _MachineError (MissingCaseBranch i) e
_ -> throwingDischarged _MachineError NonConstrScrutinized e
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ import UntypedPlutusCore.Evaluation.Machine.Cek.StepCounter

import Control.Lens hiding (Context)
import Control.Monad
import Data.List.Extras (wix)
import Data.Proxy
import Data.RandomAccessList.Class qualified as Env
import Data.Semigroup (stimes)
Expand Down Expand Up @@ -99,7 +98,7 @@ data Context uni fun ann
| FrameAwaitFunValue ann !(CekValue uni fun ann) !(Context uni fun ann)
| FrameForce ann !(Context uni fun ann) -- ^ @(force _)@
| FrameConstr ann !(CekValEnv uni fun ann) {-# UNPACK #-} !Word64 ![NTerm uni fun ann] !(ArgStack uni fun ann) !(Context uni fun ann)
| FrameCases ann !(CekValEnv uni fun ann) ![NTerm uni fun ann] !(Context uni fun ann)
| FrameCases ann !(CekValEnv uni fun ann) !(SixList (NTerm uni fun ann)) !(Context uni fun ann)
| NoFrame

deriving stock instance (GShow uni, Everywhere uni Show, Show fun, Show ann, Closed uni)
Expand Down Expand Up @@ -195,7 +194,7 @@ returnCek (FrameConstr ann env i todo done ctx) e = do
_ -> returnCek ctx $ VConstr i done'
-- s , case _ (C0 ... CN, ρ) ◅ constr i V1 .. Vm ↦ s , [_ V1 ... Vm] ; ρ ▻ Ci
returnCek (FrameCases ann env cs ctx) e = case e of
(VConstr i args) -> case cs ^? wix i of
(VConstr i args) -> case lookupSixList i cs of
Just t ->
let ctx' = transferArgStack ann args ctx
in computeCek ctx' env t
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ import UntypedPlutusCore.Core.Type qualified as UPLC
import UntypedPlutusCore.Rename (Rename (rename))

import Data.Text (Text)
import GHC.Exts (fromList)
import PlutusCore.Error (AsParserErrorBundle)
import PlutusCore.MkPlc (mkIterApp)
import PlutusCore.Parser hiding (parseProgram, parseTerm, program)
Expand Down Expand Up @@ -81,7 +82,7 @@ constrTerm = withSpan $ \sp ->
caseTerm :: Parser PTerm
caseTerm = withSpan $ \sp ->
inParens $ do
res <- UPLC.Case sp <$> (symbol "case" *> term) <*> many term
res <- UPLC.Case sp <$> (symbol "case" *> term) <*> (fromList <$> many term)
whenVersion (\v -> v < plcVersion110) $ fail "'case' is not allowed before version 1.1.0"
pure res

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,12 @@ import UntypedPlutusCore.Core

import Control.Lens (transformOf, (^?))
import Data.List.Extras
import GHC.Exts (toList)

caseReduce :: Term name uni fun a -> Term name uni fun a
caseReduce = transformOf termSubterms processTerm

processTerm :: Term name uni fun a -> Term name uni fun a
processTerm = \case
Case ann (Constr _ i args) cs | Just c <- cs ^? wix i -> mkIterApp c ((ann,) <$> args)
t -> t
Case ann (Constr _ i args) cs | Just c <- toList cs ^? wix i -> mkIterApp c ((ann,) <$> args)
t -> t
6 changes: 3 additions & 3 deletions plutus-metatheory/src/Untyped.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ import UntypedPlutusCore
import Data.ByteString as BS hiding (map)
import Data.Text as T hiding (map)
import Data.Word (Word64)
import GHC.Exts (IsList (..))
import Universe

-- Untyped (Raw) syntax
Expand Down Expand Up @@ -42,7 +43,7 @@ conv (Error _) = UError
conv (Delay _ t) = UDelay (conv t)
conv (Force _ t) = UForce (conv t)
conv (Constr _ i es) = UConstr (toInteger i) (fmap conv es)
conv (Case _ arg cs) = UCase (conv arg) (fmap conv cs)
conv (Case _ arg cs) = UCase (conv arg) (toList (fmap conv cs))

tmnames = ['a' .. 'z']

Expand All @@ -63,5 +64,4 @@ uconv i (UBuiltin b) = Builtin () b
uconv i (UDelay t) = Delay () (uconv i t)
uconv i (UForce t) = Force () (uconv i t)
uconv i (UConstr j xs) = Constr () (fromInteger j) (fmap (uconv i) xs)
uconv i (UCase t xs) = Case () (uconv i t) (fmap (uconv i) xs)

uconv i (UCase t xs) = Case () (uconv i t) (fromList (fmap (uconv i) xs))