Safe Haskell	None
Language	Haskell2010

PlutusCore.StdLib.Data.Function

Description

Combinators.

Synopsis

const :: TermLike term TyName Name uni fun => term ()
idFun :: TermLike term TyName Name uni fun => term ()
applyFun :: TermLike term TyName Name uni fun => term ()
selfData :: RecursiveType uni fun ()
unroll :: TermLike term TyName Name uni fun => term ()
fix :: TermLike term TyName Name uni fun => term ()
fixAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixBy :: TermLike term TyName Name uni fun => term ()
fixByAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixN :: TermLike term TyName Name uni fun => Integer -> term () -> term ()
fixNAndType :: TermLike term TyName Name uni fun => Integer -> term () -> (term (), Type TyName uni ())
data FunctionDef term tyname name uni fun ann = FunctionDef {
- _functionDefAnn :: ann
- _functionDefName :: name
- _functionDefType :: FunctionType tyname uni ann
- _functionDefTerm :: term ann
}
getMutualFixOf :: TermLike term TyName Name uni fun => ann -> term ann -> [FunctionDef term TyName Name uni fun ann] -> Quote (Tuple term uni ann)
getSingleFixOf :: TermLike term TyName Name uni fun => ann -> term ann -> FunctionDef term TyName Name uni fun ann -> term ann

Documentation

const :: TermLike term TyName Name uni fun => term () Source #

const as a PLC term.

/\(A B :: *) -> \(x : A) (y : B) -> x

idFun :: TermLike term TyName Name uni fun => term () Source #

id as a PLC term.

/\(A :: *) -> \(x : A) -> x

applyFun :: TermLike term TyName Name uni fun => term () Source #

($) as a PLC term.

/\(A B :: *) -> \(f : A -> B) (x : A) -> f x

selfData :: RecursiveType uni fun () Source #

Self as a PLC type.

fix \(self :: * -> *) (a :: *) -> self a -> a

unroll :: TermLike term TyName Name uni fun => term () Source #

unroll as a PLC term.

/\(a :: *) -> \(s : self a) -> unwrap s s

fix :: TermLike term TyName Name uni fun => term () Source #

fix as a PLC term.

/\(a b :: *) -> \(f : (a -> b) -> a -> b) ->
   unroll {a -> b} (iwrap selfF (a -> b) \(s : self (a -> b)) \(x : a) -> f (unroll {a -> b} s) x)

See plutusrunQuote $ docsfomega/z-combinator-benchmarks for details.

fixAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ()) Source #

fixBy :: TermLike term TyName Name uni fun => term () Source #

The fixBy combinator.

fixBy :
    forall (F :: * -> *) .
    ((F ~> Id) -> (F ~> Id)) ->
    ((F ~> F) -> (F ~> Id))

fixByAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ()) Source #

fixN :: TermLike term TyName Name uni fun => Integer -> term () -> term () Source #

Make a n-ary fixpoint combinator.

FixN n :
    forall A1 B1 ... An Bn :: * .
    (forall Q :: * .
        ((A1 -> B1) -> ... -> (An -> Bn) -> Q) ->
        (A1 -> B1) ->
        ... ->
        (An -> Bn) ->
        Q) ->
    (forall R :: * . ((A1 -> B1) -> ... (An -> Bn) -> R) -> R)

fixNAndType :: TermLike term TyName Name uni fun => Integer -> term () -> (term (), Type TyName uni ()) Source #

data FunctionDef term tyname name uni fun ann Source #

A PLC function.

Constructors

FunctionDef
Fields _functionDefAnn :: ann An annotation. _functionDefName :: name The name of a function. _functionDefType :: FunctionType tyname uni ann The type of the function. _functionDefTerm :: term ann The definition of the function.

getMutualFixOf :: TermLike term TyName Name uni fun => ann -> term ann -> [FunctionDef term TyName Name uni fun ann] -> Quote (Tuple term uni ann) Source #

Get the fixed-point of a list of mutually recursive functions.

MutualFixOf _ fixN [ FunctionDef _ fN1 (FunctionType _ a1 b1) f1
                   , ...
                   , FunctionDef _ fNn (FunctionType _ an bn) fn
                   ] =
    Tuple [(a1 -> b1) ... (an -> bn)] $
        fixN {a1} {b1} ... {an} {bn}
            /\(q :: *) -> \(choose : (a1 -> b1) -> ... -> (an -> bn) -> q) ->
                \(fN1 : a1 -> b1) ... (fNn : an -> bn) -> choose f1 ... fn

getSingleFixOf :: TermLike term TyName Name uni fun => ann -> term ann -> FunctionDef term TyName Name uni fun ann -> term ann Source #

Get the fixed-point of a single recursive function.