More work on effect and delay rendering in Type pretty-printer

Tricky interactions between the two...

Possibly uncovered a parser issue - see Test\TypePrinter.hs.
This commit is contained in:
Chris Gibbs 2018-09-16 16:24:34 +01:00
parent 7304708255
commit 05f362e359
3 changed files with 74 additions and 26 deletions

View File

@ -11,3 +11,4 @@ The format for this list: name, GitHub handle, and then optional blurb about wha
* Paul Chiusano (@pchiusano) - I've worked on just about all aspects of Unison: overall design, typechecker, runtime, parser...
* Arya Irani (@aryairani)
* Rúnar Bjarnason (@runarorama) - Typechecker, runtime, parser, code serialization
* Chris Gibbs (@atacratic) - Pretty-printer

View File

@ -10,6 +10,7 @@ import Data.List
import Data.Text (Text)
import qualified Data.Text as Text
import Data.Foldable (fold)
import Data.Maybe (isJust)
import Unison.Reference (Reference(..))
import Unison.Type
import Unison.Var (Var)
@ -27,36 +28,48 @@ pretty n p = \case
Abs' _ -> l $ "error" -- TypeParser does not currently emit Abs
Ann' _ _ -> l $ "error" -- TypeParser does not currently emit Ann
App' (Ref' (Builtin "Sequence")) x -> l"[" <> pretty n 0 x <> l"]"
Tuple' xs -> l"(" <> commaList n xs <> l")"
Tuple' xs -> l"(" <> commaList xs <> l")"
App' f x -> paren (p >= 10) $ pretty n 9 f <> b" " <> pretty n 10 x
Effect1' e t -> paren (p >= 10) $ pretty n 9 e <> l" " <> pretty n 10 t
Effects' es -> l"{" <> commaList n es <> l"}"
Effects' es -> l"{" <> commaList es <> l"}"
ForallNamed' v body -> case p of
0 -> pretty n p body
_ -> paren True $ l"" <> l (Text.unpack (Var.name v)) <> l". " <> pretty n 0 body
Arrow' (Ref' (Builtin "()")) o -> l"'" <> pretty n 9 o -- BUG fails to group with subsequent arrows -- BUG misrendering effects on the arrow?
EffectfulArrows' fst rest -> PP.Group $ paren (p > 0) $ pretty n 0 fst <> arrows 0 rest
EffectfulArrows' (Ref' (Builtin "()")) rest -> arrows True True rest
EffectfulArrows' fst rest -> PP.Group $ paren (p > 0) $ pretty n 0 fst <> arrows False False rest
_ -> l"error"
where commaList n xs = fold $ intersperse (l"," <> b" ") (map (pretty n 0) xs)
-- pure arrow to a delayed type
arrows _ ((Nothing, Ref' (Builtin "()")) : (Nothing, t) : rest) =
b" " <> l"-> '" <> arrowArg (rest /= []) n t rest
-- effectful arrow to a delayed type
arrows _ ((Just es, Ref' (Builtin "()")) : (Nothing, t) : rest) =
b" " <> l"->{" <> commaList n es <> l"} '" <> arrowArg (rest /= []) n t rest
-- pure arrow to non-delayed type
arrows p ((Nothing, t) : rest) =
b" " <> l"-> " <> pretty n p t <> arrows p rest
-- effectful arrow to non-delayed type
arrows p ((Just es, t) : rest) =
b" " <> l"->{" <> commaList n es <> l"} " <> pretty n p t <> arrows p rest
arrows _ [] = Empty
arrowArg pred n t rest = let p = if pred then 0 else 9
in paren pred $ pretty n p t <> arrows p rest
where commaList xs = fold $ intersperse (l"," <> b" ") (map (pretty n 0) xs)
effects Nothing = Empty
effects (Just es) = l"{" <> commaList es <> l"}"
arrow delay first mes = (if first then Empty else b" " <> l"->" ) <>
(if delay
then (if isJust mes || first then l"'" else l" '")
else Empty) <>
effects mes <>
if (isJust mes) || (not delay) && (not first) then l" " else Empty
arrows delay first [(mes, Ref' (Builtin "()"))] = arrow delay first mes <> l"()"
arrows False first ((mes, Ref' (Builtin "()")) : rest) =
if (isJust mes)
then arrow True first mes <> arrows False True rest
else arrows True first rest
arrows delay first ((mes, arg) : rest) = arrow delay first mes <>
(paren (delay && (not $ null rest)) $
pretty n 0 arg <> arrows False False rest)
arrows False False [] = Empty
arrows False True [] = Empty -- not reachable
arrows True _ [] = Empty -- not reachable
paren True s = l"(" <> s <> l")"
paren False s = s
l = Literal
b = Breakable
-- TODO group pretty much everywhere parens are used
-- TODO `parse . pretty = id` test on all types in test suite
-- TODO some renderBroken testing
-- TODO PR for type pretty-printer
-- TODO terms etc, and more attention to line-breaking behaviour
pretty' :: Var v => (Reference -> Text) -> AnnotatedType v a -> String
pretty' n t = PP.renderUnbroken $ pretty n 0 t

View File

@ -26,6 +26,7 @@ tc_diff s expected =
if actual == expected then ok
else do note $ "expected: " ++ show expected
note $ "actual : " ++ show actual
note $ "show(input) : " ++ show input_term
crash "actual != expected"
), (
if input_term == actual_reparsed then ok
@ -48,7 +49,7 @@ test = scope "typeprinter" . tests $
, tc "Pair a a"
, tc "(a, a)"
, tc "(a, a, a)"
, tc "(a, a, a, a)"
, tc "(a, b, c, d)"
, tc "Pair a (Pair a a)"
, tc "Pair (Pair a a) a"
, tc "{} (Pair a a)"
@ -56,6 +57,8 @@ test = scope "typeprinter" . tests $
, tc "a ->{e1} b"
, tc "a ->{e1, e2} b -> c ->{} d"
, tc "a ->{e1, e2} b ->{} c -> d"
, tc "a -> b -> c ->{} d"
, tc "a -> b ->{} c -> d"
, tc "{e1, e2} (Pair a a)"
, tc "Pair (a -> b) (c -> d)"
, tc "Pair a b ->{e1, e2} Pair a b ->{} Pair (a -> b) d -> Pair c d"
@ -64,12 +67,43 @@ test = scope "typeprinter" . tests $
, tc "'Pair a a"
, tc "a -> 'b"
, tc "'(a -> b)"
--, tc "'a -> b" --BUG
--, tc "a -> 'b -> c" --BUG
--TODO, tc "(a -> b) -> c" -- I need to strip out the effect variable added into argument for effect polymorphism.
--TODO, tc "'a -> b" -- same as above; pretty = "'{\120518} a -> b"; show input = "(𝛆. (a. (b. (() -> (({[𝛆]} a))) -> b)))"
--TODO, tc "a -> 'b -> c" -- ditto
, tc "a -> '(b -> c)"
, tc "a -> 'Pair b c"
, tc "a -> b -> 'c"
, tc "a ->{e} 'b"
, tc "a ->{e} '(b -> c)"
--, tc "'{e} a" --BUG
--BUG 1, tc "a ->{e} 'b" -- show . parse is producing "(a. (b. (e. a -> ({[e]} () -> b))))"
-- But I think it should be: "(a. (b. (e. ({[e]} a -> (() -> b)))))"
-- i.e. I think it should mean the same as "a ->{e} (() -> b)"
--BUG 2, tc "a ->'{e} b" -- I think this is how we should render "a -> () ->{e} b" (i.e. the thing the
-- parser produced in the previous case), but currently the parser chokes on it
-- with "unexpected UnknownLexeme". Observe that "'{e} b" means "() ->{e} b",
-- so my proposed behaviour is consistent with that.
--BUG 2, tc "a ->'{e} b -> c"
--BUG 2, tc "a ->'{e} b ->{f} c"
--BUG 2, tc "a ->'{e} (b -> c)"
--BUG 2, tc "a ->'{e} (b ->{f} c)"
, tc "a -> 'b"
, tc "a -> 'b ->{f} c"
, tc "a -> '(b -> c)"
, tc "a -> '(b ->{f} c)"
--BUG 2, tc "a ->'{e} (() -> b)" -- i.e. a -> () ->{e} () -> b QUESTION 1 - I'm guessing we don't
-- want to render this one as "a ->'{e} 'b", right? Since a -> ''b is
-- not accepted either?
--BUG 2, tc "a ->'{e} (() -> b -> c)"
--BUG 2, tc_diff "a -> () ->{e} () -> b -> c" $ "a ->'{e} (() -> b -> c)" -- desugared version of the above
--BUG 3 , tc "a ->{e} () ->{f} b" -- QUESTION 2 - I'm pretty sure we don't want to render
-- this as "a ->{e} '{f}b", right? Or do we?
--BUG 3, tc "a -> () ->{e} () ->{f} b"
--BUG 1, tc "a ->{e} '(b -> c)"
--BUG 2, tc "a ->'{e} (b -> c)"
--BUG 2, tc_diff "a -> () ->{e} () -> b" $ "a ->'{e} (() -> b)"
, tc "'{e} a"
, tc "'{e} (a -> b)"
, tc "'{e} (a ->{f} b)"
, tc "'(a -> 'a)"
, tc "'()"
]