From ee27e07d8a395b0caba82b8e29261da2dcfffbb2 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Mon, 26 Oct 2015 10:52:21 -0400 Subject: [PATCH] Fix printing of Pi types --- CTT.hs | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/CTT.hs b/CTT.hs index c122be1..114b316 100644 --- a/CTT.hs +++ b/CTT.hs @@ -369,7 +369,7 @@ showVal v = case v of <+> hsep (map ((char '@' <+>) . showFormula) phis) VHComp v0 v1 vs -> text "hComp" <+> showVals [v0,v1] <+> text (showSystem vs) VPi a l@(VLam x t b) - | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b + | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b | otherwise -> char '(' <> showLam v VPi a b -> text "Pi" <+> showVals [a,b] VPair u v -> parens (showVal u <> comma <> showVal v) @@ -413,12 +413,16 @@ showLam e = case e of showVal1 :: Val -> Doc showVal1 v = case v of - VU -> showVal v - VCon c [] -> showVal v - VVar{} -> showVal v - VFst{} -> showVal v - VSnd{} -> showVal v - _ -> parens (showVal v) + VU -> showVal v + VCon c [] -> showVal v + VVar{} -> showVal v + VFst{} -> showVal v + VSnd{} -> showVal v + Ter t@Sum{} rho -> showTer t <+> showEnv False rho + Ter t@HSum{} rho -> showTer t <+> showEnv False rho + Ter t@Split{} rho -> showTer t <+> showEnv False rho + Ter t rho -> showTer1 t <+> showEnv True rho + _ -> parens (showVal v) showVals :: [Val] -> Doc showVals = hsep . map showVal1 -- 2.34.1