From: Anders Date: Fri, 17 Apr 2015 15:18:04 +0000 (+0200) Subject: Fix printing of goals and environments (TODO: Fix "susp (bool)"...) X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=aed955207f1d121d8c951238d7c304f9cdfa4d87;p=cubicaltt.git Fix printing of goals and environments (TODO: Fix "susp (bool)"...) --- diff --git a/CTT.hs b/CTT.hs index 7b20d3a..e764036 100644 --- 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 8a3d65a..fe2c10b 100644 --- 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 a4c9a48..89235b5 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -146,8 +146,9 @@ check a t = case (a,t) of (_,Hole l) -> do rho <- asks env let e = unlines (reverse (contextOfEnv rho)) + k <- asks index trace $ "\nHole at " ++ show l ++ ":\n\n" ++ - e ++ replicate 80 '-' ++ "\n" ++ show a ++ "\n" + e ++ replicate 80 '-' ++ "\n" ++ show (normal k a) ++ "\n" (_,Con c es) -> do (bs,nu) <- getLblType c a checks (bs,nu) es diff --git a/examples/susp.ctt b/examples/susp.ctt index 5e51d53..ef53a7a 100644 --- a/examples/susp.ctt +++ b/examples/susp.ctt @@ -15,13 +15,14 @@ sphere : nat -> U = split -- (Similar to HoTT Book, Lemma 6.5.1) sone : U = sphere one +path : bool -> Id S1 base base = split + false -> loop1 + true -> refl S1 base + s1ToCircle : sone -> S1 = split north -> base south -> base merid b @ i -> (path b) @ i - where path : bool ->Id S1 base base = split - false -> loop1 - true -> refl S1 base m0 : Id sone north south = (merid{sone} false) @ i