From a08046c8c156e2ffdbe8c92f01a7d00bbe48fdfe Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Sat, 18 Apr 2015 04:28:18 +0200
Subject: [PATCH] bugfix in resolver

---
 CTT.hs         | 10 ++++------
 Resolver.hs    | 14 +++++++-------
 TypeChecker.hs |  7 +++----
 3 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/CTT.hs b/CTT.hs
index 0661d69..3f572e4 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -327,9 +327,8 @@ showTer v = case v of
   Where e d          -> showTer e <+> text "where" <+> showDecls d
   Var x              -> text x
   Con c es           -> text c <+> showTers es
-  PCon c a es phis   -> text c <+> char '{' <+> showTer a <+> char '}'
-                        <+> showTers es
-                        <+> (hsep $ punctuate (char '@') (map showFormula phis))
+  PCon c a es phis   -> text c <+> braces (showTer a) <+> showTers es
+                        <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
   Split f _ _ _      -> text f
   Sum _ n _          -> text n
   Undef{}            -> text "undefined"
@@ -375,9 +374,8 @@ showVal v = case v of
   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 phis -> text c <+> char '{' <+> showVal a <+> char '}'
-                       <+> showVals us
-                       <+> (hsep $ punctuate (char '@') (map showFormula phis))
+  VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us
+                       <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
   VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->"
                                                <+> showVal1 b
                        | otherwise -> showVal l
diff --git a/Resolver.hs b/Resolver.hs
index fd6b97e..8123493 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -47,10 +47,10 @@ appsToIdents = mapM unVar . uncurry (:) . flip unApps []
 
 -- Transform a sequence of applications
 -- (((u v1) .. vn) phi1) .. phim into (u,[v1,..,vn],[phi1,..,phim])
-unAppsFormulas :: Exp -> [Exp] -> [Formula]-> (Exp,[Exp],[Formula])
-unAppsFormulas (AppFormula u phi) ws phis = unAppsFormulas u ws (phi:phis)
-unAppsFormulas u ws phis = (x,xs++ws,phis)
-  where (x,xs) = unApps u ws
+unAppsFormulas :: Exp -> [Formula]-> (Exp,[Exp],[Formula])
+unAppsFormulas (AppFormula u phi) phis = unAppsFormulas u (phi:phis)
+unAppsFormulas u phis = (x,xs,phis)
+  where (x,xs) = unApps u []
 
 
 -- Flatten a tele
@@ -196,13 +196,13 @@ resolveExp e = case e of
     mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
   Path is e     -> paths is (resolveExp e)
   Hole (HoleIdent (l,_)) -> CTT.Hole <$> getLoc l
-  AppFormula e phi ->
-    let (x,xs,phis) = unAppsFormulas e [] []
+  AppFormula t phi ->
+    let (x,xs,phis) = unAppsFormulas e []
     in case x of
       PCon n a ->
         CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
                               <*> mapM resolveFormula phis
-      _ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
+      _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
   Trans x y   -> CTT.Trans <$> resolveExp x <*> resolveExp y
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
   Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
diff --git a/TypeChecker.hs b/TypeChecker.hs
index dc5fb86..a6d3694 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -442,10 +442,9 @@ infer e = case e of
   PCon c a es phis -> do
     check VU a
     va <- evalTyping a
---    (bs,nu) <- getLblType c va
---    checks (bs,nu) es
---    mapM_ checkFormula phis
-    trace $ "va = " ++ show va
+    (bs,nu) <- getLblType c va
+    checks (bs,nu) es
+    mapM_ checkFormula phis
     return va
   _ -> throwError ("infer " ++ show e)
 
-- 
2.34.1