-- editorconfig-checker-disable-file
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- | Functions for compiling PIR recursive let-bound functions into PLC.
module PlutusIR.Compiler.Recursion where

import PlutusIR
import PlutusIR.Compiler.Definitions
import PlutusIR.Compiler.Provenance
import PlutusIR.Compiler.Types
import PlutusIR.Error
import PlutusIR.MkPir qualified as PIR

import Control.Monad
import Control.Monad.Error.Lens
import Control.Monad.Trans

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

import PlutusCore qualified as PLC
import PlutusCore.MkPlc qualified as PLC
import PlutusCore.Quote
import PlutusCore.StdLib.Data.Function qualified as Function
import PlutusCore.StdLib.Meta.Data.Tuple qualified as Tuple

{- Note [Recursive lets]
We need to define these with a fixpoint. We can derive a fixpoint operator for values
already.

However, we also need to work out how to encode recursion over multiple values simultaneously.
The answer is simple - we pass them through as a tuple.

Overall, the translation looks like this. We convert this:

let rec
  f_1 : t_1 = b_1
  ..
  f_i : t_i = b_i
in
  result

into this:

(\tuple : forall r . (t_1 -> .. -> t_i -> r) -> r .
  let
    f_1 = _1 tuple
    ..
    f_i = _i tuple
  in
    result
)
($fixN i$ (\choose f_1 ... f_i . choose b_1 ... b_i))

where _i is the accessor for the ith component of a tuple.

This scheme is a little complicated - why don't we just pass a function directly to the
fixed tuple that consumes the values? Why do the second round of let-binding?

The answer is that in order to use the tuple we have to provide a result type. If we used
it directly, we would have to provide the type of the *result* term, which we may not know.
Here we merely have to provide it with the types of the f_is, which we *do* know.
-}

 -- See Note [Recursive lets]
-- | Compile a mutually recursive list of var decls bound in a body.
compileRecTerms
    :: Compiling m e uni fun a
    => PIRTerm uni fun a
    -> NonEmpty (TermDef TyName Name uni fun (Provenance a))
    -> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecTerms :: forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
PIRTerm uni fun a
-> NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
compileRecTerms PIRTerm uni fun a
body NonEmpty (TermDef TyName Name uni fun (Provenance a))
bs = do
    Provenance a
p <- m (Provenance a)
-> DefT SharedName uni fun (Provenance a) m (Provenance a)
forall (m :: * -> *) a.
Monad m =>
m a -> DefT SharedName uni fun (Provenance a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing
    Tuple (Term TyName Name uni fun) uni (Provenance a)
fixpoint <- NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Tuple (Term TyName Name uni fun) uni (Provenance a))
forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Tuple (Term TyName Name uni fun) uni (Provenance a))
mkFixpoint NonEmpty (TermDef TyName Name uni fun (Provenance a))
bs
    Provenance a
-> [Name]
-> Tuple (Term TyName Name uni fun) uni (Provenance a)
-> PIRTerm uni fun a
-> DefT SharedName uni fun (Provenance a) m (PIRTerm uni fun a)
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> [Name] -> Tuple term uni ann -> term ann -> m (term ann)
Tuple.bindTuple Provenance a
p (VarDecl TyName Name uni (Provenance a) -> Name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
PIR._varDeclName (VarDecl TyName Name uni (Provenance a) -> Name)
-> (TermDef TyName Name uni fun (Provenance a)
    -> VarDecl TyName Name uni (Provenance a))
-> TermDef TyName Name uni fun (Provenance a)
-> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermDef TyName Name uni fun (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall var val. Def var val -> var
PIR.defVar (TermDef TyName Name uni fun (Provenance a) -> Name)
-> [TermDef TyName Name uni fun (Provenance a)] -> [Name]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> [TermDef TyName Name uni fun (Provenance a)]
forall a. NonEmpty a -> [a]
toList NonEmpty (TermDef TyName Name uni fun (Provenance a))
bs) Tuple (Term TyName Name uni fun) uni (Provenance a)
fixpoint PIRTerm uni fun a
body

-- | Given a list of var decls, create a tuples of values that computes their mutually recursive fixpoint.
mkFixpoint
    :: forall m e uni fun a . Compiling m e uni fun a
    => NonEmpty (TermDef TyName Name uni fun (Provenance a))
    -> DefT SharedName uni fun (Provenance a) m (Tuple.Tuple (Term TyName Name uni fun) uni (Provenance a))
mkFixpoint :: forall (m :: * -> *) e (uni :: * -> *) fun a.
Compiling m e uni fun a =>
NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Tuple (Term TyName Name uni fun) uni (Provenance a))
mkFixpoint NonEmpty (TermDef TyName Name uni fun (Provenance a))
bs = do
    Provenance a
p0 <- m (Provenance a)
-> DefT SharedName uni fun (Provenance a) m (Provenance a)
forall (m :: * -> *) a.
Monad m =>
m a -> DefT SharedName uni fun (Provenance a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m (Provenance a)
forall (uni :: * -> *) fun a (m :: * -> *).
MonadReader (CompilationCtx uni fun a) m =>
m (Provenance a)
getEnclosing

    NonEmpty
  (FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
funs <- NonEmpty (TermDef TyName Name uni fun (Provenance a))
-> (TermDef TyName Name uni fun (Provenance a)
    -> DefT
         SharedName
         uni
         fun
         (Provenance a)
         m
         (FunctionDef
            (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (NonEmpty
        (FunctionDef
           (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty (TermDef TyName Name uni fun (Provenance a))
bs ((TermDef TyName Name uni fun (Provenance a)
  -> DefT
       SharedName
       uni
       fun
       (Provenance a)
       m
       (FunctionDef
          (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
 -> DefT
      SharedName
      uni
      fun
      (Provenance a)
      m
      (NonEmpty
         (FunctionDef
            (Term TyName Name uni fun) TyName Name uni fun (Provenance a))))
-> (TermDef TyName Name uni fun (Provenance a)
    -> DefT
         SharedName
         uni
         fun
         (Provenance a)
         m
         (FunctionDef
            (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (NonEmpty
        (FunctionDef
           (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
forall a b. (a -> b) -> a -> b
$ \(PIR.Def (PIR.VarDecl Provenance a
p Name
name Type TyName uni (Provenance a)
ty) Term TyName Name uni fun (Provenance a)
term) ->
        case Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> Term TyName Name uni fun (Provenance a)
-> Maybe
     (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall {k} ann name tyname (uni :: * -> *) (term :: * -> *)
       (fun :: k).
ann
-> name
-> Type tyname uni ann
-> term ann
-> Maybe (FunctionDef term tyname name uni fun ann)
PIR.mkFunctionDef Provenance a
p Name
name Type TyName uni (Provenance a)
ty Term TyName Name uni fun (Provenance a)
term of
            Just FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
fun -> FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall a. a -> DefT SharedName uni fun (Provenance a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
fun
            Maybe
  (FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
Nothing  -> m (FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall (m :: * -> *) a.
Monad m =>
m a -> DefT SharedName uni fun (Provenance a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (FunctionDef
      (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
 -> DefT
      SharedName
      uni
      fun
      (Provenance a)
      m
      (FunctionDef
         (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
-> m (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall a b. (a -> b) -> a -> b
$ AReview e (Error uni fun (Provenance a))
-> Error uni fun (Provenance a)
-> m (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall e (m :: * -> *) t x.
MonadError e m =>
AReview e t -> t -> m x
throwing AReview e (Error uni fun (Provenance a))
forall r (uni :: * -> *) fun a.
AsError r uni fun a =>
Prism' r (Error uni fun a)
Prism' e (Error uni fun (Provenance a))
_Error (Error uni fun (Provenance a)
 -> m (FunctionDef
         (Term TyName Name uni fun) TyName Name uni fun (Provenance a)))
-> Error uni fun (Provenance a)
-> m (FunctionDef
        (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
forall a b. (a -> b) -> a -> b
$ Provenance a -> Text -> Error uni fun (Provenance a)
forall (uni :: * -> *) fun a. a -> Text -> Error uni fun a
CompilationError (Type TyName uni (Provenance a) -> Provenance a
forall tyname (uni :: * -> *) ann. Type tyname uni ann -> ann
PLC.typeAnn Type TyName uni (Provenance a)
ty) Text
"Recursive values must be of function type"

    -- See Note [Extra definitions while compiling let-bindings]
    let
        arity :: Integer
arity = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ NonEmpty
  (FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
-> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty
  (FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
funs
        fixByKey :: SharedName
fixByKey = SharedName
FixBy
        fixNKey :: SharedName
fixNKey = Integer -> SharedName
FixpointCombinator Integer
arity

    let mkFixByDef :: DefT
  SharedName
  uni
  fun
  (Provenance a)
  m
  (Def
     (VarDecl TyName Name uni (Provenance a))
     (Term TyName Name uni fun (Provenance a), Strictness),
   Set SharedName)
mkFixByDef = do
          Name
name <- Quote Name -> DefT SharedName uni fun (Provenance a) m Name
forall a. Quote a -> DefT SharedName uni fun (Provenance a) m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote Name -> DefT SharedName uni fun (Provenance a) m Name)
-> Quote Name -> DefT SharedName uni fun (Provenance a) m Name
forall a b. (a -> b) -> a -> b
$ SharedName -> Quote Name
toProgramName SharedName
fixByKey
          let (Term TyName Name uni fun ()
fixByTerm, Type TyName uni ()
fixByType) = (Term TyName Name uni fun (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
Function.fixByAndType
          (Def
   (VarDecl TyName Name uni (Provenance a))
   (Term TyName Name uni fun (Provenance a), Strictness),
 Set SharedName)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Def
        (VarDecl TyName Name uni (Provenance a))
        (Term TyName Name uni fun (Provenance a), Strictness),
      Set SharedName)
forall a. a -> DefT SharedName uni fun (Provenance a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni (Provenance a)
-> (Term TyName Name uni fun (Provenance a), Strictness)
-> Def
     (VarDecl TyName Name uni (Provenance a))
     (Term TyName Name uni fun (Provenance a), Strictness)
forall var val. var -> val -> Def var val
PLC.Def (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
PLC.VarDecl Provenance a
forall a. Provenance a
noProvenance Name
name (Provenance a
forall a. Provenance a
noProvenance Provenance a
-> Type TyName uni () -> Type TyName uni (Provenance a)
forall a b. a -> Type TyName uni b -> Type TyName uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
fixByType)) (Provenance a
forall a. Provenance a
noProvenance Provenance a
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun (Provenance a)
forall a b.
a -> Term TyName Name uni fun b -> Term TyName Name uni fun a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term TyName Name uni fun ()
fixByTerm, Strictness
Strict), Set SharedName
forall a. Monoid a => a
mempty)

    let mkFixNDef :: DefT
  SharedName
  uni
  fun
  (Provenance a)
  m
  (Def
     (VarDecl TyName Name uni (Provenance a))
     (Term TyName Name uni fun (Provenance a), Strictness),
   Set SharedName)
mkFixNDef = do
          Name
name <- Quote Name -> DefT SharedName uni fun (Provenance a) m Name
forall a. Quote a -> DefT SharedName uni fun (Provenance a) m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote Name -> DefT SharedName uni fun (Provenance a) m Name)
-> Quote Name -> DefT SharedName uni fun (Provenance a) m Name
forall a b. (a -> b) -> a -> b
$ SharedName -> Quote Name
toProgramName SharedName
fixNKey
          ((Term TyName Name uni fun ()
fixNTerm, Type TyName uni ()
fixNType), Set SharedName
fixNDeps) <-
              if Integer
arity Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1
                  then ((Term TyName Name uni fun (), Type TyName uni ()), Set SharedName)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     ((Term TyName Name uni fun (), Type TyName uni ()), Set SharedName)
forall a. a -> DefT SharedName uni fun (Provenance a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Term TyName Name uni fun (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
Function.fixAndType, Set SharedName
forall a. Monoid a => a
mempty)
                  -- fixN depends on fixBy
                  else do
                      Term TyName Name uni fun (Provenance a)
fixBy <- Provenance a
-> SharedName
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (TermDefWithStrictness uni fun (Provenance a), Set SharedName)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Term TyName Name uni fun (Provenance a))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann
-> key
-> m (TermDefWithStrictness uni fun ann, Set key)
-> m (Term TyName Name uni fun ann)
lookupOrDefineTerm Provenance a
p0 SharedName
fixByKey DefT
  SharedName
  uni
  fun
  (Provenance a)
  m
  (TermDefWithStrictness uni fun (Provenance a), Set SharedName)
forall {a} {a}.
DefT
  SharedName
  uni
  fun
  (Provenance a)
  m
  (Def
     (VarDecl TyName Name uni (Provenance a))
     (Term TyName Name uni fun (Provenance a), Strictness),
   Set SharedName)
mkFixByDef
                      ((Term TyName Name uni fun (), Type TyName uni ()), Set SharedName)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     ((Term TyName Name uni fun (), Type TyName uni ()), Set SharedName)
forall a. a -> DefT SharedName uni fun (Provenance a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer
-> Term TyName Name uni fun ()
-> (Term TyName Name uni fun (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> (term (), Type TyName uni ())
Function.fixNAndType Integer
arity (Term TyName Name uni fun (Provenance a)
-> Term TyName Name uni fun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term TyName Name uni fun (Provenance a)
fixBy), SharedName -> Set SharedName
forall a. a -> Set a
Set.singleton SharedName
fixByKey)
          (Def
   (VarDecl TyName Name uni (Provenance a))
   (Term TyName Name uni fun (Provenance a), Strictness),
 Set SharedName)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Def
        (VarDecl TyName Name uni (Provenance a))
        (Term TyName Name uni fun (Provenance a), Strictness),
      Set SharedName)
forall a. a -> DefT SharedName uni fun (Provenance a) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni (Provenance a)
-> (Term TyName Name uni fun (Provenance a), Strictness)
-> Def
     (VarDecl TyName Name uni (Provenance a))
     (Term TyName Name uni fun (Provenance a), Strictness)
forall var val. var -> val -> Def var val
PLC.Def (Provenance a
-> Name
-> Type TyName uni (Provenance a)
-> VarDecl TyName Name uni (Provenance a)
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
PLC.VarDecl Provenance a
forall a. Provenance a
noProvenance Name
name (Provenance a
forall a. Provenance a
noProvenance Provenance a
-> Type TyName uni () -> Type TyName uni (Provenance a)
forall a b. a -> Type TyName uni b -> Type TyName uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Type TyName uni ()
fixNType)) (Provenance a
forall a. Provenance a
noProvenance Provenance a
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun (Provenance a)
forall a b.
a -> Term TyName Name uni fun b -> Term TyName Name uni fun a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Term TyName Name uni fun ()
fixNTerm, Strictness
Strict), Set SharedName
fixNDeps)
    Term TyName Name uni fun (Provenance a)
fixN <- Provenance a
-> SharedName
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (TermDefWithStrictness uni fun (Provenance a), Set SharedName)
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Term TyName Name uni fun (Provenance a))
forall key (uni :: * -> *) fun ann (m :: * -> *).
MonadDefs key uni fun ann m =>
ann
-> key
-> m (TermDefWithStrictness uni fun ann, Set key)
-> m (Term TyName Name uni fun ann)
lookupOrDefineTerm Provenance a
p0 SharedName
fixNKey DefT
  SharedName
  uni
  fun
  (Provenance a)
  m
  (TermDefWithStrictness uni fun (Provenance a), Set SharedName)
forall {a} {a}.
DefT
  SharedName
  uni
  fun
  (Provenance a)
  m
  (Def
     (VarDecl TyName Name uni (Provenance a))
     (Term TyName Name uni fun (Provenance a), Strictness),
   Set SharedName)
mkFixNDef

    Quote (Tuple (Term TyName Name uni fun) uni (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Tuple (Term TyName Name uni fun) uni (Provenance a))
forall a. Quote a -> DefT SharedName uni fun (Provenance a) m a
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (Quote (Tuple (Term TyName Name uni fun) uni (Provenance a))
 -> DefT
      SharedName
      uni
      fun
      (Provenance a)
      m
      (Tuple (Term TyName Name uni fun) uni (Provenance a)))
-> Quote (Tuple (Term TyName Name uni fun) uni (Provenance a))
-> DefT
     SharedName
     uni
     fun
     (Provenance a)
     m
     (Tuple (Term TyName Name uni fun) uni (Provenance a))
forall a b. (a -> b) -> a -> b
$ case NonEmpty
  (FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a))
funs of
        -- Takes a list of function defs and function bodies and turns them into a Scott-encoded tuple, which
        -- happens to be exactly what we want
        FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
f :| [] -> Provenance a
-> [(Type TyName uni (Provenance a),
     Term TyName Name uni fun (Provenance a))]
-> Quote (Tuple (Term TyName Name uni fun) uni (Provenance a))
forall (term :: * -> *) (uni :: * -> *) fun (m :: * -> *) ann.
(TermLike term TyName Name uni fun, MonadQuote m) =>
ann -> [(Type TyName uni ann, term ann)] -> m (Tuple term uni ann)
Tuple.getSpineToTuple Provenance a
p0 [(FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
-> Type TyName uni (Provenance a)
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> Type tyname uni ann
PLC.functionDefToType FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
f, Provenance a
-> Term TyName Name uni fun (Provenance a)
-> FunctionDef
     (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
-> Term TyName Name uni fun (Provenance a)
forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
ann
-> term ann -> FunctionDef term TyName Name uni fun ann -> term ann
Function.getSingleFixOf Provenance a
p0 Term TyName Name uni fun (Provenance a)
fixN FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
f)]
        FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
f :| [FunctionDef
   (Term TyName Name uni fun) TyName Name uni fun (Provenance a)]
fs -> Provenance a
-> Term TyName Name uni fun (Provenance a)
-> [FunctionDef
      (Term TyName Name uni fun) TyName Name uni fun (Provenance a)]
-> Quote (Tuple (Term TyName Name uni fun) uni (Provenance a))
forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
ann
-> term ann
-> [FunctionDef term TyName Name uni fun ann]
-> Quote (Tuple term uni ann)
Function.getMutualFixOf Provenance a
p0 Term TyName Name uni fun (Provenance a)
fixN (FunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
fFunctionDef
  (Term TyName Name uni fun) TyName Name uni fun (Provenance a)
-> [FunctionDef
      (Term TyName Name uni fun) TyName Name uni fun (Provenance a)]
-> [FunctionDef
      (Term TyName Name uni fun) TyName Name uni fun (Provenance a)]
forall a. a -> [a] -> [a]
:[FunctionDef
   (Term TyName Name uni fun) TyName Name uni fun (Provenance a)]
fs)