From: Anders <mortberg@chalmers.se>
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"