Skip to content

Commit a8a5a35

Browse files
zliu41zliu41
authored
Simplify inline hints by reordering check arguments (#7715)
1 parent d8f8a06 commit a8a5a35

28 files changed

Lines changed: 516 additions & 569 deletions

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Hints.hs‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@ data Inline
1919
| InlCase Inline [Inline]
2020
| InlExpand Inline
2121
| InlDrop Inline
22-
| InlLamDrop Inline
2322
deriving stock (Generic)
2423
deriving anyclass (NFData)
2524

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Inline.hs‎

Lines changed: 15 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -273,10 +273,9 @@ restoreApps defs t = makeLams [] t (reverse defs)
273273
-- `aa` is the annotation on the Apply node, and `al` is the annotation
274274
-- on the LamAbs node.
275275
makeLams args acc ((Left al, aa) : rest) =
276-
-- `Left` means the binding is dropped, so `acc` should be decorated with `al`
277-
-- plus `DLamDrop`.
276+
-- `Left` means the binding is dropped, so `acc` should be decorated with `al`.
278277
-- This corresponds to Note [Inliner's Certifier Hints], #3.
279-
makeLams ((Nothing, aa) : args) (decorateWith (al ^. decorations ++ [DLamDrop]) acc) rest
278+
makeLams ((Nothing, aa) : args) (decorateWith (al ^. decorations) acc) rest
280279
makeLams args acc ((Right (Def (UVarDecl al n) rhs), aa) : rest) =
281280
makeLams ((Just rhs, aa) : args) (LamAbs al n acc) rest
282281
makeLams args acc [] =
@@ -578,17 +577,17 @@ fullyApplyAndBetaReduce av info args0 = do
578577
-- * ...
579578
-- * decorations on the innermost Apply node, plus DDrop
580579
-- * `av` plus DExpand.
581-
-- * decorations on the first LamAbs, plus DLamDrop
582-
-- * decorations on the second LamAbs, plus DLamDrop
580+
-- * decorations on the first LamAbs
581+
-- * decorations on the second LamAbs
583582
-- * ...
584-
-- * decorations on the last LamAbs, plus DLamDrop
583+
-- * decorations on the last LamAbs
585584
--
586585
-- See Note [Inliner's Certifier Hints].
587586
decorateWith
588587
( concatMap (\(annApply, _arg) -> annApply ^. decorations ++ [DDrop]) (reverse args0)
589588
++ av ^. decorations
590589
++ [DExpand]
591-
++ concatMap (\(_name, annLam) -> annLam ^. decorations ++ [DLamDrop]) (info ^. varBinders)
590+
++ concatMap (\(_name, annLam) -> annLam ^. decorations) (info ^. varBinders)
592591
)
593592
<$> liftDupable (let Done rhsBody = info ^. varRhsBody in rhsBody)
594593
let go
@@ -669,8 +668,8 @@ inlineSaturatedApp t
669668
-- See Note [Inliner's Certifier Hints] for an overview.
670669
-------------------------------------------------------------------------------
671670

672-
-- | An enclosing Drop, LamDrop or Expand layer
673-
data Decoration = DDrop | DLamDrop | DExpand
671+
-- | An enclosing Drop or Expand layer
672+
data Decoration = DDrop | DExpand
674673

675674
type Ann a = ([Decoration], a)
676675

@@ -696,7 +695,6 @@ mkHints = go
696695
decorate :: CertifierHints.Inline -> [Decoration] -> CertifierHints.Inline
697696
decorate = foldr $ \d h -> case d of
698697
DDrop -> CertifierHints.InlDrop h
699-
DLamDrop -> CertifierHints.InlLamDrop h
700698
DExpand -> CertifierHints.InlExpand h
701699

702700
ds = termAnn t ^. decorations
@@ -727,20 +725,20 @@ inliner as a process that repeatedly performs one of the following two operation
727725
728726
Certifier hints are then defined constructively according to the following procedure.
729727
In the end, the final hints mirror the post-term structure, except that each node may be
730-
decorated with an arbitrary number of `InlExpand`, `InlDrop` and `InlLamDrop` layers,
728+
decorated with an arbitrary number of `InlExpand` and `InlDrop` layers,
731729
reflecting the inlining operations that the inliner has performed.
732730
733731
- Initially the hints mirror the pre-term structure, using constructors of `Inline`
734-
except `InlExpand`, `InlDrop` and `InlLamDrop`. Excluding these three constructors,
732+
except `InlExpand` and `InlDrop`. Excluding these two constructors,
735733
there is a 1-1 correspondence between hints constructors and AST constructors.
736734
737735
- Suppose the inliner performs operation 1, substituting term `N` for variable `v`.
738736
Before the substitution, we have
739737
740738
hints(v) = decorations(InlVar)
741739
742-
where `decorations` denotes an arbitrary number of enclosing `InlExpand`, `InlDrop` or
743-
`InlLamDrop` layers. After the substitution, the hints at this location should become
740+
where `decorations` denotes an arbitrary number of enclosing `InlExpand` or `InlDrop`
741+
layers. After the substitution, the hints at this location should become
744742
745743
decorations(InlExpand hints(N)) (#1)
746744
@@ -760,11 +758,11 @@ reflecting the inlining operations that the inliner has performed.
760758
That is, it is decorated with `decorations₁` plus `InlDrop`.
761759
The hints for `M` should become
762760
763-
decorations₂(InlLamDrop (hints(M))) (#3)
761+
decorations₂(hints(M)) (#3)
764762
765-
That is, it is decorated with `decorations₂`, plus `InlLamDrop`. Note that when `n = 0`,
763+
That is, it is decorated with `decorations₂`. Note that when `n = 0`,
766764
`(\x‾ₙ y. M) X‾ₙ` becomes `M`, and therefore, `hints(M)` should be decorated with
767-
`decorations₁` plus `InlDrop` plus `InlLamDrop` plus `decorations₂`.
765+
`decorations₁` plus `InlDrop` plus `decorations₂`.
768766
769767
Refer to the golden tests for examples of hints (look for files ending with
770768
`.golden.certifier-hints`).

‎plutus-core/untyped-plutus-core/test/Transform/basicInline.golden.certifier-hints‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,8 @@ NoHints
1818

1919
-- Certifier hints #7 (Inline) --
2020
InlDrop
21-
InlLamDrop
22-
InlExpand
23-
InlCon
21+
InlExpand
22+
InlCon
2423

2524

2625
-- Certifier hints #8 (ApplyToCase) --

‎plutus-core/untyped-plutus-core/test/Transform/callsiteInline.golden.certifier-hints‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -27,15 +27,13 @@ InlLam
2727
InlDrop
2828
InlDrop
2929
InlExpand
30-
InlLamDrop
31-
InlLamDrop
32-
InlApply
33-
InlApply
34-
InlVar
35-
InlExpand
36-
InlCon
37-
InlExpand
38-
InlCon
30+
InlApply
31+
InlApply
32+
InlVar
33+
InlExpand
34+
InlCon
35+
InlExpand
36+
InlCon
3937
InlApply
4038
InlVar
4139
InlCon

‎plutus-core/untyped-plutus-core/test/Transform/floatDelay1.golden.certifier-hints‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,14 +18,13 @@ NoHints
1818

1919
-- Certifier hints #7 (Inline) --
2020
InlDrop
21-
InlLamDrop
21+
InlApply
2222
InlApply
23-
InlApply
24-
InlBuiltin
25-
InlExpand
26-
InlCon
23+
InlBuiltin
2724
InlExpand
2825
InlCon
26+
InlExpand
27+
InlCon
2928

3029

3130
-- Certifier hints #8 (ApplyToCase) --

‎plutus-core/untyped-plutus-core/test/Transform/floatDelay3.golden.certifier-hints‎

Lines changed: 9 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,21 +18,19 @@ NoHints
1818

1919
-- Certifier hints #7 (Inline) --
2020
InlDrop
21-
InlLamDrop
21+
InlApply
2222
InlApply
23-
InlApply
24-
InlBuiltin
25-
InlForce
23+
InlBuiltin
24+
InlForce
25+
InlExpand
26+
InlDelay
27+
InlCon
28+
InlDrop
29+
InlForce
30+
InlExpand
2631
InlExpand
2732
InlDelay
2833
InlCon
29-
InlDrop
30-
InlLamDrop
31-
InlForce
32-
InlExpand
33-
InlExpand
34-
InlDelay
35-
InlCon
3634

3735

3836
-- Certifier hints #8 (ApplyToCase) --

‎plutus-core/untyped-plutus-core/test/Transform/forceDelayComplex.golden.certifier-hints‎

Lines changed: 20 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -25,33 +25,26 @@ InlLam
2525
InlDrop
2626
InlDrop
2727
InlDrop
28-
InlLamDrop
29-
InlLamDrop
30-
InlLamDrop
31-
InlLamDrop
32-
InlLamDrop
33-
InlLamDrop
34-
InlLamDrop
35-
InlApply
36-
InlApply
37-
InlApply
38-
InlApply
39-
InlApply
40-
InlApply
41-
InlExpand
42-
InlVar
43-
InlExpand
44-
InlCon
45-
InlExpand
46-
InlCon
47-
InlExpand
48-
InlCon
49-
InlExpand
50-
InlCon
51-
InlExpand
52-
InlCon
53-
InlExpand
54-
InlCon
28+
InlApply
29+
InlApply
30+
InlApply
31+
InlApply
32+
InlApply
33+
InlApply
34+
InlExpand
35+
InlVar
36+
InlExpand
37+
InlCon
38+
InlExpand
39+
InlCon
40+
InlExpand
41+
InlCon
42+
InlExpand
43+
InlCon
44+
InlExpand
45+
InlCon
46+
InlExpand
47+
InlCon
5548

5649

5750
-- Certifier hints #8 (ApplyToCase) --

‎plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiApply.golden.certifier-hints‎

Lines changed: 11 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -22,21 +22,17 @@ InlLam
2222
InlDrop
2323
InlDrop
2424
InlDrop
25-
InlLamDrop
26-
InlLamDrop
27-
InlLamDrop
28-
InlLamDrop
29-
InlApply
30-
InlApply
31-
InlApply
32-
InlExpand
33-
InlVar
34-
InlExpand
35-
InlCon
36-
InlExpand
37-
InlCon
38-
InlExpand
39-
InlCon
25+
InlApply
26+
InlApply
27+
InlApply
28+
InlExpand
29+
InlVar
30+
InlExpand
31+
InlCon
32+
InlExpand
33+
InlCon
34+
InlExpand
35+
InlCon
4036

4137

4238
-- Certifier hints #8 (ApplyToCase) --

‎plutus-core/untyped-plutus-core/test/Transform/forceDelayMultiForce.golden.certifier-hints‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,8 @@ NoHints
1818

1919
-- Certifier hints #7 (Inline) --
2020
InlDrop
21-
InlLamDrop
22-
InlExpand
23-
InlCon
21+
InlExpand
22+
InlCon
2423

2524

2625
-- Certifier hints #8 (ApplyToCase) --

‎plutus-core/untyped-plutus-core/test/Transform/forceDelaySimple.golden.certifier-hints‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,8 @@ NoHints
2020
InlDrop
2121
InlDrop
2222
InlDrop
23-
InlLamDrop
24-
InlLamDrop
25-
InlLamDrop
26-
InlExpand
27-
InlCon
23+
InlExpand
24+
InlCon
2825

2926

3027
-- Certifier hints #8 (ApplyToCase) --

0 commit comments

Comments
 (0)