Skip to content

Commit

Permalink
KnownApps
Browse files Browse the repository at this point in the history
  • Loading branch information
zliu41 committed Mar 16, 2023
1 parent c296a55 commit 68f4b19
Show file tree
Hide file tree
Showing 31 changed files with 977 additions and 29 deletions.
@@ -0,0 +1,2 @@
({cpu: 160559654
| mem: 504532})
2 changes: 2 additions & 0 deletions plutus-benchmark/lists/test/Sum/left-fold-data.budget.golden
@@ -0,0 +1,2 @@
({cpu: 422780685
| mem: 1340362})
2 changes: 2 additions & 0 deletions plutus-benchmark/lists/test/Sum/left-fold-scott.budget.golden
@@ -0,0 +1,2 @@
({cpu: 150781800
| mem: 566100})
@@ -0,0 +1,2 @@
({cpu: 167459654
| mem: 534532})
2 changes: 2 additions & 0 deletions plutus-benchmark/lists/test/Sum/right-fold-data.budget.golden
@@ -0,0 +1,2 @@
({cpu: 429680685
| mem: 1370362})
@@ -0,0 +1,2 @@
({cpu: 157681800
| mem: 596100})
9 changes: 5 additions & 4 deletions plutus-benchmark/nofib/src/PlutusBenchmark/NoFib/Queens.hs
Expand Up @@ -392,8 +392,8 @@ btr seed csp = bt csp . hrandom seed

{-# INLINABLE random2 #-}
random2 :: Integer -> Integer
random2 n = if test > 0 then test else test + 2147483647
where test = 16807 * lo - 2836 * hi
random2 n = if test > 0 then test else test Haskell.+ 2147483647
where test = 16807 Haskell.* lo - 2836 Haskell.* hi
hi = n `Haskell.div` 127773
lo = n `Haskell.rem` 127773

Expand All @@ -403,7 +403,7 @@ randoms k = iterateN k random2

{-# INLINABLE random #-}
random :: Integer -> Integer
random n = (a * n + c) -- mod m
random n = (a Haskell.* n Haskell.+ c) -- mod m
where a = 994108973
c = a

Expand Down Expand Up @@ -435,7 +435,8 @@ cacheChecks csp tbl (Node s cs) =
fillTable :: State -> CSP -> Table -> Table
fillTable [] csp tbl = tbl
fillTable ((var' := val'):as) CSP{vars=vars,vals=vals,rel=rel} tbl =
zipWith (zipWith f) tbl [[(var,val) | val <- interval 1 vals] | var <- interval (var'+1) vars]
zipWith (zipWith f) tbl
[[(var,val) | val <- interval 1 vals] | var <- interval (var' Haskell.+ 1) vars]
where f cs (var,val) = if cs == Unknown && not (rel (var' := val') (var := val)) then
Known [var',var]
else cs
Expand Down
6 changes: 3 additions & 3 deletions plutus-benchmark/nofib/test/Spec.hs
Expand Up @@ -46,7 +46,7 @@ testClausify = testGroup "clausify"
, testCase "formula3" $ mkClausifyTest Clausify.F3
, testCase "formula4" $ mkClausifyTest Clausify.F4
, testCase "formula5" $ mkClausifyTest Clausify.F5
, Tx.fitsInto "formula1 (size)" (Clausify.mkClausifyCode Clausify.F1) 4901
, Tx.fitsInto "formula1 (size)" (Clausify.mkClausifyCode Clausify.F1) 4781
, runTestNested $
Tx.goldenBudget "formulaBudget" $ Clausify.mkClausifyCode Clausify.F1
]
Expand All @@ -65,7 +65,7 @@ testKnights = testGroup "knights" -- Odd sizes call "error" because there are n
, testCase "depth 100, 4x4" $ mkKnightsTest 100 4
, testCase "depth 100, 6x6" $ mkKnightsTest 100 6
, testCase "depth 100, 8x8" $ mkKnightsTest 100 8
, Tx.fitsInto "depth 10, 4x4 (size)" (Knights.mkKnightsCode 10 4) 3516
, Tx.fitsInto "depth 10, 4x4 (size)" (Knights.mkKnightsCode 10 4) 3494
, runTestNested $ Tx.goldenBudget "knightsBudget" $ Knights.mkKnightsCode 10 4
]

Expand Down Expand Up @@ -95,7 +95,7 @@ testQueens = testGroup "queens"
, runTestNested $ Tx.goldenBudget "queens5budget" $
Queens.mkQueensCode 5 Queens.Bt
]
, Tx.fitsInto "Bt (size)" (Queens.mkQueensCode 5 Queens.Bt) 2759
, Tx.fitsInto "Bt (size)" (Queens.mkQueensCode 5 Queens.Bt) 2852
]

---------------- Primes ----------------
Expand Down
2 changes: 2 additions & 0 deletions plutus-benchmark/nofib/test/formulaBudget.budget.golden
@@ -0,0 +1,2 @@
({cpu: 26010640908
| mem: 111558948})
2 changes: 2 additions & 0 deletions plutus-benchmark/nofib/test/knightsBudget.budget.golden
@@ -0,0 +1,2 @@
({cpu: 7378435298
| mem: 27654740})
2 changes: 2 additions & 0 deletions plutus-benchmark/nofib/test/queens4budget.budget.golden
@@ -0,0 +1,2 @@
({cpu: 17033524305
| mem: 67169742})
2 changes: 2 additions & 0 deletions plutus-benchmark/nofib/test/queens5budget.budget.golden
@@ -0,0 +1,2 @@
({cpu: 236999646648
| mem: 923154380})
Expand Up @@ -11,6 +11,7 @@ import PlutusLedgerApi.V1.Value
import PlutusTx qualified as PlutusTx
import PlutusTx.Builtins qualified as PlutusTx
import PlutusTx.Prelude qualified as PlutusTx
import Prelude as Haskell

-- | A very crude deterministic generator for 'ScriptContext's with size
-- approximately proportional to the input integer.
Expand Down Expand Up @@ -53,7 +54,7 @@ checkScriptContext1 d =
let !sc = PlutusTx.unsafeFromBuiltinData d
(ScriptContext txi _) = sc
in
if PlutusTx.length (txInfoOutputs txi) `PlutusTx.modInteger` 2 PlutusTx.== 0
if PlutusTx.length (txInfoOutputs txi) `PlutusTx.modInteger` 2 Haskell.== 0
then ()
else PlutusTx.traceError "Odd number of outputs"

Expand All @@ -74,7 +75,7 @@ checkScriptContext2 d =
-- for now!
in case sc of
!_ ->
if 48*9900 PlutusTx.== (475200 :: Integer)
if 48*9900 Haskell.== (475200 :: Integer)
then ()
else PlutusTx.traceError "Got my sums wrong"

Expand Down Expand Up @@ -119,7 +120,7 @@ mkScriptContextEqualityDataCode sc =
scriptContextEqualityTerm :: ScriptContext -> PlutusTx.BuiltinData -> ()
-- See note [Redundant arguments to equality benchmarks]
scriptContextEqualityTerm sc _ =
if sc PlutusTx.== sc
if sc Haskell.== sc
then ()
else PlutusTx.traceError "The argument is not equal to itself"

Expand Down
@@ -0,0 +1,2 @@
({cpu: 52948597
| mem: 167402})
@@ -0,0 +1,2 @@
({cpu: 460269997
| mem: 1473369})
@@ -0,0 +1,2 @@
({cpu: 133937245
| mem: 431993})
@@ -0,0 +1,2 @@
({cpu: 436044997
| mem: 1387928})
@@ -0,0 +1,2 @@
({cpu: 126999877
| mem: 407384})
@@ -0,0 +1,2 @@
({cpu: 37927100
| mem: 165000})
@@ -0,0 +1,2 @@
({cpu: 841344251
| mem: 3500046})
2 changes: 1 addition & 1 deletion plutus-core/plutus-ir/src/PlutusIR/Compiler/Definitions.hs
Expand Up @@ -12,7 +12,7 @@
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
-- | Support for generating PIR with global definitions with dependencies between them.
module PlutusIR.Compiler.Definitions (DefT
module PlutusIR.Compiler.Definitions (DefT (..)
, MonadDefs (..)
, TermDefWithStrictness
, runDefT
Expand Down
6 changes: 5 additions & 1 deletion plutus-ledger-api/src/PlutusLedgerApi/V1/Contexts.hs
Expand Up @@ -132,7 +132,11 @@ data ScriptContext = ScriptContext
{ scriptContextTxInfo :: TxInfo -- ^ information about the transaction the currently-executing script is included in
, scriptContextPurpose :: ScriptPurpose -- ^ the purpose of the currently-executing script
}
deriving stock (Generic, Haskell.Eq, Haskell.Show)
deriving stock (Generic, Haskell.Show)

instance Haskell.Eq ScriptContext where
{-# INLINABLE (==) #-}
(==) = (==)

instance Eq ScriptContext where
{-# INLINABLE (==) #-}
Expand Down
1 change: 1 addition & 0 deletions plutus-tx-plugin/plutus-tx-plugin.cabal
Expand Up @@ -80,6 +80,7 @@ library
, either
, extra
, flat <0.5
, ghc-prim
, lens
, mtl
, plutus-core:{plutus-core, plutus-ir} ^>=1.3
Expand Down
100 changes: 98 additions & 2 deletions plutus-tx-plugin/src/PlutusTx/Compiler/Expr.hs
Expand Up @@ -39,6 +39,7 @@ import PlutusTx.PIRTypes
import PlutusTx.PLCTypes (PLCType, PLCVar)
-- I feel like we shouldn't need this, we only need it to spot the special String type, which is annoying
import PlutusTx.Builtins.Class qualified as Builtins
import PlutusTx.Builtins.Internal qualified as BI
import PlutusTx.Trace

import PlutusIR qualified as PIR
Expand All @@ -60,11 +61,17 @@ import Data.Array qualified as Array
import Data.ByteString qualified as BS
import Data.List (elemIndex)
import Data.List.NonEmpty qualified as NE
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Data.Text qualified as T
import Data.Text.Encoding qualified as TE
import Data.Traversable
import Data.Tuple.Extra
import GHC.Classes qualified
import GHC.Num qualified
import GHC.Real qualified
import Language.Haskell.TH qualified as TH

{- Note [System FC and System FW]
Haskell uses system FC, which includes type equalities and coercions.
Expand Down Expand Up @@ -707,7 +714,7 @@ compileExpr e = withContextM 2 (sdToTxt $ "Compiling expr:" GHC.<+> GHC.ppr e) $
PIR.TyInst annMayInline <$> errorFunc <*> compileTypeNorm t

-- See Note [Uses of Eq]
GHC.Var n | GHC.getName n == GHC.eqName -> throwPlain $ UnsupportedError "Use of == from the Haskell Eq typeclass"
-- GHC.Var n | GHC.getName n == GHC.eqName -> throwPlain $ UnsupportedError "Use of == from the Haskell Eq typeclass"
GHC.Var n | GHC.getName n == GHC.integerEqName -> throwPlain $ UnsupportedError "Use of Haskell Integer equality, possibly via the Haskell Eq typeclass"
GHC.Var n | isProbablyBytestringEq n -> throwPlain $ UnsupportedError "Use of Haskell ByteString equality, possibly via the Haskell Eq typeclass"

Expand Down Expand Up @@ -744,7 +751,8 @@ compileExpr e = withContextM 2 (sdToTxt $ "Compiling expr:" GHC.<+> GHC.ppr e) $
"Variable" GHC.<+> GHC.ppr n
GHC.$+$ (GHC.ppr $ GHC.idDetails n)
GHC.$+$ (GHC.ppr $ GHC.realIdUnfolding n)

((bimap strip (fmap strip) . GHC.collectArgs) -> (GHC.Var n, args))
| Just action <- isKnownApp n args -> action
-- ignoring applications to types of 'RuntimeRep' kind, see Note [Unboxed tuples]
l `GHC.App` GHC.Type t | GHC.isRuntimeRepKindedTy t -> compileExpr l
-- arg can be a type here, in which case it's a type instantiation
Expand Down Expand Up @@ -848,6 +856,94 @@ compileExpr e = withContextM 2 (sdToTxt $ "Compiling expr:" GHC.<+> GHC.ppr e) $
GHC.Type _ -> throwPlain $ UnsupportedError "Types as standalone expressions"
GHC.Coercion _ -> throwPlain $ UnsupportedError "Coercions as expressions"

isKnownApp ::
CompilingDefault uni fun m ann =>
GHC.Var ->
[GHC.CoreExpr] ->
Maybe (m (PIRTerm uni fun))
isKnownApp fun args = Map.lookup (splitNameString (GHC.varName fun)) knownApps >>= ($ args)

knownApps ::
CompilingDefault uni fun m ann =>
Map (Maybe String, String) ([GHC.CoreExpr] -> Maybe (m (PIRTerm uni fun)))
knownApps =
Map.fromListWithKey (\n -> error ("knownApps: key defined more than once: " <> show n))
. fmap (first (TH.nameModule &&& TH.nameBase))
$ [
( '(GHC.Classes.==)
, \case
[GHC.Type ty, _numDict, GHC.Lit (GHC.LitNumber _ i), GHC.Lit (GHC.LitNumber _ j)]
| ty `GHC.eqType` GHC.integerTy -> Just $ do
res <- lookupDataCon =<< thNameToGhcNameOrFail (if i == j then 'True else 'False)
compileDataConRef $ res
[GHC.Type ty, _eqDict]
| ty `GHC.eqType` GHC.integerTy ->
Just $
compileExpr . GHC.Var =<< lookupId =<< thNameToGhcNameOrFail 'Builtins.equalsInteger
_ -> Nothing
)
,
( '(GHC.Num.+)
, \case
[GHC.Type ty, _numDict, GHC.Lit (GHC.LitNumber numTy i), GHC.Lit (GHC.LitNumber _numTy j)]
| ty `GHC.eqType` GHC.integerTy ->
Just . compileExpr . GHC.Lit $ GHC.LitNumber numTy (i + j)
[GHC.Type ty, _numDict]
| ty `GHC.eqType` GHC.integerTy ->
Just $
compileExpr . GHC.Var =<< lookupId =<< thNameToGhcNameOrFail 'BI.addInteger
_ -> Nothing
)
,
( '(GHC.Num.*)
, \case
[GHC.Type ty, _numDict, GHC.Lit (GHC.LitNumber numTy i), GHC.Lit (GHC.LitNumber _numTy j)]
| ty `GHC.eqType` GHC.integerTy ->
Just . compileExpr . GHC.Lit $ GHC.LitNumber numTy (i * j)
[GHC.Type ty, _numDict]
| ty `GHC.eqType` GHC.integerTy ->
Just $
compileExpr . GHC.Var =<< lookupId =<< thNameToGhcNameOrFail 'BI.multiplyInteger
_ -> Nothing
)
,
( 'GHC.Num.fromInteger
, \case
[GHC.Type ty, _numDict, arg]
| ty `GHC.eqType` GHC.integerTy -> Just $ compileExpr arg
[GHC.Type ty, _numDict]
| ty `GHC.eqType` GHC.integerTy -> Just $ do
idId <- lookupId =<< thNameToGhcNameOrFail 'id
compileExpr $ GHC.mkCoreApps (GHC.Var idId) [GHC.Type GHC.integerTy]
_ -> Nothing
)
,
( 'GHC.Num.negate
, \case
[GHC.Type ty, _numDict, GHC.Lit (GHC.LitNumber numTy i)]
| ty `GHC.eqType` GHC.integerTy ->
Just . compileExpr . GHC.Lit $ GHC.LitNumber numTy (-i)
_ -> Nothing
)
,
( 'GHC.Real.toInteger
, \case
[GHC.Type ty, _numDict, arg]
| ty `GHC.eqType` GHC.integerTy -> Just $ compileExpr arg
[GHC.Type ty, _integralDict]
| ty `GHC.eqType` GHC.integerTy -> Just $ do
idId <- lookupId =<< thNameToGhcNameOrFail 'id
compileExpr $ GHC.mkCoreApps (GHC.Var idId) [GHC.Type GHC.integerTy]
_ -> Nothing
)
]

splitNameString :: GHC.Name -> (Maybe String, String)
splitNameString name = (modu, occ)
where
modu = fmap (GHC.moduleNameString . GHC.moduleName) (GHC.nameModule_maybe name)
occ = GHC.occNameString (GHC.nameOccName name)

{- Note [What source locations to cover]
We try to get as much coverage information as we can out of GHC. This means that
anything we find in the GHC Core code that hints at a source location will be
Expand Down

0 comments on commit 68f4b19

Please sign in to comment.