{-# LANGUAGE TypeApplications #-}

{-| Common UPLC term-construction helpers shared across the
@Transform.*.Spec@ test modules.

Variables are referred to by name: @var "x"@ is an occurrence, @lam "x"
body@ a binder, and @name "x"@ the bare 'Name'. See Note [Names from strings]. -}
module Transform.Lib
  ( T
  , var
  , lam
  , app
  , force
  , delay
  , case_
  , builtin
  , constr
  , sopTrue
  , sopFalse
  , builtinTrue
  , builtinFalse
  , ite
  , con
  , text
  , err
  , name
  ) where

import Data.Text (Text)
import Data.Text qualified as Text
import Data.Word (Word64)
import GHC.Exts (fromList)
import PlutusCore.Default (DefaultFun (IfThenElse), DefaultUni)
import PlutusCore.MkPlc (mkConstant)
import PlutusCore.Name.Unique (Name (..), Unique (..))
import UntypedPlutusCore.Core.Type (Term (..))

{- Note [Names from strings]
These test modules build UPLC terms purely, without using the 'Quote' monad to
allocate fresh uniques. A variable is identified entirely by its name: 'name'
maps a 'String' to a 'Name' whose 'Unique' is derived injectively from it via
'uniqueFromText', and 'var' / 'lam' wrap 'name' for occurrences and binders.

This lets a binder and its occurrences be written independently
(@lam "a" (var "a")@) yet still refer to the same variable, and lets an assertion
mention a free variable by name (@isStrictIn (name "a") term@) with no plumbing.

The trade-off against 'QuoteT' is that freshness is no longer correct by
construction: reusing one name for two variables meant to differ silently aliases
them, since 'Name' equality compares only the 'Unique'. For these small,
hand-written test terms that is an acceptable price for dropping the monadic
plumbing; where capture is a genuine concern, 'QuoteT' remains available.

Alternatives considered: an 'IsString' or 'IsLabel' instance for 'Name'
(@"a" :: Name@ / @#a@), which would be an orphan on a core type; and
'OverloadedRecordDot' handles (@var.x@), which need that uncommon extension and
read as if @x@ were a bound Haskell variable. The plain @String -> Name@ used
here is the simplest: no orphan instance and no language extension at all.

'uniqueFromText' is injective only on short ASCII names, so it fails fast on
non-ASCII characters or on names long enough to overflow the 'Int' rather than
aliasing silently.
-}

-- | Convenient alias used throughout the test modules.
type T = Term Name DefaultUni DefaultFun ()

{-| A 'Var' occurrence of the variable with the given name.
See Note [Names from strings] -}
var :: String -> T
var :: [Char] -> Term Name DefaultUni DefaultFun ()
var = () -> Name -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann
Var () (Name -> Term Name DefaultUni DefaultFun ())
-> ([Char] -> Name) -> [Char] -> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
name

{-| A lambda binding the variable with the given name.
See Note [Names from strings] -}
lam :: String -> T -> T
lam :: [Char]
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
lam = ()
-> Name
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> name -> Term name uni fun ann -> Term name uni fun ann
LamAbs () (Name
 -> Term Name DefaultUni DefaultFun ()
 -> Term Name DefaultUni DefaultFun ())
-> ([Char] -> Name)
-> [Char]
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Name
name

app :: T -> T -> T
app :: Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
app = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Term name uni fun ann
-> Term name uni fun ann
Apply ()

force :: T -> T
force :: Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
force = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Force ()

delay :: T -> T
delay :: Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
delay = ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Term name uni fun ann -> Term name uni fun ann
Delay ()

case_ :: T -> [T] -> T
case_ :: Term Name DefaultUni DefaultFun ()
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
case_ Term Name DefaultUni DefaultFun ()
scrut [Term Name DefaultUni DefaultFun ()]
branches = ()
-> Term Name DefaultUni DefaultFun ()
-> Vector (Term Name DefaultUni DefaultFun ())
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann
-> Term name uni fun ann
-> Vector (Term name uni fun ann)
-> Term name uni fun ann
Case () Term Name DefaultUni DefaultFun ()
scrut ([Item (Vector (Term Name DefaultUni DefaultFun ()))]
-> Vector (Term Name DefaultUni DefaultFun ())
forall l. IsList l => [Item l] -> l
fromList [Item (Vector (Term Name DefaultUni DefaultFun ()))]
[Term Name DefaultUni DefaultFun ()]
branches)

builtin :: DefaultFun -> T
builtin :: DefaultFun -> Term Name DefaultUni DefaultFun ()
builtin = () -> DefaultFun -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> fun -> Term name uni fun ann
Builtin ()

-- | A 'Constr' term tagged with the given index.
constr :: Word64 -> [T] -> T
constr :: Word64
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
constr = ()
-> Word64
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann.
ann -> Word64 -> [Term name uni fun ann] -> Term name uni fun ann
Constr ()

-- | @True@ as a sum-of-products value, @Constr 0 []@ (the datatype encoding of @Bool@).
sopTrue :: T
sopTrue :: Term Name DefaultUni DefaultFun ()
sopTrue = Word64
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
constr Word64
0 []

-- | @False@ as a sum-of-products value, @Constr 1 []@.
sopFalse :: T
sopFalse :: Term Name DefaultUni DefaultFun ()
sopFalse = Word64
-> [Term Name DefaultUni DefaultFun ()]
-> Term Name DefaultUni DefaultFun ()
constr Word64
1 []

-- | @True@ as the builtin @bool@ constant.
builtinTrue :: T
builtinTrue :: Term Name DefaultUni DefaultFun ()
builtinTrue = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
True

-- | @False@ as the builtin @bool@ constant.
builtinFalse :: T
builtinFalse :: Term Name DefaultUni DefaultFun ()
builtinFalse = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Bool () Bool
False

-- | @ifThenElse@ forced and applied to a condition and the two branches.
ite :: T -> T -> T -> T
ite :: Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
ite Term Name DefaultUni DefaultFun ()
cond Term Name DefaultUni DefaultFun ()
t Term Name DefaultUni DefaultFun ()
f = Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
force (DefaultFun -> Term Name DefaultUni DefaultFun ()
builtin DefaultFun
IfThenElse) Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
`app` Term Name DefaultUni DefaultFun ()
cond Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
`app` Term Name DefaultUni DefaultFun ()
t Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
-> Term Name DefaultUni DefaultFun ()
`app` Term Name DefaultUni DefaultFun ()
f

-- | An 'Integer' constant.
con :: Integer -> T
con :: Integer -> Term Name DefaultUni DefaultFun ()
con = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer ()

-- | A 'Text' constant from a literal.
text :: String -> T
text :: [Char] -> Term Name DefaultUni DefaultFun ()
text = forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Text () (Text -> Term Name DefaultUni DefaultFun ())
-> ([Char] -> Text) -> [Char] -> Term Name DefaultUni DefaultFun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Text
Text.pack

err :: T
err :: Term Name DefaultUni DefaultFun ()
err = () -> Term Name DefaultUni DefaultFun ()
forall name (uni :: * -> *) fun ann. ann -> Term name uni fun ann
Error ()

-- | Build a 'Name' from a 'String'. See Note [Names from strings]
name :: String -> Name
name :: [Char] -> Name
name [Char]
s = Text -> Unique -> Name
Name Text
t (Int -> Unique
Unique (Text -> Int
uniqueFromText Text
t))
  where
    t :: Text
t = [Char] -> Text
Text.pack [Char]
s

{-| Pack the string's bytes big-endian into an 'Int' (> 7 bytes overflow).
See Note [Names from strings] for the injectivity and fail-fast contract. -}
uniqueFromText :: Text -> Int
uniqueFromText :: Text -> Int
uniqueFromText Text
t
  | (Char -> Bool) -> Text -> Bool
Text.any ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
127) (Int -> Bool) -> (Char -> Int) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
forall a. Enum a => a -> Int
fromEnum) Text
t =
      [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char]
"Transform.Lib: non-ASCII name: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
forall a. Show a => a -> [Char]
show Text
t)
  | Text -> Int
Text.length Text
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
7 =
      [Char] -> Int
forall a. HasCallStack => [Char] -> a
error ([Char]
"Transform.Lib: name too long (would overflow Unique): " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
forall a. Show a => a -> [Char]
show Text
t)
  | Bool
otherwise = (Int -> Char -> Int) -> Int -> Text -> Int
forall a. (a -> Char -> a) -> a -> Text -> a
Text.foldl' (\Int
acc Char
c -> Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
256 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c) Int
0 Text
t