-- | Functions that generate Plutus Core terms from Haskell values and vice versa.

{-# 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

-- | Convert an 'Integer' to a @nat@. TODO: convert PLC's @integer@ to @nat@ instead.
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)

-- | Convert a Haskell 'Either' to a PLC @sum@.
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

-- | Convert a Haskell list of 'Term's to a PLC @list@.
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)