{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wall #-}

module FFI.AgdaUnparse where

import Data.ByteString (ByteString)
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 PlutusCore.Value (Value)
import PlutusPrelude
import Prettyprinter
import Prettyprinter.Render.String (renderString)
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Transform.Certify.Hints qualified as Hints
import UntypedPlutusCore.Transform.Certify.Trace

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 -> Doc ann

-- | Render an 'AgdaUnparse' value to a 'String'.
renderAgdaUnparse :: AgdaUnparse a => a -> String
renderAgdaUnparse :: forall a. AgdaUnparse a => a -> String
renderAgdaUnparse = SimpleDocStream Any -> String
forall ann. SimpleDocStream ann -> String
renderString (SimpleDocStream Any -> String)
-> (a -> SimpleDocStream Any) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LayoutOptions -> Doc Any -> SimpleDocStream Any
forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty (PageWidth -> LayoutOptions
LayoutOptions PageWidth
Unbounded) (Doc Any -> SimpleDocStream Any)
-> (a -> Doc Any) -> a -> SimpleDocStream Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc Any
forall ann. a -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse

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

instance AgdaUnparse UPLC.DefaultFun where
  agdaUnparse :: forall ann. DefaultFun -> Doc ann
agdaUnparse = String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann)
-> (DefaultFun -> String) -> DefaultFun -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 CertifiedOptStage where
  agdaUnparse :: forall ann. CertifiedOptStage -> Doc ann
agdaUnparse CertifiedOptStage
FloatDelay = Doc ann
"floatDelayT"
  agdaUnparse CertifiedOptStage
ForceDelay = Doc ann
"forceDelayT"
  agdaUnparse CertifiedOptStage
ForceCaseDelay = Doc ann
"forceCaseDelayT"
  agdaUnparse CertifiedOptStage
Inline = Doc ann
"inlineT"
  agdaUnparse CertifiedOptStage
CSE = Doc ann
"cseT"
  agdaUnparse CertifiedOptStage
ApplyToCase = Doc ann
"applyToCaseT"
  agdaUnparse CertifiedOptStage
CaseReduce = Doc ann
"caseReduceT"
  agdaUnparse CertifiedOptStage
LetFloatOut = Doc ann
"letFloatOutT"

instance AgdaUnparse UncertifiedOptStage where
  agdaUnparse :: forall ann. UncertifiedOptStage -> Doc ann
agdaUnparse UncertifiedOptStage
CaseOfCase = Doc ann
"caseOfCaseT"
  agdaUnparse UncertifiedOptStage
ConstantFolding = Doc ann
"constantFoldingT"

instance AgdaUnparse Hints.Hints where
  agdaUnparse :: forall ann. Hints -> Doc ann
agdaUnparse = \case
    Hints
Hints.NoHints -> Doc ann
"none"
    Hints.Inline Inline
x -> Doc ann
"inline" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
x)

instance AgdaUnparse Hints.Inline where
  agdaUnparse :: forall ann. Inline -> Doc ann
agdaUnparse = \case
    Inline
Hints.InlVar -> Doc ann
"var"
    Hints.InlLam Inline
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"ƛ" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
t)
    Hints.InlApply Inline
f Inline
x -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
f Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"·" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
x)
    Hints.InlForce Inline
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"force" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
t)
    Hints.InlDelay Inline
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"delay" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
t)
    Inline
Hints.InlCon -> Doc ann
"con"
    Inline
Hints.InlBuiltin -> Doc ann
"builtin"
    Inline
Hints.InlError -> Doc ann
"error"
    Hints.InlConstr [Inline]
ts -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"constr" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Inline] -> Doc ann
forall ann. [Inline] -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse [Inline]
ts)
    Hints.InlCase Inline
t [Inline]
ts -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"case" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Inline] -> Doc ann
forall ann. [Inline] -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse [Inline]
ts)
    Hints.InlExpand Inline
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"expand" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
t)
    Hints.InlDrop Inline
t -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Inline -> Doc ann
forall ann. Inline -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Inline
t Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"·↓")

instance AgdaUnparse Natural where
  agdaUnparse :: forall ann. Natural -> Doc ann
agdaUnparse = Natural -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

instance AgdaUnparse Integer where
  agdaUnparse :: forall ann. Integer -> Doc ann
agdaUnparse Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"ℤ.negsuc" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow (Integer -> Integer
forall a. Num a => a -> a
abs Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))
    | Bool
otherwise = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"ℤ.pos" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Integer
x)

instance AgdaUnparse Bool where
  agdaUnparse :: forall ann. Bool -> Doc ann
agdaUnparse Bool
True = Doc ann
"true"
  agdaUnparse Bool
False = Doc ann
"false"

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

instance AgdaUnparse ByteString where
  agdaUnparse :: forall ann. ByteString -> Doc ann
agdaUnparse ByteString
bs = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"mkByteString" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ByteString -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow ByteString
bs)

instance AgdaUnparse () where
  agdaUnparse :: forall ann. () -> Doc ann
agdaUnparse ()
_ = Doc ann
"tt"

agdaUnfold :: (AgdaUnparse a, Foldable f) => f a -> Doc ann
agdaUnfold :: forall a (f :: * -> *) ann.
(AgdaUnparse a, Foldable f) =>
f a -> Doc ann
agdaUnfold f a
l = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ (a -> Doc ann -> Doc ann) -> Doc ann -> f a -> Doc ann
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 Doc ann
xs -> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse a
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"∷" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
xs) Doc ann
"[]" f a
l

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

instance (AgdaUnparse a, AgdaUnparse b) => AgdaUnparse (a, b) where
  agdaUnparse :: forall ann. (a, b) -> Doc ann
agdaUnparse (a
x, b
y) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (a -> Doc ann
forall ann. a -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse a
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"," Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> b -> Doc ann
forall ann. b -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse b
y)

instance AgdaUnparse a => AgdaUnparse (Vector a) where
  agdaUnparse :: forall ann. Vector a -> Doc ann
agdaUnparse Vector a
v = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"mkArray" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Vector a -> Doc ann
forall a (f :: * -> *) ann.
(AgdaUnparse a, Foldable f) =>
f a -> Doc ann
agdaUnfold Vector a
v))

instance (AgdaUnparse a, AgdaUnparse b) => AgdaUnparse (Either a b) where
  agdaUnparse :: forall ann. Either a b -> Doc ann
agdaUnparse (Left a
a) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"inj₁" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse a
a)
  agdaUnparse (Right b
b) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"inj₂" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> b -> Doc ann
forall ann. b -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse b
b)
instance AgdaUnparse Data where
  agdaUnparse :: forall ann. Data -> Doc ann
agdaUnparse (Data.Constr Integer
i [Data]
args) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"ConstrDATA" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Integer
i Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Data] -> Doc ann
forall ann. [Data] -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse [Data]
args)
  agdaUnparse (Data.Map [(Data, Data)]
assocList) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"MapDATA" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [(Data, Data)] -> Doc ann
forall ann. [(Data, Data)] -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse [(Data, Data)]
assocList)
  agdaUnparse (Data.List [Data]
xs) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"ListDATA" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Data] -> Doc ann
forall ann. [Data] -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse [Data]
xs)
  agdaUnparse (Data.I Integer
i) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"iDATA" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse Integer
i)
  agdaUnparse (Data.B ByteString
b) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"bDATA" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> ByteString -> Doc ann
forall ann. ByteString -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse ByteString
b)

-- FIXME (https://github.com/IntersectMBO/plutus-private/issues/1796)
instance AgdaUnparse Value where
  agdaUnparse :: forall ann. Value -> Doc ann
agdaUnparse Value
_ = Doc ann
"Not Implemented: AgdaUnprase Value"

instance AgdaUnparse BLS12_381.G1.Element where
  agdaUnparse :: forall ann. Element -> Doc ann
agdaUnparse = Element -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

instance AgdaUnparse BLS12_381.G2.Element where
  agdaUnparse :: forall ann. Element -> Doc ann
agdaUnparse = Element -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

instance AgdaUnparse BLS12_381.Pairing.MlResult where
  agdaUnparse :: forall ann. MlResult -> Doc ann
agdaUnparse = MlResult -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow

instance AgdaUnparse (UPLC.DefaultUni (PLC.Esc a)) where
  agdaUnparse :: forall ann. DefaultUni (Esc a) -> Doc ann
agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniInteger = Doc ann
"integer"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniByteString = Doc ann
"bytestring"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniString = Doc ann
"string"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBool = Doc ann
"bool"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniUnit = Doc ann
"unit"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniData = Doc ann
"pdata"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniValue = Doc ann
"value"
  agdaUnparse (PLC.DefaultUniList DefaultUni (Esc a1)
t) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"list" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> DefaultUni (Esc a1) -> Doc ann
forall ann. DefaultUni (Esc a1) -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse DefaultUni (Esc a1)
t)
  agdaUnparse (PLC.DefaultUniPair DefaultUni (Esc a2)
t1 DefaultUni (Esc a1)
t2) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"pair" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> DefaultUni (Esc a2) -> Doc ann
forall ann. DefaultUni (Esc a2) -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse DefaultUni (Esc a2)
t1 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> DefaultUni (Esc a1) -> Doc ann
forall ann. DefaultUni (Esc a1) -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse DefaultUni (Esc a1)
t2)
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G1_Element = Doc ann
"bls12-381-g1-element"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_G2_Element = Doc ann
"bls12-381-g2-element"
  agdaUnparse DefaultUni (Esc a)
PLC.DefaultUniBLS12_381_MlResult = Doc ann
"bls12-381-mlresult"
  agdaUnparse (PLC.DefaultUniArray DefaultUni (Esc a1)
t) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann
"array" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> DefaultUni (Esc a1) -> Doc ann
forall ann. DefaultUni (Esc a1) -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse DefaultUni (Esc a1)
t)
  agdaUnparse (PLC.DefaultUniApply DefaultUni (Esc f)
_ DefaultUni (Esc a1)
_) = String -> Doc ann
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 :: forall ann. Some (ValueOf DefaultUni) -> Doc ann
agdaUnparse (PLC.Some (PLC.ValueOf DefaultUni (Esc a)
univ a
val)) =
    Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$
      Doc ann
"tagCon"
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> DefaultUni (Esc a) -> Doc ann
forall ann. DefaultUni (Esc a) -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse DefaultUni (Esc a)
univ
        Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Proxy AgdaUnparse
-> DefaultUni (Esc a) -> (AgdaUnparse a => Doc ann) -> Doc ann
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 a)
univ (a -> Doc ann
forall ann. a -> Doc ann
forall a ann. AgdaUnparse a => a -> Doc ann
agdaUnparse a
val)