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 596824d
Show file tree
Hide file tree
Showing 25 changed files with 214 additions and 23 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
@@ -0,0 +1,2 @@
({cpu: 52948597
| mem: 167402})
@@ -0,0 +1,2 @@
({cpu: 460200997
| mem: 1473069})
@@ -0,0 +1,2 @@
({cpu: 133868245
| mem: 431693})
@@ -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: 840539251
| mem: 3496546})
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
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
98 changes: 97 additions & 1 deletion 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 @@ -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
59 changes: 59 additions & 0 deletions plutus-tx-plugin/src/PlutusTx/Compiler/Types.hs
Expand Up @@ -22,13 +22,16 @@ import PlutusCore.Annotation
import PlutusCore.Builtin qualified as PLC
import PlutusCore.Default qualified as PLC
import PlutusCore.Quote
import PlutusIR.Compiler.Definitions qualified as PIR

import GHC qualified
import GHC.Core.FamInstEnv qualified as GHC
import GHC.Plugins qualified as GHC
import GHC.Types.TyThing qualified as GHC

import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

import Data.List.NonEmpty qualified as NE
Expand Down Expand Up @@ -174,13 +177,69 @@ stableModuleCmp m1 m2 =
-- See Note [Stable name comparisons]
(GHC.moduleUnit m1 `GHC.stableUnitCmp` GHC.moduleUnit m2)

class Monad m => MonadCoreM m where
lookupId :: GHC.Name -> m GHC.Id
lookupDataCon :: GHC.Name -> m GHC.DataCon
lookupTyCon :: GHC.Name -> m GHC.TyCon
thNameToGhcName :: TH.Name -> m (Maybe GHC.Name)

instance MonadCoreM GHC.CoreM where
lookupId = GHC.lookupId
lookupDataCon = GHC.lookupDataCon
lookupTyCon = GHC.lookupTyCon
thNameToGhcName = GHC.thNameToGhcName

instance MonadCoreM m => MonadCoreM (ReaderT r m) where
lookupId = lift . lookupId
lookupDataCon = lift . lookupDataCon
lookupTyCon = lift . lookupTyCon
thNameToGhcName = lift . thNameToGhcName

instance (MonadCoreM m, Monoid w) => MonadCoreM (WriterT w m) where
lookupId = lift . lookupId
lookupDataCon = lift . lookupDataCon
lookupTyCon = lift . lookupTyCon
thNameToGhcName = lift . thNameToGhcName

instance MonadCoreM m => MonadCoreM (StateT s m) where
lookupId = lift . lookupId
lookupDataCon = lift . lookupDataCon
lookupTyCon = lift . lookupTyCon
thNameToGhcName = lift . thNameToGhcName

instance MonadCoreM m => MonadCoreM (QuoteT m) where
lookupId = lift . lookupId
lookupDataCon = lift . lookupDataCon
lookupTyCon = lift . lookupTyCon
thNameToGhcName = lift . thNameToGhcName

instance MonadCoreM m => MonadCoreM (ExceptT s m) where
lookupId = lift . lookupId
lookupDataCon = lift . lookupDataCon
lookupTyCon = lift . lookupTyCon
thNameToGhcName = lift . thNameToGhcName

deriving newtype instance MonadCoreM m => MonadCoreM (PIR.DefT key uni fun ann m)

-- | Get the 'GHC.Name' corresponding to the given 'TH.Name', or throw an error if we can't get it.
thNameToGhcNameOrFail ::
(MonadCoreM m, MonadError (CompileError uni fun ann) m) =>
TH.Name ->
m GHC.Name
thNameToGhcNameOrFail name = do
maybeName <- thNameToGhcName name
case maybeName of
Just n -> pure n
Nothing -> throwError . NoContext $ CoreNameLookupError name

-- See Note [Scopes]
type Compiling uni fun m ann =
( MonadError (CompileError uni fun ann) m
, MonadQuote m
, MonadReader (CompileContext uni fun) m
, MonadDefs LexName uni fun Ann m
, MonadWriter CoverageIndex m
, MonadCoreM m
)

-- Packing up equality constraints gives us a nice way of writing type signatures as this way
Expand Down

0 comments on commit 596824d

Please sign in to comment.