-
Notifications
You must be signed in to change notification settings - Fork 479
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
PLT-7745: Basic rewrite rules for builtins
- Loading branch information
Showing
9 changed files
with
91 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,19 +1,29 @@ | ||
{-# LANGUAGE KindSignatures #-} | ||
{-# LANGUAGE TemplateHaskell #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
module PlutusIR.Analysis.Builtins where | ||
|
||
import Data.Monoid | ||
import Control.Lens.TH | ||
import Data.Kind | ||
import PlutusCore.Builtin | ||
import PlutusCore.Builtin qualified as PLC | ||
import PlutusPrelude (Default (..)) | ||
import PlutusIR qualified as PIR | ||
|
||
newtype RewriteRules uni fun = RewriteRules { | ||
unRewriteRule :: forall tyname name a. Semigroup a => Dual (Endo (PIR.Term tyname name uni fun a)) | ||
} | ||
|
||
-- | All non-static information about builtins that the compiler might want. | ||
data BuiltinsInfo (uni :: Type -> Type) fun = BuiltinsInfo | ||
{ _biSemanticsVariant :: PLC.BuiltinSemanticsVariant fun | ||
, _rewriteRules :: RewriteRules uni fun | ||
} | ||
|
||
makeLenses ''BuiltinsInfo | ||
|
||
instance (Default (BuiltinSemanticsVariant fun)) => Default (BuiltinsInfo uni fun) where | ||
def = BuiltinsInfo def | ||
def = BuiltinsInfo | ||
def | ||
-- no rewrite rules by default (aka id). | ||
(RewriteRules mempty) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
{-# LANGUAGE GADTs #-} | ||
{-# LANGUAGE LambdaCase #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
module PlutusIR.Transform.Rewrite where | ||
|
||
import PlutusCore.Default | ||
import PlutusIR.Analysis.Builtins | ||
import PlutusIR | ||
import Data.Monoid | ||
|
||
import Control.Lens | ||
|
||
userRewrite :: (Semigroup a, t ~ Term tyname name uni fun a) | ||
=> BuiltinsInfo uni fun | ||
-> t | ||
-> t | ||
userRewrite bi t = | ||
let RewriteRules f = bi^.rewriteRules | ||
in transformOf termSubterms (appEndo $ getDual f) t | ||
|
||
defaultUniRewriteRules :: RewriteRules DefaultUni DefaultFun | ||
defaultUniRewriteRules = RewriteRules $ combineRules | ||
-- rules are applied from left to right because of Dual | ||
[ decodeEncode | ||
] | ||
where | ||
combineRules = foldMap (Dual . Endo) | ||
|
||
decodeEncode :: Semigroup a => Term tyname name uni DefaultFun a -> Term tyname name uni DefaultFun a | ||
decodeEncode = \case | ||
BA DecodeUtf8 a1 a2 (BA EncodeUtf8 a3 a4 t) -> | ||
-- place the missed annotations inside the rewritten term | ||
(<> a1 <> a2 <> a3 <> a4) <$> t | ||
t -> t | ||
|
||
pattern BA b a1 a2 t <- Apply a1 (Builtin a2 b) t |
22 changes: 22 additions & 0 deletions
22
plutus-core/plutus-ir/test/PlutusIR/Transform/Rewrite/Tests.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
module PlutusIR.Transform.Rewrite.Tests where | ||
|
||
import PlutusIR.Parser | ||
import PlutusIR.Test | ||
import PlutusIR.Analysis.Builtins | ||
import PlutusIR.Transform.Rewrite qualified as Rewrite | ||
|
||
import Data.Default.Class | ||
import Control.Lens | ||
import Test.Tasty | ||
import Test.Tasty.Extras | ||
|
||
|
||
test_commuteDefaultFun :: TestTree | ||
test_commuteDefaultFun = runTestNestedIn ["plutus-ir/test/PlutusIR/Transform"] $ | ||
testNested "Rewrite" $ | ||
fmap | ||
(goldenPir (Rewrite.userRewrite builtinsInfo) pTerm) | ||
[ "decodeEncodeUtf8" | ||
] | ||
where | ||
builtinsInfo = def & rewriteRules .~ Rewrite.defaultUniRewriteRules |
5 changes: 5 additions & 0 deletions
5
plutus-core/plutus-ir/test/PlutusIR/Transform/Rewrite/decodeEncodeUtf8
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
(lam | ||
x (con string) [ (builtin decodeUtf8) [ (builtin encodeUtf8) | ||
[ (builtin decodeUtf8) [ (builtin encodeUtf8) x | ||
] ] ] ] | ||
) |
1 change: 1 addition & 0 deletions
1
plutus-core/plutus-ir/test/PlutusIR/Transform/Rewrite/decodeEncodeUtf8.golden
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
(lam x (con string) x) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters