Fix printing of formulas in AppFormula

diff --git a/CTT.hs b/CTT.hs
index 0a0ee1ffe9c80a041ec2cc7d9053942f7f526900..dde18a65b3a940d36b9f153e8b5cf25c5379561b 100644 (file)
--- 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 176a98158e292a473d416216fd53f8721fbd4c0d..5b5aa5d181ad046e594743367ad5e9526baeee64 100644 (file)
--- 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"