Fix printing of goals and environments (TODO: Fix "susp (bool)"...)

diff --git a/CTT.hs b/CTT.hs
index 7b20d3aa7345c79d88e6015962231b46b5265070..e764036f9b0ad3acb3d2d107d819a8e20e144f59 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -194,7 +194,7 @@ isNeutralTrans (VPath i a) u = foo i a u
         foo i a u | isNeutral a = True
         foo i (Ter Sum{} _) u   = isNeutral u
         foo i (VGlue _ as) u    =
-          let shasBeta = (shape as) `face` (i ~> 0)
+          let shasBeta = shape as `face` (i ~> 0)
           in shasBeta /= Map.empty && eps `Map.notMember` shasBeta && isNeutral u
         foo _ _ _ = False
 isNeutralTrans u _ = isNeutral u
@@ -279,17 +279,22 @@ contextOfEnv rho = case rho of
 -- | Pretty printing
 
 instance Show Env where
-  show = render . showEnv
-
-showEnv, showEnv1 :: Env -> Doc
-showEnv e = case e of
-  Empty           -> PP.empty
-  Def _ env       -> showEnv env
-  Upd env (_,u)   -> parens (showEnv1 env <> showVal u)
-  Sub env (_,phi) -> parens (showEnv1 env <> text (show phi))
-showEnv1 (Upd env (_,u))   = showEnv1 env <> showVal u <> text ", "
-showEnv1 (Sub env (_,phi)) = showEnv1 env <> text (show phi) <> text ", "
-showEnv1 e                 = showEnv e
+  show = render . showEnv True
+
+showEnv :: Bool -> Env -> Doc
+showEnv b e =
+  let -- This decides if we should print "x = " or not
+      names x = if b then text x <+> equals else PP.empty
+
+      showEnv1 e = case e of
+        Upd env (x,u)   -> showEnv1 env <> names x <+> showVal u <> comma
+        Sub env (i,phi) -> showEnv1 env <> names (show i) <+> text (show phi) <> comma
+        _               -> showEnv b e
+  in case e of
+    Empty           -> PP.empty
+    Def _ env       -> showEnv b env
+    Upd env (x,u)   -> parens (showEnv1 env <+> names x <+> showVal u)
+    Sub env (i,phi) -> parens (showEnv1 env <+> names (show i) <+> text (show phi))
 
 instance Show Loc where
   show = render . showLoc
@@ -363,7 +368,9 @@ instance Show Val where
 showVal :: Val -> Doc
 showVal v = case v of
   VU                -> char 'U'
-  Ter t env         -> showTer1 t <+> showEnv env
+  Ter t@Sum{} rho   -> showTer t <+> showEnv False rho
+  Ter t@Split{} rho -> showTer t <+> showEnv False rho
+  Ter t env         -> showTer1 t <+> showEnv True env
   VCon c us         -> text c <+> showVals us
   VPCon c a us phi  -> text c <+> char '{' <+> showVal a <+> char '}' <+>
                        showVals us <+> showFormula phi
@@ -393,11 +400,12 @@ showVal v = case v of
 
 showVal1 :: Val -> Doc
 showVal1 v = case v of
-  VU              -> char 'U'
-  VCon c []       -> text c
-  VVar{}          -> showVal v
-  Ter t@Sum{} rho -> showTer t <+> showEnv rho
-  _               -> parens (showVal v)
+  VU                -> showVal v
+  VCon c []         -> showVal v
+  VVar{}            -> showVal v
+  Ter t@Sum{} rho   -> showTer t <+> showEnv False rho
+  Ter t@Split{} rho -> showTer t <+> showEnv False rho
+  _                 -> parens (showVal v)
 
 showVals :: [Val] -> Doc
 showVals = hsep . map showVal1

diff --git a/Connections.hs b/Connections.hs
index 8a3d65a85f7c68eaa2037133933c069e432e23be..fe2c10b48e7e41648ab810f5b2fe6fc55a3dac98 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -101,7 +101,7 @@ meets :: [Face] -> [Face] -> [Face]
 meets xs ys = nub [ meet x y | x <- xs, y <- ys, compatible x y ]
 
 meetss :: [[Face]] -> [Face]
-meetss xss = foldr meets [eps] xss
+meetss = foldr meets [eps]
 
 leq :: Face -> Face -> Bool
 alpha `leq` beta = meetMaybe alpha beta == Just alpha
@@ -137,7 +137,7 @@ data Formula = Dir Dir
 instance Show Formula where
   show (Dir Zero)  = "0"
   show (Dir One)   = "1"
-  show (NegAtom a) = "-" ++ show a
+  show (NegAtom a) = '-' : show a
   show (Atom a)    = show a
   show (a :\/: b)  = show1 a ++ " \\/ " ++ show1 b
     where show1 v@(a :/\: b) = "(" ++ show v ++ ")"
@@ -148,13 +148,13 @@ instance Show Formula where
 
 arbFormula :: [Name] -> Int -> Gen Formula
 arbFormula names s =
-      frequency [ (1, Dir <$> arbitrary)
-                , (1, Atom <$> elements names)
-                , (1, NegAtom <$> elements names)
-                , (s, do op <- elements [andFormula,orFormula]
-                         op <$> arbFormula names s' <*> arbFormula names s')
-                ]
-      where s' = s `div` 3
+  frequency [ (1, Dir <$> arbitrary)
+            , (1, Atom <$> elements names)
+            , (1, NegAtom <$> elements names)
+            , (s, do op <- elements [andFormula,orFormula]
+                     op <$> arbFormula names s' <*> arbFormula names s')
+            ]
+  where s' = s `div` 3
 
 instance Arbitrary Formula where
   arbitrary = do
@@ -195,10 +195,10 @@ orFormula phi (Dir Zero) = phi
 orFormula phi psi        = phi :\/: psi
 
 dnf :: Formula -> Set (Set (Name,Dir))
-dnf (Dir One) = Set.singleton Set.empty
-dnf (Dir Zero) = Set.empty
-dnf (Atom n) = Set.singleton (Set.singleton (n,1))
-dnf (NegAtom n) = Set.singleton (Set.singleton (n,0))
+dnf (Dir One)      = Set.singleton Set.empty
+dnf (Dir Zero)     = Set.empty
+dnf (Atom n)       = Set.singleton (Set.singleton (n,1))
+dnf (NegAtom n)    = Set.singleton (Set.singleton (n,0))
 dnf (phi :\/: psi) = dnf phi `Set.union` dnf psi
 dnf (phi :/\: psi) = Set.fromList [ a `Set.union` b
                                   | a <- Set.toList (dnf phi)
@@ -320,7 +320,7 @@ instance Nominal a => Nominal [a]  where
 
 instance Nominal a => Nominal (Maybe a)  where
   support    = maybe [] support
-  act v f    = fmap (\u -> act u f) v
+  act v f    = fmap (`act` f) v
   swap a n   = fmap (`swap` n) a
 
 instance Nominal Formula where
@@ -412,7 +412,7 @@ border :: Nominal a => a -> System b -> System a
 border v = Map.mapWithKey (const . face v)
 
 shape :: System a -> System ()
-shape ts = border () ts
+shape = border ()
 
 instance (Nominal a, Arbitrary a) => Arbitrary (System a) where
   arbitrary = do

diff --git a/TypeChecker.hs b/TypeChecker.hs
index a4c9a48178176daaf95d3d8bf2d7b1ed0cb5c11b..89235b5b6bdafa7e2297b2eade467ee7bd858a05 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -146,8 +146,9 @@ check a t = case (a,t) of
   (_,Hole l)  -> do\r
       rho <- asks env\r
       let e = unlines (reverse (contextOfEnv rho))\r
+      k <- asks index\r
       trace $ "\nHole at " ++ show l ++ ":\n\n" ++\r
-              e ++ replicate 80 '-' ++ "\n" ++ show a ++ "\n"\r
+              e ++ replicate 80 '-' ++ "\n" ++ show (normal k a)  ++ "\n"\r
   (_,Con c es) -> do\r
     (bs,nu) <- getLblType c a\r
     checks (bs,nu) es\r

diff --git a/examples/susp.ctt b/examples/susp.ctt
index 5e51d53890a6863e04669a6f5e06a50f5e75f57b..ef53a7afe1388a14caf9a24971cadf7144e03ef0 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -15,13 +15,14 @@ sphere : nat -> U = split
 -- (Similar to HoTT Book, Lemma 6.5.1)\r
 sone : U = sphere one\r
 \r
+path : bool -> Id S1 base base = split\r
+  false -> loop1\r
+  true  -> refl S1 base\r
+\r
 s1ToCircle : sone -> S1 = split\r
   north   -> base\r
   south   -> base\r
   merid b @ i -> (path b) @ i\r
-    where path : bool ->Id S1 base base = split\r
-            false -> loop1\r
-            true  -> refl S1 base\r
 \r
 m0 : Id sone north south = <i> (merid{sone} false) @ i\r
 \r