Update mkIterApp, mkIterInst and mkIterTyApp (#5348)

plutus-core/changelog.d/20230523_105725_unsafeFixIO_mkplc.md

@@ -0,0 +1,10 @@
+### Added
+
+- Added `PlutusCore.MkPlc.mkIterAppNoAnn`, `PlutusCore.MkPlc.mkIterInstNoAnn` and
+  `PlutusCore.MkPlc.mkIterTyAppNoAnn`.
+
+### Changed
+
+- Changed `PlutusCore.MkPlc.mkIterApp`, `PlutusCore.MkPlc.mkIterInst` and
+  `PlutusCore.MkPlc.mkIterTyApp` to require an annotation to be provided
+  for each argument.

plutus-core/cost-model/budgeting-bench/Common.hs

@@ -108,26 +108,26 @@ mkUnit = eraseTerm $  mkConstant () ()
 -- Create a term instantiating a builtin and applying it to one argument
 mkApp1 :: (uni `Includes` a, NFData a) => fun -> [Type tyname uni ()] -> a -> PlainTerm uni fun
 mkApp1 !name !tys (force -> !x) =
-    eraseTerm $ mkIterApp () instantiated [mkConstant () x]
-    where instantiated = mkIterInst () (builtin () name) tys
+    eraseTerm $ mkIterAppNoAnn instantiated [mkConstant () x]
+    where instantiated = mkIterInstNoAnn (builtin () name) tys
 
 
 -- Create a term instantiating a builtin and applying it to two arguments
 mkApp2
     :: (uni `Includes` a, uni `Includes` b, NFData a, NFData b)
     =>  fun -> [Type tyname uni ()]-> a -> b -> PlainTerm uni fun
 mkApp2 !name !tys (force -> !x) (force -> !y) =
-    eraseTerm $ mkIterApp () instantiated [mkConstant () x,  mkConstant () y]
-    where instantiated = mkIterInst () (builtin () name) tys
+    eraseTerm $ mkIterAppNoAnn instantiated [mkConstant () x,  mkConstant () y]
+    where instantiated = mkIterInstNoAnn (builtin () name) tys
 
 
 -- Create a term instantiating a builtin and applying it to three arguments
 mkApp3
     :: (uni `Includes` a, uni `Includes` b, uni `Includes` c, NFData a, NFData b, NFData c)
     => fun -> [Type tyname uni ()] -> a -> b -> c -> PlainTerm uni fun
 mkApp3 !name !tys (force -> !x) (force -> !y) (force -> !z) =
-    eraseTerm $ mkIterApp () instantiated [mkConstant () x, mkConstant () y, mkConstant () z]
-    where instantiated = mkIterInst () (builtin () name) tys
+    eraseTerm $ mkIterAppNoAnn instantiated [mkConstant () x, mkConstant () y, mkConstant () z]
+    where instantiated = mkIterInstNoAnn (builtin () name) tys
 
 
 -- Create a term instantiating a builtin and applying it to four arguments
@@ -137,9 +137,9 @@ mkApp4
         NFData a, NFData b, NFData c, NFData d)
     => fun -> [Type tyname uni ()] -> a -> b -> c -> d -> PlainTerm uni fun
 mkApp4 !name !tys (force -> !x) (force -> !y) (force -> !z) (force -> !t) =
-    eraseTerm $ mkIterApp () instantiated [ mkConstant () x, mkConstant () y
+    eraseTerm $ mkIterAppNoAnn instantiated [ mkConstant () x, mkConstant () y
                                       , mkConstant () z, mkConstant () t ]
-    where instantiated = mkIterInst () (builtin () name) tys
+    where instantiated = mkIterInstNoAnn (builtin () name) tys
 
 
 -- Create a term instantiating a builtin and applying it to five arguments
@@ -149,9 +149,9 @@ mkApp5
         NFData a, NFData b, NFData c, NFData d, NFData e)
     => fun -> [Type tyname uni ()] -> a -> b -> c -> d -> e -> PlainTerm uni fun
 mkApp5 !name !tys (force -> !x) (force -> !y) (force -> !z) (force -> !t) (force -> !u) =
-    eraseTerm $ mkIterApp () instantiated [ mkConstant () x, mkConstant () y, mkConstant () z
+    eraseTerm $ mkIterAppNoAnn instantiated [ mkConstant () x, mkConstant () y, mkConstant () z
                                       , mkConstant () t, mkConstant () u ]
-    where instantiated = mkIterInst () (builtin () name) tys
+    where instantiated = mkIterInstNoAnn (builtin () name) tys
 
 
 -- Create a term instantiating a builtin and applying it to six arguments
@@ -161,9 +161,9 @@ mkApp6
         NFData a, NFData b, NFData c, NFData d, NFData e, NFData f)
     => fun -> [Type tyname uni ()] -> a -> b -> c -> d -> e -> f-> PlainTerm uni fun
 mkApp6 name tys (force -> !x) (force -> !y) (force -> !z) (force -> !t) (force -> !u) (force -> !v)=
-    eraseTerm $ mkIterApp () instantiated [mkConstant () x, mkConstant () y, mkConstant () z,
+    eraseTerm $ mkIterAppNoAnn instantiated [mkConstant () x, mkConstant () y, mkConstant () z,
                                        mkConstant () t, mkConstant () u, mkConstant () v]
-    where instantiated = mkIterInst () (builtin () name) tys
+    where instantiated = mkIterInstNoAnn (builtin () name) tys
 
 
 ---------------- Creating benchmarks ----------------

plutus-core/plutus-core/examples/PlutusCore/Examples/Data/Data.hs

@@ -65,33 +65,33 @@ ofoldrData = runQuote $ do
     es      <- freshName "es"
     let listData = mkTyBuiltin @_ @[Data] ()
         listR = TyApp () list r
-        opair a = mkIterTyApp () pair [a, a]
+        opair a = mkIterTyAppNoAnn pair [a, a]
         unwrap' ann = apply ann $ mapFun Left caseData
     return
         . lamAbs () fConstr (TyFun () integer $ TyFun () listR r)
         . lamAbs () fMap (TyFun () (TyApp () list $ opair r) r)
         . lamAbs () fList (TyFun () listR r)
         . lamAbs () fI (TyFun () integer r)
         . lamAbs () fB (TyFun () (mkTyBuiltin @_ @ByteString ()) r)
-        . apply () (mkIterInst () fix [dataTy, r])
+        . apply () (mkIterInstNoAnn fix [dataTy, r])
         . lamAbs () rec (TyFun () dataTy r)
         . lamAbs () d dataTy
-        $ mkIterApp () (tyInst () (unwrap' () (var () d)) r)
+        $ mkIterAppNoAnn (tyInst () (unwrap' () (var () d)) r)
             [   lamAbs () i integer
               . lamAbs () ds listData
-              $ mkIterApp () (var () fConstr)
+              $ mkIterAppNoAnn (var () fConstr)
                   [ var () i
-                  , mkIterApp () (tyInst () omapList dataTy) [var () rec, var () ds]
+                  , mkIterAppNoAnn (tyInst () omapList dataTy) [var () rec, var () ds]
                   ]
             ,   lamAbs () es (TyApp () list $ opair dataTy)
               . apply () (var () fMap)
-              $ mkIterApp () (tyInst () omapList $ opair dataTy)
+              $ mkIterAppNoAnn (tyInst () omapList $ opair dataTy)
                   [ apply () (tyInst () obothPair dataTy) $ var () rec
                   , var () es
                   ]
             ,   lamAbs () ds listData
               . apply () (var () fList)
-              $ mkIterApp () (tyInst () omapList dataTy)
+              $ mkIterAppNoAnn (tyInst () omapList dataTy)
                   [ var () rec
                   , var () ds
                   ]

plutus-core/plutus-core/examples/PlutusCore/Examples/Data/InterList.hs

@@ -47,7 +47,7 @@ interListData = runQuote $ do
     b         <- freshTyName "b"
     interlist <- freshTyName "interlist"
     r         <- freshTyName "r"
-    let interlistBA = mkIterTyApp () (TyVar () interlist) [TyVar () b, TyVar () a]
+    let interlistBA = mkIterTyAppNoAnn (TyVar () interlist) [TyVar () b, TyVar () a]
     makeRecursiveType () interlist [TyVarDecl () a $ Type (), TyVarDecl () b $ Type ()]
         . TyForall () r (Type ())
         . TyFun () (TyVar () r)
@@ -62,7 +62,7 @@ interNil = runQuote $ do
     r <- freshTyName "r"
     z <- freshName "z"
     f <- freshName "f"
-    let interlistBA = mkIterTyApp () interlist [TyVar () b, TyVar () a]
+    let interlistBA = mkIterTyAppNoAnn interlist [TyVar () b, TyVar () a]
     return
         . TyAbs () a (Type ())
         . TyAbs () b (Type ())
@@ -83,7 +83,7 @@ interCons = runQuote $ do
     r  <- freshTyName "r"
     z  <- freshName "z"
     f  <- freshName "f"
-    let interlistBA = mkIterTyApp () interlist [TyVar () b, TyVar () a]
+    let interlistBA = mkIterTyAppNoAnn interlist [TyVar () b, TyVar () a]
     return
         . TyAbs () a (Type ())
         . TyAbs () b (Type ())
@@ -94,7 +94,7 @@ interCons = runQuote $ do
         . TyAbs () r (Type ())
         . LamAbs () z (TyVar () r)
         . LamAbs () f (mkIterTyFun () [TyVar () a, TyVar () b, interlistBA] $ TyVar () r)
-        $ mkIterApp () (Var () f)
+        $ mkIterAppNoAnn (Var () f)
           [ Var () x
           , Var () y
           , Var () xs
@@ -119,43 +119,43 @@ foldrInterList = runQuote $ do
     xs' <- freshName "xs'"
     x'  <- freshName "x'"
     y'  <- freshName "y'"
-    let interlistOf a' b' = mkIterTyApp () interlist [TyVar () a', TyVar () b']
+    let interlistOf a' b' = mkIterTyAppNoAnn interlist [TyVar () a', TyVar () b']
         fTy a' b' = mkIterTyFun () [TyVar () a', TyVar () b', TyVar () r] $ TyVar () r
         fixTyArg2
             = TyForall () a (Type ())
             . TyForall () b (Type ())
             . TyFun () (fTy a b)
             . TyFun () (interlistOf a b)
             $ TyVar () r
-        instedFix = mkIterInst () fix [unit, fixTyArg2]
+        instedFix = mkIterInstNoAnn fix [unit, fixTyArg2]
         unwrappedXs = TyInst () (Unwrap () (Var () xs)) $ TyVar () r
-        instedRec = mkIterInst () (Apply () (Var () rec) unitval) [TyVar () b, TyVar () a]
+        instedRec = mkIterInstNoAnn (Apply () (Var () rec) unitval) [TyVar () b, TyVar () a]
     return
         . TyAbs () a0 (Type ())
         . TyAbs () b0 (Type ())
         . TyAbs () r (Type ())
         . LamAbs () f (fTy a0 b0)
         . LamAbs () z (TyVar () r)
-        $ mkIterInst ()
-            ( mkIterApp () instedFix
+        $ mkIterInstNoAnn
+            ( mkIterAppNoAnn instedFix
                 [   LamAbs () rec (TyFun () unit fixTyArg2)
                   . LamAbs () u unit
                   . TyAbs () a (Type ())
                   . TyAbs () b (Type ())
                   . LamAbs () f' (fTy a b)
                   . LamAbs () xs (interlistOf a b)
-                  $ mkIterApp () unwrappedXs
+                  $ mkIterAppNoAnn unwrappedXs
                       [ Var () z
                       ,    LamAbs () x (TyVar () a)
                          . LamAbs () y (TyVar () b)
                          . LamAbs () xs' (interlistOf b a)
-                         $ mkIterApp () (Var () f')
+                         $ mkIterAppNoAnn (Var () f')
                              [ Var () x
                              , Var () y
-                             , mkIterApp () instedRec
+                             , mkIterAppNoAnn instedRec
                                  [    LamAbs () y' (TyVar () b)
                                     . LamAbs () x' (TyVar () a)
-                                    $ mkIterApp () (Var () f')
+                                    $ mkIterAppNoAnn (Var () f')
                                         [ Var () x'
                                         , Var () y'
                                         ]

plutus-core/plutus-core/examples/PlutusCore/Examples/Data/List.hs

@@ -33,13 +33,13 @@ omapList = runQuote $ do
     return
         . tyAbs () a (Type ())
         . lamAbs () f (TyFun () (TyVar () a) $ TyVar () a)
-        . apply () (mkIterInst () fix [listA, listA])
+        . apply () (mkIterInstNoAnn fix [listA, listA])
         . lamAbs () rec (TyFun () listA listA)
         . lamAbs () xs listA
         . apply () (apply () (tyInst () (unwrap' () (var () xs)) listA) $ var () xs)
         . lamAbs () x (TyVar () a)
         . lamAbs () xs' listA
-        $ mkIterApp () (tyInst () (builtin () $ Left MkCons) $ TyVar () a)
+        $ mkIterAppNoAnn (tyInst () (builtin () $ Left MkCons) $ TyVar () a)
             [ apply () (var () f) $ var () x
             , apply () (var () rec) $ var () xs'
             ]

plutus-core/plutus-core/examples/PlutusCore/Examples/Data/Pair.hs

@@ -23,12 +23,12 @@ obothPair = runQuote $ do
     a <- freshTyName "a"
     f <- freshName "f"
     p <- freshName "p"
-    let atAA fun = mkIterInst () (builtin () fun) [TyVar () a, TyVar () a]
+    let atAA fun = mkIterInstNoAnn (builtin () fun) [TyVar () a, TyVar () a]
     return
         . tyAbs () a (Type ())
         . lamAbs () f (TyFun () (TyVar () a) $ TyVar () a)
-        . lamAbs () p (mkIterTyApp () pair [TyVar () a, TyVar () a])
-        $ mkIterApp () (atAA $ Right Comma)
+        . lamAbs () p (mkIterTyAppNoAnn pair [TyVar () a, TyVar () a])
+        $ mkIterAppNoAnn (atAA $ Right Comma)
             [ apply () (var () f) . apply () (atAA $ Left FstPair) $ var () p
             , apply () (var () f) . apply () (atAA $ Left SndPair) $ var () p
             ]

plutus-core/plutus-core/examples/PlutusCore/Examples/Data/TreeForest.hs

@@ -116,7 +116,7 @@ asTree = runQuote $ do
     return
         . TyLam () d (star ~~> (star ~~> star ~~> star) ~~> star)
         . TyLam () a star
-        $ mkIterTyApp () (TyVar () d)
+        $ mkIterTyAppNoAnn (TyVar () d)
             [ TyVar () a
             , treeTag
             ]
@@ -128,7 +128,7 @@ asForest = runQuote $ do
     return
         . TyLam () d (star ~~> (star ~~> star ~~> star) ~~> star)
         . TyLam () a star
-        $ mkIterTyApp () (TyVar () d)
+        $ mkIterTyAppNoAnn (TyVar () d)
             [ TyVar () a
             , forestTag
             ]
@@ -142,11 +142,11 @@ treeForestData = runQuote $ do
     let vA = TyVar () a
         vR = TyVar () r
         recSpine = [TyVar () treeForest, vA]
-    let tree   = mkIterTyApp () asTree   recSpine
-        forest = mkIterTyApp () asForest recSpine
+    let tree   = mkIterTyAppNoAnn asTree   recSpine
+        forest = mkIterTyAppNoAnn asForest recSpine
         body
             = TyForall () r (Type ())
-            $ mkIterTyApp () (TyVar () tag)
+            $ mkIterTyAppNoAnn (TyVar () tag)
                 [ (vA ~~> forest ~~> vR) ~~> vR
                 , vR ~~> (tree ~~> forest ~~> vR) ~~> vR
                 ]
@@ -189,7 +189,7 @@ treeNode = runQuote $ normalizeTypesIn =<< do
         . wrapTree [vA]
         . TyAbs () r (Type ())
         . LamAbs () f (mkIterTyFun () [vA, forestA] vR)
-        $ mkIterApp () (Var () f)
+        $ mkIterAppNoAnn (Var () f)
             [ Var () x
             , Var () fr
             ]
@@ -244,7 +244,7 @@ forestCons = runQuote $ normalizeTypesIn =<< do
         . TyAbs () r (Type ())
         . LamAbs () z vR
         . LamAbs () f (mkIterTyFun () [treeA, forestA] vR)
-        $ mkIterApp () (Var () f)
+        $ mkIterAppNoAnn (Var () f)
             [ Var () tr
             , Var () fr
             ]