[CGP-338] [StdLib] Eta-expanded left folds

language-plutus-core/stdlib/Language/PlutusCore/StdLib/Data/List.hs

@@ -128,7 +128,7 @@ getBuiltinFoldrList = do
 --
 -- > /\(a :: *) (r :: *) -> \(f : r -> a -> r) ->
 -- >     fix {r} {list a -> r} \(rec : r -> list a -> r) (z : r) (xs : list a) ->
--- >         unwrap xs {r} z \(x : a) -> rec (f z x)
+-- >         unwrap xs {r} z \(x : a) (xs' : list a) -> rec (f z x) xs'
 --
 -- @listA@ appears several times in types in the term,
 -- so this is not really a definition with unique names.
@@ -143,6 +143,7 @@ getBuiltinFoldList = do
     z   <- freshName () "z"
     xs  <- freshName () "xs"
     x   <- freshName () "x"
+    xs' <- freshName () "xs'"
     let RecursiveType _ listA =
             holedToRecursive . holedTyApp list $ TyVar () a
     return
@@ -155,15 +156,15 @@ getBuiltinFoldList = do
         . LamAbs () xs listA
         . Apply () (Apply () (TyInst () (Unwrap () (Var () xs)) $ TyVar () r) $ Var () z)
         . LamAbs () x (TyVar () a)
-        . Apply () (Var () rec)
-        $ mkIterApp (Var () f)
-          [ Var () z
-          , Var () x
+        . LamAbs () xs' listA
+        . mkIterApp (Var () rec)
+        $ [ mkIterApp (Var () f) [Var () z, Var () x]
+          , Var () xs'
           ]
 
 -- |  'sum' as a PLC term.
 --
--- > /\(s :: *) -> foldl'ist {integer s} {integer s} (addInteger {s}) s!0
+-- > /\(s :: *) -> foldLst {integer s} {integer s} (addInteger {s}) s!0
 --
 -- TODO: once sizes are added, make the implementation match the comment (which is wrong).
 getBuiltinSum :: Natural -> Quote (Term TyName Name ())

language-plutus-core/stdlib/Language/PlutusCore/StdLib/Data/Nat.hs

@@ -106,7 +106,7 @@ getBuiltinFoldrNat = do
 --
 -- > /\(r :: *) -> \(f : r -> r) ->
 -- >     fix {r} {nat -> r} \(rec : r -> nat -> r) (z : r) (n : nat) ->
--- >         unwrap n {r} z (rec (f z))
+-- >         unwrap n {r} z (\(n' : nat) -> rec (f z) n')
 --
 -- @nat@ appears several times in types in the term,
 -- so this is not really a definition with unique names.
@@ -119,6 +119,7 @@ getBuiltinFoldNat = do
     rec <- freshName () "rec"
     z   <- freshName () "z"
     n   <- freshName () "n"
+    n'  <- freshName () "n'"
     return
         . TyAbs () r (Type ())
         . LamAbs () f (TyFun () (TyVar () r) (TyVar () r))
@@ -127,9 +128,11 @@ getBuiltinFoldNat = do
         . LamAbs () z (TyVar () r)
         . LamAbs () n nat
         . Apply () (Apply () (TyInst () (Unwrap () (Var () n)) $ TyVar () r) $ Var () z)
-        . Apply () (Var () rec)
-        . Apply () (Var () f)
-        $ Var () z
+        . LamAbs () n' nat
+        . mkIterApp (Var () rec)
+        $ [ Apply () (Var () f) $ Var () z
+          , Var () n'
+          ]
 
 -- | Convert a @nat@ to an 'Integer'.
 getBuiltinNatToInteger :: Natural -> Quote (Term TyName Name ())

language-plutus-core/test/Pretty/Golden/Readable/StdLib/Data/List/FoldList.plc.golden

@@ -1 +1 @@
-/\(a :: *) -> /\(r :: *) -> \(f : r -> a -> r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} (wrap self ((\(a :: *) -> self -> a) (a -> b)) (\(s : (\(a :: *) -> fix self. self -> a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} s) x))) {r} {(\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a -> r} (\(rec : r -> (\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a -> r) -> \(z : r) -> \(xs : (\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a) -> unwrap xs {r} z (\(x : a) -> rec (f z x)))
+/\(a :: *) -> /\(r :: *) -> \(f : r -> a -> r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} (wrap self ((\(a :: *) -> self -> a) (a -> b)) (\(s : (\(a :: *) -> fix self. self -> a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} s) x))) {r} {(\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a -> r} (\(rec : r -> (\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a -> r) -> \(z : r) -> \(xs : (\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a) -> unwrap xs {r} z (\(x : a) -> \(xs' : (\(a :: *) -> fix list. all (r :: *). r -> (a -> list -> r) -> r) a) -> rec (f z x) xs'))

language-plutus-core/test/Pretty/Golden/Readable/StdLib/Data/Nat/FoldNat.plc.golden

@@ -1 +1 @@
-/\(r :: *) -> \(f : r -> r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} (wrap self ((\(a :: *) -> self -> a) (a -> b)) (\(s : (\(a :: *) -> fix self. self -> a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} s) x))) {r} {(fix nat. all (r :: *). r -> (nat -> r) -> r) -> r} (\(rec : r -> (fix nat. all (r :: *). r -> (nat -> r) -> r) -> r) -> \(z : r) -> \(n : fix nat. all (r :: *). r -> (nat -> r) -> r) -> unwrap n {r} z (rec (f z)))
+/\(r :: *) -> \(f : r -> r) -> (/\(a :: *) -> /\(b :: *) -> \(f : (a -> b) -> a -> b) -> (/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} (wrap self ((\(a :: *) -> self -> a) (a -> b)) (\(s : (\(a :: *) -> fix self. self -> a) (a -> b)) -> \(x : a) -> f ((/\(a :: *) -> \(s : (\(a :: *) -> fix self. self -> a) a) -> unwrap s s) {a -> b} s) x))) {r} {(fix nat. all (r :: *). r -> (nat -> r) -> r) -> r} (\(rec : r -> (fix nat. all (r :: *). r -> (nat -> r) -> r) -> r) -> \(z : r) -> \(n : fix nat. all (r :: *). r -> (nat -> r) -> r) -> unwrap n {r} z (\(n' : fix nat. all (r :: *). r -> (nat -> r) -> r) -> rec (f z) n'))