plutus-core-1.36.0.0: Language library for Plutus Core
Safe HaskellSafe-Inferred
LanguageHaskell2010

PlutusCore.Examples.Data.Vec

Description

In this module we define Church-encoded type-level natural numbers, Church-encoded vectors and Scott-encoded vectors.

See docsfomegagadtsScottVec.agda for how Scott-encoded vectors work.

Synopsis

Documentation

natKKind () Source #

natK = (* -> *) -> * -> *

getEtaType TyName uni () → Quote (Type TyName uni ()) Source #

getEta n = \(f :: * -> *) (z :: *) -> n f z

zeroTType TyName uni () Source #

zeroT = \(f :: * -> *) (z :: *) -> z

succTType TyName uni () Source #

succT = \(n : natK) (f :: * -> *) (z :: *) -> f (n f z)

plusTType TyName uni () Source #

plusT = \(n : natK) (m : natK) (f :: * -> *) (z :: *) -> n f (m f z)

getStepFunTyNameType TyName uni () → TyNameQuote (Type TyName uni ()) Source #

stepFun a r1 r2 = all (p :: natK). a -> r1 p -> r2 (succT p)

churchVecType TyName uni () Source #

churchVec =
    \(a :: *) (n :: natK) ->
        all (r :: natK -> *). (all (p :: natK). a -> r p -> r (succT p)) -> r zeroT -> r n

churchNilTerm TyName Name uni fun () Source #

churchNil =
    /\(a :: *) ->
        /\(r :: natK -> *) -> \(f : all (p :: natK). a -> r p -> r (succT p)) (z : r zeroT) ->
            z

churchConsTerm TyName Name uni fun () Source #

churchCons =
    /\(a :: *) (n :: natK) -> \(x : a) (xs : churchVec a n) ->
        /\(r :: natK -> *) -> \(f : all (p :: natK). a -> r p -> r (succT p)) (z : r zeroT) ->
            f {n} x (xs {r} f z)

churchConcatTerm TyName Name uni fun () Source #

churchConcat =
    /\(a :: *) (n :: natK) (m :: natK) -> \(xs : churchVec a n) (ys : churchVec a m) ->
        /\(r :: natK -> *) -> \(f : all (p :: natK). a -> r p -> r (succT p)) (z : r zeroT) ->
            xs
                {\(p :: natK) -> r (plusT p m)}
                (/\(p :: natK) -> f {plusT p m})
                (ys {r} f z)

scottVecFType TyName uni () Source #

scottVecF =
    \(a :: *) (rec :: natK -> *) (n :: natK) ->
        all (r :: natK -> *). (all (p :: natK). a -> rec p -> r (succT p)) -> r zeroT -> r n

scottVecType TyName uni () Source #

scottVec = \(a :: *) (n :: natK) -> ifix (scottVecF a) n

scottNilTerm TyName Name uni fun () Source #

scottNil =
    /\(a :: *) ->
        iwrap (scottVecF a) zeroT
            (/\(r :: natK -> *) ->
                \(f : all (p :: natK). a -> scottVec a p -> r (succT p)) (z : r zeroT) ->
                    z)

scottConsTerm TyName Name uni fun () Source #

scottCons =
    /\(a :: *) (n :: natK) -> \(x : a) (xs : scottVec a n) ->
        iwrap (scottVecF a) (succT n)
            (/\(r :: natK -> *) ->
                \(f : all (p :: natK). a -> scottVec a p -> r (succT p)) (z : r zeroT) ->
                    f {n} x xs)

scottHead ∷ uni `HasTypeAndTermLevel` () ⇒ Term TyName Name uni fun () Source #

scottHead =
    /\(a :: *) (n :: natK) -> (xs : scottVec a (suc n)) ->
        unwrap
            xs
            {\(p :: natK) -> p (\(z :: *) -> a) unit}
            (/\(p :: natK) (x : a) (xs' : scottVec a p) -> x)
            unitval

scottSumHeadsOr0 ∷ (uni `HasTypeAndTermLevel` Integer, uni `HasTypeAndTermLevel` ()) ⇒ Term TyName Name uni DefaultFun () Source #

scottSumHeadsOr0 =
    /\(n :: natK) -> (xs ys : scottVec integer n) ->
        unwrap
            xs
            {\(p :: natK) -> (scottVec Integer n -> scottVec integer p) -> integer}
            (/\(p :: natK) (x : integer) (xs' : scottVec integer p)
                \(coe : scottVec Integer n -> scottVec integer (suc p)) ->
                    x + scottHead {integer} {p} (coe ys))
            (\(coe : scottVec Integer n -> scottVec integer zero) -> 0)
            (/\(xs' :: scottVec Integer n) -> xs')