Skip to content

Commit

Permalink
Fix parens in pretty printing of sequence types.
Browse files Browse the repository at this point in the history 
The fix required inserting another precedence level for sequence types
`[n]a` (level 4) in between `app_type` (level 3) and `atype` (now
level 5).

Fixes #933.
  • Loading branch information
Brian Huffman committed Nov 13, 2020
1 parent 5a2be86 commit ade7a53
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 18 deletions.
2 changes: 1 addition & 1 deletion src/Cryptol/TypeCheck/AST.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,7 @@ instance PP (WithNames Expr) where
$ ppWP 3 e <+> text "<>"

ETApp e t -> optParens (prec > 3)
$ ppWP 3 e <+> ppWP 4 t
$ ppWP 3 e <+> ppWP 5 t

EWhere e ds -> optParens (prec > 0)
( ppW e $$ text "where"
Expand Down
36 changes: 19 additions & 17 deletions src/Cryptol/TypeCheck/Type.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -909,7 +909,9 @@ instance PP (WithNames Newtype) where
--
-- * 3: @app_type@
--
-- * 4: @atype@
-- * 4: @dimensions atype@
--
-- * 5: @atype@
instance PP (WithNames Type) where
ppPrec prec ty0@(WithNames ty nmMap) =
case ty of
Expand All @@ -929,7 +931,7 @@ instance PP (WithNames Type) where
_ ->
case ts of
[] -> pp c
_ -> optParens (prec > 3) $ pp c <+> fsep (map (go 4) ts)
_ -> optParens (prec > 3) $ pp c <+> fsep (map (go 5) ts)

TCon (TC tc) ts ->
case (tc,ts) of
Expand All @@ -939,43 +941,43 @@ instance PP (WithNames Type) where
(TCInteger, []) -> text "Integer"
(TCRational, []) -> text "Rational"

(TCIntMod, [n]) -> optParens (prec > 3) $ text "Z" <+> go 4 n
(TCIntMod, [n]) -> optParens (prec > 3) $ text "Z" <+> go 5 n

(TCSeq, [t1,TCon (TC TCBit) []]) -> brackets (go 0 t1)
(TCSeq, [t1,t2]) -> optParens (prec > 3)
$ brackets (go 0 t1) <.> go 3 t2
(TCSeq, [t1,t2]) -> optParens (prec > 4)
$ brackets (go 0 t1) <.> go 4 t2

(TCFun, [t1,t2]) -> optParens (prec > 1)
$ go 2 t1 <+> text "->" <+> go 1 t2

(TCTuple _, fs) -> parens $ fsep $ punctuate comma $ map (go 0) fs

(_, _) -> optParens (prec > 3) $ pp tc <+> fsep (map (go 4) ts)
(_, _) -> optParens (prec > 3) $ pp tc <+> fsep (map (go 5) ts)

TCon (PC pc) ts ->
case (pc,ts) of
(PEqual, [t1,t2]) -> go 0 t1 <+> text "==" <+> go 0 t2
(PNeq , [t1,t2]) -> go 0 t1 <+> text "!=" <+> go 0 t2
(PGeq, [t1,t2]) -> go 0 t1 <+> text ">=" <+> go 0 t2
(PFin, [t1]) -> optParens (prec > 3) $ text "fin" <+> (go 4 t1)
(PPrime, [t1]) -> optParens (prec > 3) $ text "prime" <+> (go 4 t1)
(PFin, [t1]) -> optParens (prec > 3) $ text "fin" <+> (go 5 t1)
(PPrime, [t1]) -> optParens (prec > 3) $ text "prime" <+> (go 5 t1)
(PHas x, [t1,t2]) -> ppSelector x <+> text "of"
<+> go 0 t1 <+> text "is" <+> go 0 t2
(PAnd, [t1,t2]) -> parens (commaSep (map (go 0) (t1 : pSplitAnd t2)))

(PRing, [t1]) -> pp pc <+> go 4 t1
(PField, [t1]) -> pp pc <+> go 4 t1
(PIntegral, [t1]) -> pp pc <+> go 4 t1
(PRound, [t1]) -> pp pc <+> go 4 t1
(PRing, [t1]) -> pp pc <+> go 5 t1
(PField, [t1]) -> pp pc <+> go 5 t1
(PIntegral, [t1]) -> pp pc <+> go 5 t1
(PRound, [t1]) -> pp pc <+> go 5 t1

(PCmp, [t1]) -> pp pc <+> go 4 t1
(PSignedCmp, [t1]) -> pp pc <+> go 4 t1
(PLiteral, [t1,t2]) -> pp pc <+> go 4 t1 <+> go 4 t2
(PCmp, [t1]) -> pp pc <+> go 5 t1
(PSignedCmp, [t1]) -> pp pc <+> go 5 t1
(PLiteral, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2

(_, _) -> optParens (prec > 3) $ pp pc <+> fsep (map (go 4) ts)
(_, _) -> optParens (prec > 3) $ pp pc <+> fsep (map (go 5) ts)

TCon f ts -> optParens (prec > 3)
$ pp f <+> fsep (map (go 4) ts)
$ pp f <+> fsep (map (go 5) ts)

where
go p t = ppWithNamesPrec nmMap p t
Expand Down

0 comments on commit ade7a53

Please sign in to comment.