From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Mon, 26 Oct 2015 14:52:21 +0000 (-0400)
Subject: Fix printing of Pi types
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=ee27e07d8a395b0caba82b8e29261da2dcfffbb2;p=cubicaltt.git

Fix printing of Pi types
---

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