bugfix in resolver

diff --git a/CTT.hs b/CTT.hs
index 0661d694fce1fc703f0447c05f0ba6c8b6dad810..3f572e4406d2a52fccc94a4b86ffa844ff4f734f 100644 (file)
--- 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 fd6b97e4ddfcc9bf09ca7e73a8f0265bf4040034..81234933be0bfb3becbf53e436e69b05f4241f0a 100644 (file)
--- 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 dc5fb86c066b81c23facd7c8fe89982aca7de558..a6d36946b750ca730611b4c1a142d626b8189381 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -442,10 +442,9 @@ infer e = case e of
   PCon c a es phis -> do\r
     check VU a\r
     va <- evalTyping a\r
---    (bs,nu) <- getLblType c va\r
---    checks (bs,nu) es\r
---    mapM_ checkFormula phis\r
-    trace $ "va = " ++ show va\r
+    (bs,nu) <- getLblType c va\r
+    checks (bs,nu) es\r
+    mapM_ checkFormula phis\r
     return va\r
   _ -> throwError ("infer " ++ show e)\r
 \r