Improve printing of fst and snd

diff --git a/CTT.hs b/CTT.hs
index 8eab044815242ebc5faa421fc4692d1074863b2e..55e6af8b9a441d225b6152f702843f0a95f16374 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -277,14 +277,18 @@ showEnv b e =
       names x = if b then text x <+> equals else PP.empty
 
       showEnv1 e = case e of
-        (Upd x env,u:us,fs)   -> showEnv1 (env,us,fs) <> names x <+> showVal u <> comma
-        (Sub i env,us,phi:fs) -> showEnv1 (env,us,fs) <> names (show i) <+> text (show phi) <> comma
+        (Upd x env,u:us,fs)   ->
+          showEnv1 (env,us,fs) <> names x <+> showVal u <> comma
+        (Sub i env,us,phi:fs) ->
+          showEnv1 (env,us,fs) <> names (show i) <+> text (show phi) <> comma
         _                     -> showEnv b e
   in case e of
     (Empty,_,_)           -> PP.empty
     (Def _ env,vs,fs)     -> showEnv b (env,vs,fs)
-    (Upd x env,u:us,fs)   -> parens (showEnv1 (env,us,fs) <+> names x <+> showVal u)
-    (Sub i env,us,phi:fs) -> parens (showEnv1 (env,us,fs) <+> names (show i) <+> text (show phi))
+    (Upd x env,u:us,fs)   ->
+      parens (showEnv1 (env,us,fs) <+> names x <+> showVal u)
+    (Sub i env,us,phi:fs) ->
+      parens (showEnv1 (env,us,fs) <+> names (show i) <+> text (show phi))
 
 instance Show Loc where
   show = render . showLoc
@@ -343,6 +347,8 @@ showTer1 t = case t of
   Split{}  -> showTer t
   Sum{}    -> showTer t
   HSum{}   -> showTer t
+  Fst{}    -> showTer t
+  Snd{}    -> showTer t
   _        -> parens (showTer t)
 
 showDecls :: [Decl] -> Doc
@@ -380,7 +386,8 @@ showVal v = case v of
                          <+> text (showSystem hs)
   VIdP v0 v1 v2     -> text "IdP" <+> showVals [v0,v1,v2]
   VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi
-  VComp v0 v1 vs    -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
+  VComp v0 v1 vs    ->
+    text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
   VGlue a ts        -> text "glue" <+> showVal1 a <+> text (showSystem ts)
   VGlueElem a ts    -> text "glueElem" <+> showVal1 a <+> text (showSystem ts)
 
@@ -395,10 +402,12 @@ showLam :: Val -> Doc
 showLam e = case e of
   VLam x t a@(VLam _ t' _)
     | t == t'   -> text x <+> showLam a
-    | otherwise -> text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a
+    | otherwise ->
+      text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a
   VPi _ (VLam x t a@(VPi _ (VLam _ t' _)))
     | t == t'   -> text x <+> showLam a
-    | otherwise -> text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a
+    | otherwise ->
+      text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal a
   VLam x t e         ->
     text x <+> colon <+> showVal t <> char ')' <+> text "->" <+> showVal e
   VPi _ (VLam x t e) ->
@@ -410,6 +419,8 @@ showVal1 v = case v of
   VU        -> showVal v
   VCon c [] -> showVal v
   VVar{}    -> showVal v
+  VFst{}    -> showVal v
+  VSnd{}    -> showVal v
   _         -> parens (showVal v)
 
 showVals :: [Val] -> Doc

diff --git a/Connections.hs b/Connections.hs
index 094b3a9355f960acb191fa824caa8c045245bb9d..382db2ba53cb2b2808891ea2d8e5b2531487dd5b 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -368,6 +368,7 @@ face = Map.foldWithKey (\i d a -> act a (i,Dir d))
 type System a = Map Face a
 
 showListSystem :: Show a => [(Face,a)] -> String
+showListSystem [] = "[]"
 showListSystem ts =
   "[ " ++ intercalate ", " [ showFace alpha ++ " -> " ++ show u
                            | (alpha,u) <- ts ] ++ " ]"

diff --git a/Resolver.hs b/Resolver.hs
index 8d8585bc55ec078cf9986c60a1bbfafa02d1ff3f..f3738d455741a0bb52b06bb0680c950b1d00df75 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -156,7 +156,7 @@ path :: AIdent -> Resolver Ter -> Resolver Ter
 path i e = CTT.Path (C.Name (unAIdent i)) <$> local (insertName i) e
 
 paths :: [AIdent] -> Resolver Ter -> Resolver Ter
-paths [] _ = throwError "Empty path lambda"
+paths [] _ = throwError "Empty path abstraction"
 paths xs e = foldr path e xs
 
 bind :: (Ter -> Ter) -> (Ident,Exp) -> Resolver Ter -> Resolver Ter

diff --git a/TypeChecker.hs b/TypeChecker.hs
index e39535068c0a503413570ead8c01c9b24250f443..4348503c0b54d33b94c9d02cbef95b5632c8f2f6 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -20,7 +20,7 @@ type Typing a = ReaderT TEnv (ExceptT String IO) a
 \r
 -- Environment for type checker\r
 data TEnv =\r
-  TEnv { names   :: [String]  -- generated names\r
+  TEnv { names   :: [String] -- generated names\r
        , indent  :: Int\r
        , env     :: Env\r
        , verbose :: Bool  -- Should it be verbose and print what it typechecks?\r