{-# LANGUAGE GADTs
           , KindSignatures
           , DataKinds
           , ScopedTypeVariables
           , PatternGuards
           , Rank2Types
           , TypeOperators
           , FlexibleContexts
           , UndecidableInstances
           , LambdaCase
           #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2016.05.28
-- |
-- Module      :  Language.Hakaru.Pretty.Concrete
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  GHC-only
--
--
----------------------------------------------------------------
module Language.Hakaru.Pretty.Concrete
    (
    -- * The user-facing API
      pretty
    , prettyPrec
    , prettyType
    , prettyValue
    , prettyT
    , prettyTypeT, prettyTypeS
    -- * Helper functions (semi-public internal API)
    ) where

import           Prelude            hiding ((<>))
import           Text.PrettyPrint      (Doc, text, integer, double,
                                        (<+>), (<>), ($$), sep, cat, fsep, vcat,
                                        nest, parens, brackets, punctuate,
                                        comma, colon, equals)
import qualified Data.Foldable         as F
import qualified Data.List.NonEmpty    as L
import qualified Data.Text             as Text

-- Because older versions of "Data.Foldable" do not export 'null' apparently...
import qualified Data.Sequence         as Seq
import qualified Data.Vector           as V
import           Data.Ratio
import qualified Data.Text             as T
import           Control.Applicative   (Applicative(..))

import           Data.Number.Natural   (fromNatural, fromNonNegativeRational)
import           Data.Number.Nat
import qualified Data.Number.LogFloat  as LF

import Language.Hakaru.Syntax.IClasses (fmap11, foldMap11, jmEq1, TypeEq(..)
                                       ,Foldable21(..))
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.Coercion
import Language.Hakaru.Types.HClasses
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.Value
import Language.Hakaru.Syntax.Reducer
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Pretty.Haskell (Associativity(..))

----------------------------------------------------------------
-- | Pretty-print a term.
pretty :: (ABT Term abt) => abt '[] a -> Doc
pretty :: abt '[] a -> Doc
pretty = Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
0

-- | Pretty print a term as a Text
prettyT :: (ABT Term abt) => abt '[] a -> T.Text
prettyT :: abt '[] a -> Text
prettyT = String -> Text
T.pack (String -> Text) -> (abt '[] a -> String) -> abt '[] a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (abt '[] a -> Doc) -> abt '[] a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty

-- | Pretty-print a type as a Text
prettyTypeT :: Sing (a :: Hakaru) -> T.Text
prettyTypeT :: Sing a -> Text
prettyTypeT = String -> Text
T.pack (String -> Text) -> (Sing a -> String) -> Sing a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Sing a -> Doc) -> Sing a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sing a -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0

-- | Pretty-print a type as a String
prettyTypeS :: Sing (a :: Hakaru) -> String
prettyTypeS :: Sing a -> String
prettyTypeS = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Sing a -> Doc) -> Sing a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sing a -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0

-- | Pretty-print a term at a given precendence level.
prettyPrec :: (ABT Term abt) => Int -> abt '[] a -> Doc
prettyPrec :: Int -> abt '[] a -> Doc
prettyPrec Int
p = Int -> LC_ abt a -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
p (LC_ abt a -> Doc) -> (abt '[] a -> LC_ abt a) -> abt '[] a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_

----------------------------------------------------------------
class Pretty (f :: Hakaru -> *) where
    -- | A polymorphic variant if 'prettyPrec', for internal use.
    prettyPrec_ :: Int -> f a -> Doc

mapInit :: (a -> a) -> [a] -> [a]
mapInit :: (a -> a) -> [a] -> [a]
mapInit a -> a
f (a
x:xs :: [a]
xs@(a
_:[a]
_)) = a -> a
f a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> a) -> [a] -> [a]
forall a. (a -> a) -> [a] -> [a]
mapInit a -> a
f [a]
xs
mapInit a -> a
_ [a]
xs           = [a]
xs

sepByR :: String -> [Doc] -> Doc
sepByR :: String -> [Doc] -> Doc
sepByR String
s = [Doc] -> Doc
sep ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc -> Doc) -> [Doc] -> [Doc]
forall a. (a -> a) -> [a] -> [a]
mapInit (Doc -> Doc -> Doc
<+> String -> Doc
text String
s)

sepComma :: [Doc] -> Doc
sepComma :: [Doc] -> Doc
sepComma = [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
    -- It's safe to use fsep here despite our indentation-sensitive syntax,
    -- because commas are not a binary operator.

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

-- | Pretty-print a variable.
ppVariable :: Variable (a :: Hakaru) -> Doc
ppVariable :: Variable a -> Doc
ppVariable Variable a
x
    | Text -> Bool
Text.null (Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint Variable a
x) = String -> Doc
text (Char
'x' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show (Nat -> Int
fromNat (Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID Variable a
x))) -- We used to use '_' but...
    | Bool
otherwise             = String -> Doc
text (Text -> String
Text.unpack (Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint Variable a
x))

ppBinder :: (ABT Term abt) => abt xs a -> ([Doc], Doc)
ppBinder :: abt xs a -> ([Doc], Doc)
ppBinder abt xs a
e = [Doc] -> View (Term abt) xs a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
[Doc] -> View (Term abt) xs a -> ([Doc], Doc)
go [] (abt xs a -> View (Term abt) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs a
e)
    where
    go :: (ABT Term abt) => [Doc] -> View (Term abt) xs a -> ([Doc], Doc)
    go :: [Doc] -> View (Term abt) xs a -> ([Doc], Doc)
go [Doc]
xs (Bind Variable a
x View (Term abt) xs a
v) = [Doc] -> View (Term abt) xs a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
[Doc] -> View (Term abt) xs a -> ([Doc], Doc)
go (Variable a -> Doc
forall (a :: Hakaru). Variable a -> Doc
ppVariable Variable a
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [Doc]
xs) View (Term abt) xs a
v
    go [Doc]
xs (Var  Variable a
x)   = ([Doc] -> [Doc]
forall a. [a] -> [a]
reverse [Doc]
xs, Variable a -> Doc
forall (a :: Hakaru). Variable a -> Doc
ppVariable Variable a
x)
    go [Doc]
xs (Syn  Term abt a
t)   = ([Doc] -> [Doc]
forall a. [a] -> [a]
reverse [Doc]
xs, abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty (Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn Term abt a
t))

ppBinderAsFun :: forall abt xs a . ABT Term abt => abt xs a -> Doc
ppBinderAsFun :: abt xs a -> Doc
ppBinderAsFun abt xs a
e =
  let ([Doc]
vars, Doc
body) = abt xs a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> ([Doc], Doc)
ppBinder abt xs a
e in
  if [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
vars then Doc
body else [Doc] -> Doc
sep [[Doc] -> Doc
fsep [Doc]
vars Doc -> Doc -> Doc
<> Doc
colon, Doc
body]

ppBinder1 :: (ABT Term abt) => abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 :: abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt '[x] a
e = abt '[x] a
-> (Variable x -> abt '[] a -> (Doc, Doc, Doc)) -> (Doc, Doc, Doc)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt '[x] a
e ((Variable x -> abt '[] a -> (Doc, Doc, Doc)) -> (Doc, Doc, Doc))
-> (Variable x -> abt '[] a -> (Doc, Doc, Doc)) -> (Doc, Doc, Doc)
forall a b. (a -> b) -> a -> b
$ \Variable x
x abt '[] a
v ->
              (Variable x -> Doc
forall (a :: Hakaru). Variable a -> Doc
ppVariable Variable x
x,
               Int -> Sing x -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 (Variable x -> Sing x
forall k (a :: k). Variable a -> Sing a
varType Variable x
x),
               abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
v Variable a -> Doc
forall (a :: Hakaru). Variable a -> Doc
ppVariable (abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty (abt '[] a -> Doc)
-> (Term abt a -> abt '[] a) -> Term abt a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn))

-- TODO: since switching to ABT2, this instance requires -XFlexibleContexts; we should fix that if we can
-- BUG: since switching to ABT2, this instance requires -XUndecidableInstances; must be fixed!
instance (ABT Term abt) => Pretty (LC_ abt) where
  prettyPrec_ :: Int -> LC_ abt a -> Doc
prettyPrec_ Int
p (LC_ abt '[] a
e) =
    abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e Variable a -> Doc
forall (a :: Hakaru). Variable a -> Doc
ppVariable ((Term abt a -> Doc) -> Doc) -> (Term abt a -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        SCon args a
o :$ SArgs abt args
es      -> Int -> SCon args a -> SArgs abt args -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *)
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
ABT Term abt =>
Int -> SCon args a -> SArgs abt args -> Doc
ppSCon Int
p SCon args a
o SArgs abt args
es
        NaryOp_ NaryOp a
o Seq (abt '[] a)
es ->
            if Seq (abt '[] a) -> Bool
forall a. Seq a -> Bool
Seq.null Seq (abt '[] a)
es then NaryOp a -> Doc
forall (a :: Hakaru). NaryOp a -> Doc
identityElement NaryOp a
o
            else
                case NaryOp a
o of
                  NaryOp a
And    -> Int -> String -> Seq (abt '[] a) -> Doc
forall (a :: Hakaru).
ABT Term abt =>
Int -> String -> Seq (abt '[] a) -> Doc
asOp Int
3 String
"&&" Seq (abt '[] a)
es
                  NaryOp a
Or     -> Int -> String -> Seq (abt '[] a) -> Doc
forall (a :: Hakaru).
ABT Term abt =>
Int -> String -> Seq (abt '[] a) -> Doc
asOp Int
2 String
"||" Seq (abt '[] a)
es
                  NaryOp a
Xor    -> String -> Seq (abt '[] a) -> Doc
forall (a :: Hakaru).
ABT Term abt =>
String -> Seq (abt '[] a) -> Doc
asFun String
"xor" Seq (abt '[] a)
es
                  NaryOp a
Iff    -> String -> Seq (abt '[] a) -> Doc
forall (a :: Hakaru).
ABT Term abt =>
String -> Seq (abt '[] a) -> Doc
asFun String
"iff" Seq (abt '[] a)
es
                  Min  HOrd a
_ -> String -> Seq (abt '[] a) -> Doc
forall (a :: Hakaru).
ABT Term abt =>
String -> Seq (abt '[] a) -> Doc
asFun String
"min" Seq (abt '[] a)
es
                  Max  HOrd a
_ -> String -> Seq (abt '[] a) -> Doc
forall (a :: Hakaru).
ABT Term abt =>
String -> Seq (abt '[] a) -> Doc
asFun String
"max" Seq (abt '[] a)
es

                  Sum  HSemiring a
_ -> case Seq (abt '[] a) -> [abt '[] a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (abt '[] a)
es of
                    [abt '[] a
e1] -> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
p abt '[] a
e1
                    abt '[] a
e1:[abt '[] a]
es' -> Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
                              Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
6 abt '[] a
e1 Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                              (abt '[] a -> Doc) -> [abt '[] a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
ppNaryOpSum [abt '[] a]
es'

                  Prod HSemiring a
_ -> case Seq (abt '[] a) -> [abt '[] a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (abt '[] a)
es of
                    [abt '[] a
e1] -> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
p abt '[] a
e1
                    abt '[] a
e1:abt '[] a
e2:[abt '[] a]
es' -> Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
7) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
                                 Doc
d1' Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                                 Bool -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Bool -> abt '[] a -> Doc
ppNaryOpProd Bool
second abt '[] a
e2 Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
                                 (abt '[] a -> Doc) -> [abt '[] a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Bool -> abt '[] a -> Doc
ppNaryOpProd Bool
False) [abt '[] a]
es'
                      where d1 :: Doc
d1 = Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
7 abt '[] a
e1
                            (Doc
d1', Bool
second) =
                              abt '[] a
-> (Variable a -> (Doc, Bool))
-> (Term abt a -> (Doc, Bool))
-> (Doc, Bool)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e1 ((Doc, Bool) -> Variable a -> (Doc, Bool)
forall a b. a -> b -> a
const (Doc
d1,Bool
False)) (\Term abt a
t -> case Term abt a
t of
                                -- Use parens to distinguish division into 1
                                -- from recip
                                Literal_ (LNat Natural
1) -> (Doc -> Doc
parens Doc
d1, Bool
False)
                                Literal_ (LNat Natural
_) -> (Doc
d1, Bool
True)
                                Term abt a
_                 -> (Doc
d1, Bool
False))

          where identityElement :: NaryOp a -> Doc
                identityElement :: NaryOp a -> Doc
identityElement NaryOp a
And      = String -> Doc
text String
"true"
                identityElement NaryOp a
Or       = String -> Doc
text String
"false"
                identityElement NaryOp a
Xor      = String -> Doc
text String
"false"
                identityElement NaryOp a
Iff      = String -> Doc
text String
"true"
                identityElement (Min  HOrd a
_) = String -> Doc
forall a. HasCallStack => String -> a
error String
"min cannot be used with no arguments"
                identityElement (Max  HOrd a
_) = String -> Doc
forall a. HasCallStack => String -> a
error String
"max cannot be used with no arguments"
                identityElement (Sum  HSemiring a
_) = String -> Doc
text String
"0"
                identityElement (Prod HSemiring a
_) = String -> Doc
text String
"1"

                asOp :: (ABT Term abt)
                     => Int -> String -> Seq.Seq (abt '[] a) -> Doc
                asOp :: Int -> String -> Seq (abt '[] a) -> Doc
asOp Int
p0 String
s = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
p0)
                          (Doc -> Doc) -> (Seq (abt '[] a) -> Doc) -> Seq (abt '[] a) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Doc] -> Doc
sepByR String
s
                          ([Doc] -> Doc)
-> (Seq (abt '[] a) -> [Doc]) -> Seq (abt '[] a) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (abt '[] a -> Doc) -> [abt '[] a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec (Int
p0 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
                          ([abt '[] a] -> [Doc])
-> (Seq (abt '[] a) -> [abt '[] a]) -> Seq (abt '[] a) -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (abt '[] a) -> [abt '[] a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList

                asFun :: (ABT Term abt)
                      => String -> Seq.Seq (abt '[] a) -> Doc
                asFun :: String -> Seq (abt '[] a) -> Doc
asFun   String
s = ((Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ Int
p)
                          ((Int -> Doc) -> Doc)
-> (Seq (abt '[] a) -> Int -> Doc) -> Seq (abt '[] a) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int -> Doc) -> (Int -> Doc) -> Int -> Doc)
-> Seq (Int -> Doc) -> Int -> Doc
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
F.foldr1 (\Int -> Doc
a Int -> Doc
b Int
p' -> Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p' String
s [Int -> Doc
a, Int -> Doc
b])
                          (Seq (Int -> Doc) -> Int -> Doc)
-> (Seq (abt '[] a) -> Seq (Int -> Doc))
-> Seq (abt '[] a)
-> Int
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (abt '[] a -> Int -> Doc) -> Seq (abt '[] a) -> Seq (Int -> Doc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec)

        Literal_ Literal a
v    -> Int -> Literal a -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
p Literal a
v
        Empty_   Sing ('HArray a)
typ  -> Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5) (String -> Doc
text String
"[]." Doc -> Doc -> Doc
<+> Int -> Sing ('HArray a) -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 Sing ('HArray a)
typ)
        Array_ abt '[] 'HNat
e1 abt '[ 'HNat] a
e2  -> Bool -> Doc -> Doc
parensIf (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
$
            let (Doc
var, Doc
_, Doc
body) = abt '[ 'HNat] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt '[ 'HNat] a
e2 in
            [Doc] -> Doc
sep [ [Doc] -> Doc
sep [ String -> Doc
text String
"array" Doc -> Doc -> Doc
<+> Doc
var
                      , String -> Doc
text String
"of" Doc -> Doc -> Doc
<+> abt '[] 'HNat -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt '[] 'HNat
e1 Doc -> Doc -> Doc
<> Doc
colon ]
                , Doc
body ]

        ArrayLiteral_ [abt '[] a]
es -> [Doc] -> Doc
ppList ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (abt '[] a -> Doc) -> [abt '[] a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty [abt '[] a]
es

        Datum_ Datum (abt '[]) (HData' t)
d      -> Int -> Datum (LC_ abt) (HData' t) -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
p ((forall (i :: Hakaru). abt '[] i -> LC_ abt i)
-> Datum (abt '[]) (HData' t) -> Datum (LC_ abt) (HData' t)
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) (a :: k1 -> *)
       (b :: k1 -> *) (j :: k2).
Functor11 f =>
(forall (i :: k1). a i -> b i) -> f a j -> f b j
fmap11 forall (i :: Hakaru). abt '[] i -> LC_ abt i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_ Datum (abt '[]) (HData' t)
d)
        Case_  abt '[] a
e1 [Branch (PDatum Text
h2 PDatumCode (Code t) xs (HData' t)
_) abt xs a
e2, Branch (PDatum Text
h3 PDatumCode (Code t) xs (HData' t)
_) abt xs a
e3]
            | String
"true"  <- Text -> String
Text.unpack Text
h2
            , String
"false" <- Text -> String
Text.unpack Text
h3
            , ([], Doc
body2) <- abt xs a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> ([Doc], Doc)
ppBinder abt xs a
e2
            , ([], Doc
body3) <- abt xs a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> ([Doc], Doc)
ppBinder abt xs a
e3
            -> Bool -> Doc -> Doc
parensIf (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] -> Doc
sep [ String -> Doc
text String
"if" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt '[] a
e1 Doc -> Doc -> Doc
<> Doc
colon, Int -> Doc -> Doc
nest Int
2 Doc
body2 ]
                   , [Doc] -> Doc
sep [ String -> Doc
text String
"else" Doc -> Doc -> Doc
<> Doc
colon, Int -> Doc -> Doc
nest Int
2 Doc
body3 ] ]
        Case_  abt '[] a
e1 [Branch a abt a]
bs  -> Bool -> Doc -> Doc
parensIf (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 [ String -> Doc
text String
"match" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt '[] a
e1 Doc -> Doc -> Doc
<> Doc
colon
                , [Doc] -> Doc
vcat ((Branch a abt a -> Doc) -> [Branch a abt a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Branch a abt a -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
0) [Branch a abt a]
bs) ]
        Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes -> case NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))]
forall a. NonEmpty a -> [a]
L.toList NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pes of
                            [(abt '[] 'HProb, abt '[] ('HMeasure a))
wm] -> Int -> (abt '[] 'HProb, abt '[] ('HMeasure a)) -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> (abt '[] a, abt '[] b) -> Doc
ppWeight Int
p (abt '[] 'HProb, abt '[] ('HMeasure a))
wm
                            [(abt '[] 'HProb, abt '[] ('HMeasure a))]
wms  -> Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1)
                                  (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [Doc] -> Doc
sepByR String
"<|>"
                                  ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((abt '[] 'HProb, abt '[] ('HMeasure a)) -> Doc)
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> (abt '[] 'HProb, abt '[] ('HMeasure a)) -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> (abt '[] a, abt '[] b) -> Doc
ppWeight Int
2) [(abt '[] 'HProb, abt '[] ('HMeasure a))]
wms
          where ppWeight :: Int -> (abt '[] a, abt '[] b) -> Doc
ppWeight Int
p (abt '[] a
w,abt '[] b
m)
                    | Syn (Literal_ (LProb 1)) <- abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
w
                    = Int -> abt '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
p abt '[] b
m
                    | Bool
otherwise
                    = Int -> String -> abt '[] a -> abt '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"weight" abt '[] a
w abt '[] b
m

        Reject_ Sing ('HMeasure a)
typ -> Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5) (String -> Doc
text String
"reject." Doc -> Doc -> Doc
<+> Int -> Sing ('HMeasure a) -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 Sing ('HMeasure a)
typ)

        Bucket abt '[] 'HNat
lo abt '[] 'HNat
hi Reducer abt '[] a
red -> Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"rbucket"
                            [ (Int -> abt '[] 'HNat -> Doc) -> abt '[] 'HNat -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] 'HNat -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] 'HNat
lo, (Int -> abt '[] 'HNat -> Doc) -> abt '[] 'HNat -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] 'HNat -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] 'HNat
hi
                            , (Int -> Reducer abt '[] a -> Doc)
-> Reducer abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Reducer abt '[] a -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Reducer abt '[] a
red ]

instance ABT Term abt => Pretty (Reducer abt xs) where
  prettyPrec_ :: Int -> Reducer abt xs a -> Doc
prettyPrec_ = (Reducer abt xs a -> Int -> Doc) -> Int -> Reducer abt xs a -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reducer abt xs a -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru).
Reducer abt xs1 a -> Int -> Doc
ppr where
    ppRbinder :: abt xs1 a -> Int -> Doc
    ppRbinder :: abt xs1 a -> Int -> Doc
ppRbinder abt xs1 a
f Int
p =
      let ([Doc]
vs,Doc
b) = abt xs1 a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> ([Doc], Doc)
ppBinder abt xs1 a
f
      in Bool -> Doc -> Doc
parensIf (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] -> Doc
sepComma [Doc]
vs Doc -> Doc -> Doc
<> Doc
colon, Doc
b ]

    ppr :: Reducer abt xs1 a -> Int -> Doc
    ppr :: Reducer abt xs1 a -> Int -> Doc
ppr Reducer abt xs1 a
red Int
p =
      case Reducer abt xs1 a
red of
        Red_Fanout Reducer abt xs1 a
l Reducer abt xs1 b
r  -> Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"rfanout"
                             [ Reducer abt xs1 a -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru).
Reducer abt xs1 a -> Int -> Doc
ppr Reducer abt xs1 a
l
                             , Reducer abt xs1 b -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru).
Reducer abt xs1 a -> Int -> Doc
ppr Reducer abt xs1 b
r ]
        Red_Index abt xs1 'HNat
s abt ('HNat : xs1) 'HNat
k Reducer abt ('HNat : xs1) a
r -> Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"rindex"
                             [ abt xs1 'HNat -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru). abt xs1 a -> Int -> Doc
ppRbinder abt xs1 'HNat
s
                             , abt ('HNat : xs1) 'HNat -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru). abt xs1 a -> Int -> Doc
ppRbinder abt ('HNat : xs1) 'HNat
k
                             , Reducer abt ('HNat : xs1) a -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru).
Reducer abt xs1 a -> Int -> Doc
ppr Reducer abt ('HNat : xs1) a
r ]
        Red_Split abt ('HNat : xs1) HBool
b Reducer abt xs1 a
l Reducer abt xs1 b
r -> Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"rsplit"
                             [ abt ('HNat : xs1) HBool -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru). abt xs1 a -> Int -> Doc
ppRbinder abt ('HNat : xs1) HBool
b
                             , Reducer abt xs1 a -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru).
Reducer abt xs1 a -> Int -> Doc
ppr Reducer abt xs1 a
l
                             , Reducer abt xs1 b -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru).
Reducer abt xs1 a -> Int -> Doc
ppr Reducer abt xs1 b
r ]
        Reducer abt xs1 a
Red_Nop         -> String -> Doc
text String
"rnop"
        Red_Add HSemiring a
_ abt ('HNat : xs1) a
k     -> Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"radd" [ abt ('HNat : xs1) a -> Int -> Doc
forall (xs1 :: [Hakaru]) (a :: Hakaru). abt xs1 a -> Int -> Doc
ppRbinder abt ('HNat : xs1) a
k ]

ppNaryOpSum
    :: forall abt a . (ABT Term abt) => abt '[] a -> Doc
ppNaryOpSum :: abt '[] a -> Doc
ppNaryOpSum abt '[] a
e =
    abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e (Doc -> Variable a -> Doc
forall a b. a -> b -> a
const Doc
d) ((Term abt a -> Doc) -> Doc) -> (Term abt a -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        PrimOp_ (Negate HRing a
_) :$ abt vars a
e1 :* SArgs abt args
End -> String -> Doc
text String
"-" Doc -> Doc -> Doc
<+> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
7 abt vars a
abt '[] a
e1
        Term abt a
_ -> Doc
d
  where d :: Doc
d = String -> Doc
text String
"+" Doc -> Doc -> Doc
<+> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
7 abt '[] a
e

ppNaryOpProd
    :: forall abt a . (ABT Term abt) => Bool -> abt '[] a -> Doc
ppNaryOpProd :: Bool -> abt '[] a -> Doc
ppNaryOpProd Bool
second abt '[] a
e =
    abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e (Doc -> Variable a -> Doc
forall a b. a -> b -> a
const Doc
d) ((Term abt a -> Doc) -> Doc) -> (Term abt a -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        PrimOp_ (Recip HFractional a
_) :$ abt vars a
e1 :* SArgs abt args
End ->
            if Bool -> Bool
not Bool
second then Doc
d' else
            abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt vars a
abt '[] a
e1 (Doc -> Variable a -> Doc
forall a b. a -> b -> a
const Doc
d') ((Term abt a -> Doc) -> Doc) -> (Term abt a -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt a
t' ->
                case Term abt a
t' of
                -- Use parens to distinguish division of nats
                -- from prob literal
                Literal_ (LNat Natural
_) -> String -> Doc
text String
"/" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1)
                Term abt a
_ -> Doc
d'
          where d' :: Doc
d' = String -> Doc
text String
"/" Doc -> Doc -> Doc
<+> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
8 abt vars a
abt '[] a
e1
        Term abt a
_ -> Doc
d
  where d :: Doc
d = String -> Doc
text String
"*" Doc -> Doc -> Doc
<+> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
8 abt '[] a
e

-- | Pretty-print @(:$)@ nodes in the AST.
ppSCon :: (ABT Term abt) => Int -> SCon args a -> SArgs abt args -> Doc
ppSCon :: Int -> SCon args a -> SArgs abt args -> Doc
ppSCon Int
p SCon args a
Lam_ = \(abt vars a
e1 :* SArgs abt args
End) ->
    let (Doc
var, Doc
typ, Doc
body) = abt '[a] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[a] a
e1 in
    Bool -> Doc -> Doc
parensIf (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 [ String -> Doc
text String
"fn" Doc -> Doc -> Doc
<+> Doc
var Doc -> Doc -> Doc
<+> Doc
typ Doc -> Doc -> Doc
<> Doc
colon
        , Doc
body ]

--ppSCon p App_ = \(e1 :* e2 :* End) -> ppArg e1 ++ parens True (ppArg e2)
ppSCon Int
p SCon args a
App_ = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Int -> abt '[] (a ':-> a) -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> abt '[] (a ':-> b) -> abt '[] a -> Doc
prettyApps Int
p abt vars a
abt '[] (a ':-> a)
e1 abt vars a
abt '[] a
e2

ppSCon Int
p SCon args a
Let_ = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) ->
    -- TODO: generate 'def' if possible
    let (Doc
var, Doc
_, Doc
body) = abt '[a] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[a] a
e2 in
    Bool -> Doc -> Doc
parensIf (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
var Doc -> Doc -> Doc
<+> Doc
equals Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1 Doc -> Doc -> Doc
$$ Doc
body
{-
ppSCon p (Ann_ typ) = \(e1 :* End) ->
    parensIf (p > 5) (prettyPrec 6 e1 <> text "." <+> prettyType 0 typ)
-}

ppSCon Int
p (PrimOp_     PrimOp typs a
o) = \SArgs abt args
es          -> Int -> PrimOp typs a -> SArgs abt args -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
Int -> PrimOp typs a -> SArgs abt args -> Doc
ppPrimOp     Int
p PrimOp typs a
o SArgs abt args
es
ppSCon Int
p (ArrayOp_    ArrayOp typs a
o) = \SArgs abt args
es          -> Int -> ArrayOp typs a -> SArgs abt args -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
Int -> ArrayOp typs a -> SArgs abt args -> Doc
ppArrayOp    Int
p ArrayOp typs a
o SArgs abt args
es
ppSCon Int
p (CoerceTo_   Coercion a a
c) = \(abt vars a
e1 :* SArgs abt args
End) -> Int -> Coercion a a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> Coercion a b -> abt '[] a -> Doc
ppCoerceTo   Int
p Coercion a a
c abt vars a
abt '[] a
e1
ppSCon Int
p (UnsafeFrom_ Coercion a b
c) = \(abt vars a
e1 :* SArgs abt args
End) -> Int -> Coercion a b -> abt '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> Coercion a b -> abt '[] b -> Doc
ppUnsafeFrom Int
p Coercion a b
c abt vars a
abt '[] b
e1
ppSCon Int
p (MeasureOp_  MeasureOp typs a
o) = \SArgs abt args
es          -> Int -> MeasureOp typs a -> SArgs abt args -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
Int -> MeasureOp typs a -> SArgs abt args -> Doc
ppMeasureOp  Int
p MeasureOp typs a
o SArgs abt args
es
ppSCon Int
p SCon args a
Dirac = \(abt vars a
e1 :* SArgs abt args
End) ->
    Bool -> Doc -> Doc
parensIf (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
$
    String -> Doc
text String
"return" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1
ppSCon Int
p SCon args a
MBind = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) ->
    let (Doc
var, Doc
_, Doc
body) = abt '[a] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[a] a
e2 in
    Bool -> Doc -> Doc
parensIf (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
var Doc -> Doc -> Doc
<+> String -> Doc
text String
"<~" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1 Doc -> Doc -> Doc
$$ Doc
body

ppSCon Int
p SCon args a
Plate = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) ->
    let (Doc
var, Doc
_, Doc
body) = abt '[ 'HNat] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[ 'HNat] a
e2 in
    Bool -> Doc -> Doc
parensIf (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] -> Doc
sep [ String -> Doc
text String
"plate" Doc -> Doc -> Doc
<+> Doc
var
              , String -> Doc
text String
"of" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1 Doc -> Doc -> Doc
<> Doc
colon ]
        , Int -> Doc -> Doc
nest Int
2 Doc
body ]

ppSCon Int
p SCon args a
Chain = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
    let (Doc
var, Doc
_, Doc
body) = abt '[s] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[s] a
e3 in
    Bool -> Doc -> Doc
parensIf (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] -> Doc
sep [ String -> Doc
text String
"chain" Doc -> Doc -> Doc
<+> Doc
var
              , String -> Doc
text String
"from" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e2
              , String -> Doc
text String
"of" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1 Doc -> Doc -> Doc
<> Doc
colon ]
        , Int -> Doc -> Doc
nest Int
2 Doc
body ]

ppSCon Int
p SCon args a
Integrate = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
    let (Doc
var, Doc
_, Doc
body) = abt '[ 'HReal] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[ 'HReal] a
e3 in
    Bool -> Doc -> Doc
parensIf (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] -> Doc
sep [ String -> Doc
text String
"integrate" Doc -> Doc -> Doc
<+> Doc
var
              , String -> Doc
text String
"from" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1
              , String -> Doc
text String
"to" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e2 Doc -> Doc -> Doc
<> Doc
colon ]
        , Int -> Doc -> Doc
nest Int
2 Doc
body ]

ppSCon Int
p (Summate HDiscrete a
_ HSemiring a
_) = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
    let (Doc
var, Doc
_, Doc
body) = abt '[a] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[a] a
e3 in
    Bool -> Doc -> Doc
parensIf (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] -> Doc
sep [ String -> Doc
text String
"summate" Doc -> Doc -> Doc
<+> Doc
var
              , String -> Doc
text String
"from" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1
              , String -> Doc
text String
"to" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e2 Doc -> Doc -> Doc
<> Doc
colon ]
        , Int -> Doc -> Doc
nest Int
2 Doc
body ]

ppSCon Int
p (Product HDiscrete a
_ HSemiring a
_) = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
    let (Doc
var, Doc
_, Doc
body) = abt '[a] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[a] a
e3 in
    Bool -> Doc -> Doc
parensIf (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] -> Doc
sep [ String -> Doc
text String
"product" Doc -> Doc -> Doc
<+> Doc
var
              , String -> Doc
text String
"from" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1
              , String -> Doc
text String
"to" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e2 Doc -> Doc -> Doc
<> Doc
colon ]
        , Int -> Doc -> Doc
nest Int
2 Doc
body ]

ppSCon Int
p (Transform_ Transform args a
t) = Int -> Transform args a -> SArgs abt args -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *)
       (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
ABT Term abt =>
Int -> Transform args a -> SArgs abt args -> Doc
ppTransform Int
p Transform args a
t

ppTransform :: (ABT Term abt)
            => Int -> Transform args a
            -> SArgs abt args -> Doc
ppTransform :: Int -> Transform args a -> SArgs abt args -> Doc
ppTransform Int
p Transform args a
t SArgs abt args
es =
  case Transform args a
t of
    Transform args a
Expect ->
      case SArgs abt args
es of
        abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End ->
          let (Doc
var, Doc
_, Doc
body) = abt '[a] a -> (Doc, Doc, Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: Hakaru)
       (a :: Hakaru).
ABT Term abt =>
abt '[x] a -> (Doc, Doc, Doc)
ppBinder1 abt vars a
abt '[a] a
e2 in
          Bool -> Doc -> Doc
parensIf (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 [ String -> Doc
text String
"expect" Doc -> Doc -> Doc
<+> Doc
var Doc -> Doc -> Doc
<+> String -> Doc
text String
"<~" Doc -> Doc -> Doc
<+> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e1 Doc -> Doc -> Doc
<> Doc
colon
              , Doc
body ]
    Transform args a
_ -> Int -> String -> SArgs abt args -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *)
       (xs :: [([Hakaru], Hakaru)]).
ABT Term abt =>
Int -> String -> SArgs abt xs -> Doc
ppApply Int
p (Transform args a -> String
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
Transform args a -> String
transformName Transform args a
t) SArgs abt args
es

ppCoerceTo :: ABT Term abt => Int -> Coercion a b -> abt '[] a -> Doc
ppCoerceTo :: Int -> Coercion a b -> abt '[] a -> Doc
ppCoerceTo Int
p Coercion a b
c = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
f
    -- BUG: this may not work quite right when the coercion isn't one of the special named ones...
    where
    f :: String
f = case Coercion a b
c of
          Signed HRing b
HRing_Real             `CCons` Coercion b b
CNil -> String
"prob2real"
          Signed HRing b
HRing_Int              `CCons` Coercion b b
CNil -> String
"nat2int"
          Continuous HContinuous b
HContinuous_Real   `CCons` Coercion b b
CNil -> String
"int2real"
          Continuous HContinuous b
HContinuous_Prob   `CCons` Coercion b b
CNil -> String
"nat2prob"
          Continuous HContinuous b
HContinuous_Prob   `CCons`
            Signed HRing b
HRing_Real           `CCons` Coercion b b
CNil -> String
"nat2real"
          Signed HRing b
HRing_Int              `CCons`
            Continuous HContinuous b
HContinuous_Real `CCons` Coercion b b
CNil -> String
"nat2real"
          Coercion a b
_ -> String
"coerceTo_ (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Coercion a b -> String
forall a. Show a => a -> String
show Coercion a b
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"


ppUnsafeFrom :: ABT Term abt => Int -> Coercion a b -> abt '[] b -> Doc
ppUnsafeFrom :: Int -> Coercion a b -> abt '[] b -> Doc
ppUnsafeFrom Int
p Coercion a b
c = Int -> String -> abt '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
f
    -- BUG: this may not work quite right when the coercion isn't one of the special named ones...
    where
    f :: String
f = case Coercion a b
c of
          Signed HRing b
HRing_Real `CCons` Coercion b b
CNil -> String
"real2prob"
          Signed HRing b
HRing_Int  `CCons` Coercion b b
CNil -> String
"int2nat"
          Coercion a b
_ -> String
"unsafeFrom_ (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Coercion a b -> String
forall a. Show a => a -> String
show Coercion a b
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"


-- | Pretty-print a type.
prettyType :: Int -> Sing (a :: Hakaru) -> Doc
prettyType :: Int -> Sing a -> Doc
prettyType Int
_ Sing a
SNat         = String -> Doc
text String
"nat"
prettyType Int
_ Sing a
SInt         = String -> Doc
text String
"int"
prettyType Int
_ Sing a
SProb        = String -> Doc
text String
"prob"
prettyType Int
_ Sing a
SReal        = String -> Doc
text String
"real"
prettyType Int
p (SFun   a b) = Bool -> Doc -> Doc
parensIf (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 [ Int -> Sing a -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
1 Sing a
a Doc -> Doc -> Doc
<+> String -> Doc
text String
"->"
                                , Int -> Sing b -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 Sing b
b ]
prettyType Int
p (SMeasure a) = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"measure" [(Int -> Sing a -> Doc) -> Sing a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing a -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing a
a]
prettyType Int
p (SArray   a) = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"array" [(Int -> Sing a -> Doc) -> Sing a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing a -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing a
a]
prettyType Int
p (SData (STyCon sym `STyApp` a `STyApp` b) _)
    | Just TypeEq s "Pair"
Refl <- Sing s -> Sing "Pair" -> Maybe (TypeEq s "Pair")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Pair"
sSymbol_Pair
    = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"pair" [(Int -> Sing b -> Doc) -> Sing b -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing b -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing b
a, (Int -> Sing b -> Doc) -> Sing b -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing b -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing b
b]
    | Just TypeEq s "Either"
Refl <- Sing s -> Sing "Either" -> Maybe (TypeEq s "Either")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Either"
sSymbol_Either
    = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"either" [(Int -> Sing b -> Doc) -> Sing b -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing b -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing b
a, (Int -> Sing b -> Doc) -> Sing b -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing b -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing b
b]
prettyType Int
p (SData (STyCon sym `STyApp` a) _)
    | Just TypeEq s "Maybe"
Refl <- Sing s -> Sing "Maybe" -> Maybe (TypeEq s "Maybe")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Maybe"
sSymbol_Maybe
    = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"maybe" [(Int -> Sing b -> Doc) -> Sing b -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Sing b -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Sing b
a]
prettyType Int
p (SData (STyCon sym) _)
    | Just TypeEq s "Bool"
Refl <- Sing s -> Sing "Bool" -> Maybe (TypeEq s "Bool")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Bool"
sSymbol_Bool
    = String -> Doc
text String
"bool"
    | Just TypeEq s "Unit"
Refl <- Sing s -> Sing "Unit" -> Maybe (TypeEq s "Unit")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
sym Sing "Unit"
sSymbol_Unit
    = String -> Doc
text String
"unit"
prettyType Int
_ Sing a
typ
    = Doc -> Doc
parens (String -> Doc
text (Sing a -> String
forall a. Show a => a -> String
show Sing a
typ))


-- | Pretty-print a 'PrimOp' @(:$)@ node in the AST.
ppPrimOp
    :: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
    => Int -> PrimOp typs a -> SArgs abt args -> Doc
ppPrimOp :: Int -> PrimOp typs a -> SArgs abt args -> Doc
ppPrimOp Int
p PrimOp typs a
Not          (abt vars a
e1 :* SArgs abt args
End)
  | Syn (PrimOp_ Less{}  :$ e2 :* e3 :* End) <- abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1
  = String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
"<=" Int
4 Associativity
NonAssoc Int
p abt vars a
abt '[] a
e3 abt vars a
abt '[] a
e2
  | Syn (PrimOp_ Equal{} :$ e2 :* e3 :* End) <- abt vars a -> View (Term abt) vars a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt vars a
e1
  = String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
"/=" Int
4 Associativity
NonAssoc Int
p abt vars a
abt '[] a
e2 abt vars a
abt '[] a
e3
  | Bool
otherwise
  = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"not" abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Impl         (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"impl" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p PrimOp typs a
Diff         (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"diff" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p PrimOp typs a
Nand         (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"nand" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p PrimOp typs a
Nor          (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"nor" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
_ PrimOp typs a
Pi           SArgs abt args
End               = String -> Doc
text String
"pi"
ppPrimOp Int
p PrimOp typs a
Sin          (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"sin"   abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Cos          (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"cos"   abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Tan          (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"tan"   abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Asin         (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"asin"  abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Acos         (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"acos"  abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Atan         (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"atan"  abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Sinh         (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"sinh"  abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Cosh         (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"cosh"  abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Tanh         (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"tanh"  abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Asinh        (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"asinh" abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Acosh        (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"acosh" abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Atanh        (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"atanh" abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
RealPow      (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
"**" Int
8 Associativity
RightAssoc Int
p abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p PrimOp typs a
Choose       (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"choose" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p PrimOp typs a
Exp          (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"exp"   abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Log          (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"log"   abt vars a
abt '[] a
e1
ppPrimOp Int
_ (Infinity HIntegrable a
_) SArgs abt args
End               = String -> Doc
text String
"∞"
ppPrimOp Int
p PrimOp typs a
GammaFunc    (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"gammaFunc" abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
BetaFunc     (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"betaFunc" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p (Equal   HEq a
_)  (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
"==" Int
4 Associativity
NonAssoc   Int
p abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p (Less    HOrd a
_)  (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
"<"  Int
4 Associativity
NonAssoc   Int
p abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p (NatPow  HSemiring a
_)  (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
"^"  Int
8 Associativity
RightAssoc Int
p abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppPrimOp Int
p (Negate  HRing a
_)  (abt vars a
e1 :* SArgs abt args
End)       = Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
ppNegate Int
p abt vars a
abt '[] a
e1
ppPrimOp Int
p (Abs     HRing a
_)  (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1  Int
p String
"abs"     abt vars a
abt '[] a
e1
ppPrimOp Int
p (Signum  HRing a
_)  (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1  Int
p String
"signum"  abt vars a
abt '[] a
e1
ppPrimOp Int
p (Recip   HFractional a
_)  (abt vars a
e1 :* SArgs abt args
End)       = Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
ppRecip Int
p abt vars a
abt '[] a
e1
ppPrimOp Int
p (NatRoot HRadical a
_)  (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = Int -> abt '[] a -> abt '[] 'HNat -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> abt '[] 'HNat -> Doc
ppNatRoot Int
p abt vars a
abt '[] a
e1 abt vars a
abt '[] 'HNat
e2
ppPrimOp Int
p (Erf HContinuous a
_)      (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1  Int
p String
"erf"     abt vars a
abt '[] a
e1
ppPrimOp Int
p PrimOp typs a
Floor        (abt vars a
e1 :* SArgs abt args
End)       = Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"floor"   abt vars a
abt '[] a
e1

ppNegate :: (ABT Term abt) => Int -> abt '[] a -> Doc
ppNegate :: Int -> abt '[] a -> Doc
ppNegate Int
p abt '[] a
e = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e (Doc -> Variable a -> Doc
forall a b. a -> b -> a
const Doc
d) ((Term abt a -> Doc) -> Doc) -> (Term abt a -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        -- Use parens to distinguish between negation of nats/probs
        -- from int/real literal
        Literal_ (LNat  Natural
_) -> Doc
d'
        Literal_ (LProb NonNegativeRational
_) -> Doc
d'
        Term abt a
_                  -> Doc
d
    where d :: Doc
d  = String -> Doc
text String
"-" Doc -> Doc -> Doc
<> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
7 abt '[] a
e
          d' :: Doc
d' = String -> Doc
text String
"-" Doc -> Doc -> Doc
<> Doc -> Doc
parens (abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt '[] a
e)

ppRecip :: (ABT Term abt) => Int -> abt '[] a -> Doc
ppRecip :: Int -> abt '[] a -> Doc
ppRecip Int
p abt '[] a
e = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
7) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
    abt '[] a -> (Variable a -> Doc) -> (Term abt a -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e (Doc -> Variable a -> Doc
forall a b. a -> b -> a
const Doc
d) ((Term abt a -> Doc) -> Doc) -> (Term abt a -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
        case Term abt a
t of
        -- Use parens to distinguish between reciprocal of nat
        -- from prob literal
        Literal_ (LNat Natural
_) -> Doc
d'
        Term abt a
_                 -> Doc
d
    where d :: Doc
d  = String -> Doc
text String
"1/" Doc -> Doc -> Doc
<+> Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
8 abt '[] a
e
          d' :: Doc
d' = String -> Doc
text String
"1/" Doc -> Doc -> Doc
<+> Doc -> Doc
parens (abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt '[] a
e)

ppNatRoot
    :: (ABT Term abt)
    => Int
    -> abt '[] a
    -> abt '[] 'HNat
    -> Doc
ppNatRoot :: Int -> abt '[] a -> abt '[] 'HNat -> Doc
ppNatRoot Int
p abt '[] a
e1 abt '[] 'HNat
e2 =
    abt '[] 'HNat
-> (Variable 'HNat -> Doc) -> (Term abt 'HNat -> Doc) -> Doc
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] 'HNat
e2 (Doc -> Variable 'HNat -> Doc
forall a b. a -> b -> a
const Doc
d) ((Term abt 'HNat -> Doc) -> Doc) -> (Term abt 'HNat -> Doc) -> Doc
forall a b. (a -> b) -> a -> b
$ \Term abt 'HNat
t ->
        case Term abt 'HNat
t of
          Literal_ (LNat Natural
2) -> Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"sqrt" abt '[] a
e1
          Term abt 'HNat
_                 -> Doc
d
    where d :: Doc
d = Int -> String -> abt '[] a -> abt '[] 'HNat -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"natroot" abt '[] a
e1 abt '[] 'HNat
e2


-- | Pretty-print a 'ArrayOp' @(:$)@ node in the AST.
ppArrayOp
    :: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
    => Int -> ArrayOp typs a -> SArgs abt args -> Doc
ppArrayOp :: Int -> ArrayOp typs a -> SArgs abt args -> Doc
ppArrayOp Int
p (Index   Sing a
_) = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Bool -> Doc -> Doc
parensIf (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
cat [ Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
10 abt vars a
abt '[] a
e1, Int -> Doc -> Doc
nest Int
2 (Doc -> Doc
brackets (abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Doc
pretty abt vars a
abt '[] a
e2)) ]

ppArrayOp Int
p (Size    Sing a
_) = \(abt vars a
e1 :* SArgs abt args
End)       -> Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"size" abt vars a
abt '[] a
e1
ppArrayOp Int
p (Reduce  Sing a
_) = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
    Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"reduce"
        [ (Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt vars a
abt '[] a
e1
        , (Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt vars a
abt '[] a
e2
        , (Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt vars a
abt '[] a
e3 ]


-- | Pretty-print a 'MeasureOp' @(:$)@ node in the AST.
ppMeasureOp
    :: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
    => Int -> MeasureOp typs a -> SArgs abt args -> Doc
ppMeasureOp :: Int -> MeasureOp typs a -> SArgs abt args -> Doc
ppMeasureOp Int
p MeasureOp typs a
Lebesgue    = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"lebesgue" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppMeasureOp Int
_ MeasureOp typs a
Counting    = \SArgs abt args
End           -> String -> Doc
text String
"counting"
ppMeasureOp Int
p MeasureOp typs a
Categorical = \(abt vars a
e1 :* SArgs abt args
End)   -> Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"categorical" abt vars a
abt '[] a
e1
ppMeasureOp Int
p MeasureOp typs a
Uniform = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"uniform"     abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppMeasureOp Int
p MeasureOp typs a
Normal  = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"normal"      abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppMeasureOp Int
p MeasureOp typs a
Poisson = \(abt vars a
e1 :* SArgs abt args
End)       -> Int -> String -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
"poisson"     abt vars a
abt '[] a
e1
ppMeasureOp Int
p MeasureOp typs a
Gamma   = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"gamma"       abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
ppMeasureOp Int
p MeasureOp typs a
Beta    = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> Int -> String -> abt '[] a -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
"beta"        abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2

instance Pretty Literal where
    prettyPrec_ :: Int -> Literal a -> Doc
prettyPrec_ Int
_ (LNat  Natural
n) = Integer -> Doc
integer (Natural -> Integer
fromNatural Natural
n)
    prettyPrec_ Int
p (LInt  Integer
i) = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then String -> Doc
text String
"-" Doc -> Doc -> Doc
<> Integer -> Doc
integer (-Integer
i)
                 else String -> Doc
text String
"+" Doc -> Doc -> Doc
<> Integer -> Doc
integer   Integer
i
    prettyPrec_ Int
p (LProb NonNegativeRational
l) = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
7) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        [Doc] -> Doc
cat [ Integer -> Doc
integer Integer
n, String -> Doc
text String
"/" Doc -> Doc -> Doc
<> Integer -> Doc
integer Integer
d ]
        where r :: Rational
r = NonNegativeRational -> Rational
fromNonNegativeRational NonNegativeRational
l
              n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator   Rational
r
              d :: Integer
d = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r
    prettyPrec_ Int
p (LReal Rational
r) = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then String -> Doc
text String
"-" Doc -> Doc -> Doc
<> [Doc] -> Doc
cat [ Integer -> Doc
integer (-Integer
n), String -> Doc
text String
"/" Doc -> Doc -> Doc
<> Integer -> Doc
integer Integer
d ]
                 else String -> Doc
text String
"+" Doc -> Doc -> Doc
<> [Doc] -> Doc
cat [ Integer -> Doc
integer   Integer
n , String -> Doc
text String
"/" Doc -> Doc -> Doc
<> Integer -> Doc
integer Integer
d ]
        where n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator   Rational
r
              d :: Integer
d = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r

instance Pretty Value where
    prettyPrec_ :: Int -> Value a -> Doc
prettyPrec_ Int
_ (VNat  Natural
n)    = Integer -> Doc
integer (Natural -> Integer
fromNatural Natural
n)
    prettyPrec_ Int
p (VInt  Integer
i)    = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        if Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Integer -> Doc
integer Integer
i else String -> Doc
text String
"+" Doc -> Doc -> Doc
<> Integer -> Doc
integer Integer
i
    prettyPrec_ Int
_ (VProb LogFloat
l)    = Double -> Doc
double (LogFloat -> Double
LF.fromLogFloat LogFloat
l)
    prettyPrec_ Int
p (VReal Double
r)    = Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$
        if Double
r Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0 then Double -> Doc
double Double
r else String -> Doc
text String
"+" Doc -> Doc -> Doc
<> Double -> Doc
double Double
r
    prettyPrec_ Int
p (VDatum Datum Value (HData' t)
d)   = Int -> Datum Value (HData' t) -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
p Datum Value (HData' t)
d
    prettyPrec_ Int
_ (VLam Value a -> Value b
_)     = String -> Doc
text String
"<function>"
    prettyPrec_ Int
_ (VMeasure Value 'HProb -> GenIO -> IO (Maybe (Value a, Value 'HProb))
_) = String -> Doc
text String
"<measure>"
    prettyPrec_ Int
_ (VArray Vector (Value a)
a)   = [Doc] -> Doc
ppList ([Doc] -> Doc) -> (Vector Doc -> [Doc]) -> Vector Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Doc -> [Doc]
forall a. Vector a -> [a]
V.toList (Vector Doc -> Doc) -> Vector Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Value a -> Doc) -> Vector (Value a) -> Vector Doc
forall a b. (a -> b) -> Vector a -> Vector b
V.map (Int -> Value a -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
0) Vector (Value a)
a

prettyValue :: Value a -> Doc
prettyValue :: Value a -> Doc
prettyValue = Int -> Value a -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ Int
0

instance Pretty f => Pretty (Datum f) where
    prettyPrec_ :: Int -> Datum f a -> Doc
prettyPrec_ Int
p (Datum Text
hint Sing (HData' t)
_typ DatumCode (Code t) f (HData' t)
d)
        | Text -> Bool
Text.null Text
hint =
            Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
"datum_"
                [String -> Int -> Doc
forall a. HasCallStack => String -> a
error String
"TODO: prettyPrec_@Datum"]
        | Bool
otherwise =
            case Text -> String
Text.unpack Text
hint of
            -- Special cases for certain datums
            String
"pair"  -> Int -> [Int -> Doc] -> Doc
ppTuple Int
p ((forall (i :: Hakaru). f i -> [Int -> Doc])
-> DatumCode (Code t) f (HData' t) -> [Int -> Doc]
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
       (j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 (\f i
e -> [(Int -> f i -> Doc) -> f i -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> f i -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ f i
e]) DatumCode (Code t) f (HData' t)
d) 
            String
"true"  -> String -> Doc
text String
"true"
            String
"false" -> String -> Doc
text String
"false"
            String
"unit"  -> String -> Doc
text String
"()"
            -- General case
            String
f       -> Bool -> Doc -> Doc
parensIf (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 -> String -> [Int -> Doc] -> Doc
ppFun Int
6 String
f ((forall (i :: Hakaru). f i -> [Int -> Doc])
-> DatumCode (Code t) f (HData' t) -> [Int -> Doc]
forall k1 k2 (f :: (k1 -> *) -> k2 -> *) m (a :: k1 -> *)
       (j :: k2).
(Foldable11 f, Monoid m) =>
(forall (i :: k1). a i -> m) -> f a j -> m
foldMap11 (\f i
e -> [(Int -> f i -> Doc) -> f i -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> f i -> Doc
forall (f :: Hakaru -> *) (a :: Hakaru).
Pretty f =>
Int -> f a -> Doc
prettyPrec_ f i
e]) DatumCode (Code t) f (HData' t)
d)
                       Doc -> Doc -> Doc
<> String -> Doc
text String
"." Doc -> Doc -> Doc
<+> Int -> Sing (HData' t) -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 Sing (HData' t)
_typ


-- HACK: need to pull this out in order to get polymorphic recursion over @xs@
ppPattern :: [Doc] -> Pattern xs a -> (Int -> Doc, [Doc])
ppPattern :: [Doc] -> Pattern xs a -> (Int -> Doc, [Doc])
ppPattern [Doc]
vars   Pattern xs a
PWild = (Doc -> Int -> Doc
forall a b. a -> b -> a
const (String -> Doc
text String
"_"), [Doc]
vars)
ppPattern (Doc
v:[Doc]
vs) Pattern xs a
PVar  = (Doc -> Int -> Doc
forall a b. a -> b -> a
const Doc
v         , [Doc]
vs)
ppPattern [Doc]
vars   (PDatum Text
hint PDatumCode (Code t) xs (HData' t)
d0)
    | Text -> Bool
Text.null Text
hint = String -> (Int -> Doc, [Doc])
forall a. HasCallStack => String -> a
error String
"TODO: prettyPrec_@Pattern"
    | Bool
otherwise      =
        case Text -> String
Text.unpack Text
hint of
        -- Special cases for certain pDatums
        String
"true"  -> (Doc -> Int -> Doc
forall a b. a -> b -> a
const (String -> Doc
text String
"true" ), [Doc]
vars)
        String
"false" -> (Doc -> Int -> Doc
forall a b. a -> b -> a
const (String -> Doc
text String
"false"), [Doc]
vars)
        String
"pair"  -> (Int -> [Int -> Doc] -> Doc) -> (Int -> Doc, [Doc])
ppFunWithVars Int -> [Int -> Doc] -> Doc
ppTuple
        -- General case
        String
f       -> (Int -> [Int -> Doc] -> Doc) -> (Int -> Doc, [Doc])
ppFunWithVars ((Int -> String -> [Int -> Doc] -> Doc)
-> String -> Int -> [Int -> Doc] -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> String -> [Int -> Doc] -> Doc
ppFun String
f)
    where
    ppFunWithVars :: (Int -> [Int -> Doc] -> Doc) -> (Int -> Doc, [Doc])
ppFunWithVars Int -> [Int -> Doc] -> Doc
ppHint = ((Int -> [Int -> Doc] -> Doc) -> [Int -> Doc] -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> [Int -> Doc] -> Doc
ppHint [Int -> Doc]
g, [Doc]
vars')
       where ([Int -> Doc]
g, [Doc]
vars') = PDatumCode (Code t) xs (HData' t) -> [Doc] -> ([Int -> Doc], [Doc])
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumCode xss vars a -> [Doc] -> ([Int -> Doc], [Doc])
goCode PDatumCode (Code t) xs (HData' t)
d0 [Doc]
vars

    goCode :: PDatumCode xss vars a -> [Doc] -> ([Int -> Doc], [Doc])
    goCode :: PDatumCode xss vars a -> [Doc] -> ([Int -> Doc], [Doc])
goCode (PInr PDatumCode xss vars a
d) = PDatumCode xss vars a -> [Doc] -> ([Int -> Doc], [Doc])
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumCode xss vars a -> [Doc] -> ([Int -> Doc], [Doc])
goCode   PDatumCode xss vars a
d
    goCode (PInl PDatumStruct xs vars a
d) = PDatumStruct xs vars a -> [Doc] -> ([Int -> Doc], [Doc])
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumStruct xs vars a -> [Doc] -> ([Int -> Doc], [Doc])
goStruct PDatumStruct xs vars a
d

    goStruct :: PDatumStruct xs vars a -> [Doc] -> ([Int -> Doc], [Doc])
    goStruct :: PDatumStruct xs vars a -> [Doc] -> ([Int -> Doc], [Doc])
goStruct PDatumStruct xs vars a
PDone       [Doc]
vars  = ([], [Doc]
vars)
    goStruct (PEt PDatumFun x vars1 a
d1 PDatumStruct xs vars2 a
d2) [Doc]
vars = ([Int -> Doc]
gF [Int -> Doc] -> [Int -> Doc] -> [Int -> Doc]
forall a. [a] -> [a] -> [a]
++ [Int -> Doc]
gS, [Doc]
vars'')
       where ([Int -> Doc]
gF, [Doc]
vars')  = PDatumFun x vars1 a -> [Doc] -> ([Int -> Doc], [Doc])
forall (x :: HakaruFun) (vars :: [Hakaru]) (a :: Hakaru).
PDatumFun x vars a -> [Doc] -> ([Int -> Doc], [Doc])
goFun PDatumFun x vars1 a
d1 [Doc]
vars
             ([Int -> Doc]
gS, [Doc]
vars'') = PDatumStruct xs vars2 a -> [Doc] -> ([Int -> Doc], [Doc])
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumStruct xs vars a -> [Doc] -> ([Int -> Doc], [Doc])
goStruct PDatumStruct xs vars2 a
d2 [Doc]
vars' 

    goFun :: PDatumFun x vars a -> [Doc] -> ([Int -> Doc], [Doc])
    goFun :: PDatumFun x vars a -> [Doc] -> ([Int -> Doc], [Doc])
goFun (PKonst Pattern vars b
d) [Doc]
vars = ([Int -> Doc
g], [Doc]
vars')
       where (Int -> Doc
g, [Doc]
vars') = [Doc] -> Pattern vars b -> (Int -> Doc, [Doc])
forall (xs :: [Hakaru]) (a :: Hakaru).
[Doc] -> Pattern xs a -> (Int -> Doc, [Doc])
ppPattern [Doc]
vars Pattern vars b
d
    goFun (PIdent Pattern vars a
d) [Doc]
vars = ([Int -> Doc
g], [Doc]
vars')
       where (Int -> Doc
g, [Doc]
vars') = [Doc] -> Pattern vars a -> (Int -> Doc, [Doc])
forall (xs :: [Hakaru]) (a :: Hakaru).
[Doc] -> Pattern xs a -> (Int -> Doc, [Doc])
ppPattern [Doc]
vars Pattern vars a
d


instance (ABT Term abt) => Pretty (Branch a abt) where
    prettyPrec_ :: Int -> Branch a abt a -> Doc
prettyPrec_ Int
p (Branch Pattern xs a
pat abt xs a
e) =
        let ([Doc]
vars, Doc
body) = abt xs a -> ([Doc], Doc)
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> ([Doc], Doc)
ppBinder abt xs a
e
            (Int -> Doc
pp, []) = [Doc] -> Pattern xs a -> (Int -> Doc, [Doc])
forall (xs :: [Hakaru]) (a :: Hakaru).
[Doc] -> Pattern xs a -> (Int -> Doc, [Doc])
ppPattern [Doc]
vars Pattern xs a
pat
        in [Doc] -> Doc
sep [ Int -> Doc
pp Int
0 Doc -> Doc -> Doc
<> Doc
colon, Int -> Doc -> Doc
nest Int
2 Doc
body ]

----------------------------------------------------------------
prettyApps :: (ABT Term abt) => Int -> abt '[] (a ':-> b) -> abt '[] a -> Doc
prettyApps :: Int -> abt '[] (a ':-> b) -> abt '[] a -> Doc
prettyApps = \ Int
p abt '[] (a ':-> b)
e1 abt '[] a
e2 ->
{- TODO: confirm not using reduceLams
    case reduceLams e1 e2 of
    Just e2' -> ppArg e2'
    Nothing  ->
-}
      ((Int -> Doc) -> [Int -> Doc] -> Doc)
-> (Int -> Doc, [Int -> Doc]) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Int -> (Int -> Doc) -> [Int -> Doc] -> Doc
ppApp Int
p) (abt '[] (a ':-> b) -> [Int -> Doc] -> (Int -> Doc, [Int -> Doc])
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> [Int -> Doc] -> (Int -> Doc, [Int -> Doc])
collectApps abt '[] (a ':-> b)
e1 [(Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] a
e2])
    where
    reduceLams
        :: (ABT Term abt)
        => abt '[] (a ':-> b) -> abt '[] a -> Maybe (abt '[] b)
    reduceLams :: abt '[] (a ':-> b) -> abt '[] a -> Maybe (abt '[] b)
reduceLams abt '[] (a ':-> b)
e1 abt '[] a
e2 =
        abt '[] (a ':-> b)
-> (Variable (a ':-> b) -> Maybe (abt '[] b))
-> (Term abt (a ':-> b) -> Maybe (abt '[] b))
-> Maybe (abt '[] b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] (a ':-> b)
e1 (Maybe (abt '[] b) -> Variable (a ':-> b) -> Maybe (abt '[] b)
forall a b. a -> b -> a
const Maybe (abt '[] b)
forall a. Maybe a
Nothing) ((Term abt (a ':-> b) -> Maybe (abt '[] b)) -> Maybe (abt '[] b))
-> (Term abt (a ':-> b) -> Maybe (abt '[] b)) -> Maybe (abt '[] b)
forall a b. (a -> b) -> a -> b
$ \Term abt (a ':-> b)
t ->
            case Term abt (a ':-> b)
t of
            SCon args (a ':-> b)
Lam_ :$ abt vars a
e1 :* SArgs abt args
End ->
              abt '[a] a
-> (Variable a -> abt '[] a -> Maybe (abt '[] a))
-> Maybe (abt '[] a)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e1 ((Variable a -> abt '[] a -> Maybe (abt '[] a))
 -> Maybe (abt '[] a))
-> (Variable a -> abt '[] a -> Maybe (abt '[] a))
-> Maybe (abt '[] a)
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e1' ->
                abt '[] a -> Maybe (abt '[] a)
forall a. a -> Maybe a
Just (Variable a -> abt '[] a -> abt '[] a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) (xs :: [k]) (b :: k).
(JmEq1 Sing, Show1 Sing, Traversable21 syn, ABT syn abt) =>
Variable a -> abt '[] a -> abt xs b -> abt xs b
subst Variable a
x abt '[] a
e2 abt '[] a
e1')
            Term abt (a ':-> b)
_                 -> Maybe (abt '[] b)
forall a. Maybe a
Nothing

    -- collectApps makes sure f(x,y) is not printed f(x)(y)
    collectApps
        :: (ABT Term abt)
        => abt '[] (a ':-> b) -> [Int -> Doc] -> (Int -> Doc, [Int -> Doc])
    collectApps :: abt '[] (a ':-> b) -> [Int -> Doc] -> (Int -> Doc, [Int -> Doc])
collectApps abt '[] (a ':-> b)
e [Int -> Doc]
es = 
        abt '[] (a ':-> b)
-> (Variable (a ':-> b) -> (Int -> Doc, [Int -> Doc]))
-> (Term abt (a ':-> b) -> (Int -> Doc, [Int -> Doc]))
-> (Int -> Doc, [Int -> Doc])
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] (a ':-> b)
e ((Int -> Doc, [Int -> Doc])
-> Variable (a ':-> b) -> (Int -> Doc, [Int -> Doc])
forall a b. a -> b -> a
const (Int -> Doc, [Int -> Doc])
ret) ((Term abt (a ':-> b) -> (Int -> Doc, [Int -> Doc]))
 -> (Int -> Doc, [Int -> Doc]))
-> (Term abt (a ':-> b) -> (Int -> Doc, [Int -> Doc]))
-> (Int -> Doc, [Int -> Doc])
forall a b. (a -> b) -> a -> b
$ \Term abt (a ':-> b)
t ->
            case Term abt (a ':-> b)
t of
            SCon args (a ':-> b)
App_ :$ abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End -> abt '[] (a ':-> (a ':-> b))
-> [Int -> Doc] -> (Int -> Doc, [Int -> Doc])
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] (a ':-> b) -> [Int -> Doc] -> (Int -> Doc, [Int -> Doc])
collectApps abt vars a
abt '[] (a ':-> (a ':-> b))
e1 ((Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt vars a
abt '[] a
e2 (Int -> Doc) -> [Int -> Doc] -> [Int -> Doc]
forall a. a -> [a] -> [a]
: [Int -> Doc]
es)
            Term abt (a ':-> b)
_                       -> (Int -> Doc, [Int -> Doc])
ret
        where ret :: (Int -> Doc, [Int -> Doc])
ret = ((Int -> abt '[] (a ':-> b) -> Doc)
-> abt '[] (a ':-> b) -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] (a ':-> b) -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] (a ':-> b)
e, [Int -> Doc]
es)



ppList :: [Doc] -> Doc
ppList :: [Doc] -> Doc
ppList = Doc -> Doc
brackets (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
sepComma

ppTuple :: Int -> [Int -> Doc] -> Doc
ppTuple :: Int -> [Int -> Doc] -> Doc
ppTuple Int
_ = Doc -> Doc
parens (Doc -> Doc) -> ([Int -> Doc] -> Doc) -> [Int -> Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
sepComma ([Doc] -> Doc) -> ([Int -> Doc] -> [Doc]) -> [Int -> Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int -> Doc) -> Doc) -> [Int -> Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Doc) -> Int -> Doc
forall a b. (a -> b) -> a -> b
$ Int
0)

ppApp :: Int -> (Int -> Doc) -> [Int -> Doc] -> Doc
ppApp :: Int -> (Int -> Doc) -> [Int -> Doc] -> Doc
ppApp Int
p Int -> Doc
f [Int -> Doc]
ds = Bool -> Doc -> Doc
parensIf (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
cat [ Int -> Doc
f Int
10, Int -> Doc -> Doc
nest Int
2 (Int -> [Int -> Doc] -> Doc
ppTuple Int
11 [Int -> Doc]
ds) ]

ppFun :: Int -> String -> [Int -> Doc] -> Doc
ppFun :: Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p = Int -> (Int -> Doc) -> [Int -> Doc] -> Doc
ppApp Int
p ((Int -> Doc) -> [Int -> Doc] -> Doc)
-> (String -> Int -> Doc) -> String -> [Int -> Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Int -> Doc
forall a b. a -> b -> a
const (Doc -> Int -> Doc) -> (String -> Doc) -> String -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text

ppApply1 :: (ABT Term abt) => Int -> String -> abt '[] a -> Doc
ppApply1 :: Int -> String -> abt '[] a -> Doc
ppApply1 Int
p String
f abt '[] a
e1 = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
f [(Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] a
e1]

ppApply2 :: (ABT Term abt) => Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 :: Int -> String -> abt '[] a -> abt '[] b -> Doc
ppApply2 Int
p String
f abt '[] a
e1 abt '[] b
e2 = Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
f [(Int -> abt '[] a -> Doc) -> abt '[] a -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] a
e1, (Int -> abt '[] b -> Doc) -> abt '[] b -> Int -> Doc
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> abt '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec abt '[] b
e2]

ppApply :: ABT Term abt => Int -> String
        -> SArgs abt xs -> Doc
ppApply :: Int -> String -> SArgs abt xs -> Doc
ppApply Int
p String
f SArgs abt xs
es =
  Int -> String -> [Int -> Doc] -> Doc
ppFun Int
p String
f ([Int -> Doc] -> Doc) -> [Int -> Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (forall (h :: [Hakaru]) (i :: Hakaru). abt h i -> [Int -> Doc])
-> SArgs abt xs -> [Int -> Doc]
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *) m
       (a :: k1 -> k2 -> *) (j :: k3).
(Foldable21 f, Monoid m) =>
(forall (h :: k1) (i :: k2). a h i -> m) -> f a j -> m
foldMap21 ((Int -> Doc) -> [Int -> Doc]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Int -> Doc) -> [Int -> Doc])
-> (abt h i -> Int -> Doc) -> abt h i -> [Int -> Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> Int -> Doc
forall a b. a -> b -> a
const (Doc -> Int -> Doc) -> (abt h i -> Doc) -> abt h i -> Int -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt h i -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> Doc
ppBinderAsFun) SArgs abt xs
es

ppBinop
    :: (ABT Term abt)
    => String -> Int -> Associativity
    -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop :: String
-> Int -> Associativity -> Int -> abt '[] a -> abt '[] b -> Doc
ppBinop String
op Int
p0 Associativity
assoc =
    let (Int
p1,Int
p2,Doc -> Doc
f1,Doc -> Doc
f2) =
            case Associativity
assoc of
            Associativity
NonAssoc   -> (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p0, Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p0, Doc -> Doc
forall a. a -> a
id, (String -> Doc
text String
op Doc -> Doc -> Doc
<+>))
            Associativity
LeftAssoc  -> (    Int
p0, Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p0, Doc -> Doc
forall a. a -> a
id, (String -> Doc
text String
op Doc -> Doc -> Doc
<+>))
            Associativity
RightAssoc -> (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p0,     Int
p0, (Doc -> Doc -> Doc
<+> String -> Doc
text String
op), Doc -> Doc
forall a. a -> a
id)
    in \Int
p abt '[] a
e1 abt '[] b
e2 ->
        Bool -> Doc -> Doc
parensIf (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
p0) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
sep [ Doc -> Doc
f1 (Int -> abt '[] a -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
p1 abt '[] a
e1)
                                , Doc -> Doc
f2 (Int -> abt '[] b -> Doc
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Int -> abt '[] a -> Doc
prettyPrec Int
p2 abt '[] b
e2) ]

----------------------------------------------------------------
----------------------------------------------------------- fin.