{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE PatternSynonyms #-}

module Covenant.Internal.Type
  ( AbstractTy (..),
    Renamed (..),
    CompT (..),
    CompTBody (..),
    DataDeclaration (..),
    Constructor (..),
    ConstructorName (..),
    ValT (..),
    BuiltinFlatT (..),
    TyName (..),
    runConstructorName,
    abstraction,
    thunkT,
    builtinFlat,
    datatype,
    checkStrategy,
    naturalBaseFunctor,
    negativeBaseFunctor,
    byteStringBaseFunctor,
  )
where

import Covenant.DeBruijn (DeBruijn (Z))
import Covenant.Index
  ( Count,
    Index,
    count1,
    intCount,
    intIndex,
    ix0,
  )
import Covenant.Internal.PrettyPrint
  ( PrettyM,
    bindVars,
    lookupAbstraction,
    mkForall,
    runPrettyM,
  )
import Covenant.Internal.Strategy
  ( DataEncoding
      ( BuiltinStrategy,
        PlutusData,
        SOP
      ),
    InternalStrategy
      ( InternalAssocMapStrat,
        InternalDataStrat,
        InternalListStrat,
        InternalOpaqueStrat,
        InternalPairStrat
      ),
    PlutusDataConstructor,
    PlutusDataStrategy
      ( ConstrData,
        EnumData,
        NewtypeData,
        ProductListData
      ),
  )
import Covenant.Util (pattern ConsV, pattern NilV)
import Data.Functor.Classes (Eq1 (liftEq))
import Data.Kind (Type)
import Data.Set (Set)
import Data.String (IsString)
import Data.Text (Text)
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Data.Vector.NonEmpty (NonEmptyVector)
import Data.Vector.NonEmpty qualified as NonEmpty
import Data.Word (Word64)
import Optics.Core
  ( A_Fold,
    A_Lens,
    LabelOptic (labelOptic),
    Prism',
    folding,
    lens,
    preview,
    prism,
    review,
  )
import Prettyprinter
  ( Doc,
    Pretty (pretty),
    hsep,
    indent,
    parens,
    vcat,
    viaShow,
    (<+>),
  )
import Test.QuickCheck.Instances.Text ()

-- | A type abstraction, using a combination of a DeBruijn index (to indicate
-- which scope it refers to) and a positional index (to indicate which bound
-- variable in that scope it refers to).
--
-- = Important note
--
-- This is a /relative/ representation: any given 'AbstractTy' could refer to
-- different things when placed in different positions in the ASG. This stems
-- from how DeBruijn indices behave: 'Z' refers to \'our immediate enclosing
-- scope\', @'S' 'Z'@ to \'one scope outside our immediate enclosing scope\',
-- etc. This can mean different things depending on what these scope(s) are.
--
-- @since 1.0.0
data AbstractTy = BoundAt DeBruijn (Index "tyvar")
  deriving stock
    ( -- | @since 1.0.0
      AbstractTy -> AbstractTy -> Bool
(AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool) -> Eq AbstractTy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbstractTy -> AbstractTy -> Bool
== :: AbstractTy -> AbstractTy -> Bool
$c/= :: AbstractTy -> AbstractTy -> Bool
/= :: AbstractTy -> AbstractTy -> Bool
Eq,
      -- | @since 1.0.0
      Eq AbstractTy
Eq AbstractTy =>
(AbstractTy -> AbstractTy -> Ordering)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> Bool)
-> (AbstractTy -> AbstractTy -> AbstractTy)
-> (AbstractTy -> AbstractTy -> AbstractTy)
-> Ord AbstractTy
AbstractTy -> AbstractTy -> Bool
AbstractTy -> AbstractTy -> Ordering
AbstractTy -> AbstractTy -> AbstractTy
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: AbstractTy -> AbstractTy -> Ordering
compare :: AbstractTy -> AbstractTy -> Ordering
$c< :: AbstractTy -> AbstractTy -> Bool
< :: AbstractTy -> AbstractTy -> Bool
$c<= :: AbstractTy -> AbstractTy -> Bool
<= :: AbstractTy -> AbstractTy -> Bool
$c> :: AbstractTy -> AbstractTy -> Bool
> :: AbstractTy -> AbstractTy -> Bool
$c>= :: AbstractTy -> AbstractTy -> Bool
>= :: AbstractTy -> AbstractTy -> Bool
$cmax :: AbstractTy -> AbstractTy -> AbstractTy
max :: AbstractTy -> AbstractTy -> AbstractTy
$cmin :: AbstractTy -> AbstractTy -> AbstractTy
min :: AbstractTy -> AbstractTy -> AbstractTy
Ord,
      -- | @since 1.0.0
      Int -> AbstractTy -> ShowS
[AbstractTy] -> ShowS
AbstractTy -> String
(Int -> AbstractTy -> ShowS)
-> (AbstractTy -> String)
-> ([AbstractTy] -> ShowS)
-> Show AbstractTy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AbstractTy -> ShowS
showsPrec :: Int -> AbstractTy -> ShowS
$cshow :: AbstractTy -> String
show :: AbstractTy -> String
$cshowList :: [AbstractTy] -> ShowS
showList :: [AbstractTy] -> ShowS
Show
    )

-- | A type abstraction that has undergone renaming from a specific context.
--
-- @since 1.0.0
data Renamed
  = -- | Set by an enclosing scope, and thus is essentially a
    -- concrete type, we just don't know which. First field is its \'true
    -- level\', second field is the positional index in that scope.
    Rigid Int (Index "tyvar")
  | -- | Can be unified with something, but must be consistent: that is, only one
    -- unification for every instance. Field is this variable's positional index;
    -- we don't need to track the scope, as only one scope contains unifiable
    -- bindings.
    Unifiable (Index "tyvar")
  | -- | /Must/ unify with everything, except with other distinct wildcards in the
    -- same scope. First field is a unique /scope/ identifier; second is its
    -- \'true level\' simialr to @'Rigid'@; third is the positional index within
    -- its scope. We must have unique identifiers for wildcard scopes, as
    -- wildcards unify with everything /except/ other wildcards in the /same/
    -- scope, and child scopes aren't unique.
    Wildcard Word64 Int (Index "tyvar")
  deriving stock
    ( -- | @since 1.0.0
      Renamed -> Renamed -> Bool
(Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool) -> Eq Renamed
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Renamed -> Renamed -> Bool
== :: Renamed -> Renamed -> Bool
$c/= :: Renamed -> Renamed -> Bool
/= :: Renamed -> Renamed -> Bool
Eq,
      -- | @since 1.0.0
      Eq Renamed
Eq Renamed =>
(Renamed -> Renamed -> Ordering)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Bool)
-> (Renamed -> Renamed -> Renamed)
-> (Renamed -> Renamed -> Renamed)
-> Ord Renamed
Renamed -> Renamed -> Bool
Renamed -> Renamed -> Ordering
Renamed -> Renamed -> Renamed
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Renamed -> Renamed -> Ordering
compare :: Renamed -> Renamed -> Ordering
$c< :: Renamed -> Renamed -> Bool
< :: Renamed -> Renamed -> Bool
$c<= :: Renamed -> Renamed -> Bool
<= :: Renamed -> Renamed -> Bool
$c> :: Renamed -> Renamed -> Bool
> :: Renamed -> Renamed -> Bool
$c>= :: Renamed -> Renamed -> Bool
>= :: Renamed -> Renamed -> Bool
$cmax :: Renamed -> Renamed -> Renamed
max :: Renamed -> Renamed -> Renamed
$cmin :: Renamed -> Renamed -> Renamed
min :: Renamed -> Renamed -> Renamed
Ord,
      -- | @since 1.0.0
      Int -> Renamed -> ShowS
[Renamed] -> ShowS
Renamed -> String
(Int -> Renamed -> ShowS)
-> (Renamed -> String) -> ([Renamed] -> ShowS) -> Show Renamed
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Renamed -> ShowS
showsPrec :: Int -> Renamed -> ShowS
$cshow :: Renamed -> String
show :: Renamed -> String
$cshowList :: [Renamed] -> ShowS
showList :: [Renamed] -> ShowS
Show
    )

-- | The \'body\' of a computation type, consisting of the types of its
-- arguments and the type of its result.
--
-- @since 1.0.0
newtype CompTBody (a :: Type) = CompTBody (NonEmptyVector (ValT a))
  deriving stock
    ( -- | @since 1.0.0
      CompTBody a -> CompTBody a -> Bool
(CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool) -> Eq (CompTBody a)
forall a. Eq a => CompTBody a -> CompTBody a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => CompTBody a -> CompTBody a -> Bool
== :: CompTBody a -> CompTBody a -> Bool
$c/= :: forall a. Eq a => CompTBody a -> CompTBody a -> Bool
/= :: CompTBody a -> CompTBody a -> Bool
Eq,
      -- | @since 1.0.0
      Eq (CompTBody a)
Eq (CompTBody a) =>
(CompTBody a -> CompTBody a -> Ordering)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> Bool)
-> (CompTBody a -> CompTBody a -> CompTBody a)
-> (CompTBody a -> CompTBody a -> CompTBody a)
-> Ord (CompTBody a)
CompTBody a -> CompTBody a -> Bool
CompTBody a -> CompTBody a -> Ordering
CompTBody a -> CompTBody a -> CompTBody a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (CompTBody a)
forall a. Ord a => CompTBody a -> CompTBody a -> Bool
forall a. Ord a => CompTBody a -> CompTBody a -> Ordering
forall a. Ord a => CompTBody a -> CompTBody a -> CompTBody a
$ccompare :: forall a. Ord a => CompTBody a -> CompTBody a -> Ordering
compare :: CompTBody a -> CompTBody a -> Ordering
$c< :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
< :: CompTBody a -> CompTBody a -> Bool
$c<= :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
<= :: CompTBody a -> CompTBody a -> Bool
$c> :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
> :: CompTBody a -> CompTBody a -> Bool
$c>= :: forall a. Ord a => CompTBody a -> CompTBody a -> Bool
>= :: CompTBody a -> CompTBody a -> Bool
$cmax :: forall a. Ord a => CompTBody a -> CompTBody a -> CompTBody a
max :: CompTBody a -> CompTBody a -> CompTBody a
$cmin :: forall a. Ord a => CompTBody a -> CompTBody a -> CompTBody a
min :: CompTBody a -> CompTBody a -> CompTBody a
Ord,
      -- | @since 1.0.0
      Int -> CompTBody a -> ShowS
[CompTBody a] -> ShowS
CompTBody a -> String
(Int -> CompTBody a -> ShowS)
-> (CompTBody a -> String)
-> ([CompTBody a] -> ShowS)
-> Show (CompTBody a)
forall a. Show a => Int -> CompTBody a -> ShowS
forall a. Show a => [CompTBody a] -> ShowS
forall a. Show a => CompTBody a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> CompTBody a -> ShowS
showsPrec :: Int -> CompTBody a -> ShowS
$cshow :: forall a. Show a => CompTBody a -> String
show :: CompTBody a -> String
$cshowList :: forall a. Show a => [CompTBody a] -> ShowS
showList :: [CompTBody a] -> ShowS
Show
    )

-- | @since 1.0.0
instance Eq1 CompTBody where
  {-# INLINEABLE liftEq #-}
  liftEq :: forall a b. (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool
liftEq a -> b -> Bool
f (CompTBody NonEmptyVector (ValT a)
xs) (CompTBody NonEmptyVector (ValT b)
ys) =
    (ValT a -> ValT b -> Bool)
-> NonEmptyVector (ValT a) -> NonEmptyVector (ValT b) -> Bool
forall a b.
(a -> b -> Bool) -> NonEmptyVector a -> NonEmptyVector b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall a b. (a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f) NonEmptyVector (ValT a)
xs NonEmptyVector (ValT b)
ys

-- | A computation type, with abstractions indicated by the type argument. In
-- pretty much any case imaginable, this would be either 'AbstractTy' (in the
-- ASG), or 'Renamed' (after renaming).
--
-- @since 1.0.0
data CompT (a :: Type) = CompT (Count "tyvar") (CompTBody a)
  deriving stock
    ( -- | @since 1.0.0
      CompT a -> CompT a -> Bool
(CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool) -> Eq (CompT a)
forall a. Eq a => CompT a -> CompT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => CompT a -> CompT a -> Bool
== :: CompT a -> CompT a -> Bool
$c/= :: forall a. Eq a => CompT a -> CompT a -> Bool
/= :: CompT a -> CompT a -> Bool
Eq,
      -- | @since 1.0.0
      Eq (CompT a)
Eq (CompT a) =>
(CompT a -> CompT a -> Ordering)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> Bool)
-> (CompT a -> CompT a -> CompT a)
-> (CompT a -> CompT a -> CompT a)
-> Ord (CompT a)
CompT a -> CompT a -> Bool
CompT a -> CompT a -> Ordering
CompT a -> CompT a -> CompT a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (CompT a)
forall a. Ord a => CompT a -> CompT a -> Bool
forall a. Ord a => CompT a -> CompT a -> Ordering
forall a. Ord a => CompT a -> CompT a -> CompT a
$ccompare :: forall a. Ord a => CompT a -> CompT a -> Ordering
compare :: CompT a -> CompT a -> Ordering
$c< :: forall a. Ord a => CompT a -> CompT a -> Bool
< :: CompT a -> CompT a -> Bool
$c<= :: forall a. Ord a => CompT a -> CompT a -> Bool
<= :: CompT a -> CompT a -> Bool
$c> :: forall a. Ord a => CompT a -> CompT a -> Bool
> :: CompT a -> CompT a -> Bool
$c>= :: forall a. Ord a => CompT a -> CompT a -> Bool
>= :: CompT a -> CompT a -> Bool
$cmax :: forall a. Ord a => CompT a -> CompT a -> CompT a
max :: CompT a -> CompT a -> CompT a
$cmin :: forall a. Ord a => CompT a -> CompT a -> CompT a
min :: CompT a -> CompT a -> CompT a
Ord,
      -- | @since 1.0.0
      Int -> CompT a -> ShowS
[CompT a] -> ShowS
CompT a -> String
(Int -> CompT a -> ShowS)
-> (CompT a -> String) -> ([CompT a] -> ShowS) -> Show (CompT a)
forall a. Show a => Int -> CompT a -> ShowS
forall a. Show a => [CompT a] -> ShowS
forall a. Show a => CompT a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> CompT a -> ShowS
showsPrec :: Int -> CompT a -> ShowS
$cshow :: forall a. Show a => CompT a -> String
show :: CompT a -> String
$cshowList :: forall a. Show a => [CompT a] -> ShowS
showList :: [CompT a] -> ShowS
Show
    )

-- | @since 1.0.0
instance Eq1 CompT where
  {-# INLINEABLE liftEq #-}
  liftEq :: forall a b. (a -> b -> Bool) -> CompT a -> CompT b -> Bool
liftEq a -> b -> Bool
f (CompT Count "tyvar"
abses1 CompTBody a
xs) (CompT Count "tyvar"
abses2 CompTBody b
ys) =
    Count "tyvar"
abses1 Count "tyvar" -> Count "tyvar" -> Bool
forall a. Eq a => a -> a -> Bool
== Count "tyvar"
abses2 Bool -> Bool -> Bool
&& (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool
forall a b. (a -> b -> Bool) -> CompTBody a -> CompTBody b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f CompTBody a
xs CompTBody b
ys

-- | @since 1.0.0
instance Pretty (CompT Renamed) where
  pretty :: forall ann. CompT Renamed -> Doc ann
pretty = PrettyM ann (Doc ann) -> Doc ann
forall ann a. PrettyM ann a -> a
runPrettyM (PrettyM ann (Doc ann) -> Doc ann)
-> (CompT Renamed -> PrettyM ann (Doc ann))
-> CompT Renamed
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompT Renamed -> PrettyM ann (Doc ann)
forall ann. CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext

-- | The name of a data type. This refers specifically to non-\'flat\' types
-- either provided by the ledger, or defined by the user.
--
-- @since 1.1.0
newtype TyName = TyName Text
  deriving
    ( -- | @since 1.1.0
      Int -> TyName -> ShowS
[TyName] -> ShowS
TyName -> String
(Int -> TyName -> ShowS)
-> (TyName -> String) -> ([TyName] -> ShowS) -> Show TyName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TyName -> ShowS
showsPrec :: Int -> TyName -> ShowS
$cshow :: TyName -> String
show :: TyName -> String
$cshowList :: [TyName] -> ShowS
showList :: [TyName] -> ShowS
Show,
      -- | @since 1.1.0
      TyName -> TyName -> Bool
(TyName -> TyName -> Bool)
-> (TyName -> TyName -> Bool) -> Eq TyName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TyName -> TyName -> Bool
== :: TyName -> TyName -> Bool
$c/= :: TyName -> TyName -> Bool
/= :: TyName -> TyName -> Bool
Eq,
      -- | @since 1.1.0
      Eq TyName
Eq TyName =>
(TyName -> TyName -> Ordering)
-> (TyName -> TyName -> Bool)
-> (TyName -> TyName -> Bool)
-> (TyName -> TyName -> Bool)
-> (TyName -> TyName -> Bool)
-> (TyName -> TyName -> TyName)
-> (TyName -> TyName -> TyName)
-> Ord TyName
TyName -> TyName -> Bool
TyName -> TyName -> Ordering
TyName -> TyName -> TyName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: TyName -> TyName -> Ordering
compare :: TyName -> TyName -> Ordering
$c< :: TyName -> TyName -> Bool
< :: TyName -> TyName -> Bool
$c<= :: TyName -> TyName -> Bool
<= :: TyName -> TyName -> Bool
$c> :: TyName -> TyName -> Bool
> :: TyName -> TyName -> Bool
$c>= :: TyName -> TyName -> Bool
>= :: TyName -> TyName -> Bool
$cmax :: TyName -> TyName -> TyName
max :: TyName -> TyName -> TyName
$cmin :: TyName -> TyName -> TyName
min :: TyName -> TyName -> TyName
Ord,
      -- | @since 1.1.0
      String -> TyName
(String -> TyName) -> IsString TyName
forall a. (String -> a) -> IsString a
$cfromString :: String -> TyName
fromString :: String -> TyName
IsString
    )
    via Text

-- | A value type, with abstractions indicated by the type argument. In pretty
-- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or
-- 'Renamed' (after renaming).
--
-- @since 1.0.0
data ValT (a :: Type)
  = -- | An abstract type.
    Abstraction a
  | -- | A suspended computation.
    ThunkT (CompT a)
  | -- | A builtin type without any nesting.
    BuiltinFlat BuiltinFlatT
  | -- | An applied type constructor for a non-\'flat\' data type.
    -- | @since 1.1.0
    Datatype TyName (Vector (ValT a))
  deriving stock
    ( -- | @since 1.0.0
      ValT a -> ValT a -> Bool
(ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool) -> Eq (ValT a)
forall a. Eq a => ValT a -> ValT a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => ValT a -> ValT a -> Bool
== :: ValT a -> ValT a -> Bool
$c/= :: forall a. Eq a => ValT a -> ValT a -> Bool
/= :: ValT a -> ValT a -> Bool
Eq,
      -- | @since 1.0.0
      Eq (ValT a)
Eq (ValT a) =>
(ValT a -> ValT a -> Ordering)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> Bool)
-> (ValT a -> ValT a -> ValT a)
-> (ValT a -> ValT a -> ValT a)
-> Ord (ValT a)
ValT a -> ValT a -> Bool
ValT a -> ValT a -> Ordering
ValT a -> ValT a -> ValT a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (ValT a)
forall a. Ord a => ValT a -> ValT a -> Bool
forall a. Ord a => ValT a -> ValT a -> Ordering
forall a. Ord a => ValT a -> ValT a -> ValT a
$ccompare :: forall a. Ord a => ValT a -> ValT a -> Ordering
compare :: ValT a -> ValT a -> Ordering
$c< :: forall a. Ord a => ValT a -> ValT a -> Bool
< :: ValT a -> ValT a -> Bool
$c<= :: forall a. Ord a => ValT a -> ValT a -> Bool
<= :: ValT a -> ValT a -> Bool
$c> :: forall a. Ord a => ValT a -> ValT a -> Bool
> :: ValT a -> ValT a -> Bool
$c>= :: forall a. Ord a => ValT a -> ValT a -> Bool
>= :: ValT a -> ValT a -> Bool
$cmax :: forall a. Ord a => ValT a -> ValT a -> ValT a
max :: ValT a -> ValT a -> ValT a
$cmin :: forall a. Ord a => ValT a -> ValT a -> ValT a
min :: ValT a -> ValT a -> ValT a
Ord,
      -- | @since 1.0.0
      Int -> ValT a -> ShowS
[ValT a] -> ShowS
ValT a -> String
(Int -> ValT a -> ShowS)
-> (ValT a -> String) -> ([ValT a] -> ShowS) -> Show (ValT a)
forall a. Show a => Int -> ValT a -> ShowS
forall a. Show a => [ValT a] -> ShowS
forall a. Show a => ValT a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> ValT a -> ShowS
showsPrec :: Int -> ValT a -> ShowS
$cshow :: forall a. Show a => ValT a -> String
show :: ValT a -> String
$cshowList :: forall a. Show a => [ValT a] -> ShowS
showList :: [ValT a] -> ShowS
Show
    )

-- | @since 1.0.0
instance Eq1 ValT where
  {-# INLINEABLE liftEq #-}
  liftEq :: forall a b. (a -> b -> Bool) -> ValT a -> ValT b -> Bool
liftEq a -> b -> Bool
f = \case
    Abstraction a
abs1 -> \case
      Abstraction b
abs2 -> a -> b -> Bool
f a
abs1 b
abs2
      ValT b
_ -> Bool
False
    ThunkT CompT a
t1 -> \case
      ThunkT CompT b
t2 -> (a -> b -> Bool) -> CompT a -> CompT b -> Bool
forall a b. (a -> b -> Bool) -> CompT a -> CompT b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f CompT a
t1 CompT b
t2
      ValT b
_ -> Bool
False
    BuiltinFlat BuiltinFlatT
t1 -> \case
      BuiltinFlat BuiltinFlatT
t2 -> BuiltinFlatT
t1 BuiltinFlatT -> BuiltinFlatT -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinFlatT
t2
      ValT b
_ -> Bool
False
    Datatype TyName
tn1 Vector (ValT a)
args1 -> \case
      Datatype TyName
tn2 Vector (ValT b)
args2 -> TyName
tn1 TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
tn2 Bool -> Bool -> Bool
&& (ValT a -> ValT b -> Bool)
-> Vector (ValT a) -> Vector (ValT b) -> Bool
forall a b. (a -> b -> Bool) -> Vector a -> Vector b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall a b. (a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f) Vector (ValT a)
args1 Vector (ValT b)
args2
      ValT b
_ -> Bool
False

-- | /Do not/ use this instance to write other 'Pretty' instances. It exists to
-- ensure readable tests without having to expose a lot of internals.
--
-- @since 1.0.0
instance Pretty (ValT Renamed) where
  pretty :: forall ann. ValT Renamed -> Doc ann
pretty = PrettyM ann (Doc ann) -> Doc ann
forall ann a. PrettyM ann a -> a
runPrettyM (PrettyM ann (Doc ann) -> Doc ann)
-> (ValT Renamed -> PrettyM ann (Doc ann))
-> ValT Renamed
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext

abstraction :: forall (a :: Type). Prism' (ValT a) a
abstraction :: forall a. Prism' (ValT a) a
abstraction = (a -> ValT a)
-> (ValT a -> Either (ValT a) a) -> Prism (ValT a) (ValT a) a a
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism a -> ValT a
forall a. a -> ValT a
Abstraction (\case (Abstraction a
a) -> a -> Either (ValT a) a
forall a b. b -> Either a b
Right a
a; ValT a
other -> ValT a -> Either (ValT a) a
forall a b. a -> Either a b
Left ValT a
other)

thunkT :: forall (a :: Type). Prism' (ValT a) (CompT a)
thunkT :: forall a. Prism' (ValT a) (CompT a)
thunkT = (CompT a -> ValT a)
-> (ValT a -> Either (ValT a) (CompT a))
-> Prism (ValT a) (ValT a) (CompT a) (CompT a)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism CompT a -> ValT a
forall a. CompT a -> ValT a
ThunkT (\case (ThunkT CompT a
compT) -> CompT a -> Either (ValT a) (CompT a)
forall a b. b -> Either a b
Right CompT a
compT; ValT a
other -> ValT a -> Either (ValT a) (CompT a)
forall a b. a -> Either a b
Left ValT a
other)

builtinFlat :: forall (a :: Type). Prism' (ValT a) BuiltinFlatT
builtinFlat :: forall a. Prism' (ValT a) BuiltinFlatT
builtinFlat = (BuiltinFlatT -> ValT a)
-> (ValT a -> Either (ValT a) BuiltinFlatT)
-> Prism (ValT a) (ValT a) BuiltinFlatT BuiltinFlatT
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism BuiltinFlatT -> ValT a
forall a. BuiltinFlatT -> ValT a
BuiltinFlat (\case (BuiltinFlat BuiltinFlatT
bi) -> BuiltinFlatT -> Either (ValT a) BuiltinFlatT
forall a b. b -> Either a b
Right BuiltinFlatT
bi; ValT a
other -> ValT a -> Either (ValT a) BuiltinFlatT
forall a b. a -> Either a b
Left ValT a
other)

datatype :: forall (a :: Type). Prism' (ValT a) (TyName, Vector (ValT a))
datatype :: forall a. Prism' (ValT a) (TyName, Vector (ValT a))
datatype =
  ((TyName, Vector (ValT a)) -> ValT a)
-> (ValT a -> Either (ValT a) (TyName, Vector (ValT a)))
-> Prism
     (ValT a)
     (ValT a)
     (TyName, Vector (ValT a))
     (TyName, Vector (ValT a))
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism
    ((TyName -> Vector (ValT a) -> ValT a)
-> (TyName, Vector (ValT a)) -> ValT a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyName -> Vector (ValT a) -> ValT a
forall a. TyName -> Vector (ValT a) -> ValT a
Datatype)
    (\case (Datatype TyName
tn Vector (ValT a)
args) -> (TyName, Vector (ValT a))
-> Either (ValT a) (TyName, Vector (ValT a))
forall a b. b -> Either a b
Right (TyName
tn, Vector (ValT a)
args); ValT a
other -> ValT a -> Either (ValT a) (TyName, Vector (ValT a))
forall a b. a -> Either a b
Left ValT a
other)

-- | All builtin types that are \'flat\': that is, do not have other types
-- \'nested inside them\'.
--
-- @since 1.0.0
data BuiltinFlatT
  = UnitT
  | BoolT
  | IntegerT
  | StringT
  | ByteStringT
  | BLS12_381_G1_ElementT
  | BLS12_381_G2_ElementT
  | BLS12_381_MlResultT
  deriving stock
    ( -- | @since 1.0.0
      BuiltinFlatT -> BuiltinFlatT -> Bool
(BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool) -> Eq BuiltinFlatT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BuiltinFlatT -> BuiltinFlatT -> Bool
== :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c/= :: BuiltinFlatT -> BuiltinFlatT -> Bool
/= :: BuiltinFlatT -> BuiltinFlatT -> Bool
Eq,
      -- | @since 1.0.0
      Eq BuiltinFlatT
Eq BuiltinFlatT =>
(BuiltinFlatT -> BuiltinFlatT -> Ordering)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> Bool)
-> (BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT)
-> (BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT)
-> Ord BuiltinFlatT
BuiltinFlatT -> BuiltinFlatT -> Bool
BuiltinFlatT -> BuiltinFlatT -> Ordering
BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: BuiltinFlatT -> BuiltinFlatT -> Ordering
compare :: BuiltinFlatT -> BuiltinFlatT -> Ordering
$c< :: BuiltinFlatT -> BuiltinFlatT -> Bool
< :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c<= :: BuiltinFlatT -> BuiltinFlatT -> Bool
<= :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c> :: BuiltinFlatT -> BuiltinFlatT -> Bool
> :: BuiltinFlatT -> BuiltinFlatT -> Bool
$c>= :: BuiltinFlatT -> BuiltinFlatT -> Bool
>= :: BuiltinFlatT -> BuiltinFlatT -> Bool
$cmax :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
max :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
$cmin :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
min :: BuiltinFlatT -> BuiltinFlatT -> BuiltinFlatT
Ord,
      -- | @since 1.0.0
      Int -> BuiltinFlatT -> ShowS
[BuiltinFlatT] -> ShowS
BuiltinFlatT -> String
(Int -> BuiltinFlatT -> ShowS)
-> (BuiltinFlatT -> String)
-> ([BuiltinFlatT] -> ShowS)
-> Show BuiltinFlatT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BuiltinFlatT -> ShowS
showsPrec :: Int -> BuiltinFlatT -> ShowS
$cshow :: BuiltinFlatT -> String
show :: BuiltinFlatT -> String
$cshowList :: [BuiltinFlatT] -> ShowS
showList :: [BuiltinFlatT] -> ShowS
Show
    )

-- | The name of a data type constructor.
--
-- @since 1.1.0
newtype ConstructorName = ConstructorName Text
  deriving
    ( -- | @since 1.1.0
      Int -> ConstructorName -> ShowS
[ConstructorName] -> ShowS
ConstructorName -> String
(Int -> ConstructorName -> ShowS)
-> (ConstructorName -> String)
-> ([ConstructorName] -> ShowS)
-> Show ConstructorName
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConstructorName -> ShowS
showsPrec :: Int -> ConstructorName -> ShowS
$cshow :: ConstructorName -> String
show :: ConstructorName -> String
$cshowList :: [ConstructorName] -> ShowS
showList :: [ConstructorName] -> ShowS
Show,
      -- | @since 1.1.0
      ConstructorName -> ConstructorName -> Bool
(ConstructorName -> ConstructorName -> Bool)
-> (ConstructorName -> ConstructorName -> Bool)
-> Eq ConstructorName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConstructorName -> ConstructorName -> Bool
== :: ConstructorName -> ConstructorName -> Bool
$c/= :: ConstructorName -> ConstructorName -> Bool
/= :: ConstructorName -> ConstructorName -> Bool
Eq,
      -- | @since 1.1.0
      Eq ConstructorName
Eq ConstructorName =>
(ConstructorName -> ConstructorName -> Ordering)
-> (ConstructorName -> ConstructorName -> Bool)
-> (ConstructorName -> ConstructorName -> Bool)
-> (ConstructorName -> ConstructorName -> Bool)
-> (ConstructorName -> ConstructorName -> Bool)
-> (ConstructorName -> ConstructorName -> ConstructorName)
-> (ConstructorName -> ConstructorName -> ConstructorName)
-> Ord ConstructorName
ConstructorName -> ConstructorName -> Bool
ConstructorName -> ConstructorName -> Ordering
ConstructorName -> ConstructorName -> ConstructorName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ConstructorName -> ConstructorName -> Ordering
compare :: ConstructorName -> ConstructorName -> Ordering
$c< :: ConstructorName -> ConstructorName -> Bool
< :: ConstructorName -> ConstructorName -> Bool
$c<= :: ConstructorName -> ConstructorName -> Bool
<= :: ConstructorName -> ConstructorName -> Bool
$c> :: ConstructorName -> ConstructorName -> Bool
> :: ConstructorName -> ConstructorName -> Bool
$c>= :: ConstructorName -> ConstructorName -> Bool
>= :: ConstructorName -> ConstructorName -> Bool
$cmax :: ConstructorName -> ConstructorName -> ConstructorName
max :: ConstructorName -> ConstructorName -> ConstructorName
$cmin :: ConstructorName -> ConstructorName -> ConstructorName
min :: ConstructorName -> ConstructorName -> ConstructorName
Ord,
      -- | @since 1.1.0
      String -> ConstructorName
(String -> ConstructorName) -> IsString ConstructorName
forall a. (String -> a) -> IsString a
$cfromString :: String -> ConstructorName
fromString :: String -> ConstructorName
IsString
    )
    via Text

-- | @since 1.1.0
runConstructorName :: ConstructorName -> Text
runConstructorName :: ConstructorName -> Text
runConstructorName (ConstructorName Text
nm) = Text
nm

-- | A single constructor of a data type, with its fields.
--
-- @since 1.1.0
data Constructor (a :: Type)
  = Constructor ConstructorName (Vector (ValT a))
  deriving stock
    ( -- | @since 1.1.0
      Int -> Constructor a -> ShowS
[Constructor a] -> ShowS
Constructor a -> String
(Int -> Constructor a -> ShowS)
-> (Constructor a -> String)
-> ([Constructor a] -> ShowS)
-> Show (Constructor a)
forall a. Show a => Int -> Constructor a -> ShowS
forall a. Show a => [Constructor a] -> ShowS
forall a. Show a => Constructor a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Constructor a -> ShowS
showsPrec :: Int -> Constructor a -> ShowS
$cshow :: forall a. Show a => Constructor a -> String
show :: Constructor a -> String
$cshowList :: forall a. Show a => [Constructor a] -> ShowS
showList :: [Constructor a] -> ShowS
Show,
      -- | @since 1.1.0
      Constructor a -> Constructor a -> Bool
(Constructor a -> Constructor a -> Bool)
-> (Constructor a -> Constructor a -> Bool) -> Eq (Constructor a)
forall a. Eq a => Constructor a -> Constructor a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Constructor a -> Constructor a -> Bool
== :: Constructor a -> Constructor a -> Bool
$c/= :: forall a. Eq a => Constructor a -> Constructor a -> Bool
/= :: Constructor a -> Constructor a -> Bool
Eq
    )

-- | @since 1.1.0
instance Eq1 Constructor where
  liftEq :: forall a b.
(a -> b -> Bool) -> Constructor a -> Constructor b -> Bool
liftEq a -> b -> Bool
f (Constructor ConstructorName
nm Vector (ValT a)
args) (Constructor ConstructorName
nm' Vector (ValT b)
args') =
    ConstructorName
nm ConstructorName -> ConstructorName -> Bool
forall a. Eq a => a -> a -> Bool
== ConstructorName
nm' Bool -> Bool -> Bool
&& (ValT a -> ValT b -> Bool)
-> Vector (ValT a) -> Vector (ValT b) -> Bool
forall a b. (a -> b -> Bool) -> Vector a -> Vector b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq ((a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall a b. (a -> b -> Bool) -> ValT a -> ValT b -> Bool
forall (f :: Type -> Type) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq a -> b -> Bool
f) Vector (ValT a)
args Vector (ValT b)
args'

-- | @since 1.1.0
instance
  (k ~ A_Lens, a ~ ConstructorName, b ~ ConstructorName) =>
  LabelOptic "constructorName" k (Constructor c) (Constructor c) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (Constructor c) (Constructor c) a b
labelOptic = (Constructor c -> a)
-> (Constructor c -> b -> Constructor c)
-> Lens (Constructor c) (Constructor c) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\(Constructor ConstructorName
n Vector (ValT c)
_) -> a
ConstructorName
n) (\(Constructor ConstructorName
_ Vector (ValT c)
args) b
n -> ConstructorName -> Vector (ValT c) -> Constructor c
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor b
ConstructorName
n Vector (ValT c)
args)

-- | @since 1.1.0
instance
  (k ~ A_Lens, a ~ Vector (ValT c), b ~ Vector (ValT c)) =>
  LabelOptic "constructorArgs" k (Constructor c) (Constructor c) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (Constructor c) (Constructor c) a b
labelOptic = (Constructor c -> a)
-> (Constructor c -> b -> Constructor c)
-> Lens (Constructor c) (Constructor c) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\(Constructor ConstructorName
_ Vector (ValT c)
args) -> a
Vector (ValT c)
args) (\(Constructor ConstructorName
n Vector (ValT c)
_) b
args -> ConstructorName -> Vector (ValT c) -> Constructor c
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
n b
Vector (ValT c)
args)

-- | Description of a non-\'flat\' type, together with how it is encoded.
--
-- @since 1.1.0
data DataDeclaration a
  = -- | A \'standard\' datatype, with its constructors and encoding.
    --
    -- @since 1.1.0
    DataDeclaration TyName (Count "tyvar") (Vector (Constructor a)) DataEncoding
  | -- | An \'opaque\' datatype, with the permitted constructors of
    -- @Data@ we can use to build and tear it down.
    --
    -- @since 1.1.0
    OpaqueData TyName (Set PlutusDataConstructor)
  deriving stock
    ( -- | @since 1.1.0
      Int -> DataDeclaration a -> ShowS
[DataDeclaration a] -> ShowS
DataDeclaration a -> String
(Int -> DataDeclaration a -> ShowS)
-> (DataDeclaration a -> String)
-> ([DataDeclaration a] -> ShowS)
-> Show (DataDeclaration a)
forall a. Show a => Int -> DataDeclaration a -> ShowS
forall a. Show a => [DataDeclaration a] -> ShowS
forall a. Show a => DataDeclaration a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> DataDeclaration a -> ShowS
showsPrec :: Int -> DataDeclaration a -> ShowS
$cshow :: forall a. Show a => DataDeclaration a -> String
show :: DataDeclaration a -> String
$cshowList :: forall a. Show a => [DataDeclaration a] -> ShowS
showList :: [DataDeclaration a] -> ShowS
Show,
      -- | @since 1.1.0
      DataDeclaration a -> DataDeclaration a -> Bool
(DataDeclaration a -> DataDeclaration a -> Bool)
-> (DataDeclaration a -> DataDeclaration a -> Bool)
-> Eq (DataDeclaration a)
forall a. Eq a => DataDeclaration a -> DataDeclaration a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => DataDeclaration a -> DataDeclaration a -> Bool
== :: DataDeclaration a -> DataDeclaration a -> Bool
$c/= :: forall a. Eq a => DataDeclaration a -> DataDeclaration a -> Bool
/= :: DataDeclaration a -> DataDeclaration a -> Bool
Eq
    )

-- | @since 1.1.0
instance Pretty (DataDeclaration Renamed) where
  pretty :: forall ann. DataDeclaration Renamed -> Doc ann
pretty = PrettyM ann (Doc ann) -> Doc ann
forall ann a. PrettyM ann a -> a
runPrettyM (PrettyM ann (Doc ann) -> Doc ann)
-> (DataDeclaration Renamed -> PrettyM ann (Doc ann))
-> DataDeclaration Renamed
-> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclaration Renamed -> PrettyM ann (Doc ann)
forall ann. DataDeclaration Renamed -> PrettyM ann (Doc ann)
prettyDataDeclWithContext

-- | @since 1.1.0
instance
  (k ~ A_Lens, a ~ TyName, b ~ TyName) =>
  LabelOptic "datatypeName" k (DataDeclaration c) (DataDeclaration c) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DataDeclaration c) (DataDeclaration c) a b
labelOptic =
    (DataDeclaration c -> a)
-> (DataDeclaration c -> b -> DataDeclaration c)
-> Lens (DataDeclaration c) (DataDeclaration c) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\case OpaqueData TyName
tn Set PlutusDataConstructor
_ -> a
TyName
tn; DataDeclaration TyName
tn Count "tyvar"
_ Vector (Constructor c)
_ DataEncoding
_ -> a
TyName
tn)
      (\DataDeclaration c
decl b
tn -> case DataDeclaration c
decl of OpaqueData TyName
_ Set PlutusDataConstructor
x -> TyName -> Set PlutusDataConstructor -> DataDeclaration c
forall a. TyName -> Set PlutusDataConstructor -> DataDeclaration a
OpaqueData b
TyName
tn Set PlutusDataConstructor
x; DataDeclaration TyName
_ Count "tyvar"
x Vector (Constructor c)
y DataEncoding
z -> TyName
-> Count "tyvar"
-> Vector (Constructor c)
-> DataEncoding
-> DataDeclaration c
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration b
TyName
tn Count "tyvar"
x Vector (Constructor c)
y DataEncoding
z)

-- | @since 1.1.0
instance
  (k ~ A_Fold, a ~ Count "tyvar", b ~ Count "tyvar") =>
  LabelOptic "datatypeBinders" k (DataDeclaration c) (DataDeclaration c) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DataDeclaration c) (DataDeclaration c) a b
labelOptic =
    (DataDeclaration c -> Maybe a) -> Fold (DataDeclaration c) a
forall (f :: Type -> Type) s a.
Foldable f =>
(s -> f a) -> Fold s a
folding ((DataDeclaration c -> Maybe a) -> Fold (DataDeclaration c) a)
-> (DataDeclaration c -> Maybe a) -> Fold (DataDeclaration c) a
forall a b. (a -> b) -> a -> b
$ \case
      DataDeclaration TyName
_ Count "tyvar"
cnt Vector (Constructor c)
_ DataEncoding
_ -> a -> Maybe a
forall a. a -> Maybe a
Just a
Count "tyvar"
cnt
      DataDeclaration c
_ -> Maybe a
forall a. Maybe a
Nothing

-- | @since 1.1.0
instance
  (k ~ A_Fold, a ~ Vector (Constructor c), b ~ Vector (Constructor c)) =>
  LabelOptic "datatypeConstructors" k (DataDeclaration c) (DataDeclaration c) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DataDeclaration c) (DataDeclaration c) a b
labelOptic =
    (DataDeclaration c -> Maybe a) -> Fold (DataDeclaration c) a
forall (f :: Type -> Type) s a.
Foldable f =>
(s -> f a) -> Fold s a
folding ((DataDeclaration c -> Maybe a) -> Fold (DataDeclaration c) a)
-> (DataDeclaration c -> Maybe a) -> Fold (DataDeclaration c) a
forall a b. (a -> b) -> a -> b
$ \case
      DataDeclaration TyName
_ Count "tyvar"
_ Vector (Constructor c)
ctors DataEncoding
_ -> a -> Maybe a
forall a. a -> Maybe a
Just a
Vector (Constructor c)
ctors
      DataDeclaration c
_ -> Maybe a
forall a. Maybe a
Nothing

-- | @since 1.1.0
instance
  (k ~ A_Lens, a ~ DataEncoding, b ~ DataEncoding) =>
  LabelOptic "datatypeEncoding" k (DataDeclaration c) (DataDeclaration c) a b
  where
  {-# INLINEABLE labelOptic #-}
  labelOptic :: Optic k NoIx (DataDeclaration c) (DataDeclaration c) a b
labelOptic =
    (DataDeclaration c -> a)
-> (DataDeclaration c -> b -> DataDeclaration c)
-> Lens (DataDeclaration c) (DataDeclaration c) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\case OpaqueData {} -> InternalStrategy -> DataEncoding
BuiltinStrategy InternalStrategy
InternalOpaqueStrat; DataDeclaration TyName
_ Count "tyvar"
_ Vector (Constructor c)
_ DataEncoding
enc -> a
DataEncoding
enc)
      (\DataDeclaration c
decl b
enc -> case DataDeclaration c
decl of OpaqueData TyName
tn Set PlutusDataConstructor
x -> TyName -> Set PlutusDataConstructor -> DataDeclaration c
forall a. TyName -> Set PlutusDataConstructor -> DataDeclaration a
OpaqueData TyName
tn Set PlutusDataConstructor
x; DataDeclaration TyName
tn Count "tyvar"
x Vector (Constructor c)
y DataEncoding
_ -> TyName
-> Count "tyvar"
-> Vector (Constructor c)
-> DataEncoding
-> DataDeclaration c
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration TyName
tn Count "tyvar"
x Vector (Constructor c)
y b
DataEncoding
enc)

checkStrategy :: forall (a :: Type). DataDeclaration a -> Bool
checkStrategy :: forall a. DataDeclaration a -> Bool
checkStrategy = \case
  OpaqueData TyName
_ Set PlutusDataConstructor
_ -> Bool
True
  DataDeclaration TyName
tn Count "tyvar"
_ Vector (Constructor a)
ctors DataEncoding
strat -> case DataEncoding
strat of
    DataEncoding
SOP -> Bool
True
    BuiltinStrategy InternalStrategy
internalStrat -> case InternalStrategy
internalStrat of
      InternalStrategy
InternalListStrat -> TyName
tn TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"List"
      InternalStrategy
InternalPairStrat -> TyName
tn TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"Pair"
      InternalStrategy
InternalDataStrat -> TyName
tn TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"Data"
      InternalStrategy
InternalAssocMapStrat -> TyName
tn TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
"Map"
      InternalStrategy
InternalOpaqueStrat -> Bool
False
    PlutusData PlutusDataStrategy
plutusStrat -> case PlutusDataStrategy
plutusStrat of
      PlutusDataStrategy
ConstrData -> Bool
True
      PlutusDataStrategy
EnumData -> (Constructor a -> Bool) -> Vector (Constructor a) -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (\(Constructor ConstructorName
_ Vector (ValT a)
args) -> Vector (ValT a) -> Bool
forall a. Vector a -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null Vector (ValT a)
args) Vector (Constructor a)
ctors
      PlutusDataStrategy
ProductListData -> Vector (Constructor a) -> Int
forall a. Vector a -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length Vector (Constructor a)
ctors Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
      PlutusDataStrategy
NewtypeData -> case Vector (Constructor a)
ctors of
        ConsV Constructor a
x Vector (Constructor a)
NilV -> case Optic' A_Lens NoIx (Constructor a) (Vector (ValT a))
-> Constructor a -> Maybe (Vector (ValT a))
forall k (is :: IxList) s a.
Is k An_AffineFold =>
Optic' k is s a -> s -> Maybe a
preview Optic' A_Lens NoIx (Constructor a) (Vector (ValT a))
#constructorArgs Constructor a
x of
          Just (ConsV ValT a
_ Vector (ValT a)
NilV) -> Bool
True
          Maybe (Vector (ValT a))
_ -> Bool
False
        Vector (Constructor a)
_ -> Bool
False

naturalBaseFunctor :: DataDeclaration AbstractTy
naturalBaseFunctor :: DataDeclaration AbstractTy
naturalBaseFunctor = TyName
-> Count "tyvar"
-> Vector (Constructor AbstractTy)
-> DataEncoding
-> DataDeclaration AbstractTy
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration TyName
"Natural_F" Count "tyvar"
forall (ofWhat :: Symbol). Count ofWhat
count1 Vector (Constructor AbstractTy)
constrs DataEncoding
SOP
  where
    constrs :: Vector (Constructor AbstractTy)
    constrs :: Vector (Constructor AbstractTy)
constrs =
      [ ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
"ZeroNat_F" [],
        ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
"SuccNat_F" [AbstractTy -> Item (Vector (ValT AbstractTy))
AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> Item (Vector (ValT AbstractTy)))
-> (Index "tyvar" -> AbstractTy)
-> Index "tyvar"
-> Item (Vector (ValT AbstractTy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z (Index "tyvar" -> Item (Vector (ValT AbstractTy)))
-> Index "tyvar" -> Item (Vector (ValT AbstractTy))
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0]
      ]

negativeBaseFunctor :: DataDeclaration AbstractTy
negativeBaseFunctor :: DataDeclaration AbstractTy
negativeBaseFunctor = TyName
-> Count "tyvar"
-> Vector (Constructor AbstractTy)
-> DataEncoding
-> DataDeclaration AbstractTy
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration TyName
"Negative_F" Count "tyvar"
forall (ofWhat :: Symbol). Count ofWhat
count1 Vector (Constructor AbstractTy)
constrs DataEncoding
SOP
  where
    constrs :: Vector (Constructor AbstractTy)
    constrs :: Vector (Constructor AbstractTy)
constrs =
      [ ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
"ZeroNeg_F" [],
        ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
"PredNeg_F" [AbstractTy -> Item (Vector (ValT AbstractTy))
AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> Item (Vector (ValT AbstractTy)))
-> (Index "tyvar" -> AbstractTy)
-> Index "tyvar"
-> Item (Vector (ValT AbstractTy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z (Index "tyvar" -> Item (Vector (ValT AbstractTy)))
-> Index "tyvar" -> Item (Vector (ValT AbstractTy))
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0]
      ]

byteStringBaseFunctor :: DataDeclaration AbstractTy
byteStringBaseFunctor :: DataDeclaration AbstractTy
byteStringBaseFunctor = TyName
-> Count "tyvar"
-> Vector (Constructor AbstractTy)
-> DataEncoding
-> DataDeclaration AbstractTy
forall a.
TyName
-> Count "tyvar"
-> Vector (Constructor a)
-> DataEncoding
-> DataDeclaration a
DataDeclaration TyName
"ByteString_F" Count "tyvar"
forall (ofWhat :: Symbol). Count ofWhat
count1 Vector (Constructor AbstractTy)
constrs DataEncoding
SOP
  where
    constrs :: Vector (Constructor AbstractTy)
    constrs :: Vector (Constructor AbstractTy)
constrs =
      [ ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
"EmptyByteString_F" [],
        ConstructorName
-> Vector (ValT AbstractTy) -> Constructor AbstractTy
forall a. ConstructorName -> Vector (ValT a) -> Constructor a
Constructor ConstructorName
"ConsByteString_F" [BuiltinFlatT -> ValT AbstractTy
forall a. BuiltinFlatT -> ValT a
BuiltinFlat BuiltinFlatT
IntegerT, AbstractTy -> Item (Vector (ValT AbstractTy))
AbstractTy -> ValT AbstractTy
forall a. a -> ValT a
Abstraction (AbstractTy -> Item (Vector (ValT AbstractTy)))
-> (Index "tyvar" -> AbstractTy)
-> Index "tyvar"
-> Item (Vector (ValT AbstractTy))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DeBruijn -> Index "tyvar" -> AbstractTy
BoundAt DeBruijn
Z (Index "tyvar" -> Item (Vector (ValT AbstractTy)))
-> Index "tyvar" -> Item (Vector (ValT AbstractTy))
forall a b. (a -> b) -> a -> b
$ Index "tyvar"
forall (ofWhat :: Symbol). Index ofWhat
ix0]
      ]

-- Helpers

prettyCompTWithContext :: forall (ann :: Type). CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext :: forall ann. CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext (CompT Count "tyvar"
count (CompTBody NonEmptyVector (ValT Renamed)
funArgs))
  | Optic' A_Prism NoIx Int (Count "tyvar") -> Count "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Count "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)
intCount Count "tyvar"
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
forall ann. NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
prettyFunTy' NonEmptyVector (ValT Renamed)
funArgs
  | Bool
otherwise = Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall ann a.
Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
bindVars Count "tyvar"
count ((Vector (Doc ann) -> PrettyM ann (Doc ann))
 -> PrettyM ann (Doc ann))
-> (Vector (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ \Vector (Doc ann)
newVars -> do
      Doc ann
funTy <- NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
forall ann. NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
prettyFunTy' NonEmptyVector (ValT Renamed)
funArgs
      Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Vector (Doc ann) -> Doc ann -> Doc ann
forall ann. Vector (Doc ann) -> Doc ann -> Doc ann
mkForall Vector (Doc ann)
newVars Doc ann
funTy

prettyFunTy' ::
  forall (ann :: Type).
  NonEmptyVector (ValT Renamed) ->
  PrettyM ann (Doc ann)
prettyFunTy' :: forall ann. NonEmptyVector (ValT Renamed) -> PrettyM ann (Doc ann)
prettyFunTy' NonEmptyVector (ValT Renamed)
args = case NonEmptyVector (ValT Renamed)
-> (Vector (ValT Renamed), ValT Renamed)
forall a. NonEmptyVector a -> (Vector a, a)
NonEmpty.unsnoc NonEmptyVector (ValT Renamed)
args of
  (Vector (ValT Renamed)
rest, ValT Renamed
resTy) -> do
    Doc ann
resTy' <- (Doc ann
"!" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<>) (Doc ann -> Doc ann)
-> PrettyM ann (Doc ann) -> PrettyM ann (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext ValT Renamed
resTy
    case Vector (ValT Renamed)
-> Maybe (ValT Renamed, Vector (ValT Renamed))
forall a. Vector a -> Maybe (a, Vector a)
Vector.uncons Vector (ValT Renamed)
rest of
      Maybe (ValT Renamed, Vector (ValT Renamed))
Nothing -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
resTy'
      Just (ValT Renamed
firstArg, Vector (ValT Renamed)
otherArgs) -> do
        Doc ann
prettyArg1 <- ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext ValT Renamed
firstArg
        Doc ann
argsWithoutResult <- (Doc ann -> ValT Renamed -> PrettyM ann (Doc ann))
-> Doc ann -> Vector (ValT Renamed) -> PrettyM ann (Doc ann)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> b -> m a) -> a -> Vector b -> m a
Vector.foldM (\Doc ann
acc ValT Renamed
x -> (\Doc ann
z -> Doc ann
acc 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
z) (Doc ann -> Doc ann)
-> PrettyM ann (Doc ann) -> PrettyM ann (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext ValT Renamed
x) Doc ann
prettyArg1 Vector (ValT Renamed)
otherArgs
        Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> (Doc ann -> Doc ann) -> Doc ann -> PrettyM ann (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann
argsWithoutResult 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
resTy'

prettyValTWithContext :: forall (ann :: Type). ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext :: forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext = \case
  Abstraction Renamed
abstr -> Renamed -> PrettyM ann (Doc ann)
forall ann. Renamed -> PrettyM ann (Doc ann)
prettyRenamedWithContext Renamed
abstr
  ThunkT CompT Renamed
compT -> CompT Renamed -> PrettyM ann (Doc ann)
forall ann. CompT Renamed -> PrettyM ann (Doc ann)
prettyCompTWithContext CompT Renamed
compT
  BuiltinFlat BuiltinFlatT
biFlat -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ BuiltinFlatT -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow BuiltinFlatT
biFlat
  Datatype (TyName Text
tn) Vector (ValT Renamed)
args -> do
    Vector (Doc ann)
args' <- (ValT Renamed -> PrettyM ann (Doc ann))
-> Vector (ValT Renamed) -> PrettyM ann (Vector (Doc ann))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext Vector (ValT Renamed)
args
    let tn' :: Doc ann
tn' = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
tn
    case Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
Vector.toList Vector (Doc ann)
args' of
      [] -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Doc ann
tn'
      [Doc ann]
argsList -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> (Doc ann -> Doc ann) -> Doc ann -> PrettyM ann (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann
tn' Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann]
argsList

prettyCtorWithContext :: forall (ann :: Type). Constructor Renamed -> PrettyM ann (Doc ann)
prettyCtorWithContext :: forall ann. Constructor Renamed -> PrettyM ann (Doc ann)
prettyCtorWithContext (Constructor ConstructorName
ctorNm Vector (ValT Renamed)
ctorArgs)
  | Vector (ValT Renamed) -> Bool
forall a. Vector a -> Bool
Vector.null Vector (ValT Renamed)
ctorArgs = Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ConstructorName -> Text
runConstructorName ConstructorName
ctorNm)
  | Bool
otherwise = do
      let ctorNm' :: Doc ann
ctorNm' = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (ConstructorName -> Text
runConstructorName ConstructorName
ctorNm)
      [Doc ann]
args' <- Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
Vector.toList (Vector (Doc ann) -> [Doc ann])
-> PrettyM ann (Vector (Doc ann)) -> PrettyM ann [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (ValT Renamed -> PrettyM ann (Doc ann))
-> Vector (ValT Renamed) -> PrettyM ann (Vector (Doc ann))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse ValT Renamed -> PrettyM ann (Doc ann)
forall ann. ValT Renamed -> PrettyM ann (Doc ann)
prettyValTWithContext Vector (ValT Renamed)
ctorArgs
      Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann
ctorNm' Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann]
args'

prettyRenamedWithContext :: forall (ann :: Type). Renamed -> PrettyM ann (Doc ann)
prettyRenamedWithContext :: forall ann. Renamed -> PrettyM ann (Doc ann)
prettyRenamedWithContext = \case
  Rigid Int
offset Index "tyvar"
index -> Int -> Index "tyvar" -> PrettyM ann (Doc ann)
forall ann. Int -> Index "tyvar" -> PrettyM ann (Doc ann)
lookupAbstraction Int
offset Index "tyvar"
index
  Unifiable Index "tyvar"
i -> Int -> Index "tyvar" -> PrettyM ann (Doc ann)
forall ann. Int -> Index "tyvar" -> PrettyM ann (Doc ann)
lookupAbstraction Int
0 Index "tyvar"
i
  Wildcard Word64
w64 Int
offset Index "tyvar"
i -> Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
offset Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"_" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Word64 -> Doc ann
forall a ann. Show a => a -> Doc ann
viaShow Word64
w64 Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"#" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Optic' A_Prism NoIx Int (Index "tyvar") -> Index "tyvar" -> Int
forall k (is :: IxList) t b.
Is k A_Review =>
Optic' k is t b -> b -> t
review Optic' A_Prism NoIx Int (Index "tyvar")
forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)
intIndex Index "tyvar"
i)

prettyDataDeclWithContext :: forall (ann :: Type). DataDeclaration Renamed -> PrettyM ann (Doc ann)
prettyDataDeclWithContext :: forall ann. DataDeclaration Renamed -> PrettyM ann (Doc ann)
prettyDataDeclWithContext (OpaqueData (TyName Text
tn) Set PlutusDataConstructor
_) = Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> (Text -> Doc ann) -> Text -> PrettyM ann (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> PrettyM ann (Doc ann)) -> Text -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Text
tn
prettyDataDeclWithContext (DataDeclaration (TyName Text
tn) Count "tyvar"
numVars Vector (Constructor Renamed)
ctors DataEncoding
_) = Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall ann a.
Count "tyvar"
-> (Vector (Doc ann) -> PrettyM ann a) -> PrettyM ann a
bindVars Count "tyvar"
numVars ((Vector (Doc ann) -> PrettyM ann (Doc ann))
 -> PrettyM ann (Doc ann))
-> (Vector (Doc ann) -> PrettyM ann (Doc ann))
-> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ \Vector (Doc ann)
boundVars -> do
  let tn' :: Doc ann
tn' = Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
tn
  Vector (Doc ann)
ctors' <- (Constructor Renamed -> PrettyM ann (Doc ann))
-> Vector (Constructor Renamed) -> PrettyM ann (Vector (Doc ann))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse Constructor Renamed -> PrettyM ann (Doc ann)
forall ann. Constructor Renamed -> PrettyM ann (Doc ann)
prettyCtorWithContext Vector (Constructor Renamed)
ctors
  let prettyCtors :: Doc ann
prettyCtors = Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (Doc ann -> Doc ann)
-> (Vector (Doc ann) -> Doc ann) -> Vector (Doc ann) -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann)
-> (Vector (Doc ann) -> [Doc ann]) -> Vector (Doc ann) -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> [Doc ann] -> [Doc ann]
prefix Doc ann
"| " ([Doc ann] -> [Doc ann])
-> (Vector (Doc ann) -> [Doc ann]) -> Vector (Doc ann) -> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
Vector.toList (Vector (Doc ann) -> Doc ann) -> Vector (Doc ann) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Vector (Doc ann)
ctors'
  if Vector (Constructor Renamed) -> Bool
forall a. Vector a -> Bool
Vector.null Vector (Constructor Renamed)
ctors
    then Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann
"data" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
tn' Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
Vector.toList Vector (Doc ann)
boundVars)
    else Doc ann -> PrettyM ann (Doc ann)
forall a. a -> PrettyM ann a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Doc ann -> PrettyM ann (Doc ann))
-> Doc ann -> PrettyM ann (Doc ann)
forall a b. (a -> b) -> a -> b
$ Doc ann
"data" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
tn' Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
Vector.toList Vector (Doc ann)
boundVars) 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
prettyCtors
  where
    -- I don't think there's a library fn that does this? This is for the `|` in a sum type.
    prefix :: Doc ann -> [Doc ann] -> [Doc ann]
    prefix :: Doc ann -> [Doc ann] -> [Doc ann]
prefix Doc ann
_ [] = []
    prefix Doc ann
_ [Item [Doc ann]
x] = [Item [Doc ann]
x]
    prefix Doc ann
sep (Doc ann
x : [Doc ann]
xs) = Doc ann
x Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann] -> [Doc ann]
goPrefix [Doc ann]
xs
      where
        goPrefix :: [Doc ann] -> [Doc ann]
goPrefix [] = []
        goPrefix (Doc ann
y : [Doc ann]
ys) = (Doc ann
sep Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
y) Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: [Doc ann] -> [Doc ann]
goPrefix [Doc ann]
ys