From: Anders Date: Fri, 20 Mar 2015 10:08:18 +0000 (+0100) Subject: Fix printing of formulas in AppFormula X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=697f32fb656a38999db9d79d9c3c55bc28be010f;p=cubicaltt.git Fix printing of formulas in AppFormula --- diff --git a/CTT.hs b/CTT.hs index 0a0ee1f..dde18a6 100644 --- a/CTT.hs +++ b/CTT.hs @@ -194,6 +194,12 @@ instance Show Loc where showLoc :: Loc -> Doc showLoc (Loc name (i,j)) = hcat [text name,text "_L",int i,text "_C",int j] +showFormula :: Formula -> Doc +showFormula phi = case phi of + _ :\/: _ -> parens (text (show phi)) + _ :/\: _ -> parens (text (show phi)) + _ -> text $ show phi + instance Show Ter where show = render . showTer @@ -215,7 +221,7 @@ showTer v = case v of Undef _ -> text "undefined" IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2] Path i e -> char '<' <> text (show i) <> char '>' <+> showTer e - AppFormula e phi -> showTer1 e <+> char '@' <+> text (show phi) + AppFormula e phi -> showTer1 e <+> char '@' <+> showFormula phi Comp e0 e1 es -> text "comp" <+> showTers [e0,e1] <+> text (showSystem es) Trans e0 e1 -> text "transport" <+> showTers [e0,e1] @@ -253,7 +259,7 @@ showVal v = case v of VSnd u -> showVal u <> text ".2" VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VPath i v -> char '<' <> text (show i) <> char '>' <+> showVal v - VAppFormula v phi -> showVal1 v <+> char '@' <+> text (show phi) + VAppFormula v phi -> showVal1 v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) VTrans v0 v1 -> text "trans" <+> showVals [v0,v1] showVal1 v = case v of diff --git a/Resolver.hs b/Resolver.hs index 176a981..5b5aa5d 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -205,7 +205,7 @@ resolveWhere = resolveExp . unWhere resolveSystem :: Exp -> Resolver (C.System Ter) resolveSystem (System ts) = - -- TODO: Erase alpha when resolving u?? + -- Note: the symbols in alpha are in scope in u, but they mean 0 or 1 Map.fromList <$> sequence [ (,) <$> resolveFace alpha <*> resolveExp u | Side alpha u <- ts ] resolveSystem e = throwError $ show e ++ " is not a system"