{-# LANGUAGE OverloadedStrings #-}
module PlutusCore.StdLib.Meta
( metaIntegerToNat
, metaEitherToSum
, metaListToScottList
) where
import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.StdLib.Data.Nat as Plc
import PlutusCore.StdLib.Data.ScottList
import PlutusCore.StdLib.Data.Sum
metaIntegerToNat :: TermLike term TyName Name uni fun => Integer -> term ()
metaIntegerToNat :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term ()
metaIntegerToNat Integer
n
| Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = [Char] -> term ()
forall a. HasCallStack => [Char] -> a
Prelude.error ([Char] -> term ()) -> [Char] -> term ()
forall a b. (a -> b) -> a -> b
$ [Char]
"getBuiltinIntegerToNat: negative argument: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n
| Bool
otherwise = Integer -> term ()
forall {t} {term :: * -> *} {uni :: * -> *} {fun}.
(Eq t, Num t, TermLike term TyName Name uni fun) =>
t -> term ()
go Integer
n where
go :: t -> term ()
go t
0 = term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
zero
go t
m = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
Plc.succ (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ t -> term ()
go (t
m t -> t -> t
forall a. Num a => a -> a -> a
- t
1)
metaEitherToSum
:: TermLike term TyName Name uni fun
=> Type TyName uni ()
-> Type TyName uni ()
-> Either (term ()) (term ())
-> term ()
metaEitherToSum :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Type TyName uni ()
-> Type TyName uni () -> Either (term ()) (term ()) -> term ()
metaEitherToSum Type TyName uni ()
a Type TyName uni ()
b (Left term ()
x) = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
left [Type TyName uni ()
a, Type TyName uni ()
b]) term ()
x
metaEitherToSum Type TyName uni ()
a Type TyName uni ()
b (Right term ()
y) = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
right [Type TyName uni ()
a, Type TyName uni ()
b]) term ()
y
metaListToScottList
:: TermLike term TyName Name uni fun => Type TyName uni () -> [term ()] -> term ()
metaListToScottList :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Type TyName uni () -> [term ()] -> term ()
metaListToScottList Type TyName uni ()
ty =
(term () -> term () -> term ()) -> term () -> [term ()] -> term ()
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
(\term ()
x term ()
xs -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
cons Type TyName uni ()
ty) [term ()
x, term ()
xs])
(() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
nil Type TyName uni ()
ty)