{-# LANGUAGE FlexibleInstances #-}

module FFI.AgdaUnparse where

import Data.ByteString (ByteString)
import Data.Functor.Identity
import Data.Proxy
import Data.Text (Text)
import Data.Text qualified as T
import Data.Vector.Strict (Vector)
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 PlutusPrelude
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Transform.Simplifier

usToHyphen :: String -> String
usToHyphen :: String -> String
usToHyphen = (Char -> Char) -> String -> String
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 -> String
agdaUnparse =
    \case
      AgdaFFI.UVar Integer
n -> String
"(UVar " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n :: Natural) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.ULambda UTerm
term -> String
"(ULambda " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UTerm -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse UTerm
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.UApp UTerm
t UTerm
u -> String
"(UApp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UTerm -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse UTerm
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UTerm -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse UTerm
u String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.UCon Some (ValueOf DefaultUni)
someValue -> String
"(UCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Some (ValueOf DefaultUni) -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse Some (ValueOf DefaultUni)
someValue String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      UTerm
AgdaFFI.UError -> String
"UError"
      AgdaFFI.UBuiltin DefaultFun
fun -> String
"(UBuiltin " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DefaultFun -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse DefaultFun
fun String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.UDelay UTerm
term -> String
"(UDelay " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UTerm -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse UTerm
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.UForce UTerm
term -> String
"(UForce " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UTerm -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse UTerm
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.UConstr Integer
i [UTerm]
terms -> String
"(UConstr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i :: Natural)
                                      String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [UTerm] -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse [UTerm]
terms String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
      AgdaFFI.UCase UTerm
term [UTerm]
cases -> String
"(UCase " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UTerm -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse UTerm
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [UTerm] -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse [UTerm]
cases String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

instance AgdaUnparse SimplifierStage where
  agdaUnparse :: SimplifierStage -> String
agdaUnparse SimplifierStage
FloatDelay     = String
"floatDelayT"
  agdaUnparse SimplifierStage
ForceDelay     = String
"forceDelayT"
  agdaUnparse SimplifierStage
ForceCaseDelay = String
"forceCaseDelayT"
  agdaUnparse SimplifierStage
CaseOfCase     = String
"caseOfCaseT"
  agdaUnparse SimplifierStage
CaseReduce     = String
"caseReduceT"
  agdaUnparse SimplifierStage
Inline         = String
"inlineT"
  agdaUnparse SimplifierStage
CSE            = String
"cseT"

instance AgdaUnparse Natural where
  agdaUnparse :: Natural -> String
agdaUnparse = Natural -> String
forall a. Show a => a -> String
show

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

instance AgdaUnparse Bool where
  agdaUnparse :: Bool -> String
agdaUnparse Bool
True  = String
"true"
  agdaUnparse Bool
False = String
"false"

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

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

instance AgdaUnparse () where
  agdaUnparse :: () -> String
agdaUnparse ()
_ = String
"tt"

agdaUnfold :: (AgdaUnparse a , Foldable f) => f a -> String
agdaUnfold :: forall a (f :: * -> *).
(AgdaUnparse a, Foldable f) =>
f a -> String
agdaUnfold f a
l = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a -> String -> String) -> String -> f a -> String
forall a b. (a -> b -> b) -> b -> f a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x String
xs -> a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ∷ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
xs) String
"[]" f a
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

instance AgdaUnparse a => AgdaUnparse [a] where
  agdaUnparse :: [a] -> String
agdaUnparse = [a] -> String
forall a (f :: * -> *).
(AgdaUnparse a, Foldable f) =>
f a -> String
agdaUnfold

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

instance (AgdaUnparse a) => AgdaUnparse (Vector a) where
  agdaUnparse :: Vector a -> String
agdaUnparse Vector a
v = String
"(mkArray (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Vector a -> String
forall a (f :: * -> *).
(AgdaUnparse a, Foldable f) =>
f a -> String
agdaUnfold Vector a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

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

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

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

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

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

instance AgdaUnparse (PLC.Some (PLC.ValueOf UPLC.DefaultUni)) where
  agdaUnparse :: Some (ValueOf DefaultUni) -> String
agdaUnparse (PLC.Some ValueOf DefaultUni a
valOf) =
    String
"(tagCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++
      case ValueOf DefaultUni a
valOf of
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniInteger a
val ->
          String
"integer " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniByteString a
val ->
          String
"bytestring " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniString a
val ->
          String
"string " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBool a
val ->
          String
"bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniUnit a
_ ->
          String
"unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ () -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse ()
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniData a
val ->
          String
"pdata " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf univ :: DefaultUni (Esc a)
univ@(PLC.DefaultUniList DefaultUni (Esc a1)
elemType) a
val ->
          DefaultUni (Esc a) -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse DefaultUni (Esc a)
univ
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++
            ( Proxy AgdaUnparse
-> DefaultUni (Esc a1) -> (AgdaUnparse a1 => String) -> String
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
PLC.bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @AgdaUnparse) DefaultUni (Esc a1)
DefaultUni (Esc a1)
elemType
            ((AgdaUnparse a1 => String) -> String)
-> (AgdaUnparse a1 => String) -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
            )
        PLC.ValueOf univ :: DefaultUni (Esc a)
univ@(PLC.DefaultUniPair DefaultUni (Esc a2)
type1 DefaultUni (Esc a1)
type2) a
val ->
          DefaultUni (Esc a) -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse DefaultUni (Esc a)
univ
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++
            ( Proxy AgdaUnparse
-> DefaultUni (Esc a2) -> (AgdaUnparse a2 => String) -> String
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
PLC.bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @AgdaUnparse) DefaultUni (Esc a2)
DefaultUni (Esc a2)
type1
            ((AgdaUnparse a2 => String) -> String)
-> (AgdaUnparse a2 => String) -> String
forall a b. (a -> b) -> a -> b
$ Proxy AgdaUnparse
-> DefaultUni (Esc a1) -> (AgdaUnparse a1 => String) -> String
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
PLC.bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @AgdaUnparse) DefaultUni (Esc a1)
DefaultUni (Esc a1)
type2
            ((AgdaUnparse a1 => String) -> String)
-> (AgdaUnparse a1 => String) -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
            )
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G1_Element a
val ->
          String
"bls12-381-g1-element " String -> String -> String
forall a. [a] -> [a] -> [a]
++  a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G2_Element a
val ->
          String
"bls12-381-g2-element " String -> String -> String
forall a. [a] -> [a] -> [a]
++  a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_MlResult a
val ->
          String
"bls12-381-mlresult " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
        PLC.ValueOf univ :: DefaultUni (Esc a)
univ@(PLC.DefaultUniArray DefaultUni (Esc a1)
elemType)  a
val ->
          DefaultUni (Esc a) -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse DefaultUni (Esc a)
univ
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
          String -> String -> String
forall a. [a] -> [a] -> [a]
++
            ( Proxy AgdaUnparse
-> DefaultUni (Esc a1) -> (AgdaUnparse a1 => String) -> String
forall (uni :: * -> *) (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
(Closed uni, Everywhere uni constr) =>
proxy constr -> uni (Esc a) -> (constr a => r) -> r
forall (constr :: * -> Constraint)
       (proxy :: (* -> Constraint) -> *) a r.
Everywhere DefaultUni constr =>
proxy constr -> DefaultUni (Esc a) -> (constr a => r) -> r
PLC.bring (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @AgdaUnparse) DefaultUni (Esc a1)
DefaultUni (Esc a1)
elemType
            ((AgdaUnparse a1 => String) -> String)
-> (AgdaUnparse a1 => String) -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. AgdaUnparse a => a -> String
agdaUnparse a
val
            )
        PLC.ValueOf (PLC.DefaultUniApply DefaultUni (Esc f)
_ DefaultUni (Esc a1)
_) a
_ ->
          String -> String
forall a. HasCallStack => String -> a
error String
"Application of an unknown type is not supported."
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"