View on GitHub
File Changes
    , unroll
    , fix
    , fixAndType
+
    , fixBy
+
    , fixByAndType
    , fixN
    , fixNAndType
    , FunctionDef (..)
-- >     ((F ~> Id) -> (F ~> Id)) ->
-- >     ((F ~> F) -> (F ~> Id))
fixBy :: TermLike term TyName Name => term ()
-
fixBy = runQuote $ do
+
fixBy = fst fixByAndType
+

                      
+
fixByAndType :: TermLike term TyName Name => (term (), Type TyName ())
+
fixByAndType = runQuote $ do
    f <- freshTyName () "F"

                      
    -- by : (F ~> Id) -> (F ~> Id)
        nt2 <- natTransId (TyVar () f)
        pure $ TyFun () nt1 nt2

                      
+
    resTy <- do
+
        nt1 <- natTrans (TyVar () f) (TyVar () f)
+
        nt2 <- natTransId (TyVar () f)
+
        pure $ TyFun () nt1 nt2
+

                      
    -- instantiatedFix = fix {F ~> F} {F ~> Id}
    instantiatedFix <- do
        nt1 <- natTrans (TyVar () f) (TyVar () f)
                lamAbs () fq fqTy $
                apply () (tyInst () (apply () (var () recc) (var () h)) (TyVar () q)) $
                apply () (tyInst () (var () h) (TyVar () q)) (var () fq)
-
    pure $
-
        tyAbs () f (KindArrow () (Type ()) (Type ())) $
-
        lamAbs () by byTy $
-
        apply () instantiatedFix $
-
        lamAbs () recc reccTy $
-
        lamAbs () h hty $
-
        tyAbs () r (Type ()) $
-
        lamAbs () fr frTy $
-
        apply () (tyInst () inner (TyVar () r)) (var () fr)
+
    let fixByTerm =
+
            tyAbs () f (KindArrow () (Type ()) (Type ())) $
+
            lamAbs () by byTy $
+
            apply () instantiatedFix $
+
            lamAbs () recc reccTy $
+
            lamAbs () h hty $
+
            tyAbs () r (Type ()) $
+
            lamAbs () fr frTy $
+
            apply () (tyInst () inner (TyVar () r)) (var () fr)
+
    let fixByType =
+
            TyForall () f (KindArrow () (Type ()) (Type ())) $
+
            TyFun () byTy resTy
+
    pure (fixByTerm, fixByType)
+

                      

                      
-- | Make a @[email protected] fixpoint combinator.
--
-- >         (An -> Bn) ->
-- >         Q) ->
-- >     (forall R :: * . ((A1 -> B1) -> ... (An -> Bn) -> R) -> R)
-
fixN :: TermLike term TyName Name => Integer -> term ()
-
fixN n = fst (fixNAndType n)
+
fixN :: TermLike term TyName Name => Integer -> term () -> term ()
+
fixN n fixByTerm = fst (fixNAndType n fixByTerm)

                      
-
fixNAndType :: TermLike term TyName Name => Integer -> (term (), Type TyName ())
-
fixNAndType n = runQuote $ do
+
fixNAndType :: TermLike term TyName Name => Integer -> term () -> (term (), Type TyName ())
+
fixNAndType n fixByTerm = runQuote $ do
    -- the list of pairs of A and B types
    asbs <- replicateM (fromIntegral n) $ do
        a <- freshTyName () "a"
    -- instantiatedFix = fixBy { \X :: * -> (A1 -> B1) -> ... -> (An -> Bn) -> X }
    instantiatedFix <- do
        x <- freshTyName () "X"
-
        pure $ tyInst () fixBy (TyLam () x (Type ()) (funTysTo (TyVar () x)))
+
        pure $ tyInst () fixByTerm (TyLam () x (Type ()) (funTysTo (TyVar () x)))

                      
    -- f : forall Q :: * . ((A1 -> B1) -> ... -> (An -> Bn) -> Q) -> (A1 -> B1) -> ... -> (An -> Bn) -> Q)
    f <- freshName () "f"
                  , plcTypeFile "Self"   $ _recursiveType selfData
                  , plcTermFile "Unroll" unroll
                  , plcTermFile "Fix"    fix
-
                  , plcTermFile "Fix2"   $ fixN 2
+
                  , plcTermFile "Fix2"   $ fixN 2 fixBy
                  ]
              , treeFolderContents "Integer"
                  [ plcTermFile "SuccInteger" succInteger
    evenF <- FunctionDef () evenn (FunctionType () nat bool) <$> eoFunc true oddd
    oddF  <- FunctionDef () oddd  (FunctionType () nat bool) <$> eoFunc false evenn

                      
-
    getMutualFixOf () (fixN 2) [evenF, oddF]
+
    getMutualFixOf () (fixN 2 fixBy) [evenF, oddF]

                      
even :: Term TyName Name ()
even = runQuote $ tupleTermAt () 0 evenAndOdd
            LamAbs () t listNat $
            Apply () (Var () evenn) (Var () t)

                      
-
    getMutualFixOf () (fixN 2) [evenF, oddF]
+
    getMutualFixOf () (fixN 2 fixBy) [evenF, oddF]

                      
evenList :: Term TyName Name ()
evenList = runQuote $ tupleTermAt () 0 evenAndOddList
import           Control.Monad.Trans

                      
import           Data.List.NonEmpty hiding (length)
+
import qualified Data.Set as Set

                      
import qualified Language.PlutusCore                        as PLC
import qualified Language.PlutusCore.MkPlc                  as PLC
            Nothing  -> lift $ throwing _Error $ CompilationError (PLC.typeAnn ty) "Recursive values must be of function type"

                      
    -- See Note [Extra definitions while compiling let-bindings]
-
    let arity = fromIntegral $ length funs
-
        key = FixpointCombinator arity
+
    let
+
        fixByKey = FixBy
+
        arity = fromIntegral $ length funs
+
        fixNKey = FixpointCombinator arity
+

                      
+
    -- TODO: reduce duplication
+
    fixBy <- do
+
        maybeFix <- lookupTerm p0 fixByKey
+
        case maybeFix of
+
            Just f -> pure f
+
            Nothing -> do
+
                name <- liftQuote $ toProgramName fixByKey
+
                let (fixByTerm, fixByType) = Function.fixByAndType
+
                    var :: PLC.VarDecl TyName Name (Provenance a)
+
                    var = PLC.VarDecl NoProvenance (NoProvenance <$ name) (NoProvenance <$ fixByType)
+
                defineTerm fixByKey (PLC.Def var (NoProvenance <$ fixByTerm, Strict)) mempty
+

                      
+
                pure $ PIR.mkVar p0 var
+

                      
    fixN <- do
-
        maybeFix <- lookupTerm p0 key
+
        maybeFix <- lookupTerm p0 fixNKey
        case maybeFix of
            Just f -> pure f
            Nothing -> do
-
                name <- liftQuote $ toProgramName key
-
                let (fixNTerm, fixNType) = if arity == 1 then Function.fixAndType else Function.fixNAndType arity
+
                name <- liftQuote $ toProgramName fixNKey
+
                let (fixNTerm, fixNType) = if arity == 1 then Function.fixAndType else Function.fixNAndType arity (void fixBy)
                    var :: PLC.VarDecl TyName Name (Provenance a)
                    var = PLC.VarDecl NoProvenance (NoProvenance <$ name) (NoProvenance <$ fixNType)
-
                defineTerm key (PLC.Def var (NoProvenance <$ fixNTerm, Strict)) mempty
+
                defineTerm fixNKey (PLC.Def var (NoProvenance <$ fixNTerm, Strict)) (Set.singleton fixByKey)

                      
                pure $ PIR.mkVar p0 var

                      

                      
-- | We generate some shared definitions compilation, this datatype
-- defines the "keys" for those definitions.
-
data SharedName = FixpointCombinator Integer deriving (Show, Eq, Ord)
+
data SharedName =
+
    FixpointCombinator Integer
+
    | FixBy
+
    deriving (Show, Eq, Ord)

                      
toProgramName :: SharedName -> Quote (PLC.Name ())
toProgramName (FixpointCombinator n) = freshName () ("fix" <> T.pack (show n))
+
toProgramName FixBy = freshName () "fixBy"
(program 1.0.0
  [
    (lam
-
      fix2_i0
-
      (all a_i0 (type) (all b_i0 (type) (all a_i0 (type) (all b_i0 (type) (fun (all Q_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)) (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)))) (all R_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) R_i1)) R_i1)))))))
+
      fixBy_i0
+
      (all F_i0 (fun (type) (type)) (fun (fun (all Q_i0 (type) (fun [F_i2 Q_i1] Q_i1)) (all Q_i0 (type) (fun [F_i2 Q_i1] Q_i1))) (fun (all Q_i0 (type) (fun [F_i2 Q_i1] [F_i2 Q_i1])) (all Q_i0 (type) (fun [F_i2 Q_i1] Q_i1)))))
      [
-
        [
+
        (lam
+
          fix2_i0
+
          (all a_i0 (type) (all b_i0 (type) (all a_i0 (type) (all b_i0 (type) (fun (all Q_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)) (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)))) (all R_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) R_i1)) R_i1)))))))
          [
-
            {
-
              (abs
-
                Nat_i0
-
                (type)
-
                (lam
-
                  Zero_i0
-
                  Nat_i2
-
                  (lam
-
                    Suc_i0
-
                    (fun Nat_i3 Nat_i3)
+
            [
+
              [
+
                {
+
                  (abs
+
                    Nat_i0
+
                    (type)
                    (lam
-
                      match_Nat_i0
-
                      (fun Nat_i4 (all out_Nat_i0 (type) (fun out_Nat_i1 (fun (fun Nat_i5 out_Nat_i1) out_Nat_i1))))
-
                      [
-
                        [
+
                      Zero_i0
+
                      Nat_i2
+
                      (lam
+
                        Suc_i0
+
                        (fun Nat_i3 Nat_i3)
+
                        (lam
+
                          match_Nat_i0
+
                          (fun Nat_i4 (all out_Nat_i0 (type) (fun out_Nat_i1 (fun (fun Nat_i5 out_Nat_i1) out_Nat_i1))))
                          [
-
                            {
-
                              (abs
-
                                Bool_i0
-
                                (type)
-
                                (lam
-
                                  True_i0
-
                                  Bool_i2
-
                                  (lam
-
                                    False_i0
-
                                    Bool_i3
+
                            [
+
                              [
+
                                {
+
                                  (abs
+
                                    Bool_i0
+
                                    (type)
                                    (lam
-
                                      match_Bool_i0
-
                                      (fun Bool_i4 (all out_Bool_i0 (type) (fun out_Bool_i1 (fun out_Bool_i1 out_Bool_i1))))
-
                                      [
+
                                      True_i0
+
                                      Bool_i2
+
                                      (lam
+
                                        False_i0
+
                                        Bool_i3
                                        (lam
-
                                          three_i0
-
                                          Nat_i9
+
                                          match_Bool_i0
+
                                          (fun Bool_i4 (all out_Bool_i0 (type) (fun out_Bool_i1 (fun out_Bool_i1 out_Bool_i1))))
                                          [
                                            (lam
-
                                              tup_i0
-
                                              (all r_i0 (type) (fun (fun (fun Nat_i11 Bool_i7) (fun (fun Nat_i11 Bool_i7) r_i1)) r_i1))
+
                                              three_i0
+
                                              Nat_i9
                                              [
                                                (lam
-
                                                  even_i0
-
                                                  (fun Nat_i11 Bool_i7)
-
                                                  [ even_i1 three_i3 ]
-
                                                )
-
                                                [
-
                                                  {
-
                                                    tup_i1 (fun Nat_i10 Bool_i6)
-
                                                  }
-
                                                  (lam
-
                                                    arg_0_i0
-
                                                    (fun Nat_i11 Bool_i7)
+
                                                  tup_i0
+
                                                  (all r_i0 (type) (fun (fun (fun Nat_i11 Bool_i7) (fun (fun Nat_i11 Bool_i7) r_i1)) r_i1))
+
                                                  [
                                                    (lam
-
                                                      arg_1_i0
-
                                                      (fun Nat_i12 Bool_i8)
-
                                                      arg_0_i2
+
                                                      even_i0
+
                                                      (fun Nat_i11 Bool_i7)
+
                                                      [ even_i1 three_i3 ]
                                                    )
-
                                                  )
-
                                                ]
-
                                              ]
-
                                            )
-
                                            [
-
                                              {
-
                                                {
+
                                                    [
+
                                                      {
+
                                                        tup_i1
+
                                                        (fun Nat_i10 Bool_i6)
+
                                                      }
+
                                                      (lam
+
                                                        arg_0_i0
+
                                                        (fun Nat_i11 Bool_i7)
+
                                                        (lam
+
                                                          arg_1_i0
+
                                                          (fun Nat_i12 Bool_i8)
+
                                                          arg_0_i2
+
                                                        )
+
                                                      )
+
                                                    ]
+
                                                  ]
+
                                                )
+
                                                [
                                                  {
-
                                                    { fix2_i10 Nat_i9 } Bool_i5
+
                                                    {
+
                                                      {
+
                                                        { fix2_i10 Nat_i9 }
+
                                                        Bool_i5
+
                                                      }
+
                                                      Nat_i9
+
                                                    }
+
                                                    Bool_i5
                                                  }
-
                                                  Nat_i9
-
                                                }
-
                                                Bool_i5
-
                                              }
-
                                              (abs
-
                                                Q_i0
-
                                                (type)
-
                                                (lam
-
                                                  choose_i0
-
                                                  (fun (fun Nat_i11 Bool_i7) (fun (fun Nat_i11 Bool_i7) Q_i2))
-
                                                  (lam
-
                                                    even_i0
-
                                                    (fun Nat_i12 Bool_i8)
+
                                                  (abs
+
                                                    Q_i0
+
                                                    (type)
                                                    (lam
-
                                                      odd_i0
-
                                                      (fun Nat_i13 Bool_i9)
-
                                                      [
-
                                                        [
-
                                                          choose_i3
-
                                                          (lam
-
                                                            n_i0
-
                                                            Nat_i14
-
                                                            [
-
                                                              [
-
                                                                {
-
                                                                  [
-
                                                                    match_Nat_i11
-
                                                                    n_i1
-
                                                                  ]
-
                                                                  Bool_i10
-
                                                                }
-
                                                                True_i9
-
                                                              ]
-
                                                              (lam
-
                                                                pred_i0
-
                                                                Nat_i15
-
                                                                [
-
                                                                  odd_i3 pred_i1
-
                                                                ]
-
                                                              )
-
                                                            ]
-
                                                          )
-
                                                        ]
+
                                                      choose_i0
+
                                                      (fun (fun Nat_i11 Bool_i7) (fun (fun Nat_i11 Bool_i7) Q_i2))
+
                                                      (lam
+
                                                        even_i0
+
                                                        (fun Nat_i12 Bool_i8)
                                                        (lam
-
                                                          n_i0
-
                                                          Nat_i14
+
                                                          odd_i0
+
                                                          (fun Nat_i13 Bool_i9)
                                                          [
                                                            [
-
                                                              {
+
                                                              choose_i3
(abs
-
  out_Bool_90
+
  out_Bool_96
  (type)
-
  (lam case_True_91 out_Bool_90 (lam case_False_92 out_Bool_90 case_False_92))
+
  (lam case_True_97 out_Bool_96 (lam case_False_98 out_Bool_96 case_False_98))
)
\ No newline at end of file
(program 1.0.0
  [
    (lam
-
      fix2_i0
-
      (all a_i0 (type) (all b_i0 (type) (all a_i0 (type) (all b_i0 (type) (fun (all Q_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)) (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)))) (all R_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) R_i1)) R_i1)))))))
+
      fixBy_i0
+
      (all F_i0 (fun (type) (type)) (fun (fun (all Q_i0 (type) (fun [F_i2 Q_i1] Q_i1)) (all Q_i0 (type) (fun [F_i2 Q_i1] Q_i1))) (fun (all Q_i0 (type) (fun [F_i2 Q_i1] [F_i2 Q_i1])) (all Q_i0 (type) (fun [F_i2 Q_i1] Q_i1)))))
      [
        (lam
-
          tup_i0
-
          (all r_i0 (type) (fun (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) r_i1)) r_i1))
+
          fix2_i0
+
          (all a_i0 (type) (all b_i0 (type) (all a_i0 (type) (all b_i0 (type) (fun (all Q_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)) (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) Q_i1)))) (all R_i0 (type) (fun (fun (fun a_i5 b_i4) (fun (fun a_i3 b_i2) R_i1)) R_i1)))))))
          [
            (lam
-
              x_i0
-
              (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
-
              [ x_i1 (abs a_i0 (type) (lam x_i0 a_i2 x_i1)) ]
+
              tup_i0
+
              (all r_i0 (type) (fun (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) r_i1)) r_i1))
+
              [
+
                (lam
+
                  x_i0
+
                  (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                  [ x_i1 (abs a_i0 (type) (lam x_i0 a_i2 x_i1)) ]
+
                )
+
                [
+
                  {
+
                    tup_i1
+
                    (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                  }
+
                  (lam
+
                    arg_0_i0
+
                    (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                    (lam
+
                      arg_1_i0
+
                      (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                      arg_0_i2
+
                    )
+
                  )
+
                ]
+
              ]
            )
            [
              {
-
                tup_i1
-
                (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                {
+
                  {
+
                    { fix2_i1 (all a_i0 (type) (fun a_i1 a_i1)) }
+
                    (all a_i0 (type) (fun a_i1 a_i1))
+
                  }
+
                  (all a_i0 (type) (fun a_i1 a_i1))
+
                }
+
                (all a_i0 (type) (fun a_i1 a_i1))
              }
-
              (lam
-
                arg_0_i0
-
                (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
              (abs
+
                Q_i0
+
                (type)
                (lam
-
                  arg_1_i0
-
                  (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
-
                  arg_0_i2
+
                  choose_i0
+
                  (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) Q_i2))
+
                  (lam
+
                    x_i0
+
                    (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                    (lam
+
                      y_i0
+
                      (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                      [
+
                        [
+
                          choose_i3
+
                          (lam
+
                            arg_i0
+
                            (all a_i0 (type) (fun a_i1 a_i1))
+
                            [ y_i2 (abs a_i0 (type) (lam x_i0 a_i2 x_i1)) ]
+
                          )
+
                        ]
+
                        (lam
+
                          arg_i0
+
                          (all a_i0 (type) (fun a_i1 a_i1))
+
                          (abs a_i0 (type) (lam x_i0 a_i2 x_i1))
+
                        )
+
                      ]
+
                    )
+
                  )
                )
              )
            ]
          ]
        )
-
        [
-
          {
-
            {
-
              {
-
                { fix2_i1 (all a_i0 (type) (fun a_i1 a_i1)) }
-
                (all a_i0 (type) (fun a_i1 a_i1))
-
              }
-
              (all a_i0 (type) (fun a_i1 a_i1))
-
            }
-
            (all a_i0 (type) (fun a_i1 a_i1))
-
          }
+
        (abs
+
          a_i0
+
          (type)
          (abs
-
            Q_i0
+
            b_i0
            (type)
-
            (lam
-
              choose_i0
-
              (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) (fun (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1))) Q_i2))
-
              (lam
-
                x_i0
-
                (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
            (abs
+
              a_i0
+
              (type)
+
              (abs
+
                b_i0
+
                (type)
                (lam
-
                  y_i0
-
                  (fun (all a_i0 (type) (fun a_i1 a_i1)) (all a_i0 (type) (fun a_i1 a_i1)))
+
                  f_i0
+
                  (all Q_i0 (type) (fun (fun (fun a_i6 b_i5) (fun (fun a_i4 b_i3) Q_i1)) (fun (fun a_i6 b_i5) (fun (fun a_i4 b_i3) Q_i1))))
                  [
                    [
-
                      choose_i3
+
                      {
+
                        fixBy_i6
+
                        (lam X_i0 (type) (fun (fun a_i6 b_i5) (fun (fun a_i4 b_i3) X_i1)))
+
                      }
                      (lam
-
                        arg_i0
-
                        (all a_i0 (type) (fun a_i1 a_i1))
-
                        [ y_i2 (abs a_i0 (type) (lam x_i0 a_i2 x_i1)) ]
+
                        k_i0
+
                        (all Q_i0 (type) (fun (fun (fun a_i7 b_i6) (fun (fun a_i5 b_i4) Q_i1)) Q_i1))
+
                        (abs
+
                          S_i0
+
                          (type)
+
                          (lam
+
                            h_i0
+
                            (fun (fun a_i8 b_i7) (fun (fun a_i6 b_i5) S_i2))
+
                            [
+
                              [
+
                                h_i1
+
                                (lam
+
                                  x_i0
+
                                  a_i9
+
                                  [
+
                                    { k_i4 b_i8 }
+
                                    (lam
+
                                      f_0_i0
+
                                      (fun a_i10 b_i9)
+
                                      (lam
+
                                        f_1_i0 (fun a_i9 b_i8) [ f_0_i2 x_i3 ]
+
                                      )
+
                                    )
+
                                  ]
+
                                )
+
                              ]
+
                              (lam
+
                                x_i0
+
                                a_i7
+
                                [
+
                                  { k_i4 b_i6 }
+
                                  (lam
+
                                    f_0_i0
+
                                    (fun a_i10 b_i9)
+
                                    (lam f_1_i0 (fun a_i9 b_i8) [ f_1_i1 x_i3 ])
+
                                  )
+
                                ]
+
                              )
+
                            ]
+
                          )
+
                        )
                      )
                    ]
-
                    (lam
-
                      arg_i0
-
                      (all a_i0 (type) (fun a_i1 a_i1))
-
                      (abs a_i0 (type) (lam x_i0 a_i2 x_i1))
-
                    )
+
                    f_i1
                  ]
                )
              )
            )
          )
-
        ]
+
        )
      ]
(iwrap
-
  (lam rec_70 (fun (fun (type) (type)) (type)) (lam f_71 (fun (type) (type)) [f_71 [rec_70 f_71]]))
-
  (lam EmptyRose_72 (type) (all out_EmptyRose_73 (type) (fun (fun [List_27 EmptyRose_72] out_EmptyRose_73) out_EmptyRose_73)))
+
  (lam rec_111 (fun (fun (type) (type)) (type)) (lam f_112 (fun (type) (type)) [f_112 [rec_111 f_112]]))
+
  (lam EmptyRose_113 (type) (all out_EmptyRose_114 (type) (fun (fun [List_68 EmptyRose_113] out_EmptyRose_114) out_EmptyRose_114)))
  (abs
-
    out_EmptyRose_74
+
    out_EmptyRose_115
    (type)
    (lam
-
      case_EmptyRose_75
-
      (fun [List_27 (ifix (lam rec_76 (fun (fun (type) (type)) (type)) (lam f_77 (fun (type) (type)) [f_77 [rec_76 f_77]])) (lam EmptyRose_78 (type) (all out_EmptyRose_79 (type) (fun (fun [List_27 EmptyRose_78] out_EmptyRose_79) out_EmptyRose_79))))] out_EmptyRose_74)
+
      case_EmptyRose_116
+
      (fun [List_68 (ifix (lam rec_117 (fun (fun (type) (type)) (type)) (lam f_118 (fun (type) (type)) [f_118 [rec_117 f_118]])) (lam EmptyRose_119 (type) (all out_EmptyRose_120 (type) (fun (fun [List_68 EmptyRose_119] out_EmptyRose_120) out_EmptyRose_120))))] out_EmptyRose_115)
      [
-
        case_EmptyRose_75
+
        case_EmptyRose_116
        (iwrap
-
          (lam List_107 (fun (type) (type)) (lam a_108 (type) (all out_List_109 (type) (fun out_List_109 (fun (fun a_108 (fun [List_107 a_108] out_List_109)) out_List_109)))))
-
          a_100
+
          (lam List_148 (fun (type) (type)) (lam a_149 (type) (all out_List_150 (type) (fun out_List_150 (fun (fun a_149 (fun [List_148 a_149] out_List_150)) out_List_150)))))
+
          a_141
          (abs
-
            out_List_110
+
            out_List_151
            (type)
            (lam
-
              case_Nil_111
-
              out_List_110
+
              case_Nil_152
+
              out_List_151
              (lam
-
                case_Cons_112
-
                (fun a_100 (fun [(lam a_113 (type) (ifix (lam List_114 (fun (type) (type)) (lam a_115 (type) (all out_List_116 (type) (fun out_List_116 (fun (fun a_115 (fun [List_114 a_115] out_List_116)) out_List_116))))) a_113)) a_100] out_List_110))
+
                case_Cons_153
+
                (fun a_141 (fun [(lam a_154 (type) (ifix (lam List_155 (fun (type) (type)) (lam a_156 (type) (all out_List_157 (type) (fun out_List_157 (fun (fun a_156 (fun [List_155 a_156] out_List_157)) out_List_157))))) a_154)) a_141] out_List_151))
                [
                  [
-
                    case_Cons_112
+
                    case_Cons_153
                    (iwrap
-
                      (lam rec_70 (fun (fun (type) (type)) (type)) (lam f_71 (fun (type) (type)) [f_71 [rec_70 f_71]]))
-
                      (lam EmptyRose_72 (type) (all out_EmptyRose_73 (type) (fun (fun [List_27 EmptyRose_72] out_EmptyRose_73) out_EmptyRose_73)))
+
                      (lam rec_111 (fun (fun (type) (type)) (type)) (lam f_112 (fun (type) (type)) [f_112 [rec_111 f_112]]))
+
                      (lam EmptyRose_113 (type) (all out_EmptyRose_114 (type) (fun (fun [List_68 EmptyRose_113] out_EmptyRose_114) out_EmptyRose_114)))
                      (abs
-
                        out_EmptyRose_74
+
                        out_EmptyRose_115
                        (type)
                        (lam
-
                          case_EmptyRose_75
-
                          (fun [List_27 (ifix (lam rec_76 (fun (fun (type) (type)) (type)) (lam f_77 (fun (type) (type)) [f_77 [rec_76 f_77]])) (lam EmptyRose_78 (type) (all out_EmptyRose_79 (type) (fun (fun [List_27 EmptyRose_78] out_EmptyRose_79) out_EmptyRose_79))))] out_EmptyRose_74)
+
                          case_EmptyRose_116
+
                          (fun [List_68 (ifix (lam rec_117 (fun (fun (type) (type)) (type)) (lam f_118 (fun (type) (type)) [f_118 [rec_117 f_118]])) (lam EmptyRose_119 (type) (all out_EmptyRose_120 (type) (fun (fun [List_68 EmptyRose_119] out_EmptyRose_120) out_EmptyRose_120))))] out_EmptyRose_115)
                          [
-
                            case_EmptyRose_75
+
                            case_EmptyRose_116
                            (iwrap
-
                              (lam List_90 (fun (type) (type)) (lam a_91 (type) (all out_List_92 (type) (fun out_List_92 (fun (fun a_91 (fun [List_90 a_91] out_List_92)) out_List_92)))))
-
                              a_89
+
                              (lam List_131 (fun (type) (type)) (lam a_132 (type) (all out_List_133 (type) (fun out_List_133 (fun (fun a_132 (fun [List_131 a_132] out_List_133)) out_List_133)))))
+
                              a_130
                              (abs
-
                                out_List_93
+
                                out_List_134
                                (type)
                                (lam
-
                                  case_Nil_94
-
                                  out_List_93
+
                                  case_Nil_135
+
                                  out_List_134
                                  (lam
-
                                    case_Cons_95
-
                                    (fun a_89 (fun [(lam a_96 (type) (ifix (lam List_97 (fun (type) (type)) (lam a_98 (type) (all out_List_99 (type) (fun out_List_99 (fun (fun a_98 (fun [List_97 a_98] out_List_99)) out_List_99))))) a_96)) a_89] out_List_93))
-
                                    case_Nil_94
+
                                    case_Cons_136
+
                                    (fun a_130 (fun [(lam a_137 (type) (ifix (lam List_138 (fun (type) (type)) (lam a_139 (type) (all out_List_140 (type) (fun out_List_140 (fun (fun a_139 (fun [List_138 a_139] out_List_140)) out_List_140))))) a_137)) a_130] out_List_134))
+
                                    case_Nil_135
                                  )
                                )
                              )
                    )
                  ]
                  (iwrap
-
                    (lam List_107 (fun (type) (type)) (lam a_108 (type) (all out_List_109 (type) (fun out_List_109 (fun (fun a_108 (fun [List_107 a_108] out_List_109)) out_List_109)))))
-
                    a_100
+
                    (lam List_148 (fun (type) (type)) (lam a_149 (type) (all out_List_150 (type) (fun out_List_150 (fun (fun a_149 (fun [List_148 a_149] out_List_150)) out_List_150)))))
+
                    a_141
                    (abs
-
                      out_List_110
+
                      out_List_151
                      (type)
                      (lam
-
                        case_Nil_111
-
                        out_List_110
+
                        case_Nil_152
+
                        out_List_151
                        (lam
-
                          case_Cons_112
-
                          (fun a_100 (fun [(lam a_113 (type) (ifix (lam List_114 (fun (type) (type)) (lam a_115 (type) (all out_List_116 (type) (fun out_List_116 (fun (fun a_115 (fun [List_114 a_115] out_List_116)) out_List_116))))) a_113)) a_100] out_List_110))
+
                          case_Cons_153
+
                          (fun a_141 (fun [(lam a_154 (type) (ifix (lam List_155 (fun (type) (type)) (lam a_156 (type) (all out_List_157 (type) (fun out_List_157 (fun (fun a_156 (fun [List_155 a_156] out_List_157)) out_List_157))))) a_154)) a_141] out_List_151))
                          [
                            [
-
                              case_Cons_112
+
                              case_Cons_153
                              (iwrap
-
                                (lam rec_70 (fun (fun (type) (type)) (type)) (lam f_71 (fun (type) (type)) [f_71 [rec_70 f_71]]))
-
                                (lam EmptyRose_72 (type) (all out_EmptyRose_73 (type) (fun (fun [List_27 EmptyRose_72] out_EmptyRose_73) out_EmptyRose_73)))
+
                                (lam rec_111 (fun (fun (type) (type)) (type)) (lam f_112 (fun (type) (type)) [f_112 [rec_111 f_112]]))
+
                                (lam EmptyRose_113 (type) (all out_EmptyRose_114 (type) (fun (fun [List_68 EmptyRose_113] out_EmptyRose_114) out_EmptyRose_114)))
                                (abs
-
                                  out_EmptyRose_74
+
                                  out_EmptyRose_115
                                  (type)
                                  (lam
-
                                    case_EmptyRose_75
-
                                    (fun [List_27 (ifix (lam rec_76 (fun (fun (type) (type)) (type)) (lam f_77 (fun (type) (type)) [f_77 [rec_76 f_77]])) (lam EmptyRose_78 (type) (all out_EmptyRose_79 (type) (fun (fun [List_27 EmptyRose_78] out_EmptyRose_79) out_EmptyRose_79))))] out_EmptyRose_74)
+
                                    case_EmptyRose_116
+
                                    (fun [List_68 (ifix (lam rec_117 (fun (fun (type) (type)) (type)) (lam f_118 (fun (type) (type)) [f_118 [rec_117 f_118]])) (lam EmptyRose_119 (type) (all out_EmptyRose_120 (type) (fun (fun [List_68 EmptyRose_119] out_EmptyRose_120) out_EmptyRose_120))))] out_EmptyRose_115)
                                    [
-
                                      case_EmptyRose_75
+
                                      case_EmptyRose_116
                                      (iwrap
-
                                        (lam List_90 (fun (type) (type)) (lam a_91 (type) (all out_List_92 (type) (fun out_List_92 (fun (fun a_91 (fun [List_90 a_91] out_List_92)) out_List_92)))))
-
                                        a_89
+
                                        (lam List_131 (fun (type) (type)) (lam a_132 (type) (all out_List_133 (type) (fun out_List_133 (fun (fun a_132 (fun [List_131 a_132] out_List_133)) out_List_133)))))
+
                                        a_130
                                        (abs
-
                                          out_List_93
+
                                          out_List_134
                                          (type)
                                          (lam
-
                                            case_Nil_94
-
                                            out_List_93
+
                                            case_Nil_135
+
                                            out_List_134
                                            (lam
-
                                              case_Cons_95
-
                                              (fun a_89 (fun [(lam a_96 (type) (ifix (lam List_97 (fun (type) (type)) (lam a_98 (type) (all out_List_99 (type) (fun out_List_99 (fun (fun a_98 (fun [List_97 a_98] out_List_99)) out_List_99))))) a_96)) a_89] out_List_93))
-
                                              case_Nil_94
+
                                              case_Cons_136
+
                                              (fun a_130 (fun [(lam a_137 (type) (ifix (lam List_138 (fun (type) (type)) (lam a_139 (type) (all out_List_140 (type) (fun out_List_140 (fun (fun a_139 (fun [List_138 a_139] out_List_140)) out_List_140))))) a_137)) a_130] out_List_134))
+
                                              case_Nil_135
                                            )
                                          )
                                        )
                              )
                            ]
                            (iwrap
-
                              (lam List_90 (fun (type) (type)) (lam a_91 (type) (all out_List_92 (type) (fun out_List_92 (fun (fun a_91 (fun [List_90 a_91] out_List_92)) out_List_92)))))
-
                              a_89
+
                              (lam List_131 (fun (type) (type)) (lam a_132 (type) (all out_List_133 (type) (fun out_List_133 (fun (fun a_132 (fun [List_131 a_132] out_List_133)) out_List_133)))))
+
                              a_130
                              (abs
-
                                out_List_93
+
                                out_List_134
                                (type)
                                (lam
-
                                  case_Nil_94
-
                                  out_List_93
+
                                  case_Nil_135
+
                                  out_List_134
                                  (lam
-
                                    case_Cons_95
-
                                    (fun a_89 (fun [(lam a_96 (type) (ifix (lam List_97 (fun (type) (type)) (lam a_98 (type) (all out_List_99 (type) (fun out_List_99 (fun (fun a_98 (fun [List_97 a_98] out_List_99)) out_List_99))))) a_96)) a_89] out_List_93))
-
                                    case_Nil_94
+
                                    case_Cons_136
+
                                    (fun a_130 (fun [(lam a_137 (type) (ifix (lam List_138 (fun (type) (type)) (lam a_139 (type) (all out_List_140 (type) (fun out_List_140 (fun (fun a_139 (fun [List_138 a_139] out_List_140)) out_List_140))))) a_137)) a_130] out_List_134))
+
                                    case_Nil_135
                                  )
                                )
                              )
(abs
-
  out_Bool_62
+
  out_Bool_103
  (type)
-
  (lam case_True_63 out_Bool_62 (lam case_False_64 out_Bool_62 case_False_64))
+
  (lam
+
    case_True_104 out_Bool_103 (lam case_False_105 out_Bool_103 case_False_105)
+
  )
)
\ No newline at end of file
(abs
-
  out_Bool_59
+
  out_Bool_100
  (type)
-
  (lam case_True_60 out_Bool_59 (lam case_False_61 out_Bool_59 case_True_60))
+
  (lam
+
    case_True_101 out_Bool_100 (lam case_False_102 out_Bool_100 case_True_101)
+
  )
)
\ No newline at end of file
(abs
-
  out_Bool_145
+
  out_Bool_186
  (type)
  (lam
-
    case_True_146 out_Bool_145 (lam case_False_147 out_Bool_145 case_True_146)
+
    case_True_187 out_Bool_186 (lam case_False_188 out_Bool_186 case_True_187)
  )
)
\ No newline at end of file