Skip to content

Commit 57844c6

Browse files
AilrunAilrun
committed
Add CBPV pretty printer for easier testing
1 parent f9941a3 commit 57844c6

27 files changed

Lines changed: 1312 additions & 4147 deletions

‎lambdacomp.cabal‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,7 @@ library
8383
LambdaComp.CBPV.Optimization.EtaReduction
8484
LambdaComp.CBPV.Optimization.InlineBinding
8585
LambdaComp.CBPV.Optimization.Local
86+
LambdaComp.CBPV.PrettyPrinter
8687
LambdaComp.CBPV.Syntax
8788
LambdaComp.CBPV.ToAM
8889
LambdaComp.CBPV.ToC
@@ -111,6 +112,7 @@ library
111112
, optparse-applicative ^>=0.18.1.0
112113
, parser-combinators ^>=1.3.0
113114
, pretty-simple ^>=4.1.3.0
115+
, prettyprinter ^>=1.7.1
114116
, process ^>=1.6.25.0
115117
, temporary ^>=1.3
116118
, text ^>=2.1.2

‎src/LambdaComp/CBPV/PrettyPrinter.hs‎

Lines changed: 277 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,277 @@
1+
{-# OPTIONS_GHC -Wno-orphans #-}
2+
module LambdaComp.CBPV.PrettyPrinter
3+
(
4+
) where
5+
6+
import Data.Text (Text)
7+
import Data.Text qualified as T
8+
import Prettyprinter
9+
import Prettyprinter.Util
10+
11+
import LambdaComp.CBPV.Syntax
12+
import LambdaComp.CBPV.TypeCheck (TypeError (..))
13+
14+
instance {-# OVERLAPPING #-} Pretty Program where
15+
pretty = align . concatWith (surround (line <> ";;" <> line)) . fmap pretty
16+
17+
instance Pretty Top where
18+
pretty TopTmDef {..} = pretty tmDefName <+> "=" <> nest 2 (group $ line <> pretty tmDefBody)
19+
20+
instance Pretty (Tp c) where
21+
pretty = prettyTpPrec 0
22+
23+
prettyTpPrec :: Int -> Tp c -> Doc ann
24+
prettyTpPrec _ TpUnit = "Unit"
25+
prettyTpPrec _ TpBool = "Bool"
26+
prettyTpPrec _ TpInt = "Int"
27+
prettyTpPrec _ TpDouble = "Double"
28+
prettyTpPrec pr (TpUp tp) = group $ prefixOfPrec1 pr ("Up", tpUpPrec) (group . (line <>) . (`prettyTpPrec` tp))
29+
prettyTpPrec pr (tpP :->: tpR) = group $ prettyTpFun pr [tpP] tpR
30+
prettyTpPrec pr (TpDown tp) = group $ prefixOfPrec1 pr ("Down", tpDownPrec) (group . (line <>) . (`prettyTpPrec` tp))
31+
32+
prettyTpFun :: Int -> [Tp Val] -> Tp Com -> Doc ann
33+
prettyTpFun pr rtpPs (tpP :->: tpR) = prettyTpFun pr (tpP : rtpPs) tpR
34+
prettyTpFun pr rtpPs tp = prefixOfPrec0 pr (align (sep $ (<+> "->") . prettyTpPrec (tpFunPrec + 1) <$> reverse rtpPs), tpFunPrec) (group . (line <>) . (`prettyTpPrec` tp))
35+
36+
tpFunPrec :: Int
37+
tpUpPrec :: Int
38+
tpDownPrec :: Int
39+
40+
tpFunPrec = 0
41+
tpUpPrec = 1
42+
tpDownPrec = 1
43+
44+
instance Pretty (Tm c) where
45+
pretty = prettyTmPrec 0
46+
47+
prettyTmPrec :: Int -> Tm c -> Doc ann
48+
prettyTmPrec _ (TmVar x) = pretty x
49+
prettyTmPrec _ (TmGlobal x) = "#" <> pretty x
50+
prettyTmPrec _ TmUnit = "()"
51+
prettyTmPrec _ TmTrue = "True"
52+
prettyTmPrec _ TmFalse = "False"
53+
prettyTmPrec _ (TmInt i) = pretty i
54+
prettyTmPrec _ (TmDouble d) = pretty d
55+
prettyTmPrec pr (TmThunk tm) = group $ prefixOfPrec2 pr ("thunk", tmThunkPrec) (group . (line <>) . (`prettyTmPrec` tm))
56+
prettyTmPrec pr (TmIf tm0 tm1 tm2) = group $ condParens (pr > tmIfPrec) $ align $ vsep $ fmap group ["if" <> line <> pretty tm0, "then" <> line <> prettyTmPrec (tmIfPrec + 1) tm1, "else" <> line <> prettyTmPrec (tmIfPrec + 1) tm2]
57+
prettyTmPrec pr (TmLam p tm) = group $ prettyTmLam pr [p] tm
58+
prettyTmPrec pr (tmf `TmApp` tma) = group $ infixlOfPrec pr (`prettyTmPrec` tmf) (emptyDoc, tmAppPrec) (group . (line <>) . (`prettyTmPrec` tma))
59+
prettyTmPrec pr (TmForce tm) = group $ prefixOfPrec2 pr ("force", tmForcePrec) (group . (line <>) . (`prettyTmPrec` tm))
60+
prettyTmPrec pr (TmReturn tm) = group $ prefixOfPrec2 pr ("return", tmReturnPrec) (group . (line <>) . (`prettyTmPrec` tm))
61+
prettyTmPrec pr (TmTo tm0 x tm1) = group $ condParens (pr > tmToPrec) $ align $ group (prettyTmPrec (tmToPrec + 1) tm0 <> line <> "to" <+> pretty x <+> "->") <> line <> group (prettyTmPrec 0 tm1)
62+
prettyTmPrec pr (TmLet x tm0 tm1) = group $ condParens (pr > tmLetPrec) $ align $ prettyTmLet [(x, tm0)] tm1
63+
prettyTmPrec pr (TmPrimBinOp op tm0 tm1) = group $ prettyTmPrimBinOp pr op tm0 tm1
64+
prettyTmPrec pr (TmPrimUnOp op tm) = group $ prettyTmPrimUnOp pr op tm
65+
prettyTmPrec pr (TmPrintInt tm0 tm1) = condParens (pr > tmPrintPrec) $ align $ vsep ["printInt" <+> pretty tm0 <+> "before", pretty tm1]
66+
prettyTmPrec pr (TmPrintDouble tm0 tm1) = condParens (pr > tmPrintPrec) $ align $ vsep ["printDouble" <+> pretty tm0 <+> "before", pretty tm1]
67+
prettyTmPrec pr (TmRec p tm) = group $ prefixOfPrec0 pr ("rec" <+> pretty p <+> "->", tmRecPrec) (group . (line <>) . (`prettyTmPrec` tm))
68+
69+
prettyTmLam :: Int -> [Param] -> Tm Com -> Doc ann
70+
prettyTmLam pr rps (TmLam p tm) = prettyTmLam pr (p : rps) tm
71+
prettyTmLam pr rps tm = prefixOfPrec0 pr ("\\" <+> align (sep $ pretty <$> reverse rps) <+> "->", tmLamPrec) (group . (line <>) . (`prettyTmPrec` tm))
72+
73+
prettyTmLet :: [(Ident, Tm Val)] -> Tm Com -> Doc ann
74+
prettyTmLet rbs (TmLet x tm0 tm1) = prettyTmLet ((x, tm0) : rbs) tm1
75+
prettyTmLet rbs tm = vsep ["let", indent 2 . concatWith (surround $ ";" <> "line") . fmap prettyBinding $ reverse rbs, "in", pretty tm]
76+
where
77+
prettyBinding :: (Ident, Tm Val) -> Doc ann
78+
prettyBinding (x, tm') = pretty x <+> "=" <> softline <> pretty tm'
79+
80+
prettyTmPrimBinOp :: Int -> PrimOp Binary -> Tm Val -> Tm Val -> Doc ann
81+
prettyTmPrimBinOp pr op tm0 tm1 = go op
82+
where
83+
go PrimIAdd = gol "+" tmAdditivePrec
84+
go PrimISub = gol "-" tmAdditivePrec
85+
go PrimIMul = gol "*" tmMultiplicativePrec
86+
go PrimIDiv = gol "/" tmMultiplicativePrec
87+
go PrimIMod = gol "%" tmMultiplicativePrec
88+
go PrimIEq = gon "=" tmComparativePrec
89+
go PrimINEq = gon "<>" tmComparativePrec
90+
go PrimILt = gon "<" tmComparativePrec
91+
go PrimILe = gon "<=" tmComparativePrec
92+
go PrimIGt = gon ">" tmComparativePrec
93+
go PrimIGe = gon ">=" tmComparativePrec
94+
go PrimDAdd = gol "+." tmComparativePrec
95+
go PrimDSub = gol "-." tmComparativePrec
96+
go PrimDMul = gol "*." tmComparativePrec
97+
go PrimDDiv = gol "/." tmComparativePrec
98+
go PrimDEq = gol "=." tmComparativePrec
99+
go PrimDNEq = gon "<>." tmComparativePrec
100+
go PrimDLt = gon "<." tmComparativePrec
101+
go PrimDLe = gon "<=." tmComparativePrec
102+
go PrimDGt = gon ">." tmComparativePrec
103+
go PrimDGe = gon ">=." tmComparativePrec
104+
go PrimBAnd = gol "&&" tmAndPrec
105+
go PrimBOr = gol "||" tmOrPrec
106+
107+
gol opDoc opPrec = infixlOfPrec pr (`prettyTmPrec` tm0) (softline <> opDoc <> space, opPrec) (`prettyTmPrec` tm1)
108+
gon opDoc opPrec = infixnOfPrec pr (`prettyTmPrec` tm0) (softline <> opDoc <> space, opPrec) (`prettyTmPrec` tm1)
109+
110+
prettyTmPrimUnOp :: Int -> PrimOp Unary -> Tm Val -> Doc ann
111+
prettyTmPrimUnOp pr op tm = go op
112+
where
113+
go PrimINeg = go1 "-" tmNegPrec
114+
go PrimIToD = go1' "intToDouble" tmAppPrec
115+
go PrimDNeg = go1 "-." tmNegPrec
116+
go PrimDToI = go1' "doubleToInt" tmAppPrec
117+
go PrimBNot = go1 "~" tmNotPrec
118+
119+
go1 opDoc opPrec = prefixOfPrec1 pr (opDoc <> space, opPrec) (`prettyTmPrec` tm)
120+
go1' opDoc opPrec = prefixOfPrec1 pr (opDoc <> softline, opPrec) (`prettyTmPrec` tm)
121+
122+
tmIfPrec :: Int
123+
tmLamPrec :: Int
124+
tmLetPrec :: Int
125+
tmPrintPrec :: Int
126+
tmRecPrec :: Int
127+
tmThunkPrec :: Int
128+
tmForcePrec :: Int
129+
tmReturnPrec :: Int
130+
tmToPrec :: Int
131+
tmAppPrec :: Int
132+
133+
tmIfPrec = 0
134+
tmLamPrec = 0
135+
tmLetPrec = 0
136+
tmPrintPrec = 0
137+
tmRecPrec = 0
138+
tmThunkPrec = 6
139+
tmForcePrec = 6
140+
tmReturnPrec = 6
141+
tmToPrec = 6
142+
tmAppPrec = 7
143+
144+
tmOrPrec :: Int
145+
tmAndPrec :: Int
146+
tmComparativePrec :: Int
147+
tmAdditivePrec :: Int
148+
tmMultiplicativePrec :: Int
149+
tmNotPrec :: Int
150+
tmNegPrec :: Int
151+
152+
tmOrPrec = 1
153+
tmAndPrec = 2
154+
tmComparativePrec = 3
155+
tmAdditivePrec = 4
156+
tmMultiplicativePrec = 5
157+
tmNotPrec = 6
158+
tmNegPrec = 8
159+
160+
instance Pretty Param where
161+
pretty Param {..} = parens . align . nest 2 $ pretty paramName <+> group (":" <+> pretty paramType)
162+
163+
instance Pretty TypeError where
164+
pretty (NonIntLastTopDecl x) =
165+
align
166+
$ vsep
167+
[ align
168+
$ fillSep
169+
[ reflow "Last top-level definition"
170+
, dquotes $ pretty x
171+
, reflow "of the main module does not have the Int type"
172+
]
173+
, prettyErrorNote
174+
[ "the last top-level declaration determines"
175+
, "exit code of the entire program."
176+
]
177+
]
178+
pretty (NotInScope x) =
179+
align
180+
$ fillSep
181+
[ reflow "Variable"
182+
, dquotes $ pretty x
183+
, reflow "is not in the scope of the usage"
184+
]
185+
pretty (NotDefined x) =
186+
align
187+
$ vsep
188+
[ align
189+
$ fillSep
190+
[ reflow "No top-level definition"
191+
, dquotes $ pretty x
192+
, reflow "is given but used"
193+
]
194+
, prettyErrorNote
195+
[ "A body of a top-level definition can only access"
196+
, "top-levels defined before that."
197+
]
198+
]
199+
pretty (TypeMismatch pos tpExp tpAct) =
200+
align
201+
$ vsep
202+
[ reflow $ pos <> " expects"
203+
, indent 2 $ pretty tpExp
204+
, reflow "but found"
205+
, indent 2 $ pretty tpAct
206+
]
207+
pretty (BranchTypeMismatch tpTrue tpFalse) =
208+
align
209+
$ vsep
210+
[ reflow "Branches of if have different types. One is with"
211+
, indent 2 $ pretty tpTrue
212+
, reflow "but the other is with"
213+
, indent 2 $ pretty tpFalse
214+
]
215+
pretty (InvalidConsType tpChk tps) =
216+
align
217+
$ vsep
218+
[ reflow "A constructor is checked against"
219+
, indent 2 $ pretty tpChk
220+
, reflow $ "but it should have" <> (if null (drop 1 tps) then "" else " one of")
221+
, indent 2 . vsep $ fmap pretty tps
222+
]
223+
pretty (NonFunType tpAct) =
224+
align
225+
$ vsep
226+
[ reflow "Application expects a function type but found"
227+
, indent 2 $ pretty tpAct
228+
]
229+
pretty (NonUpType tpAct) =
230+
align
231+
$ vsep
232+
[ reflow "Force expects a Up type but found"
233+
, indent 2 $ pretty tpAct
234+
]
235+
pretty (NonDownType pos tpAct) =
236+
align
237+
$ vsep
238+
[ reflow $ pos <> " expects a Down type but found"
239+
, indent 2 $ pretty tpAct
240+
]
241+
pretty err@(OfTop _ _) = align $ prettyDecoratedErr err
242+
pretty err@(OfRec _ _) = align $ prettyDecoratedErr err
243+
244+
prettyDecoratedErr :: TypeError -> Doc ann
245+
prettyDecoratedErr (OfTop topName err) = "In top-level definition" <+> pretty topName <+> ":" <> softline <> prettyDecoratedErr err
246+
prettyDecoratedErr (OfRec recName err) = "In recursive expression" <+> pretty recName <+> ":" <> softline <> prettyDecoratedErr err
247+
prettyDecoratedErr err = indent 2 $ pretty err
248+
249+
prettyErrorNote :: [Text] -> Doc ann
250+
prettyErrorNote =
251+
((line <> "Note:" <> softline) <>)
252+
. align
253+
. reflow
254+
. T.intercalate " "
255+
256+
------------------------------------------------------------
257+
-- Utility functions
258+
------------------------------------------------------------
259+
260+
prefixOfPrec0 :: Int -> (Doc ann, Int) -> (Int -> Doc ann) -> Doc ann
261+
prefixOfPrec0 pr (pre, prePrec) op = condParens (pr > prePrec) $ align $ pre <> nest 2 (op prePrec)
262+
263+
prefixOfPrec1 :: Int -> (Doc ann, Int) -> (Int -> Doc ann) -> Doc ann
264+
prefixOfPrec1 pr (pre, prePrec) op = condParens (pr > prePrec) $ align $ pre <> nest 2 (op $ prePrec + 1)
265+
266+
prefixOfPrec2 :: Int -> (Doc ann, Int) -> (Int -> Doc ann) -> Doc ann
267+
prefixOfPrec2 pr (pre, prePrec) op = condParens (pr > prePrec) $ align $ pre <> nest 2 (op $ prePrec + 2)
268+
269+
infixlOfPrec :: Int -> (Int -> Doc ann) -> (Doc ann, Int) -> (Int -> Doc ann) -> Doc ann
270+
infixlOfPrec pr op0 (inl, inlPrec) op1 = condParens (pr > inlPrec) $ align $ op0 inlPrec <> nest 2 (inl <> op1 (inlPrec + 1))
271+
272+
infixnOfPrec :: Int -> (Int -> Doc ann) -> (Doc ann, Int) -> (Int -> Doc ann) -> Doc ann
273+
infixnOfPrec pr op0 (inl, inlPrec) op1 = condParens (pr > inlPrec) $ align $ op0 (inlPrec + 1) <> nest 2 (inl <> op1 (inlPrec + 1))
274+
275+
condParens :: Bool -> Doc ann -> Doc ann
276+
condParens True = parens
277+
condParens False = id

‎src/LambdaComp/CBPV/TypeCheck.hs‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ module LambdaComp.CBPV.TypeCheck
99
, askTypeCheckInfo
1010
, asksTypeCheckInfo
1111

12-
, TypeError
12+
, TypeError(..)
1313
) where
1414

1515
import Control.Monad (foldM, when)
@@ -18,7 +18,6 @@ import Control.Monad.Reader (MonadReader (ask, local), ReaderT (runReaderT), ask
1818
import Data.Map (Map)
1919
import Data.Map qualified as Map
2020
import Data.Text (Text)
21-
import Data.Text qualified as T
2221

2322
import LambdaComp.CBPV.Syntax
2423
import LambdaComp.PrimOp (PrimOpTypeBase (..), getPrimOpType)
@@ -47,7 +46,7 @@ topInfer top = do
4746
tp <- withError (OfTop (tmDefName top)) . infer . tmDefBody $ top
4847
case tp of
4948
TpDown tp' -> pure tp'
50-
_ -> throwError $ NonDownType "top" tp
49+
_ -> throwError $ NonDownType "top-level definition" tp
5150

5251
check :: (TypeErrorC m) => Tm c -> Tp c -> TypeCheckT m ()
5352
check TmUnit = \case
@@ -70,19 +69,19 @@ check (TmThunk tm) = \case
7069
tp -> throwError $ NonUpType tp
7170
check (TmReturn tm) = \case
7271
TpDown tp -> check tm tp
73-
tp -> throwError $ NonDownType "TmReturn Check" tp
72+
tp -> throwError $ NonDownType "Return" tp
7473
check (TmTo tm0 x tm1) = \tp -> do
7574
tp0 <- infer tm0
7675
case tp0 of
7776
TpDown tp0' -> local (insertEntryToInfo x tp0') $ check tm1 tp
78-
_ -> throwError $ NonDownType "TmToCheck" tp0
77+
_ -> throwError $ NonDownType "To" tp0
7978
check (TmLet x tm0 tm1) = \tp -> do
8079
tp0 <- infer tm0
8180
local (insertEntryToInfo x tp0) $ check tm1 tp
8281
check tm = \tp -> do
8382
tp' <- infer tm
8483
when (tp /= tp') $
85-
throwError $ TypeMismatch "infer to check" tp tp'
84+
throwError $ TypeMismatch "An inferable expression" tp tp'
8685

8786
infer :: (TypeErrorC m) => Tm c -> TypeCheckT m (Tp c)
8887
infer (TmVar x) = asksTypeCheckInfo (Map.lookup x . localCtx) >>= maybe (throwError $ NotInScope x) pure
@@ -119,7 +118,7 @@ infer (TmTo tm0 x tm1) = do
119118
tp0 <- infer tm0
120119
case tp0 of
121120
TpDown tp0' -> local (insertEntryToInfo x tp0') $ infer tm1
122-
_ -> throwError $ NonDownType ("TmTo" <> T.show tm0) tp0
121+
_ -> throwError $ NonDownType "To" tp0
123122
infer (TmLet x tm0 tm1) = do
124123
tp0 <- infer tm0
125124
local (insertEntryToInfo x tp0) $ infer tm1

‎src/LambdaComp/Driver.hs‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,15 @@ import LambdaComp.CBPV.Optimization.Local qualified as CBPV
2323
import LambdaComp.CBPV.ToAM (runToAM)
2424
import LambdaComp.CBPV.ToC (runToC)
2525
import LambdaComp.CBPV.TypeCheck qualified as CBPV
26+
import LambdaComp.CBPV.PrettyPrinter ()
2627
import LambdaComp.Driver.Argument
2728
import LambdaComp.Elaborated.CBV.ToCBPV (runToCBPV)
2829
import LambdaComp.Elaborated.Optimization.Local qualified as El
2930
import LambdaComp.Elaborated.TypeCheck qualified as El
3031
import LambdaComp.External.Parser (runProgramParser)
3132
import LambdaComp.External.ToElaborated (ElaborationError, runToElaborated)
33+
import Prettyprinter.Render.Text (hPutDoc)
34+
import Prettyprinter (Pretty(pretty))
3235

3336
mainFuncWithOptions :: Handle -> Options -> IO ExitCode
3437
mainFuncWithOptions outH (Options inputFp backend phase mayFp) = (<* hFlush outH) . exceptTToExitCode $ do
@@ -50,8 +53,8 @@ mainFuncWithOptions outH (Options inputFp backend phase mayFp) = (<* hFlush outH
5053
UntilAST -> getTm >>= pHPrintNoColor outH
5154
UntilElaboration -> getElTmTc >>= pHPrintNoColor outH
5255
UntilElaborationOpt -> getElOptTmTc >>= pHPrintNoColor outH
53-
UntilCBPV -> getCBPVTmAATc >>= pHPrintNoColor outH
54-
UntilCBPVOpt -> getCBPVOptTmTc >>= pHPrintNoColor outH
56+
UntilCBPV -> getCBPVTmAATc >>= lift . hPutDoc outH . pretty
57+
UntilCBPVOpt -> getCBPVOptTmTc >>= lift . hPutDoc outH . pretty
5558
UntilC -> getCCode >>= (\cCode -> runWithFp (\real -> lift . if real then (`writeFile` cCode) else const $ hPutStr outH cCode) mayFp)
5659
UntilExe -> getCCode >>= (\cCode -> runWithFp (const $ genCExe outH cCode) mayFp)
5760
UntilAM -> getAMTm >>= pHPrintNoColor outH

‎src/LambdaComp/Ident.hs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,12 @@ module LambdaComp.Ident
22
( module LambdaComp.Ident
33
) where
44

5-
import Data.String (IsString)
6-
import Data.Text (Text)
5+
import Data.String (IsString)
6+
import Data.Text (Text)
7+
import Prettyprinter (Pretty)
78

89
newtype Ident = Ident Text
9-
deriving newtype (Eq, Ord, Show, Read, IsString, Semigroup)
10+
deriving newtype (Eq, Ord, Show, Read, IsString, Semigroup, Pretty)
1011

1112
-- Variables obtained by elaboration
1213
toExtVar :: Ident -> Ident

0 commit comments

Comments
 (0)