{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
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
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
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"
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)
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
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)