Safe Haskell	Safe-Inferred
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)) ->
        f (\(x : a) -> 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.