{-# LANGUAGE GADTs
, KindSignatures
, DataKinds
, ScopedTypeVariables
, PatternGuards
, Rank2Types
, TypeOperators
, FlexibleContexts
, UndecidableInstances
, LambdaCase
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Pretty.Concrete
(
pretty
, prettyPrec
, prettyType
, prettyValue
, prettyT
, prettyTypeT, prettyTypeS
) 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
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 :: (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
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
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
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
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
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
parensIf :: Bool -> Doc -> Doc
parensIf :: Bool -> Doc -> Doc
parensIf Bool
False = Doc -> Doc
forall a. a -> a
id
parensIf Bool
True = Doc -> Doc
parens
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)))
| 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))
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
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
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
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 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) ->
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 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
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
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
")"
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))
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
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
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
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 ]
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
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
"()"
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
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
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
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 ->
((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
:: (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) ]