{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingVia           #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE NumericUnderscores    #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

module Plutus.Contract.Test.Coverage.Analysis.Pretty where

import Control.Arrow hiding ((<+>))
import Control.Lens ((^.))
import Data.Foldable
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Text qualified as Text
import PlutusCore.Core (TyDecl (..))
import PlutusCore.DeBruijn hiding (DeBruijn)
import PlutusCore.Default
import PlutusCore.Name
import PlutusIR
import PlutusTx.Code qualified as PlutusTx
import PlutusTx.Coverage
import Prettyprinter qualified as Pp
import Test.QuickCheck
import Text.PrettyPrint hiding (integer, (<>))
import Text.Read (readMaybe)

import UntypedPlutusCore qualified as UPLC

import Plutus.Contract.Test.Coverage.Analysis.Types

{- Note [Prettyprinting of PIR in plutus-apps]
   This code will be migrated to plutus-core in a future release. However, in order to make
   the static anylsis code in `Plutus.Contract.Test.Coverage.Analysis.Interpreter` debuggable
   now we need this here until that is done. Therefore, we will have to accept the slight
   inconvenience of this being in the wrong place (and using the wrong prettyprinting library)
   for now.
-}

-- Sane pretty printer for Plutus IR

class Pretty a where
  pretty     :: a -> Doc
  prettyPrec :: Int -> a -> Doc

  pretty = Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
0
  prettyPrec Int
_ = a -> Doc
forall a. Pretty a => a -> Doc
pretty

  {-# MINIMAL pretty | prettyPrec #-}

(<?>) :: Doc -> Doc -> Doc
Doc
a <?> :: Doc -> Doc -> Doc
<?> Doc
b = Doc -> Int -> Doc -> Doc
hang Doc
a Int
2 Doc
b

pParen :: Bool -> Doc -> Doc
pParen :: Bool -> Doc -> Doc
pParen Bool
False = Doc -> Doc
forall a. a -> a
id
pParen Bool
True  = Doc -> Doc
parens

type PrettyTm tyname name uni fun = (Eq tyname, Pretty tyname
                                    , Pretty name, Pretty (SomeTypeIn uni)
                                    , Pretty (Some (ValueOf uni)), Pretty fun)
type PrettyTy tyname uni = (Eq tyname, Pretty tyname, Pretty (SomeTypeIn uni))

instance Pretty Text.Text where
  pretty :: Text -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Text -> String) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Text.unpack

instance Pretty (PlutusTx.CompiledCode a) where
  pretty :: CompiledCode a -> Doc
pretty = Doc
-> (Program TyName Name DefaultUni DefaultFun () -> Doc)
-> Maybe (Program TyName Name DefaultUni DefaultFun ())
-> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"Nothing" Program TyName Name DefaultUni DefaultFun () -> Doc
forall a. Pretty a => a -> Doc
pretty (Maybe (Program TyName Name DefaultUni DefaultFun ()) -> Doc)
-> (CompiledCode a
    -> Maybe (Program TyName Name DefaultUni DefaultFun ()))
-> CompiledCode a
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompiledCode a
-> Maybe (Program TyName Name DefaultUni DefaultFun ())
forall (uni :: * -> *) fun a.
(Closed uni, Everywhere uni Flat, Flat fun) =>
CompiledCodeIn uni fun a -> Maybe (Program TyName Name uni fun ())
PlutusTx.getPir

instance PrettyTm tyname name uni fun => Pretty (Program tyname name uni fun ann) where
  prettyPrec :: Int -> Program tyname name uni fun ann -> Doc
prettyPrec Int
p (Program ann
_ Term tyname name uni fun ann
t) = Int -> Term tyname name uni fun ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term tyname name uni fun ann
t

instance Pretty (SomeTypeIn DefaultUni) where
  pretty :: SomeTypeIn DefaultUni -> Doc
pretty = String -> Doc
text (String -> Doc)
-> (SomeTypeIn DefaultUni -> String)
-> SomeTypeIn DefaultUni
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (SomeTypeIn DefaultUni -> Doc Any)
-> SomeTypeIn DefaultUni
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTypeIn DefaultUni -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty

instance Pretty (Some (ValueOf DefaultUni)) where
  pretty :: Some (ValueOf DefaultUni) -> Doc
pretty Some (ValueOf DefaultUni)
c = case String -> Maybe CoverageAnnotation
forall a. Read a => String -> Maybe a
readMaybe (String -> Maybe CoverageAnnotation)
-> Maybe String -> Maybe CoverageAnnotation
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> Maybe String
forall a. Read a => String -> Maybe a
readMaybe String
s of
      Just CoverageAnnotation
ann -> CoverageAnnotation -> Doc
forall a. Pretty a => a -> Doc
pretty (CoverageAnnotation
ann :: CoverageAnnotation)
      Maybe CoverageAnnotation
Nothing  -> String -> Doc
text String
s
    where s :: String
s = Doc Any -> String
forall a. Show a => a -> String
show (Some (ValueOf DefaultUni) -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty Some (ValueOf DefaultUni)
c)

instance Pretty DefaultFun where
  pretty :: DefaultFun -> Doc
pretty = String -> Doc
text (String -> Doc) -> (DefaultFun -> String) -> DefaultFun -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String)
-> (DefaultFun -> Doc Any) -> DefaultFun -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefaultFun -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty

instance Pretty Name where
  pretty :: Name -> Doc
pretty (Name Text
x Unique
u)
    | Text -> Bool
forall a. Pretty a => a -> Bool
isDead Text
x  = Doc
"_"
    | Bool
otherwise = String -> Doc
text (String -> Doc) -> (Text -> String) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Unique -> Int
unUnique Unique
u) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}")) (String -> String) -> (Text -> String) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> (Text -> Doc Any) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty (Text -> Doc) -> Text -> Doc
forall a b. (a -> b) -> a -> b
$ Text
x
    where
      isDead :: a -> Bool
isDead a
x = Doc Any -> String
forall a. Show a => a -> String
show (a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty a
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"dead"

instance Pretty NamedDeBruijn where
  pretty :: NamedDeBruijn -> Doc
pretty (NamedDeBruijn Text
x Index
idx)
    | Text -> Bool
forall a. Pretty a => a -> Bool
isDead Text
x  = Doc
"_"
    | Bool
otherwise = String -> Doc
text (String -> Doc) -> (Text -> String) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Index -> String
forall a. Show a => a -> String
show Index
idx String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}")) (String -> String) -> (Text -> String) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> (Text -> Doc Any) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty (Text -> Doc) -> Text -> Doc
forall a b. (a -> b) -> a -> b
$ Text
x
    where
      isDead :: a -> Bool
isDead a
x = Doc Any -> String
forall a. Show a => a -> String
show (a -> Doc Any
forall a ann. Pretty a => a -> Doc ann
Pp.pretty a
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"dead"

instance Pretty TyName where
  pretty :: TyName -> Doc
pretty (TyName Name
x) = Name -> Doc
forall a. Pretty a => a -> Doc
pretty Name
x

instance Pretty NamedTyDeBruijn where
  pretty :: NamedTyDeBruijn -> Doc
pretty (NamedTyDeBruijn NamedDeBruijn
x) = NamedDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedDeBruijn
x

instance Pretty CoverageAnnotation where
  pretty :: CoverageAnnotation -> Doc
pretty (CoverLocation CovLoc
loc) = [Doc] -> Doc
hcat [Doc
"\"", CovLoc -> Doc
forall a. Pretty a => a -> Doc
pretty CovLoc
loc, Doc
"\""]
  pretty (CoverBool CovLoc
loc Bool
b)   = [Doc] -> Doc
hcat [Doc
"\"", CovLoc -> Doc
forall a. Pretty a => a -> Doc
pretty CovLoc
loc, if Bool
b then Doc
"/True" else Doc
"/False", Doc
"\""]

instance Pretty CovLoc where
  pretty :: CovLoc -> Doc
pretty (CovLoc String
_ Int
l1 Int
l2 Int
c1 Int
c2)
    | Int
l1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
Prelude.== Int
l2 = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Int -> String
forall a. Show a => a -> String
show Int
l1, String
":", Int -> String
forall a. Show a => a -> String
show Int
c1, String
"-", Int -> String
forall a. Show a => a -> String
show Int
c2]
    | Bool
otherwise        = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Int -> String
forall a. Show a => a -> String
show Int
l1, String
":", Int -> String
forall a. Show a => a -> String
show Int
c1, String
"-", Int -> String
forall a. Show a => a -> String
show Int
l2, String
":", Int -> String
forall a. Show a => a -> String
show Int
c2]

instance Pretty (Kind ann) where
  prettyPrec :: Int -> Kind ann -> Doc
prettyPrec Int
_ (Type ann
_)           = Doc
"*"
  prettyPrec Int
p (KindArrow ann
_ Kind ann
k Kind ann
k') = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [Int -> Kind ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
2 Kind ann
k, Doc
"->" Doc -> Doc -> Doc
<+> Int -> Kind ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 Kind ann
k']

ppTyBind :: Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind :: (tyname, Kind ann) -> Doc
ppTyBind (tyname
x, Type{}) = tyname -> Doc
forall a. Pretty a => a -> Doc
pretty tyname
x
ppTyBind (tyname
x, Kind ann
k)      = Doc -> Doc
parens (tyname -> Doc
forall a. Pretty a => a -> Doc
pretty tyname
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Kind ann -> Doc
forall a. Pretty a => a -> Doc
pretty Kind ann
k)

ppAbstr :: Pretty b => Int -> (arg -> Doc) -> Doc -> ([arg], b) -> Doc
ppAbstr :: Int -> (arg -> Doc) -> Doc -> ([arg], b) -> Doc
ppAbstr Int
p arg -> Doc
ppBind Doc
binder ([arg]
binds, b
body) = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0)  (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
binder Doc -> Doc -> Doc
<+> ([Doc] -> Doc
fsep ((arg -> Doc) -> [arg] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map arg -> Doc
ppBind [arg]
binds) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".")) Doc -> Doc -> Doc
<?> b -> Doc
forall a. Pretty a => a -> Doc
pretty b
body

instance PrettyTy tyname uni => Pretty (Type tyname uni ann) where
  prettyPrec :: Int -> Type tyname uni ann -> Doc
prettyPrec Int
p Type tyname uni ann
a = case Type tyname uni ann
a of
    TyVar ann
_ tyname
x     -> tyname -> Doc
forall a. Pretty a => a -> Doc
pretty tyname
x
    TyBuiltin ann
_ SomeTypeIn uni
c -> SomeTypeIn uni -> Doc
forall a. Pretty a => a -> Doc
pretty SomeTypeIn uni
c
    TyFun ann
_ Type tyname uni ann
a Type tyname uni ann
b   -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1)  (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [Int -> Type tyname uni ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
2 Type tyname uni ann
a, Doc
"->" Doc -> Doc -> Doc
<+> Int -> Type tyname uni ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1 Type tyname uni ann
b]
    TyIFix ann
_ Type tyname uni ann
a Type tyname uni ann
b  -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Fix" Doc -> Doc -> Doc
<+> [Doc] -> Doc
sep [Int -> Type tyname uni ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Type tyname uni ann
a, Int -> Type tyname uni ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Type tyname uni ann
b]
    -- TyForall _ x Type{} (TyVar _ x') | x == x' -> "⊥"
    TyForall{}    -> Int
-> ((tyname, Kind ann) -> Doc)
-> Doc
-> ([(tyname, Kind ann)], Type tyname uni ann)
-> Doc
forall b arg.
Pretty b =>
Int -> (arg -> Doc) -> Doc -> ([arg], b) -> Doc
ppAbstr Int
p (tyname, Kind ann) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind Doc
"∀" (Type tyname uni ann -> ([(tyname, Kind ann)], Type tyname uni ann)
forall a (uni :: * -> *) ann.
Type a uni ann -> ([(a, Kind ann)], Type a uni ann)
view Type tyname uni ann
a)
      where
        view :: Type a uni ann -> ([(a, Kind ann)], Type a uni ann)
view (TyForall ann
_ a
x Kind ann
k Type a uni ann
b) = ([(a, Kind ann)] -> [(a, Kind ann)])
-> ([(a, Kind ann)], Type a uni ann)
-> ([(a, Kind ann)], Type a uni ann)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((a
x, Kind ann
k)(a, Kind ann) -> [(a, Kind ann)] -> [(a, Kind ann)]
forall a. a -> [a] -> [a]
:) (([(a, Kind ann)], Type a uni ann)
 -> ([(a, Kind ann)], Type a uni ann))
-> ([(a, Kind ann)], Type a uni ann)
-> ([(a, Kind ann)], Type a uni ann)
forall a b. (a -> b) -> a -> b
$ Type a uni ann -> ([(a, Kind ann)], Type a uni ann)
view Type a uni ann
b
        view Type a uni ann
a                  = ([], Type a uni ann
a)
    TyLam{}     -> Int
-> ((tyname, Kind ann) -> Doc)
-> Doc
-> ([(tyname, Kind ann)], Type tyname uni ann)
-> Doc
forall b arg.
Pretty b =>
Int -> (arg -> Doc) -> Doc -> ([arg], b) -> Doc
ppAbstr Int
p (tyname, Kind ann) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind Doc
"Λ" (Type tyname uni ann -> ([(tyname, Kind ann)], Type tyname uni ann)
forall a (uni :: * -> *) ann.
Type a uni ann -> ([(a, Kind ann)], Type a uni ann)
viewLam Type tyname uni ann
a)
      where
        viewLam :: Type a uni ann -> ([(a, Kind ann)], Type a uni ann)
viewLam (TyLam ann
_ a
x Kind ann
k Type a uni ann
b) = ([(a, Kind ann)] -> [(a, Kind ann)])
-> ([(a, Kind ann)], Type a uni ann)
-> ([(a, Kind ann)], Type a uni ann)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((a
x, Kind ann
k)(a, Kind ann) -> [(a, Kind ann)] -> [(a, Kind ann)]
forall a. a -> [a] -> [a]
:) (([(a, Kind ann)], Type a uni ann)
 -> ([(a, Kind ann)], Type a uni ann))
-> ([(a, Kind ann)], Type a uni ann)
-> ([(a, Kind ann)], Type a uni ann)
forall a b. (a -> b) -> a -> b
$ Type a uni ann -> ([(a, Kind ann)], Type a uni ann)
viewLam Type a uni ann
b
        viewLam Type a uni ann
b               = ([], Type a uni ann
b)
    TyApp{} -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Type tyname uni ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Type tyname uni ann
hd Doc -> Doc -> Doc
<?> [Doc] -> Doc
fsep ((Type tyname uni ann -> Doc) -> [Type tyname uni ann] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Type tyname uni ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11) [Type tyname uni ann]
args)
      where
        (Type tyname uni ann
hd, [Type tyname uni ann]
args) = Type tyname uni ann
-> [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, [Type tyname uni ann])
viewApp Type tyname uni ann
a []
        viewApp :: Type tyname uni ann
-> [Type tyname uni ann]
-> (Type tyname uni ann, [Type tyname uni ann])
viewApp (TyApp ann
_ Type tyname uni ann
a Type tyname uni ann
b) [Type tyname uni ann]
args = Type tyname uni ann
-> [Type tyname uni ann]
-> (Type tyname uni ann, [Type tyname uni ann])
viewApp Type tyname uni ann
a (Type tyname uni ann
b Type tyname uni ann
-> [Type tyname uni ann] -> [Type tyname uni ann]
forall a. a -> [a] -> [a]
: [Type tyname uni ann]
args)
        viewApp Type tyname uni ann
a [Type tyname uni ann]
args             = (Type tyname uni ann
a, [Type tyname uni ann]
args)

-- data Binding tyname name uni fun a = TermBind a Strictness (VarDecl tyname name uni fun a) (Term tyname name uni fun a)
--                            | TypeBind a (TyVarDecl tyname a) (Type tyname uni a)
--                            | DatatypeBind a (Datatype tyname name uni fun a)

instance PrettyTm tyname name uni fun => Pretty (Binding tyname name uni fun ann) where
  pretty :: Binding tyname name uni fun ann -> Doc
pretty Binding tyname name uni fun ann
bind = case Binding tyname name uni fun ann
bind of
    TermBind ann
_ Strictness
s VarDecl tyname name uni fun ann
vdec Term tyname name uni fun ann
t -> (VarDecl tyname name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty VarDecl tyname name uni fun ann
vdec Doc -> Doc -> Doc
<+> Doc
eq) Doc -> Doc -> Doc
<?> Term tyname name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty Term tyname name uni fun ann
t
      where
        eq :: Doc
eq | Strictness
PlutusIR.Strict <- Strictness
s = Doc
"[!]="
           | Bool
otherwise            = Doc
"[~]="
    TypeBind ann
_ TyVarDecl tyname ann
tydec Type tyname uni ann
a -> (TyVarDecl tyname ann -> Doc
forall a. Pretty a => a -> Doc
pretty TyVarDecl tyname ann
tydec Doc -> Doc -> Doc
<+> Doc
"=") Doc -> Doc -> Doc
<?> Type tyname uni ann -> Doc
forall a. Pretty a => a -> Doc
pretty Type tyname uni ann
a
    DatatypeBind ann
_ Datatype tyname name uni fun ann
dt -> Datatype tyname name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty Datatype tyname name uni fun ann
dt

-- data Datatype tyname name uni fun a = Datatype a (TyVarDecl tyname a) [TyVarDecl tyname a] name [VarDecl tyname name uni fun a]

instance PrettyTy tyname uni => Pretty (TyDecl tyname uni ann) where
  prettyPrec :: Int -> TyDecl tyname uni ann -> Doc
prettyPrec Int
p (TyDecl ann
_ Type tyname uni ann
x Kind ann
k) = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Doc
forall a. Pretty a => a -> Doc
pretty Type tyname uni ann
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Kind ann -> Doc
forall a. Pretty a => a -> Doc
pretty Kind ann
k

instance Pretty tyname => Pretty (TyVarDecl tyname ann) where
  prettyPrec :: Int -> TyVarDecl tyname ann -> Doc
prettyPrec Int
p (TyVarDecl ann
_ tyname
x Kind ann
k) = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (tyname, Kind ann) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind (tyname
x, Kind ann
k)

instance (PrettyTy tyname uni, Pretty name) => Pretty (VarDecl tyname name uni fun ann) where
  prettyPrec :: Int -> VarDecl tyname name uni fun ann -> Doc
prettyPrec Int
p (VarDecl ann
_ name
x Type tyname uni ann
a) = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ name -> Doc
forall a. Pretty a => a -> Doc
pretty name
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Type tyname uni ann -> Doc
forall a. Pretty a => a -> Doc
pretty Type tyname uni ann
a

instance PrettyTm tyname name uni fun => Pretty (Datatype tyname name uni fun ann) where
  pretty :: Datatype tyname name uni fun ann -> Doc
pretty (Datatype ann
_ TyVarDecl tyname ann
tydec [TyVarDecl tyname ann]
pars name
name [VarDecl tyname name uni fun ann]
cs) =
    [Doc] -> Doc
vcat [ Doc
"data" Doc -> Doc -> Doc
<+> TyVarDecl tyname ann -> Doc
forall a. Pretty a => a -> Doc
pretty TyVarDecl tyname ann
tydec Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((TyVarDecl tyname ann -> Doc) -> [TyVarDecl tyname ann] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map TyVarDecl tyname ann -> Doc
forall a. Pretty a => a -> Doc
pretty [TyVarDecl tyname ann]
pars) Doc -> Doc -> Doc
<+> Doc
"/" Doc -> Doc -> Doc
<+> name -> Doc
forall a. Pretty a => a -> Doc
pretty name
name Doc -> Doc -> Doc
<+> Doc
"where"
         , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (VarDecl tyname name uni fun ann -> Doc)
-> [VarDecl tyname name uni fun ann] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map VarDecl tyname name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty [VarDecl tyname name uni fun ann]
cs ]

instance PrettyTm tyname name uni fun => Pretty (Term tyname name uni fun ann) where
  prettyPrec :: Int -> Term tyname name uni fun ann -> Doc
prettyPrec Int
p Term tyname name uni fun ann
t = case Term tyname name uni fun ann
t of
    Let ann
_ Recursivity
rec NonEmpty (Binding tyname name uni fun ann)
binds Term tyname name uni fun ann
body -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [Doc
kw Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat ((Binding tyname name uni fun ann -> Doc)
-> [Binding tyname name uni fun ann] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Binding tyname name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty ([Binding tyname name uni fun ann] -> [Doc])
-> [Binding tyname name uni fun ann] -> [Doc]
forall a b. (a -> b) -> a -> b
$ NonEmpty (Binding tyname name uni fun ann)
-> [Binding tyname name uni fun ann]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Binding tyname name uni fun ann)
binds), Doc
"in" Doc -> Doc -> Doc
<+> Term tyname name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty Term tyname name uni fun ann
body]
      where
        kw :: Doc
kw | Recursivity
Rec <- Recursivity
rec = Doc
"letrec"
           | Bool
otherwise  = Doc
"let"
    Var ann
_ name
x              -> name -> Doc
forall a. Pretty a => a -> Doc
pretty name
x
    TyAbs{}              -> Int
-> ((tyname, Kind ann) -> Doc)
-> Doc
-> ([(tyname, Kind ann)], Term tyname name uni fun ann)
-> Doc
forall b arg.
Pretty b =>
Int -> (arg -> Doc) -> Doc -> ([arg], b) -> Doc
ppAbstr Int
p (tyname, Kind ann) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind Doc
"Λ" (Term tyname name uni fun ann
-> ([(tyname, Kind ann)], Term tyname name uni fun ann)
forall a name (uni :: * -> *) fun a.
Term a name uni fun a -> ([(a, Kind a)], Term a name uni fun a)
viewLam Term tyname name uni fun ann
t)
      where
        viewLam :: Term a name uni fun a -> ([(a, Kind a)], Term a name uni fun a)
viewLam (TyAbs a
_ a
x Kind a
k Term a name uni fun a
b) = ([(a, Kind a)] -> [(a, Kind a)])
-> ([(a, Kind a)], Term a name uni fun a)
-> ([(a, Kind a)], Term a name uni fun a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((a
x, Kind a
k)(a, Kind a) -> [(a, Kind a)] -> [(a, Kind a)]
forall a. a -> [a] -> [a]
:) (([(a, Kind a)], Term a name uni fun a)
 -> ([(a, Kind a)], Term a name uni fun a))
-> ([(a, Kind a)], Term a name uni fun a)
-> ([(a, Kind a)], Term a name uni fun a)
forall a b. (a -> b) -> a -> b
$ Term a name uni fun a -> ([(a, Kind a)], Term a name uni fun a)
viewLam Term a name uni fun a
b
        viewLam Term a name uni fun a
b               = ([], Term a name uni fun a
b)
    LamAbs{}             -> Int
-> (VarDecl tyname name uni Any ann -> Doc)
-> Doc
-> ([VarDecl tyname name uni Any ann],
    Term tyname name uni fun ann)
-> Doc
forall b arg.
Pretty b =>
Int -> (arg -> Doc) -> Doc -> ([arg], b) -> Doc
ppAbstr Int
p (Int -> VarDecl tyname name uni Any ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
1) Doc
"λ" (Term tyname name uni fun ann
-> ([VarDecl tyname name uni Any ann],
    Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann fun.
Term tyname name uni fun ann
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
viewLam Term tyname name uni fun ann
t)
      where
        viewLam :: Term tyname name uni fun ann
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
viewLam (LamAbs ann
_ name
x Type tyname uni ann
a Term tyname name uni fun ann
t) = ([VarDecl tyname name uni fun ann]
 -> [VarDecl tyname name uni fun ann])
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl ann
forall a. HasCallStack => a
undefined name
x Type tyname uni ann
aVarDecl tyname name uni fun ann
-> [VarDecl tyname name uni fun ann]
-> [VarDecl tyname name uni fun ann]
forall a. a -> [a] -> [a]
:) (([VarDecl tyname name uni fun ann], Term tyname name uni fun ann)
 -> ([VarDecl tyname name uni fun ann],
     Term tyname name uni fun ann))
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term tyname name uni fun ann
-> ([VarDecl tyname name uni fun ann],
    Term tyname name uni fun ann)
viewLam Term tyname name uni fun ann
t
        viewLam Term tyname name uni fun ann
t                = ([], Term tyname name uni fun ann
t)
    Apply{}              -> Int -> Term tyname name uni fun ann -> Doc
forall tyname name (uni :: * -> *) fun ann.
PrettyTm tyname name uni fun =>
Int -> Term tyname name uni fun ann -> Doc
ppApp Int
p Term tyname name uni fun ann
t
    TyInst{}             -> Int -> Term tyname name uni fun ann -> Doc
forall tyname name (uni :: * -> *) fun ann.
PrettyTm tyname name uni fun =>
Int -> Term tyname name uni fun ann -> Doc
ppApp Int
p Term tyname name uni fun ann
t
    Constant ann
_ Some (ValueOf uni)
c         -> Some (ValueOf uni) -> Doc
forall a. Pretty a => a -> Doc
pretty Some (ValueOf uni)
c
    Builtin ann
_ fun
b          -> fun -> Doc
forall a. Pretty a => a -> Doc
pretty fun
b
    Error ann
_ Type tyname uni ann
ty           -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"error" Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Type tyname uni ann -> Doc
forall a. Pretty a => a -> Doc
pretty Type tyname uni ann
ty
    IWrap ann
_ Type tyname uni ann
a Type tyname uni ann
b Term tyname name uni fun ann
t        -> Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
forall tyname name (uni :: * -> *) fun ann.
PrettyTm tyname name uni fun =>
Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
ppApp' Int
p Doc
"Wrap" [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
a, 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
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
t]
    Unwrap ann
_ Term tyname name uni fun ann
t           -> Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
forall tyname name (uni :: * -> *) fun ann.
PrettyTm tyname name uni fun =>
Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
ppApp' Int
p Doc
"unwrap" [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
t]

instance Pretty a => Pretty (Set a) where
  pretty :: Set a -> Doc
pretty = Doc -> Doc
braces (Doc -> Doc) -> (Set a -> Doc) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> (Set a -> [Doc]) -> Set a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> (Set a -> [Doc]) -> Set a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty ([a] -> [Doc]) -> (Set a -> [a]) -> Set a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList

instance {-# OVERLAPPABLE #-} Pretty a => Pretty [a] where
  pretty :: [a] -> Doc
pretty = Doc -> Doc
brackets (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> ([a] -> [Doc]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty

instance Pretty a => Pretty (SnocList a) where
  pretty :: SnocList a -> Doc
pretty = Doc -> Doc
angles (Doc -> Doc) -> (SnocList a -> Doc) -> SnocList a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> (SnocList a -> [Doc]) -> SnocList a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> (SnocList a -> [Doc]) -> SnocList a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty ([a] -> [Doc]) -> (SnocList a -> [a]) -> SnocList a -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SnocList a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

instance Pretty TyCtxEntry where
  pretty :: TyCtxEntry -> Doc
pretty (NamedTyDeBruijn
n ::: Kin
k)        = (NamedTyDeBruijn, Kin) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind (NamedTyDeBruijn
n, Kin
k)
  pretty (TyCtxDat DDat
d)     = DDat -> Doc
forall a. Pretty a => a -> Doc
pretty DDat
d
  pretty (TyCtxRecDat SnocList DDat
ds) = SnocList DDat -> Doc
forall a. Pretty a => a -> Doc
pretty SnocList DDat
ds

instance Pretty DDat where
  pretty :: DDat -> Doc
pretty (DDat Bool
r NamedTyDeBruijn
n Kin
k [NamedTyDeBruijn]
pars [DCon]
cons) = (if Bool
r then Doc
"recdata" else Doc
"data") Doc -> Doc -> Doc
<+> (NamedTyDeBruijn, Kin) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind (NamedTyDeBruijn
n, Kin
k) Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((NamedTyDeBruijn -> Doc) -> [NamedTyDeBruijn] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedTyDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty [NamedTyDeBruijn]
pars) Doc -> Doc -> Doc
<+> Doc
"where" Doc -> Doc -> Doc
<?> (Doc -> Doc
braces (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
fsep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (DCon -> Doc) -> [DCon] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map DCon -> Doc
forall a. Pretty a => a -> Doc
pretty [DCon]
cons)

instance Pretty DCon where
  pretty :: DCon -> Doc
pretty (DCon [DTyp]
ds) = [DTyp] -> Doc
forall a. Pretty a => a -> Doc
pretty [DTyp]
ds

ppApp :: PrettyTm tyname name uni fun => Int -> Term tyname name uni fun ann -> Doc
ppApp :: Int -> Term tyname name uni fun ann -> Doc
ppApp Int
p Term tyname name uni fun ann
t = (Term tyname name uni fun ann
 -> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
 -> Doc)
-> (Term tyname name uni fun ann,
    [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
-> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
forall tyname name (uni :: * -> *) fun ann.
PrettyTm tyname name uni fun =>
Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
ppApp' Int
p (Doc
 -> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
 -> Doc)
-> (Term tyname name uni fun ann -> Doc)
-> Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Term tyname name uni fun ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) (Term tyname name uni fun ann
-> (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
-> (Term tyname name uni fun ann,
    [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
viewApp Term tyname name uni fun ann
t)

ppApp' :: PrettyTm tyname name uni fun => Int -> Doc -> [Either (Type tyname uni ann) (Term tyname name uni fun ann)] -> Doc
ppApp' :: Int
-> Doc
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> Doc
ppApp' Int
p Doc
hd [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
hd Doc -> Doc -> Doc
<?> [Doc] -> Doc
fsep ((Either (Type tyname uni ann) (Term tyname name uni fun ann)
 -> Doc)
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Either (Type tyname uni ann) (Term tyname name uni fun ann) -> Doc
forall a a. (Pretty a, Pretty a) => Either a a -> Doc
ppArg [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
args)
  where
    ppArg :: Either a a -> Doc
ppArg (Left a
a)  = Doc
"@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 a
a
    ppArg (Right a
t) = Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 a
t

viewApp :: Term tyname name uni fun ann -> (Term tyname name uni fun ann, [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
viewApp :: Term tyname name uni fun ann
-> (Term tyname name uni fun ann,
    [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
viewApp Term tyname name uni fun ann
t = Term tyname name uni fun ann
-> [Either (Type tyname uni ann) (Term tyname name uni fun ann)]
-> (Term tyname name uni fun ann,
    [Either (Type tyname uni ann) (Term tyname name uni fun ann)])
forall tyname name (uni :: * -> *) fun a.
Term tyname name uni fun a
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
-> (Term tyname name uni fun a,
    [Either (Type tyname uni a) (Term tyname name uni fun a)])
go Term tyname name uni fun ann
t []
  where
    go :: Term tyname name uni fun a
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
-> (Term tyname name uni fun a,
    [Either (Type tyname uni a) (Term tyname name uni fun a)])
go (Apply a
_ Term tyname name uni fun a
t Term tyname name uni fun a
s)  [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)]
-> (Term tyname name uni fun a,
    [Either (Type tyname uni a) (Term tyname name uni fun a)])
go Term tyname name uni fun a
t (Term tyname name uni fun a
-> Either (Type tyname uni a) (Term tyname name uni fun a)
forall a b. b -> Either a b
Right Term tyname name uni fun a
s Either (Type tyname uni a) (Term tyname name uni fun a)
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
forall a. a -> [a] -> [a]
: [Either (Type tyname uni a) (Term tyname name uni fun a)]
args)
    go (TyInst a
_ Term tyname name uni fun a
t Type tyname uni a
a) [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)]
-> (Term tyname name uni fun a,
    [Either (Type tyname uni a) (Term tyname name uni fun a)])
go Term tyname name uni fun a
t (Type tyname uni a
-> Either (Type tyname uni a) (Term tyname name uni fun a)
forall a b. a -> Either a b
Left Type tyname uni a
a Either (Type tyname uni a) (Term tyname name uni fun a)
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
-> [Either (Type tyname uni a) (Term tyname name uni fun a)]
forall a. a -> [a] -> [a]
: [Either (Type tyname uni a) (Term tyname name uni fun a)]
args)
    go Term tyname name uni fun a
t [Either (Type tyname uni a) (Term tyname name uni fun a)]
args              = (Term tyname name uni fun a
t, [Either (Type tyname uni a) (Term tyname name uni fun a)]
args)

ppSubst :: Pretty a => Subst a -> Doc
ppSubst :: Subst a -> Doc
ppSubst Subst a
subst = Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
d | a
d <- Subst a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Subst a
subst ]

angles :: Doc -> Doc
angles :: Doc -> Doc
angles Doc
d = [Doc] -> Doc
hcat [Doc
"<", Doc
d, Doc
">"]

instance Pretty DTyp where
  prettyPrec :: Int -> DTyp -> Doc
prettyPrec Int
p DTyp
t = case DTyp
t of
    DTVar NamedTyDeBruijn
x []     -> NamedTyDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedTyDeBruijn
x
    DTVar NamedTyDeBruijn
x [DTyp]
ts     -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ NamedTyDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedTyDeBruijn
x Doc -> Doc -> Doc
<?> [Doc] -> Doc
fsep ((DTyp -> Doc) -> [DTyp] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> DTyp -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11) [DTyp]
ts)
    DTFun DTyp
s DTyp
t      -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> DTyp -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
6 DTyp
s Doc -> Doc -> Doc
<?> (Doc
"->" Doc -> Doc -> Doc
<+> Int -> DTyp -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
5 DTyp
t)
    DTLam NamedTyDeBruijn
x Kin
k DTyp
t    -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Λ" Doc -> Doc -> Doc
<+> ((NamedTyDeBruijn, Kin) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind (NamedTyDeBruijn
x, Kin
k) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".") Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
t
    DTForall NamedTyDeBruijn
x Type{} (DTVar NamedTyDeBruijn
x' [])
      | NamedTyDeBruijn
x NamedTyDeBruijn -> NamedTyDeBruijn -> Bool
forall a. Eq a => a -> a -> Bool
== NamedTyDeBruijn
x'    -> Doc
"⊥"
    DTForall NamedTyDeBruijn
x Kin
k DTyp
t -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"∀" Doc -> Doc -> Doc
<+> ((NamedTyDeBruijn, Kin) -> Doc
forall tyname ann. Pretty tyname => (tyname, Kind ann) -> Doc
ppTyBind (NamedTyDeBruijn
x, Kin
k) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
".") Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
t
    DTWk Weakening
w DTyp
t       -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Wk" Doc -> Doc -> Doc
<+> Weakening -> Doc
forall a. Pretty a => a -> Doc
pretty Weakening
w Doc -> Doc -> Doc
<+> Int -> DTyp -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 DTyp
t
    DTyBuiltin Kin
k   -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Builtin" Doc -> Doc -> Doc
<+> Int -> Kin -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Kin
k

instance Pretty DArg where
  prettyPrec :: Int -> DArg -> Doc
prettyPrec Int
_ (TyArg DTyp
t) = Doc
"@" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Int -> DTyp -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 DTyp
t
  prettyPrec Int
p (DArg Dom
d)  = Int -> Dom -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Dom
d

instance Pretty Int where
  pretty :: Int -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Int -> String) -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show

instance Pretty Index where
  pretty :: Index -> Doc
pretty (Index Word64
i) = String -> Doc
text (String -> Doc) -> (Word64 -> String) -> Word64 -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word64 -> String
forall a. Show a => a -> String
show (Word64 -> Doc) -> Word64 -> Doc
forall a b. (a -> b) -> a -> b
$ Word64
i

instance Pretty Weakening where
  pretty :: Weakening -> Doc
pretty (Wk [(Index, Index)]
w) = [(Index, Index)] -> Doc
forall a. Pretty a => a -> Doc
pretty [(Index, Index)]
w

instance (Pretty a, Pretty b) => Pretty (a, b) where
  pretty :: (a, b) -> Doc
pretty (a
a, b
b) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma, b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b]

instance (Pretty a, Pretty b, Pretty c) => Pretty (a, b, c) where
  pretty :: (a, b, c) -> Doc
pretty (a
a, b
b, c
c) = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma, b -> Doc
forall a. Pretty a => a -> Doc
pretty b
b Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma, c -> Doc
forall a. Pretty a => a -> Doc
pretty c
c]

instance Pretty Dom where
  prettyPrec :: Int -> Dom -> Doc
prettyPrec Int
p0 Dom
d = Doc -> Doc
locs (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ case Dom
d of
    DTop{Int
Set CoverageAnnotation
DTyp
_locations :: Dom -> Set CoverageAnnotation
depth :: Dom -> Int
ty :: Dom -> DTyp
_locations :: Set CoverageAnnotation
depth :: Int
ty :: DTyp
..}   -> (Doc
"T" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets ((DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
",") Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
depth))
    DError{}   -> Doc
"error"
    DTySusp{}  -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep [Doc
"Λ", [Doc] -> Doc
hcat [[Doc] -> Doc
fsep [Doc]
args, Doc
"."]] Doc -> Doc -> Doc
<?> Int -> Dom -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Dom
body
      where
        ([Doc]
args, Dom
body) = Dom -> ([Doc], Dom)
view Dom
d
        ppBind :: a -> Kind ann -> Doc
ppBind a
x Type{} = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x
        ppBind a
x Kind ann
k      = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Kind ann -> Doc
forall a. Pretty a => a -> Doc
pretty Kind ann
k
        view :: Dom -> ([Doc], Dom)
view (DTySusp NamedTyDeBruijn
x Kin
k Set CoverageAnnotation
_ Dom
b) = ([Doc] -> [Doc]) -> ([Doc], Dom) -> ([Doc], Dom)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (NamedTyDeBruijn -> Kin -> Doc
forall a ann. Pretty a => a -> Kind ann -> Doc
ppBind NamedTyDeBruijn
x Kin
kDoc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:) (([Doc], Dom) -> ([Doc], Dom)) -> ([Doc], Dom) -> ([Doc], Dom)
forall a b. (a -> b) -> a -> b
$ Dom -> ([Doc], Dom)
view Dom
b
        view Dom
b                 = ([], Dom
b)
    DSusp{Set CoverageAnnotation
Dom
inner :: Dom -> Dom
inner :: Dom
_locations :: Set CoverageAnnotation
_locations :: Dom -> Set CoverageAnnotation
..} -> [Doc] -> Doc
hcat [Doc
"~", Int -> Dom -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Dom
inner]
    DTrace{} -> Doc
"trace"
    DLoc{CoverageAnnotation
location :: Dom -> CoverageAnnotation
location :: CoverageAnnotation
..}   -> CoverageAnnotation -> Doc
forall a. Pretty a => a -> Doc
pretty CoverageAnnotation
location
    DLam NamedDeBruijn
x DTyp
ty Subst Dom
substD Subst DTyp
substT Trm
body Set CoverageAnnotation
_ -> Doc -> Doc
locs (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
angles (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ [Doc] -> Doc
hcat [Subst Dom -> Doc
forall a. Pretty a => SnocList a -> Doc
ppSubst Subst Dom
substD, Doc
","], [Doc] -> Doc
hcat [Subst DTyp -> Doc
forall a. Pretty a => SnocList a -> Doc
ppSubst Subst DTyp
substT, Doc
","]
                                                          , (Doc
"λ" Doc -> Doc -> Doc
<+> [Doc] -> Doc
hcat [Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ NamedDeBruijn -> Doc
forall a. Pretty a => a -> Doc
pretty NamedDeBruijn
x Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
ty, Doc
"."]) Doc -> Doc -> Doc
<?> Trm -> Doc
forall a. Pretty a => a -> Doc
pretty Trm
body ]
    DConstr{Int
Set CoverageAnnotation
DTyp
Subst Dom
argsD :: Dom -> Subst Dom
constr :: Dom -> Int
dat :: Dom -> DTyp
_locations :: Set CoverageAnnotation
argsD :: Subst Dom
constr :: Int
dat :: DTyp
_locations :: Dom -> Set CoverageAnnotation
..} -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (String -> Doc
text (String
"Con" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
constr) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets (DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
dat)) Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((Dom -> Doc) -> [Dom] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Dom -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11) ([Dom] -> [Doc]) -> [Dom] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Subst Dom -> [Dom]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Subst Dom
argsD)
    DUnion [Dom]
ds    -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> Doc
brains Doc
"|" ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Dom -> Doc) -> [Dom] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Dom -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) [Dom]
ds
    DIf{} -> Doc
"DIf"
    DMatch DTyp
t Set CoverageAnnotation
_ -> Doc
"DMatch" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
brackets (DTyp -> Doc
forall a. Pretty a => a -> Doc
pretty DTyp
t)
    DWeaken Weakening
w Dom
t -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Wk" Doc -> Doc -> Doc
<+> Weakening -> Doc
forall a. Pretty a => a -> Doc
pretty Weakening
w Doc -> Doc -> Doc
<+> Int -> Dom -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Dom
t
    where
      p :: Int
p = if [CoverageAnnotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoverageAnnotation]
ls then Int
p0 else Int
0
      ls :: [CoverageAnnotation]
ls | DWeaken{} <- Dom
d = []
         | DUnion{} <- Dom
d  = []
         | Bool
otherwise      = Set CoverageAnnotation -> [CoverageAnnotation]
forall a. Set a -> [a]
Set.toList (Set CoverageAnnotation -> [CoverageAnnotation])
-> Set CoverageAnnotation -> [CoverageAnnotation]
forall a b. (a -> b) -> a -> b
$ HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
d
      brains :: Doc -> [Doc] -> Doc
brains Doc
s (Doc
x : [Doc]
xs) = [Doc] -> Doc
sep (Doc
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc
s Doc -> Doc -> Doc
<+>) [Doc]
xs)
      brains Doc
_ []       = String -> Doc
forall a. HasCallStack => String -> a
error String
"impossible"
      locs :: Doc -> Doc
locs Doc
doc
        | [CoverageAnnotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoverageAnnotation]
ls   = Doc
doc
        | Bool
otherwise = Bool -> Doc -> Doc
pParen (Int
p0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
hsep [Doc
doc, Doc
"@", Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (CoverageAnnotation -> Doc) -> [CoverageAnnotation] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map CoverageAnnotation -> Doc
forall a. Pretty a => a -> Doc
pretty [CoverageAnnotation]
ls]
        where

instance Pretty CoverageIndex where
  pretty :: CoverageIndex -> Doc
pretty CoverageIndex
covidx = [CoverageAnnotation] -> Doc
forall a. Pretty a => a -> Doc
pretty ([CoverageAnnotation] -> Doc)
-> (Map CoverageAnnotation CoverageMetadata
    -> [CoverageAnnotation])
-> Map CoverageAnnotation CoverageMetadata
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CoverageAnnotation, CoverageMetadata) -> CoverageAnnotation)
-> [(CoverageAnnotation, CoverageMetadata)] -> [CoverageAnnotation]
forall a b. (a -> b) -> [a] -> [b]
map (CoverageAnnotation, CoverageMetadata) -> CoverageAnnotation
forall a b. (a, b) -> a
fst ([(CoverageAnnotation, CoverageMetadata)] -> [CoverageAnnotation])
-> (Map CoverageAnnotation CoverageMetadata
    -> [(CoverageAnnotation, CoverageMetadata)])
-> Map CoverageAnnotation CoverageMetadata
-> [CoverageAnnotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map CoverageAnnotation CoverageMetadata
-> [(CoverageAnnotation, CoverageMetadata)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map CoverageAnnotation CoverageMetadata -> Doc)
-> Map CoverageAnnotation CoverageMetadata -> Doc
forall a b. (a -> b) -> a -> b
$ CoverageIndex
covidx CoverageIndex
-> Getting
     (Map CoverageAnnotation CoverageMetadata)
     CoverageIndex
     (Map CoverageAnnotation CoverageMetadata)
-> Map CoverageAnnotation CoverageMetadata
forall s a. s -> Getting a s a -> a
^. Getting
  (Map CoverageAnnotation CoverageMetadata)
  CoverageIndex
  (Map CoverageAnnotation CoverageMetadata)
Iso' CoverageIndex (Map CoverageAnnotation CoverageMetadata)
coverageMetadata

deriving via a instance Pretty a => Pretty (NonNegative a)

instance (Pretty k, Pretty v) => Pretty (Map k v) where
  pretty :: Map k v -> Doc
pretty = [(k, v)] -> Doc
forall a. Pretty a => a -> Doc
pretty ([(k, v)] -> Doc) -> (Map k v -> [(k, v)]) -> Map k v -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList

instance Pretty Doc where
  pretty :: Doc -> Doc
pretty = Doc -> Doc
forall a. a -> a
id

instance {-# OVERLAPPING #-} Pretty String where
  pretty :: String -> Doc
pretty = String -> Doc
text

instance Pretty Bool where
  pretty :: Bool -> Doc
pretty = String -> Doc
text (String -> Doc) -> (Bool -> String) -> Bool -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> String
forall a. Show a => a -> String
show

instance Pretty a => Pretty (Maybe a) where
  prettyPrec :: Int -> Maybe a -> Doc
prettyPrec Int
_ Maybe a
Nothing  = Doc
"Nothing"
  prettyPrec Int
p (Just a
x) = Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Just" Doc -> Doc -> Doc
<+> Int -> a -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 a
x

instance Pretty () where
  pretty :: () -> Doc
pretty () = Doc
"()"

instance (Pretty name, Pretty (Some (ValueOf uni)), Pretty fun) => Pretty (UPLC.Program name uni fun ann) where
  prettyPrec :: Int -> Program name uni fun ann -> Doc
prettyPrec Int
p (UPLC.Program ann
_ Version ann
_ Term name uni fun ann
t) = Int -> Term name uni fun ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
p Term name uni fun ann
t

instance (Pretty name, Pretty (Some (ValueOf uni)), Pretty fun) => Pretty (UPLC.Term name uni fun ann) where
  prettyPrec :: Int -> Term name uni fun ann -> Doc
prettyPrec Int
p Term name uni fun ann
t = case Term name uni fun ann
t of
    UPLC.Var ann
_ name
x      -> name -> Doc
forall a. Pretty a => a -> Doc
pretty name
x
    UPLC.Constant ann
_ Some (ValueOf uni)
c -> Some (ValueOf uni) -> Doc
forall a. Pretty a => a -> Doc
pretty Some (ValueOf uni)
c
    UPLC.Builtin ann
_ fun
b  -> fun -> Doc
forall a. Pretty a => a -> Doc
pretty fun
b
    UPLC.Error ann
_      -> String -> Doc
text String
"error"
    UPLC.LamAbs{}     -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.> Int
0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
"λ" Doc -> Doc -> Doc
<+> [Doc] -> Doc
fsep ((name -> Doc) -> [name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map name -> Doc
forall a. Pretty a => a -> Doc
pretty [name]
args) Doc -> Doc -> Doc
<+> Doc
"->") Doc -> Doc -> Doc
<?> Term name uni fun ann -> Doc
forall a. Pretty a => a -> Doc
pretty Term name uni fun ann
body
      where
        ([name]
args, Term name uni fun ann
body) = Term name uni fun ann -> ([name], Term name uni fun ann)
forall a (uni :: * -> *) fun ann.
Term a uni fun ann -> ([a], Term a uni fun ann)
viewLam Term name uni fun ann
t
        viewLam :: Term a uni fun ann -> ([a], Term a uni fun ann)
viewLam (UPLC.LamAbs ann
_ a
x Term a uni fun ann
b) = ([a] -> [a])
-> ([a], Term a uni fun ann) -> ([a], Term a uni fun ann)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (([a], Term a uni fun ann) -> ([a], Term a uni fun ann))
-> ([a], Term a uni fun ann) -> ([a], Term a uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term a uni fun ann -> ([a], Term a uni fun ann)
viewLam Term a uni fun ann
b
        viewLam Term a uni fun ann
b                   = ([], Term a uni fun ann
b)
    UPLC.Apply{} -> Bool -> Doc -> Doc
pParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.> Int
10) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Term name uni fun ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10 Term name uni fun ann
hd Doc -> Doc -> Doc
<?> [Doc] -> Doc
fsep ((Term name uni fun ann -> Doc) -> [Term name uni fun ann] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Term name uni fun ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11) [Term name uni fun ann]
args)
      where
        (Term name uni fun ann
hd, [Term name uni fun ann]
args) = Term name uni fun ann
-> [Term name uni fun ann]
-> (Term name uni fun ann, [Term name uni fun ann])
forall name (uni :: * -> *) fun ann.
Term name uni fun ann
-> [Term name uni fun ann]
-> (Term name uni fun ann, [Term name uni fun ann])
viewApp Term name uni fun ann
t []
        viewApp :: Term name uni fun ann
-> [Term name uni fun ann]
-> (Term name uni fun ann, [Term name uni fun ann])
viewApp (UPLC.Apply ann
_ Term name uni fun ann
a Term name uni fun ann
b) [Term name uni fun ann]
args = Term name uni fun ann
-> [Term name uni fun ann]
-> (Term name uni fun ann, [Term name uni fun ann])
viewApp Term name uni fun ann
a (Term name uni fun ann
b Term name uni fun ann
-> [Term name uni fun ann] -> [Term name uni fun ann]
forall a. a -> [a] -> [a]
: [Term name uni fun ann]
args)
        viewApp Term name uni fun ann
a [Term name uni fun ann]
args                  = (Term name uni fun ann
a, [Term name uni fun ann]
args)
    Term name uni fun ann
_ -> [Doc] -> Doc
hcat ([Doc]
fds [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Term name uni fun ann -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
11 Term name uni fun ann
body])
      where
        ([Doc]
fds, Term name uni fun ann
body) = Term name uni fun ann -> ([Doc], Term name uni fun ann)
forall a name (uni :: * -> *) fun ann.
IsString a =>
Term name uni fun ann -> ([a], Term name uni fun ann)
viewForce Term name uni fun ann
t
        viewForce :: Term name uni fun ann -> ([a], Term name uni fun ann)
viewForce (UPLC.Force ann
_ Term name uni fun ann
t) = ([a] -> [a])
-> ([a], Term name uni fun ann) -> ([a], Term name uni fun ann)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a
"!"a -> [a] -> [a]
forall a. a -> [a] -> [a]
:) (([a], Term name uni fun ann) -> ([a], Term name uni fun ann))
-> ([a], Term name uni fun ann) -> ([a], Term name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> ([a], Term name uni fun ann)
viewForce Term name uni fun ann
t
        viewForce (UPLC.Delay ann
_ Term name uni fun ann
t) = ([a] -> [a])
-> ([a], Term name uni fun ann) -> ([a], Term name uni fun ann)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a
"~"a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)  (([a], Term name uni fun ann) -> ([a], Term name uni fun ann))
-> ([a], Term name uni fun ann) -> ([a], Term name uni fun ann)
forall a b. (a -> b) -> a -> b
$ Term name uni fun ann -> ([a], Term name uni fun ann)
viewForce Term name uni fun ann
t
        viewForce Term name uni fun ann
t                = ([], Term name uni fun ann
t)