{-# LANGUAGE FlexibleInstances #-}

module FFI.AgdaUnparse where

import Data.ByteString (ByteString)
import Data.Functor.Identity
import Data.Text (Text)
import Data.Text qualified as T
import FFI.Untyped qualified as AgdaFFI
import PlutusCore qualified as PLC
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing
import PlutusCore.Data (Data)
import PlutusCore.Data qualified as Data
import PlutusCore.Default (DSum (..))
import PlutusPrelude
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Transform.Simplifier

usToHyphen :: String -> String
usToHyphen :: [Char] -> [Char]
usToHyphen = (Char -> Char) -> [Char] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' then Char
'-' else Char
c)

-- | A class for types that can be unparsed to Agda code.
class AgdaUnparse a where
  agdaUnparse :: a -> String

instance AgdaUnparse AgdaFFI.UTerm where
  agdaUnparse :: UTerm -> [Char]
agdaUnparse =
    \case
      AgdaFFI.UVar Integer
n -> [Char]
"(UVar " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n :: Natural) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.ULambda UTerm
term -> [Char]
"(ULambda " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse UTerm
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.UApp UTerm
t UTerm
u -> [Char]
"(UApp " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse UTerm
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse UTerm
u [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.UCon Some (ValueOf DefaultUni)
someValue -> [Char]
"(UCon " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (DSum (ValueOf DefaultUni) Identity -> [Char]
agdaUnparseValue (DSum (ValueOf DefaultUni) Identity -> [Char])
-> (Some (ValueOf DefaultUni)
    -> DSum (ValueOf DefaultUni) Identity)
-> Some (ValueOf DefaultUni)
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
mkValueDSum) Some (ValueOf DefaultUni)
someValue [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      UTerm
AgdaFFI.UError -> [Char]
"UError"
      AgdaFFI.UBuiltin DefaultFun
fun -> [Char]
"(UBuiltin " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultFun -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultFun
fun [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.UDelay UTerm
term -> [Char]
"(UDelay " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse UTerm
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.UForce UTerm
term -> [Char]
"(UForce " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse UTerm
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.UConstr Integer
i [UTerm]
terms -> [Char]
"(UConstr " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Natural -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i :: Natural)
                                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [UTerm] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse [UTerm]
terms [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      AgdaFFI.UCase UTerm
term [UTerm]
cases -> [Char]
"(UCase " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ UTerm -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse UTerm
term [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [UTerm] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse [UTerm]
cases [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance AgdaUnparse UPLC.DefaultFun where
  agdaUnparse :: DefaultFun -> [Char]
agdaUnparse = [Char] -> [Char]
usToHyphen ([Char] -> [Char])
-> (DefaultFun -> [Char]) -> DefaultFun -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
lowerInitialChar ([Char] -> [Char])
-> (DefaultFun -> [Char]) -> DefaultFun -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun -> [Char]
forall a. Show a => a -> [Char]
show

instance AgdaUnparse SimplifierStage where
  agdaUnparse :: SimplifierStage -> [Char]
agdaUnparse SimplifierStage
FloatDelay = [Char]
"floatDelayT"
  agdaUnparse SimplifierStage
ForceDelay = [Char]
"forceDelayT"
  agdaUnparse SimplifierStage
CaseOfCase = [Char]
"caseOfCaseT"
  agdaUnparse SimplifierStage
CaseReduce = [Char]
"caseReduceT"
  agdaUnparse SimplifierStage
Inline     = [Char]
"inlineT"
  agdaUnparse SimplifierStage
CSE        = [Char]
"cseT"

instance AgdaUnparse Natural where
  agdaUnparse :: Natural -> [Char]
agdaUnparse = Natural -> [Char]
forall a. Show a => a -> [Char]
show

instance AgdaUnparse Integer where
  agdaUnparse :: Integer -> [Char]
agdaUnparse Integer
x =
    case (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) of
      Bool
True  -> [Char]
"(ℤ.negsuc " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
      Bool
False ->  [Char]
"(ℤ.pos " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance AgdaUnparse Bool where
  agdaUnparse :: Bool -> [Char]
agdaUnparse Bool
True  = [Char]
"true"
  agdaUnparse Bool
False = [Char]
"false"

instance AgdaUnparse Char where
  agdaUnparse :: Char -> [Char]
agdaUnparse Char
c = Char -> [Char]
forall a. Show a => a -> [Char]
show Char
c
instance AgdaUnparse Text where
  agdaUnparse :: Text -> [Char]
agdaUnparse = [Char] -> [Char]
forall a. Show a => a -> [Char]
show ([Char] -> [Char]) -> (Text -> [Char]) -> Text -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
T.unpack

instance AgdaUnparse ByteString where
  agdaUnparse :: ByteString -> [Char]
agdaUnparse ByteString
bs = [Char]
"(mkByteString " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> ByteString -> [Char]
forall a. Show a => a -> [Char]
show ByteString
bs [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
")"

instance AgdaUnparse () where
  agdaUnparse :: () -> [Char]
agdaUnparse ()
_ = [Char]
"tt"

instance AgdaUnparse a => AgdaUnparse [a] where
  agdaUnparse :: [a] -> [Char]
agdaUnparse [a]
l = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (a -> [Char] -> [Char]) -> [Char] -> [a] -> [Char]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x [Char]
xs -> a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ∷ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
xs) [Char]
"[]" [a]
l [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance (AgdaUnparse a, AgdaUnparse b) => AgdaUnparse (a, b) where
  agdaUnparse :: (a, b) -> [Char]
agdaUnparse (a
x, b
y) = [Char]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" , " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ b -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse b
y [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance AgdaUnparse Data where
  agdaUnparse :: Data -> [Char]
agdaUnparse (Data.Constr Integer
i [Data]
args) =
    [Char]
"(ConstrDATA" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse Integer
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Data] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse [Data]
args [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  agdaUnparse (Data.Map [(Data, Data)]
assocList) =
    [Char]
"(MapDATA" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Data, Data)] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse [(Data, Data)]
assocList [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  agdaUnparse (Data.List [Data]
xs) =
    [Char]
"(ListDATA" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Data] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse [Data]
xs [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  agdaUnparse (Data.I Integer
i) =
    [Char]
"(iDATA" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse Integer
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  agdaUnparse (Data.B ByteString
b) =
    [Char]
"(bDATA" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ByteString -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse ByteString
b [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"

instance AgdaUnparse BLS12_381.G1.Element where
  agdaUnparse :: Element -> [Char]
agdaUnparse = Element -> [Char]
forall a. Show a => a -> [Char]
show

instance AgdaUnparse BLS12_381.G2.Element where
  agdaUnparse :: Element -> [Char]
agdaUnparse = Element -> [Char]
forall a. Show a => a -> [Char]
show

instance AgdaUnparse BLS12_381.Pairing.MlResult where
  agdaUnparse :: MlResult -> [Char]
agdaUnparse = MlResult -> [Char]
forall a. Show a => a -> [Char]
show

instance AgdaUnparse (UPLC.DefaultUni (PLC.Esc a)) where
  agdaUnparse :: DefaultUni (Esc a) -> [Char]
agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniInteger = [Char]
"integer"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniByteString = [Char]
"bytestring"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniString = [Char]
"string"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBool = [Char]
"bool"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniUnit = [Char]
"unit"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniData = [Char]
"pdata"
  agdaUnparse (PLC.DefaultUniList DefaultUni (Esc a1)
t) =
    [Char]
"(list " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a1) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultUni (Esc a1)
t [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  agdaUnparse (PLC.DefaultUniPair DefaultUni (Esc a2)
t1 DefaultUni (Esc a1)
t2) =
    [Char]
"(pair " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a2) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultUni (Esc a2)
t1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a1) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultUni (Esc a1)
t2 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G1_Element = [Char]
"bls12-381-g1-element"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G2_Element = [Char]
"bls12-381-g2-element"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_MlResult = [Char]
"bls12-381-mlresult"
  agdaUnparse (PLC.DefaultUniArray DefaultUni (Esc a1)
_) = [Char] -> [Char]
forall a. HasCallStack => [Char] -> a
error [Char]
"Arrays are currently not supported."
  agdaUnparse (PLC.DefaultUniApply DefaultUni (Esc f)
_ DefaultUni (Esc a1)
_) = [Char] -> [Char]
forall a. HasCallStack => [Char] -> a
error [Char]
"Application of an unknown type is not supported."

agdaUnparseValue :: DSum (PLC.ValueOf UPLC.DefaultUni) Identity -> String
agdaUnparseValue :: DSum (ValueOf DefaultUni) Identity -> [Char]
agdaUnparseValue DSum (ValueOf DefaultUni) Identity
dSum =
  [Char]
"(tagCon " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    case DSum (ValueOf DefaultUni) Identity
dSum of
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniInteger a
_ :=> Identity a
val ->
        [Char]
"integer " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniByteString a
_ :=> Identity a
val ->
        [Char]
"bytestring " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniString a
_ :=> Identity a
val ->
        [Char]
"string " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBool a
_ :=> Identity a
val ->
        [Char]
"bool " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniUnit a
_ :=> Identity a
_ ->
        [Char]
"unit " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ () -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse ()
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniData a
_ :=> Identity a
val ->
        [Char]
"pdata " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf (PLC.DefaultUniList DefaultUni (Esc a1)
elemType) a
_ :=> Identity a
val ->
        [Char]
"(list " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a1) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultUni (Esc a1)
elemType [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a1) -> [a1] -> [Char]
forall {a}. DefaultUni (Esc a) -> [a] -> [Char]
agdaUnparseDList DefaultUni (Esc a1)
DefaultUni (Esc a1)
elemType a
[a1]
val
      PLC.ValueOf (PLC.DefaultUniPair DefaultUni (Esc a2)
type1 DefaultUni (Esc a1)
type2) a
_ :=> Identity a
val ->
        [Char]
"(pair "
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a2) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultUni (Esc a2)
type1
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" "
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a1) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse DefaultUni (Esc a1)
type2
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
") "
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DefaultUni (Esc a2) -> DefaultUni (Esc a1) -> (a2, a1) -> [Char]
forall {a} {a}.
DefaultUni (Esc a) -> DefaultUni (Esc a) -> (a, a) -> [Char]
agdaUnparseDPair DefaultUni (Esc a2)
DefaultUni (Esc a2)
type1 DefaultUni (Esc a1)
DefaultUni (Esc a1)
type2 a
(a2, a1)
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G1_Element a
_ :=> Identity a
val ->
        [Char]
"bls12-381-g1-element " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G2_Element a
_ :=> Identity a
val ->
        [Char]
"bls12-381-g2-element " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++  a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_MlResult a
_ :=> Identity a
val ->
        [Char]
"bls12-381-mlresult " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse a
val
      PLC.ValueOf (PLC.DefaultUniArray DefaultUni (Esc a1)
_) a
_ :=> Identity a
_ ->
        [Char] -> [Char]
forall a. HasCallStack => [Char] -> a
error [Char]
"Arrays are currently not supported."
      PLC.ValueOf (PLC.DefaultUniApply DefaultUni (Esc f)
_ DefaultUni (Esc a1)
_) a
_ :=> Identity a
_ ->
        [Char] -> [Char]
forall a. HasCallStack => [Char] -> a
error [Char]
"Application of an unknown type is not supported."
  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"
  where
    agdaUnparseDList :: DefaultUni (Esc a) -> [a] -> [Char]
agdaUnparseDList DefaultUni (Esc a)
elemType [a]
xs =
      let xs' :: [DSum (PLC.ValueOf PLC.DefaultUni) Identity]
          xs' :: [DSum (ValueOf DefaultUni) Identity]
xs' = Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
mkValueDSum (Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity)
-> (a -> Some (ValueOf DefaultUni))
-> a
-> DSum (ValueOf DefaultUni) Identity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueOf DefaultUni a -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
PLC.Some (ValueOf DefaultUni a -> Some (ValueOf DefaultUni))
-> (a -> ValueOf DefaultUni a) -> a -> Some (ValueOf DefaultUni)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultUni (Esc a) -> a -> ValueOf DefaultUni a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
PLC.ValueOf DefaultUni (Esc a)
elemType (a -> DSum (ValueOf DefaultUni) Identity)
-> [a] -> [DSum (ValueOf DefaultUni) Identity]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs
        in [[Char]] -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ DSum (ValueOf DefaultUni) Identity -> [Char]
agdaUnparseValue (DSum (ValueOf DefaultUni) Identity -> [Char])
-> [DSum (ValueOf DefaultUni) Identity] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DSum (ValueOf DefaultUni) Identity]
xs'
    agdaUnparseDPair :: DefaultUni (Esc a) -> DefaultUni (Esc a) -> (a, a) -> [Char]
agdaUnparseDPair DefaultUni (Esc a)
type1 DefaultUni (Esc a)
type2 (a
x, a
y) =
      let x' :: DSum (ValueOf DefaultUni) Identity
x' = Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
mkValueDSum (Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity)
-> Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
forall a b. (a -> b) -> a -> b
$ ValueOf DefaultUni a -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
PLC.Some (ValueOf DefaultUni a -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni a -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> a -> ValueOf DefaultUni a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
PLC.ValueOf DefaultUni (Esc a)
type1 a
x
          y' :: DSum (ValueOf DefaultUni) Identity
y' = Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
mkValueDSum (Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity)
-> Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
forall a b. (a -> b) -> a -> b
$ ValueOf DefaultUni a -> Some (ValueOf DefaultUni)
forall {k} (tag :: k -> *) (a :: k). tag a -> Some tag
PLC.Some (ValueOf DefaultUni a -> Some (ValueOf DefaultUni))
-> ValueOf DefaultUni a -> Some (ValueOf DefaultUni)
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> a -> ValueOf DefaultUni a
forall (uni :: * -> *) a. uni (Esc a) -> a -> ValueOf uni a
PLC.ValueOf DefaultUni (Esc a)
type2 a
y
        in ([Char], [Char]) -> [Char]
forall a. AgdaUnparse a => a -> [Char]
agdaUnparse (DSum (ValueOf DefaultUni) Identity -> [Char]
agdaUnparseValue DSum (ValueOf DefaultUni) Identity
x', DSum (ValueOf DefaultUni) Identity -> [Char]
agdaUnparseValue DSum (ValueOf DefaultUni) Identity
y')

mkValueDSum :: PLC.Some (PLC.ValueOf UPLC.DefaultUni) -> DSum (PLC.ValueOf UPLC.DefaultUni) Identity
mkValueDSum :: Some (ValueOf DefaultUni) -> DSum (ValueOf DefaultUni) Identity
mkValueDSum (PLC.Some valueOf :: ValueOf DefaultUni a
valueOf@(PLC.ValueOf DefaultUni (Esc a)
_ a
a)) = ValueOf DefaultUni a
valueOf ValueOf DefaultUni a
-> Identity a -> DSum (ValueOf DefaultUni) Identity
forall {k} (tag :: k -> *) (f :: k -> *) (a :: k).
tag a -> f a -> DSum tag f
:=> a -> Identity a
forall a. a -> Identity a
Identity a
a