Skip to content

Commit

Permalink
WIP multilambda
Browse files Browse the repository at this point in the history
  • Loading branch information
@michaelpj
michaelpj committed Nov 24, 2022
1 parent 4bcc13c commit 5fa97f4
Show file tree
Hide file tree
Showing 179 changed files with 6,079 additions and 6,266 deletions.
9 changes: 5 additions & 4 deletions plutus-benchmark/lists/src/PlutusBenchmark/Lists/Sum/HandWritten.hs
View file
Expand Up @@ -8,6 +8,7 @@ import PlutusBenchmark.Common (Term, compiledCodeToTerm)
import Control.Monad.Except
import Data.Either
import PlutusCore.Compiler.Erase (eraseTerm)
import PlutusCore.MkPlc qualified as PLC
import PlutusCore.StdLib.Data.List qualified as BuiltinList
import PlutusCore.StdLib.Data.ScottList qualified as ScottList
import PlutusTx qualified as Tx
Expand All @@ -21,19 +22,19 @@ mkBuiltinList :: [Integer] -> Term
mkBuiltinList l = compiledCodeToTerm (Tx.liftCode $ BI.BuiltinList l)

mkSumLeftBuiltinTerm :: [Integer] -> Term
mkSumLeftBuiltinTerm l = UPLC.Apply () (debruijnTermUnsafe $ eraseTerm BuiltinList.sum) (mkBuiltinList l)
mkSumLeftBuiltinTerm l = PLC.apply () (debruijnTermUnsafe $ eraseTerm BuiltinList.sum) (mkBuiltinList l)

mkSumRightBuiltinTerm :: [Integer] -> Term
mkSumRightBuiltinTerm l = UPLC.Apply () (debruijnTermUnsafe $ eraseTerm BuiltinList.sumr) (mkBuiltinList l)
mkSumRightBuiltinTerm l = PLC.apply () (debruijnTermUnsafe $ eraseTerm BuiltinList.sumr) (mkBuiltinList l)

mkScottList :: [Integer] -> Term
mkScottList l = compiledCodeToTerm (Tx.liftCode l)

mkSumLeftScottTerm :: [Integer] -> Term
mkSumLeftScottTerm l = UPLC.Apply () (debruijnTermUnsafe $ eraseTerm ScottList.sum) (mkScottList l)
mkSumLeftScottTerm l = PLC.apply () (debruijnTermUnsafe $ eraseTerm ScottList.sum) (mkScottList l)

mkSumRightScottTerm :: [Integer] -> Term
mkSumRightScottTerm l = UPLC.Apply () (debruijnTermUnsafe $ eraseTerm ScottList.sumr) (mkScottList l)
mkSumRightScottTerm l = PLC.apply () (debruijnTermUnsafe $ eraseTerm ScottList.sumr) (mkScottList l)


debruijnTermUnsafe :: UPLC.Term UPLC.Name uni fun ann
Expand Down
6,105 changes: 3,042 additions & 3,063 deletions plutus-benchmark/nofib/test/formula-uplc.plc.golden
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions plutus-benchmark/nofib/test/formulaBudget.budget.golden
View file
@@ -1,3 +1,3 @@
({ cpu: 22297635908
| mem: 95415448
({ cpu: 23196958908
| mem: 99325548
})
4 changes: 2 additions & 2 deletions plutus-benchmark/nofib/test/knightsBudget.budget.golden
View file
@@ -1,3 +1,3 @@
({ cpu: 5028042298
| mem: 17435640
({ cpu: 5435326298
| mem: 19206440
})
4 changes: 2 additions & 2 deletions plutus-benchmark/nofib/test/queens4budget.budget.golden
View file
@@ -1,3 +1,3 @@
({ cpu: 10372034305
| mem: 38206742
({ cpu: 10873411305
| mem: 40386642
})
640 changes: 316 additions & 324 deletions plutus-benchmark/nofib/test/queens5-uplc.plc.golden
View file

Large diffs are not rendered by default.

640 changes: 316 additions & 324 deletions plutus-benchmark/nofib/test/queens5.plc.golden
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions plutus-benchmark/nofib/test/queens5budget.budget.golden
View file
@@ -1,3 +1,3 @@
({ cpu: 139818252648
| mem: 500626580
({ cpu: 146485837648
| mem: 529616080
})
2 changes: 1 addition & 1 deletion plutus-core/executables/Common.hs
View file
Expand Up @@ -192,7 +192,7 @@ printBudgetStateTally term model (Cek.CekExTally costs) = do
putStrLn ""
putStrLn $ "startup " ++ pbudget Cek.BStartup
putStrLn $ "compute " ++ printf "%-20s" (budgetToString totalComputeCost)
putStrLn $ "AST nodes " ++ printf "%15d" (UPLC.termSize term)
putStrLn $ "AST nodes " ++ printf "%15d" (toInteger $ UPLC.termSize term)
putStrLn ""
putStrLn $ "BuiltinApp " ++ budgetToString builtinCosts
case model of
Expand Down
3 changes: 1 addition & 2 deletions plutus-core/plutus-core.cabal
View file
Expand Up @@ -6,8 +6,6 @@ license-files:
LICENSE
NOTICE

maintainer: michael.peyton-jones@iohk.io
author: Plutus Core Team
synopsis: Language library for Plutus Core
description: Pretty-printer, parser, and typechecker for Plutus Core.
category: Language, Plutus
Expand Down Expand Up @@ -311,6 +309,7 @@ library
, monoidal-containers
, mtl
, multiset
, nonempty-vector
, nothunks >=0.1.1
, parser-combinators >=0.4.0
, prettyprinter >=1.1.0.1
Expand Down
38 changes: 19 additions & 19 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Data/InterList.hs
View file
Expand Up @@ -68,8 +68,8 @@ interNil = runQuote $ do
. TyAbs () b (Type ())
. wrapInterList [TyVar () a, TyVar () b]
. TyAbs () r (Type ())
. LamAbs () z (TyVar () r)
. LamAbs () f (mkIterTyFun () [TyVar () a, TyVar () b, interlistBA] $ TyVar () r)
. lamAbs () z (TyVar () r)
. lamAbs () f (mkIterTyFun () [TyVar () a, TyVar () b, interlistBA] $ TyVar () r)
$ Var () z

interCons :: Term TyName Name uni fun ()
Expand All @@ -87,13 +87,13 @@ interCons = runQuote $ do
return
. TyAbs () a (Type ())
. TyAbs () b (Type ())
. LamAbs () x (TyVar () a)
. LamAbs () y (TyVar () b)
. LamAbs () xs interlistBA
. lamAbs () x (TyVar () a)
. lamAbs () y (TyVar () b)
. lamAbs () xs interlistBA
. wrapInterList [TyVar () a, TyVar () b]
. TyAbs () r (Type ())
. LamAbs () z (TyVar () r)
. LamAbs () f (mkIterTyFun () [TyVar () a, TyVar () b, interlistBA] $ TyVar () r)
. lamAbs () z (TyVar () r)
. lamAbs () f (mkIterTyFun () [TyVar () a, TyVar () b, interlistBA] $ TyVar () r)
$ mkIterApp () (Var () f)
[ Var () x
, Var () y
Expand Down Expand Up @@ -129,32 +129,32 @@ foldrInterList = runQuote $ do
$ TyVar () r
instedFix = mkIterInst () fix [unit, fixTyArg2]
unwrappedXs = TyInst () (Unwrap () (Var () xs)) $ TyVar () r
instedRec = mkIterInst () (Apply () (Var () rec) unitval) [TyVar () b, TyVar () a]
instedRec = mkIterInst () (apply () (Var () rec) unitval) [TyVar () b, TyVar () a]
return
. TyAbs () a0 (Type ())
. TyAbs () b0 (Type ())
. TyAbs () r (Type ())
. LamAbs () f (fTy a0 b0)
. LamAbs () z (TyVar () r)
. lamAbs () f (fTy a0 b0)
. lamAbs () z (TyVar () r)
$ mkIterInst ()
( mkIterApp () instedFix
[ LamAbs () rec (TyFun () unit fixTyArg2)
. LamAbs () u unit
[ lamAbs () rec (TyFun () unit fixTyArg2)
. lamAbs () u unit
. TyAbs () a (Type ())
. TyAbs () b (Type ())
. LamAbs () f' (fTy a b)
. LamAbs () xs (interlistOf a b)
. lamAbs () f' (fTy a b)
. lamAbs () xs (interlistOf a b)
$ mkIterApp () unwrappedXs
[ Var () z
, LamAbs () x (TyVar () a)
. LamAbs () y (TyVar () b)
. LamAbs () xs' (interlistOf b a)
, lamAbs () x (TyVar () a)
. lamAbs () y (TyVar () b)
. lamAbs () xs' (interlistOf b a)
$ mkIterApp () (Var () f')
[ Var () x
, Var () y
, mkIterApp () instedRec
[ LamAbs () y' (TyVar () b)
. LamAbs () x' (TyVar () a)
[ lamAbs () y' (TyVar () b)
. lamAbs () x' (TyVar () a)
$ mkIterApp () (Var () f')
[ Var () x'
, Var () y'
Expand Down
8 changes: 4 additions & 4 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Data/Shad.hs
View file
Expand Up @@ -72,9 +72,9 @@ mkShad = runQuote $ do
return
. TyAbs () a (Type ())
. IWrap () shadF (TyVar () a)
. LamAbs () x (TyVar () a)
. lamAbs () x (TyVar () a)
. TyAbs () f (KindArrow () (Type ()) $ Type ())
. LamAbs () y (TyApp () (TyVar () f) $ TyVar () a)
. lamAbs () y (TyApp () (TyVar () f) $ TyVar () a)
$ mkConstant @Integer () 0

-- |
Expand Down Expand Up @@ -123,6 +123,6 @@ runRecUnit = runQuote $ do
ru <- freshName "ru"
return
. TyAbs () a (Type ())
. LamAbs () ru recUnit
. Apply () (TyInst () (Unwrap () $ Var () ru) $ TyVar () a)
. lamAbs () ru recUnit
. apply () (TyInst () (Unwrap () $ Var () ru) $ TyVar () a)
$ Var () ru
18 changes: 9 additions & 9 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Data/TreeForest.hs
View file
Expand Up @@ -183,11 +183,11 @@ treeNode = runQuote $ normalizeTypesIn =<< do
Normalized forestA <- normalizeType $ TyApp () forest vA
return
. TyAbs () a (Type ())
. LamAbs () x vA
. LamAbs () fr forestA
. lamAbs () x vA
. lamAbs () fr forestA
. wrapTree [vA]
. TyAbs () r (Type ())
. LamAbs () f (mkIterTyFun () [vA, forestA] vR)
. lamAbs () f (mkIterTyFun () [vA, forestA] vR)
$ mkIterApp () (Var () f)
[ Var () x
, Var () fr
Expand All @@ -213,8 +213,8 @@ forestNil = runQuote $ normalizeTypesIn =<< do
. TyAbs () a (Type ())
. wrapForest [vA]
. TyAbs () r (Type ())
. LamAbs () z vR
. LamAbs () f (mkIterTyFun () [treeA, forestA] vR)
. lamAbs () z vR
. lamAbs () f (mkIterTyFun () [treeA, forestA] vR)
$ Var () z

-- |
Expand All @@ -237,12 +237,12 @@ forestCons = runQuote $ normalizeTypesIn =<< do
Normalized forestA <- normalizeType $ TyApp () forest vA
return
. TyAbs () a (Type ())
. LamAbs () tr treeA
. LamAbs () fr forestA
. lamAbs () tr treeA
. lamAbs () fr forestA
. wrapForest [vA]
. TyAbs () r (Type ())
. LamAbs () z vR
. LamAbs () f (mkIterTyFun () [treeA, forestA] vR)
. lamAbs () z vR
. lamAbs () f (mkIterTyFun () [treeA, forestA] vR)
$ mkIterApp () (Var () f)
[ Var () tr
, Var () fr
Expand Down
56 changes: 28 additions & 28 deletions plutus-core/plutus-core/examples/PlutusCore/Examples/Data/Vec.hs
View file
Expand Up @@ -146,8 +146,8 @@ churchNil = runQuote $ do
return
. TyAbs () a (Type ())
. TyAbs () r (KindArrow () natK $ Type ())
. LamAbs () f stepFun
. LamAbs () z (TyApp () (TyVar () r) zeroT)
. lamAbs () f stepFun
. lamAbs () z (TyApp () (TyVar () r) zeroT)
$ Var () z

-- |
Expand All @@ -169,11 +169,11 @@ churchCons = runQuote $ do
return
. TyAbs () a (Type ())
. TyAbs () n natK
. LamAbs () x (TyVar () a)
. LamAbs () xs (mkIterTyApp () churchVec [TyVar () a, TyVar () n])
. lamAbs () x (TyVar () a)
. lamAbs () xs (mkIterTyApp () churchVec [TyVar () a, TyVar () n])
. TyAbs () r (KindArrow () natK $ Type ())
. LamAbs () f stepFun
. LamAbs () z (TyApp () (TyVar () r) zeroT)
. lamAbs () f stepFun
. lamAbs () z (TyApp () (TyVar () r) zeroT)
$ mkIterApp () (TyInst () (Var () f) $ TyVar () n)
[ Var () x
, mkIterApp () (TyInst () (Var () xs) $ TyVar () r)
Expand Down Expand Up @@ -209,11 +209,11 @@ churchConcat = runQuote $ do
. TyAbs () a (Type ())
. TyAbs () n natK
. TyAbs () m natK
. LamAbs () xs (mkIterTyApp () churchVec [TyVar () a, TyVar () n])
. LamAbs () ys (mkIterTyApp () churchVec [TyVar () a, mEta])
. lamAbs () xs (mkIterTyApp () churchVec [TyVar () a, TyVar () n])
. lamAbs () ys (mkIterTyApp () churchVec [TyVar () a, mEta])
. TyAbs () r (KindArrow () natK $ Type ())
. LamAbs () f stepFun
. LamAbs () z (TyApp () (TyVar () r) zeroT)
. lamAbs () f stepFun
. lamAbs () z (TyApp () (TyVar () r) zeroT)
$ mkIterApp () (TyInst () (Var () xs) . TyLam () p natK $ TyApp () (TyVar () r) plusTPM)
[ TyAbs () p natK $ TyInst () (Var () f) plusTPM
, mkIterApp () (TyInst () (Var () ys) $ TyVar () r)
Expand Down Expand Up @@ -276,8 +276,8 @@ scottNil = runQuote $ do
. TyAbs () a (Type ())
. IWrap () (TyApp () scottVecF $ TyVar () a) zeroT
. TyAbs () r (KindArrow () natK $ Type ())
. LamAbs () f stepFun
. LamAbs () z (TyApp () (TyVar () r) zeroT)
. lamAbs () f stepFun
. lamAbs () z (TyApp () (TyVar () r) zeroT)
$ Var () z

-- |
Expand All @@ -301,12 +301,12 @@ scottCons = runQuote $ do
return
. TyAbs () a (Type ())
. TyAbs () n natK
. LamAbs () x (TyVar () a)
. LamAbs () xs (mkIterTyApp () scottVec [TyVar () a, TyVar () n])
. lamAbs () x (TyVar () a)
. lamAbs () xs (mkIterTyApp () scottVec [TyVar () a, TyVar () n])
. IWrap () (TyApp () scottVecF $ TyVar () a) (TyApp () succT $ TyVar () n)
. TyAbs () r (KindArrow () natK $ Type ())
. LamAbs () f stepFun
. LamAbs () z (TyApp () (TyVar () r) zeroT)
. lamAbs () f stepFun
. lamAbs () z (TyApp () (TyVar () r) zeroT)
$ mkIterApp () (TyInst () (Var () f) $ TyVar () n)
[ Var () x
, Var () xs
Expand All @@ -333,7 +333,7 @@ scottHead = runQuote $ do
return
. TyAbs () a (Type ())
. TyAbs () n natK
. LamAbs () xs (mkIterTyApp () scottVec [TyVar () a, TyApp () succT $ TyVar () n])
. lamAbs () xs (mkIterTyApp () scottVec [TyVar () a, TyApp () succT $ TyVar () n])
$ mkIterApp ()
( TyInst () (Unwrap () $ Var () xs)
. TyLam () p natK
Expand All @@ -342,8 +342,8 @@ scottHead = runQuote $ do
, unit
])
[ TyAbs () p natK
. LamAbs () x (TyVar () a)
. LamAbs () xs' (mkIterTyApp () scottVec [TyVar () a, TyVar () p])
. lamAbs () x (TyVar () a)
. lamAbs () xs' (mkIterTyApp () scottVec [TyVar () a, TyVar () p])
$ Var () x
, unitval
]
Expand Down Expand Up @@ -374,26 +374,26 @@ scottSumHeadsOr0 = runQuote $ do
let vecInteger l = mkIterTyApp () scottVec [integer, l]
return
. TyAbs () n natK
. LamAbs () xs (vecInteger $ TyVar () n)
. LamAbs () ys (vecInteger $ TyVar () n)
. lamAbs () xs (vecInteger $ TyVar () n)
. lamAbs () ys (vecInteger $ TyVar () n)
$ mkIterApp ()
( TyInst () (Unwrap () $ Var () xs)
. TyLam () p natK
. TyFun () (TyFun () (vecInteger $ TyVar () n) $ vecInteger (TyVar () p))
$ integer
)
[ TyAbs () p natK
. LamAbs () x integer
. LamAbs () xs' (vecInteger $ TyVar () p)
. LamAbs () coe
. lamAbs () x integer
. lamAbs () xs' (vecInteger $ TyVar () p)
. lamAbs () coe
(TyFun () (vecInteger $ TyVar () n) $ vecInteger (TyApp () succT $ TyVar () p))
$ mkIterApp () (builtin () AddInteger)
[ Var () x
, Apply () (mkIterInst () scottHead [integer, TyVar () p])
. Apply () (Var () coe)
, apply () (mkIterInst () scottHead [integer, TyVar () p])
. apply () (Var () coe)
$ Var () ys
]
, LamAbs () coe (TyFun () (vecInteger $ TyVar () n) $ vecInteger zeroT)
, lamAbs () coe (TyFun () (vecInteger $ TyVar () n) $ vecInteger zeroT)
$ mkConstant @Integer () 0
, LamAbs () xs' (vecInteger $ TyVar () n) $ Var () xs'
, lamAbs () xs' (vecInteger $ TyVar () n) $ Var () xs'
]
3 changes: 2 additions & 1 deletion plutus-core/plutus-core/src/PlutusCore.hs
View file
Expand Up @@ -118,6 +118,7 @@ module PlutusCore
, typeSize
, kindSize
, programSize
, Size (..)
, serialisedSize
) where

Expand Down Expand Up @@ -147,4 +148,4 @@ applyProgram
-- TODO: 'mappend' annotations, ignore versions and return the default one (whatever that means),
-- what a mess. Needs to be fixed.
applyProgram (Program a1 _ t1) (Program a2 _ t2) =
Program (a1 <> a2) (defaultVersion mempty) (Apply mempty t1 t2)
Program (a1 <> a2) (defaultVersion mempty) (Apply mempty t1 (pure t2))
4 changes: 3 additions & 1 deletion plutus-core/plutus-core/src/PlutusCore/Analysis/Definitions.hs
View file
Expand Up @@ -138,7 +138,9 @@ termDefs
-> m ()
termDefs = cata $ \case
VarF ann n -> addUsage n ann TermScope
LamAbsF ann n ty t -> addDef n ann TermScope >> typeDefs ty >> t
LamAbsF ann vars t -> do
for_ vars $ \(n, ty) -> addDef n ann TermScope >> typeDefs ty
t
IWrapF _ pat arg t -> typeDefs pat >> typeDefs arg >> t
TyAbsF ann tn _ t -> addDef tn ann TypeScope >> t
TyInstF _ t ty -> t >> typeDefs ty
Expand Down
6 changes: 3 additions & 3 deletions plutus-core/plutus-core/src/PlutusCore/Check/Normal.hs
View file
Expand Up @@ -16,7 +16,7 @@ import PlutusCore.Core
import PlutusCore.Error

import Control.Monad.Except
import Data.Foldable (traverse_)
import Data.Foldable (for_, traverse_)

-- | Ensure that all types in the 'Program' are normalized.
checkProgram
Expand All @@ -35,8 +35,8 @@ check (Error _ ty) = normalType ty
check (TyInst _ t ty) = check t >> normalType ty
check (IWrap _ pat arg term) = normalType pat >> normalType arg >> check term
check (Unwrap _ t) = check t
check (LamAbs _ _ ty t) = normalType ty >> check t
check (Apply _ t1 t2) = check t1 >> check t2
check (LamAbs _ vars t) = for_ vars (\(_, ty) -> normalType ty) >> check t
check (Apply _ f args) = check f >> for_ args check
check (TyAbs _ _ _ t) = check t
check (Constr _ ty _ es) = normalType ty >> traverse_ check es
check (Case _ ty arg cs) = normalType ty >> check arg >> traverse_ check cs
Expand Down

0 comments on commit 5fa97f4

Please sign in to comment.