-- | A "readable" Agda-like way to pretty-print PLC entities.

{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

module PlutusCore.Core.Instance.Pretty.Readable () where

import PlutusPrelude

import PlutusCore.Core.Type
import PlutusCore.Pretty.PrettyConst
import PlutusCore.Pretty.Readable

import Prettyprinter
import Prettyprinter.Custom
import Universe

-- | Split an iterated 'KindArrow' (if any) into the list of argument types and the resulting type.
viewKindArrow :: Kind ann -> Maybe ([Kind ann], Kind ann)
viewKindArrow :: forall ann. Kind ann -> Maybe ([Kind ann], Kind ann)
viewKindArrow kind0 :: Kind ann
kind0@KindArrow{} = ([Kind ann], Kind ann) -> Maybe ([Kind ann], Kind ann)
forall a. a -> Maybe a
Just (([Kind ann], Kind ann) -> Maybe ([Kind ann], Kind ann))
-> ([Kind ann], Kind ann) -> Maybe ([Kind ann], Kind ann)
forall a b. (a -> b) -> a -> b
$ Kind ann -> ([Kind ann], Kind ann)
forall {ann}. Kind ann -> ([Kind ann], Kind ann)
go Kind ann
kind0 where
    go :: Kind ann -> ([Kind ann], Kind ann)
go (KindArrow ann
_ Kind ann
dom Kind ann
cod) = ([Kind ann] -> [Kind ann])
-> ([Kind ann], Kind ann) -> ([Kind ann], Kind ann)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Kind ann
dom Kind ann -> [Kind ann] -> [Kind ann]
forall a. a -> [a] -> [a]
:) (([Kind ann], Kind ann) -> ([Kind ann], Kind ann))
-> ([Kind ann], Kind ann) -> ([Kind ann], Kind ann)
forall a b. (a -> b) -> a -> b
$ Kind ann -> ([Kind ann], Kind ann)
go Kind ann
cod
    go Kind ann
kind                  = ([], Kind ann
kind)
viewKindArrow Kind ann
_ = Maybe ([Kind ann], Kind ann)
forall a. Maybe a
Nothing

-- | Split an iterated 'TyFun' (if any) into the list of argument types and the resulting type.
viewTyFun :: Type tyname uni ann -> Maybe ([Type tyname uni ann], Type tyname uni ann)
viewTyFun :: forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe ([Type tyname uni ann], Type tyname uni ann)
viewTyFun ty0 :: Type tyname uni ann
ty0@TyFun{} = ([Type tyname uni ann], Type tyname uni ann)
-> Maybe ([Type tyname uni ann], Type tyname uni ann)
forall a. a -> Maybe a
Just (([Type tyname uni ann], Type tyname uni ann)
 -> Maybe ([Type tyname uni ann], Type tyname uni ann))
-> ([Type tyname uni ann], Type tyname uni ann)
-> Maybe ([Type tyname uni ann], Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> ([Type tyname uni ann], Type tyname uni ann)
forall {tyname} {uni :: * -> *} {ann}.
Type tyname uni ann -> ([Type tyname uni ann], Type tyname uni ann)
go Type tyname uni ann
ty0 where
    go :: Type tyname uni ann -> ([Type tyname uni ann], Type tyname uni ann)
go (TyFun ann
_ Type tyname uni ann
dom Type tyname uni ann
cod) = ([Type tyname uni ann] -> [Type tyname uni ann])
-> ([Type tyname uni ann], Type tyname uni ann)
-> ([Type tyname uni ann], Type tyname uni ann)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Type tyname uni ann
dom Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
forall a. a -> [a] -> [a]
:) (([Type tyname uni ann], Type tyname uni ann)
 -> ([Type tyname uni ann], Type tyname uni ann))
-> ([Type tyname uni ann], Type tyname uni ann)
-> ([Type tyname uni ann], Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> ([Type tyname uni ann], Type tyname uni ann)
go Type tyname uni ann
cod
    go Type tyname uni ann
ty                = ([], Type tyname uni ann
ty)
viewTyFun Type tyname uni ann
_ = Maybe ([Type tyname uni ann], Type tyname uni ann)
forall a. Maybe a
Nothing

-- | Split an iterated 'TyForall' (if any) into a list of variables that it binds and its body.
viewTyForall :: Type tyname uni ann -> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
viewTyForall :: forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
viewTyForall ty0 :: Type tyname uni ann
ty0@TyForall{} = ([TyVarDecl tyname ann], Type tyname uni ann)
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
forall a. a -> Maybe a
Just (([TyVarDecl tyname ann], Type tyname uni ann)
 -> Maybe ([TyVarDecl tyname ann], Type tyname uni ann))
-> ([TyVarDecl tyname ann], Type tyname uni ann)
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
forall {tyname} {uni :: * -> *} {ann}.
Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
go Type tyname uni ann
ty0 where
    go :: Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
go (TyForall ann
ann tyname
name Kind ann
kind Type tyname uni ann
body) = ([TyVarDecl tyname ann] -> [TyVarDecl tyname ann])
-> ([TyVarDecl tyname ann], Type tyname uni ann)
-> ([TyVarDecl tyname ann], Type tyname uni ann)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ann -> tyname -> Kind ann -> TyVarDecl tyname ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl ann
ann tyname
name Kind ann
kind TyVarDecl tyname ann
-> [TyVarDecl tyname ann] -> [TyVarDecl tyname ann]
forall a. a -> [a] -> [a]
:) (([TyVarDecl tyname ann], Type tyname uni ann)
 -> ([TyVarDecl tyname ann], Type tyname uni ann))
-> ([TyVarDecl tyname ann], Type tyname uni ann)
-> ([TyVarDecl tyname ann], Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
go Type tyname uni ann
body
    go Type tyname uni ann
ty                            = ([], Type tyname uni ann
ty)
viewTyForall Type tyname uni ann
_ = Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
forall a. Maybe a
Nothing

-- | Split an iterated 'TyLam' (if any) into a list of variables that it binds and its body.
viewTyLam :: Type tyname uni ann -> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
viewTyLam :: forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
viewTyLam ty0 :: Type tyname uni ann
ty0@TyLam{} = ([TyVarDecl tyname ann], Type tyname uni ann)
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
forall a. a -> Maybe a
Just (([TyVarDecl tyname ann], Type tyname uni ann)
 -> Maybe ([TyVarDecl tyname ann], Type tyname uni ann))
-> ([TyVarDecl tyname ann], Type tyname uni ann)
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
forall {tyname} {uni :: * -> *} {ann}.
Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
go Type tyname uni ann
ty0 where
    go :: Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
go (TyLam ann
ann tyname
name Kind ann
kind Type tyname uni ann
body) = ([TyVarDecl tyname ann] -> [TyVarDecl tyname ann])
-> ([TyVarDecl tyname ann], Type tyname uni ann)
-> ([TyVarDecl tyname ann], Type tyname uni ann)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ann -> tyname -> Kind ann -> TyVarDecl tyname ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl ann
ann tyname
name Kind ann
kind TyVarDecl tyname ann
-> [TyVarDecl tyname ann] -> [TyVarDecl tyname ann]
forall a. a -> [a] -> [a]
:) (([TyVarDecl tyname ann], Type tyname uni ann)
 -> ([TyVarDecl tyname ann], Type tyname uni ann))
-> ([TyVarDecl tyname ann], Type tyname uni ann)
-> ([TyVarDecl tyname ann], Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
-> ([TyVarDecl tyname ann], Type tyname uni ann)
go Type tyname uni ann
body
    go Type tyname uni ann
ty                         = ([], Type tyname uni ann
ty)
viewTyLam Type tyname uni ann
_ = Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
forall a. Maybe a
Nothing

-- | Split an iterated 'LamAbs' (if any) into a list of variables that it binds and its body.
viewLamAbs
    :: Term tyname name uni fun ann
    -> Maybe ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
viewLamAbs :: forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> Maybe
     ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
viewLamAbs term0 :: Term tyname name uni fun ann
term0@LamAbs{} = ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
-> Maybe
     ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (([VarDecl tyname name uni ann], Term tyname name uni fun ann)
 -> Maybe
      ([VarDecl tyname name uni ann], Term tyname name uni fun ann))
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
-> Maybe
     ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
forall {tyname} {name} {uni :: * -> *} {fun} {ann}.
Term tyname name uni fun ann
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
go Term tyname name uni fun ann
term0 where
    go :: Term tyname name uni fun ann
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
go (LamAbs ann
ann name
name Type tyname uni ann
ty Term tyname name uni fun ann
body) = ([VarDecl tyname name uni ann] -> [VarDecl tyname name uni ann])
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
ann name
name Type tyname uni ann
ty VarDecl tyname name uni ann
-> [VarDecl tyname name uni ann] -> [VarDecl tyname name uni ann]
forall a. a -> [a] -> [a]
:) (([VarDecl tyname name uni ann], Term tyname name uni fun ann)
 -> ([VarDecl tyname name uni ann], Term tyname name uni fun ann))
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
go Term tyname name uni fun ann
body
    go Term tyname name uni fun ann
term                      = ([], Term tyname name uni fun ann
term)
viewLamAbs Term tyname name uni fun ann
_ = Maybe ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
forall a. Maybe a
Nothing

-- | Split an iterated 'TyAbs' (if any) into a list of variables that it binds and its body.
viewTyAbs
    :: Term tyname name uni fun ann -> Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann)
viewTyAbs :: forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann)
viewTyAbs term0 :: Term tyname name uni fun ann
term0@TyAbs{} = ([TyVarDecl tyname ann], Term tyname name uni fun ann)
-> Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann)
forall a. a -> Maybe a
Just (([TyVarDecl tyname ann], Term tyname name uni fun ann)
 -> Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann))
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
-> Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
forall {tyname} {name} {uni :: * -> *} {fun} {ann}.
Term tyname name uni fun ann
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
go Term tyname name uni fun ann
term0 where
    go :: Term tyname name uni fun ann
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
go (TyAbs ann
ann tyname
name Kind ann
kind Term tyname name uni fun ann
body) = ([TyVarDecl tyname ann] -> [TyVarDecl tyname ann])
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ann -> tyname -> Kind ann -> TyVarDecl tyname ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl ann
ann tyname
name Kind ann
kind TyVarDecl tyname ann
-> [TyVarDecl tyname ann] -> [TyVarDecl tyname ann]
forall a. a -> [a] -> [a]
:) (([TyVarDecl tyname ann], Term tyname name uni fun ann)
 -> ([TyVarDecl tyname ann], Term tyname name uni fun ann))
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ([TyVarDecl tyname ann], Term tyname name uni fun ann)
go Term tyname name uni fun ann
body
    go Term tyname name uni fun ann
term                       = ([], Term tyname name uni fun ann
term)
viewTyAbs Term tyname name uni fun ann
_ = Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann)
forall a. Maybe a
Nothing

-- | Split an iterated 'TyApp' (if any) into the head of the application and the spine.
viewTyApp
    :: Type tyname uni ann -> Maybe (Type tyname uni ann, [Type tyname uni ann])
viewTyApp :: forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
viewTyApp Type tyname uni ann
ty0 = Type tyname uni ann
-> [Type tyname uni ann]
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
forall {tyname} {uni :: * -> *} {ann}.
Type tyname uni ann
-> [Type tyname uni ann]
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
go Type tyname uni ann
ty0 [] where
    go :: Type tyname uni ann
-> [Type tyname uni ann]
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
go (TyApp ann
_ Type tyname uni ann
fun Type tyname uni ann
arg) [Type tyname uni ann]
args = Type tyname uni ann
-> [Type tyname uni ann]
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
go Type tyname uni ann
fun ([Type tyname uni ann]
 -> Maybe (Type tyname uni ann, [Type tyname uni ann]))
-> [Type tyname uni ann]
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
arg Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
forall a. a -> [a] -> [a]
: [Type tyname uni ann]
args
    go Type tyname uni ann
_                 []   = Maybe (Type tyname uni ann, [Type tyname uni ann])
forall a. Maybe a
Nothing
    go Type tyname uni ann
fun               [Type tyname uni ann]
args = (Type tyname uni ann, [Type tyname uni ann])
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
forall a. a -> Maybe a
Just (Type tyname uni ann
fun, [Type tyname uni ann]
args)

-- | Split an iterated 'Apply'/'TyInst' (if any) into the head of the application and the spine.
viewApp
    :: Term tyname name uni fun ann
    -> Maybe
        ( Term tyname name uni fun ann
        , [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
        )
viewApp :: forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
viewApp Term tyname name uni fun ann
term0 = Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
forall {tyname} {name} {uni :: * -> *} {fun} {ann}.
Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
go Term tyname name uni fun ann
term0 [] where
    go :: Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
go (Apply ann
_ Term tyname name uni fun ann
fun Term tyname name uni fun ann
argTerm) [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args = Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
go Term tyname name uni fun ann
fun ([Either (Type tyname uni ann) (Term tyname name uni fun ann)]
 -> Maybe
      (Term tyname name uni fun ann,
       [Either (Type tyname uni ann) (Term tyname name uni fun ann)]))
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> Either (Type tyname uni ann) (Term tyname name uni fun ann)
forall a b. b -> Either a b
Right Term tyname name uni fun ann
argTerm Either (Type tyname uni ann) (Term tyname name uni fun ann)
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
forall a. a -> [a] -> [a]
: [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args
    go (TyInst ann
_ Term tyname name uni fun ann
fun Type tyname uni ann
argTy)  [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args = Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
go Term tyname name uni fun ann
fun ([Either (Type tyname uni ann) (Term tyname name uni fun ann)]
 -> Maybe
      (Term tyname name uni fun ann,
       [Either (Type tyname uni ann) (Term tyname name uni fun ann)]))
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann
-> Either (Type tyname uni ann) (Term tyname name uni fun ann)
forall a b. a -> Either a b
Left Type tyname uni ann
argTy Either (Type tyname uni ann) (Term tyname name uni fun ann)
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
forall a. a -> [a] -> [a]
: [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args
    go Term tyname name uni fun ann
_                     []   = Maybe
  (Term tyname name uni fun ann,
   [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
forall a. Maybe a
Nothing
    go Term tyname name uni fun ann
fun                   [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args = (Term tyname name uni fun ann,
 [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
forall a. a -> Maybe a
Just (Term tyname name uni fun ann
fun, [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args)

instance PrettyReadableBy configName tyname =>
        PrettyBy (PrettyConfigReadable configName) (TyVarDecl tyname ann) where
  prettyBy :: forall ann.
PrettyConfigReadable configName -> TyVarDecl tyname ann -> Doc ann
prettyBy = (TyVarDecl tyname ann
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> TyVarDecl tyname ann
-> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((TyVarDecl tyname ann
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> PrettyConfigReadable configName
 -> TyVarDecl tyname ann
 -> Doc ann)
-> (TyVarDecl tyname ann
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> TyVarDecl tyname ann
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
      TyVarDecl ann
_ tyname
x Kind ann
k -> do
          ShowKinds
showKinds <- Getting
  ShowKinds (Sole (PrettyConfigReadable configName)) ShowKinds
-> InContextM (PrettyConfigReadable configName) ShowKinds
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting
   ShowKinds (Sole (PrettyConfigReadable configName)) ShowKinds
 -> InContextM (PrettyConfigReadable configName) ShowKinds)
-> Getting
     ShowKinds (Sole (PrettyConfigReadable configName)) ShowKinds
-> InContextM (PrettyConfigReadable configName) ShowKinds
forall a b. (a -> b) -> a -> b
$ (PrettyConfigReadable configName
 -> Const ShowKinds (PrettyConfigReadable configName))
-> Sole (PrettyConfigReadable configName)
-> Const ShowKinds (Sole (PrettyConfigReadable configName))
forall env config. HasPrettyConfig env config => Lens' env config
Lens'
  (Sole (PrettyConfigReadable configName))
  (PrettyConfigReadable configName)
prettyConfig ((PrettyConfigReadable configName
  -> Const ShowKinds (PrettyConfigReadable configName))
 -> Sole (PrettyConfigReadable configName)
 -> Const ShowKinds (Sole (PrettyConfigReadable configName)))
-> ((ShowKinds -> Const ShowKinds ShowKinds)
    -> PrettyConfigReadable configName
    -> Const ShowKinds (PrettyConfigReadable configName))
-> Getting
     ShowKinds (Sole (PrettyConfigReadable configName)) ShowKinds
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowKinds -> Const ShowKinds ShowKinds)
-> PrettyConfigReadable configName
-> Const ShowKinds (PrettyConfigReadable configName)
forall configName (f :: * -> *).
Functor f =>
(ShowKinds -> f ShowKinds)
-> PrettyConfigReadable configName
-> f (PrettyConfigReadable configName)
pcrShowKinds
          Direction
-> Fixity
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann r.
MonadPrettyContext config env m =>
Direction -> Fixity -> (AnyToDoc config ann -> m r) -> m r
withPrettyAt Direction
ToTheRight Fixity
botFixity ((AnyToDoc (PrettyConfigReadable configName) ann
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
prettyBot -> do
              case ShowKinds
showKinds of
                  ShowKinds
ShowKindsYes -> Fixity
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
Fixity -> Doc ann -> m (Doc ann)
encloseM Fixity
binderFixity (Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ (tyname -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot tyname
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
<?> Kind ann -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot Kind ann
k
                  ShowKinds
ShowKindsNonType -> case Kind ann
k of
                      Type{} -> Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. a -> InContextM (PrettyConfigReadable configName) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ tyname -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot tyname
x
                      Kind ann
_      -> Fixity
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
Fixity -> Doc ann -> m (Doc ann)
encloseM Fixity
binderFixity (Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ (tyname -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot tyname
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
<?> Kind ann -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot Kind ann
k
                  ShowKinds
ShowKindsNo -> Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. a -> InContextM (PrettyConfigReadable configName) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ tyname -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot tyname
x

instance
        ( PrettyReadableBy configName tyname
        , PrettyReadableBy configName name
        , PrettyUni uni
        ) => PrettyBy (PrettyConfigReadable configName) (VarDecl tyname name uni ann) where
  prettyBy :: forall ann.
PrettyConfigReadable configName
-> VarDecl tyname name uni ann -> Doc ann
prettyBy = (VarDecl tyname name uni ann
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> VarDecl tyname name uni ann
-> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((VarDecl tyname name uni ann
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> PrettyConfigReadable configName
 -> VarDecl tyname name uni ann
 -> Doc ann)
-> (VarDecl tyname name uni ann
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> VarDecl tyname name uni ann
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
      VarDecl ann
_ name
x Type tyname uni ann
t -> do
          Direction
-> Fixity
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann r.
MonadPrettyContext config env m =>
Direction -> Fixity -> (AnyToDoc config ann -> m r) -> m r
withPrettyAt Direction
ToTheRight Fixity
botFixity ((AnyToDoc (PrettyConfigReadable configName) ann
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
prettyBot -> do
              Fixity
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
Fixity -> Doc ann -> m (Doc ann)
encloseM Fixity
binderFixity (Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ (name -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot name
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
<?> Type tyname uni ann -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyBot Type tyname uni ann
t

instance PrettyBy (PrettyConfigReadable configName) (Kind a) where
    prettyBy :: forall ann. PrettyConfigReadable configName -> Kind a -> Doc ann
prettyBy = (Kind a -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName -> Kind a -> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((Kind a -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> PrettyConfigReadable configName -> Kind a -> Doc ann)
-> (Kind a
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> Kind a
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
        (Kind a -> Maybe ([Kind a], Kind a)
forall ann. Kind ann -> Maybe ([Kind ann], Kind ann)
viewKindArrow -> Just ([Kind a]
args, Kind a
res)) -> [Kind a]
-> Kind a -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) a ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName a) =>
[a] -> a -> m (Doc ann)
iterArrowPrettyM [Kind a]
args Kind a
res
        KindArrow {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'KindArrow' is not covered by 'viewKindArrow'"
        Type{} -> InContextM (PrettyConfigReadable configName) (Doc ann)
"*"

instance (PrettyReadableBy configName tyname, PrettyParens (SomeTypeIn uni)) =>
            PrettyBy (PrettyConfigReadable configName) (Type tyname uni a) where
    prettyBy :: forall ann.
PrettyConfigReadable configName -> Type tyname uni a -> Doc ann
prettyBy = (Type tyname uni a
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName -> Type tyname uni a -> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((Type tyname uni a
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> PrettyConfigReadable configName -> Type tyname uni a -> Doc ann)
-> (Type tyname uni a
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> Type tyname uni a
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
        (Type tyname uni a -> Maybe (Type tyname uni a, [Type tyname uni a])
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe (Type tyname uni ann, [Type tyname uni ann])
viewTyApp -> Just (Type tyname uni a
fun, [Type tyname uni a]
args)) -> Type tyname uni a
-> [Type tyname uni a]
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) fun term ann.
(MonadPrettyContext config env m, PrettyBy config fun,
 PrettyBy config term) =>
fun -> [term] -> m (Doc ann)
iterAppPrettyM Type tyname uni a
fun [Type tyname uni a]
args
        TyApp {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'TyApp' is not covered by 'viewTyApp'"
        TyVar a
_ tyname
name -> tyname -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) a ann.
(MonadPretty config env m, PrettyBy config a) =>
a -> m (Doc ann)
prettyM tyname
name
        (Type tyname uni a -> Maybe ([Type tyname uni a], Type tyname uni a)
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe ([Type tyname uni ann], Type tyname uni ann)
viewTyFun -> Just ([Type tyname uni a]
args, Type tyname uni a
res)) -> [Type tyname uni a]
-> Type tyname uni a
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) a ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName a) =>
[a] -> a -> m (Doc ann)
iterArrowPrettyM [Type tyname uni a]
args Type tyname uni a
res
        TyFun {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'TyFun' is not covered by 'viewTyFun'"
        TyIFix a
_ Type tyname uni a
pat Type tyname uni a
arg -> (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"ifix" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| (Type tyname uni a -> Doc ann) -> [Type tyname uni a] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Type tyname uni a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg [Type tyname uni a
pat, Type tyname uni a
arg]
        (Type tyname uni a
-> Maybe ([TyVarDecl tyname a], Type tyname uni a)
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
viewTyForall -> Just ([TyVarDecl tyname a]
args, Type tyname uni a
body)) -> [TyVarDecl tyname a]
-> Type tyname uni a
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) arg body ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName arg,
 PrettyReadableBy configName body) =>
[arg] -> body -> m (Doc ann)
iterTyForallPrettyM [TyVarDecl tyname a]
args Type tyname uni a
body
        TyForall {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'TyForall' is not covered by 'viewTyForall'"
        TyBuiltin a
_ SomeTypeIn uni
someUni -> (PrettyConfigReadable configName -> RenderContextOver Precedence)
-> InContextM (RenderContextOver Precedence) (Doc ann)
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b c. (a -> b) -> InContextM b c -> InContextM a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap PrettyConfigReadable configName -> RenderContextOver Precedence
forall configName.
PrettyConfigReadable configName -> RenderContextOver Precedence
_pcrRenderContext (InContextM (RenderContextOver Precedence) (Doc ann)
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> InContextM (RenderContextOver Precedence) (Doc ann)
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ SomeTypeIn uni
-> InContextM (RenderContextOver Precedence) (Doc ann)
forall config env (m :: * -> *) a ann.
(MonadPretty config env m, PrettyBy config a) =>
a -> m (Doc ann)
prettyM SomeTypeIn uni
someUni
        (Type tyname uni a
-> Maybe ([TyVarDecl tyname a], Type tyname uni a)
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> Maybe ([TyVarDecl tyname ann], Type tyname uni ann)
viewTyLam -> Just ([TyVarDecl tyname a]
args, Type tyname uni a
body)) -> [TyVarDecl tyname a]
-> Type tyname uni a
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) arg body ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName arg,
 PrettyReadableBy configName body) =>
[arg] -> body -> m (Doc ann)
iterLamAbsPrettyM [TyVarDecl tyname a]
args Type tyname uni a
body
        TyLam {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'TyLam' is not covered by 'viewTyLam'"
        TySOP a
_ [[Type tyname uni a]]
tls -> (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"sop" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| ([Type tyname uni a] -> Doc ann)
-> [[Type tyname uni a]] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Type tyname uni a] -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg [[Type tyname uni a]]
tls

instance
        ( PrettyReadableBy configName tyname
        , PrettyReadableBy configName name
        , PrettyUni uni
        , Pretty fun
        ) => PrettyBy (PrettyConfigReadable configName) (Term tyname name uni fun a) where
    prettyBy :: forall ann.
PrettyConfigReadable configName
-> Term tyname name uni fun a -> Doc ann
prettyBy = (Term tyname name uni fun a
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> Term tyname name uni fun a
-> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((Term tyname name uni fun a
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> PrettyConfigReadable configName
 -> Term tyname name uni fun a
 -> Doc ann)
-> (Term tyname name uni fun a
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> Term tyname name uni fun a
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \case
        Constant a
_ Some (ValueOf uni)
con -> (PrettyConfigReadable configName -> ConstConfig)
-> InContextM ConstConfig (Doc ann)
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b c. (a -> b) -> InContextM b c -> InContextM a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (RenderContextOver Precedence -> ConstConfig
ConstConfig (RenderContextOver Precedence -> ConstConfig)
-> (PrettyConfigReadable configName
    -> RenderContextOver Precedence)
-> PrettyConfigReadable configName
-> ConstConfig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrettyConfigReadable configName -> RenderContextOver Precedence
forall configName.
PrettyConfigReadable configName -> RenderContextOver Precedence
_pcrRenderContext) (InContextM ConstConfig (Doc ann)
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> InContextM ConstConfig (Doc ann)
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ Some (ValueOf uni) -> InContextM ConstConfig (Doc ann)
forall config env (m :: * -> *) a ann.
(MonadPretty config env m, PrettyBy config a) =>
a -> m (Doc ann)
prettyM Some (ValueOf uni)
con
        Builtin a
_ fun
bi -> Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
Doc ann -> m (Doc ann)
unitDocM (Doc ann -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> Doc ann
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ fun -> Doc ann
forall ann. fun -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty fun
bi
        (Term tyname name uni fun a
-> Maybe
     (Term tyname name uni fun a,
      [Either (Type tyname uni a) (Term tyname name uni fun a)])
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> Maybe
     (Term tyname name uni fun ann,
      [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
viewApp -> Just (Term tyname name uni fun a
fun, [Either (Type tyname uni a) (Term tyname name uni fun a)]
args)) -> Term tyname name uni fun a
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) fun ty term ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName fun, PrettyReadableBy configName ty,
 PrettyReadableBy configName term) =>
fun -> [Either ty term] -> m (Doc ann)
iterInterAppPrettyM Term tyname name uni fun a
fun [Either (Type tyname uni a) (Term tyname name uni fun a)]
args
        Apply {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'Apply' is not covered by 'viewApp'"
        TyInst {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'TyInst' is not covered by 'viewApp'"
        Var a
_ name
name -> name -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) a ann.
(MonadPretty config env m, PrettyBy config a) =>
a -> m (Doc ann)
prettyM name
name
        (Term tyname name uni fun a
-> Maybe ([TyVarDecl tyname a], Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> Maybe ([TyVarDecl tyname ann], Term tyname name uni fun ann)
viewTyAbs -> Just ([TyVarDecl tyname a]
args, Term tyname name uni fun a
body)) -> [TyVarDecl tyname a]
-> Term tyname name uni fun a
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) arg body ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName arg,
 PrettyReadableBy configName body) =>
[arg] -> body -> m (Doc ann)
iterTyAbsPrettyM [TyVarDecl tyname a]
args Term tyname name uni fun a
body
        TyAbs {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'TyAbs' is not covered by 'viewTyAbs'"
        (Term tyname name uni fun a
-> Maybe ([VarDecl tyname name uni a], Term tyname name uni fun a)
forall tyname name (uni :: * -> *) fun ann.
Term tyname name uni fun ann
-> Maybe
     ([VarDecl tyname name uni ann], Term tyname name uni fun ann)
viewLamAbs -> Just ([VarDecl tyname name uni a]
args, Term tyname name uni fun a
body)) -> [VarDecl tyname name uni a]
-> Term tyname name uni fun a
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall configName env (m :: * -> *) arg body ann.
(MonadPrettyReadable configName env m,
 PrettyReadableBy configName arg,
 PrettyReadableBy configName body) =>
[arg] -> body -> m (Doc ann)
iterLamAbsPrettyM [VarDecl tyname name uni a]
args Term tyname name uni fun a
body
        LamAbs {} -> [Char] -> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a. HasCallStack => [Char] -> a
error [Char]
"Panic: 'LamAbs' is not covered by 'viewLamAbs'"
        Unwrap a
_ Term tyname name uni fun a
term -> (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"unwrap" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| [Term tyname name uni fun a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Term tyname name uni fun a
term]
        IWrap a
_ Type tyname uni a
pat Type tyname uni a
arg Term tyname name uni fun a
term ->
            (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg ->
                Doc ann
"iwrap" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| [Type tyname uni a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Type tyname uni a
pat, Type tyname uni a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Type tyname uni a
arg, Term tyname name uni fun a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Term tyname name uni fun a
term]
        Error a
_ Type tyname uni a
ty -> (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"error" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| [Parened (Type tyname uni a) -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg (Parened (Type tyname uni a) -> Doc ann)
-> Parened (Type tyname uni a) -> Doc ann
forall a b. (a -> b) -> a -> b
$ Type tyname uni a -> Parened (Type tyname uni a)
forall a. a -> Parened a
inBraces Type tyname uni a
ty]
        Constr a
_ Type tyname uni a
ty Word64
i [Term tyname name uni fun a]
es ->
            (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"constr" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| [Type tyname uni a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Type tyname uni a
ty, Word64 -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Word64
i, [Term tyname name uni fun a] -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg [Term tyname name uni fun a]
es]
        Case a
_ Type tyname uni a
ty Term tyname name uni fun a
arg [Term tyname name uni fun a]
cs ->
            (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"case" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| [Type tyname uni a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Type tyname uni a
ty, Term tyname name uni fun a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Term tyname name uni fun a
arg, [Term tyname name uni fun a] -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg [Term tyname name uni fun a]
cs]

instance PrettyReadableBy configName (Term tyname name uni fun a) =>
        PrettyBy (PrettyConfigReadable configName) (Program tyname name uni fun a) where
    prettyBy :: forall ann.
PrettyConfigReadable configName
-> Program tyname name uni fun a -> Doc ann
prettyBy = (Program tyname name uni fun a
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> Program tyname name uni fun a
-> Doc ann
forall a config ann.
(a -> InContextM config (Doc ann)) -> config -> a -> Doc ann
inContextM ((Program tyname name uni fun a
  -> InContextM (PrettyConfigReadable configName) (Doc ann))
 -> PrettyConfigReadable configName
 -> Program tyname name uni fun a
 -> Doc ann)
-> (Program tyname name uni fun a
    -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> PrettyConfigReadable configName
-> Program tyname name uni fun a
-> Doc ann
forall a b. (a -> b) -> a -> b
$ \(Program a
_ Version
version Term tyname name uni fun a
term) ->
        (AnyToDoc (PrettyConfigReadable configName) ann
 -> AnyToDoc (PrettyConfigReadable configName) ann
 -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall config env (m :: * -> *) ann.
MonadPrettyContext config env m =>
(AnyToDoc config ann -> AnyToDoc config ann -> NonEmpty (Doc ann))
-> m (Doc ann)
iterAppDocM ((AnyToDoc (PrettyConfigReadable configName) ann
  -> AnyToDoc (PrettyConfigReadable configName) ann
  -> NonEmpty (Doc ann))
 -> InContextM (PrettyConfigReadable configName) (Doc ann))
-> (AnyToDoc (PrettyConfigReadable configName) ann
    -> AnyToDoc (PrettyConfigReadable configName) ann
    -> NonEmpty (Doc ann))
-> InContextM (PrettyConfigReadable configName) (Doc ann)
forall a b. (a -> b) -> a -> b
$ \AnyToDoc (PrettyConfigReadable configName) ann
_ AnyToDoc (PrettyConfigReadable configName) ann
prettyArg -> Doc ann
"program" Doc ann -> [Doc ann] -> NonEmpty (Doc ann)
forall a. a -> [a] -> NonEmpty a
:| [Version -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Version -> Doc ann
pretty Version
version, Term tyname name uni fun a -> Doc ann
AnyToDoc (PrettyConfigReadable configName) ann
prettyArg Term tyname name uni fun a
term]