From: Simon Huber Date: Sat, 18 Apr 2015 02:28:18 +0000 (+0200) Subject: bugfix in resolver X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a08046c8c156e2ffdbe8c92f01a7d00bbe48fdfe;p=cubicaltt.git bugfix in resolver --- 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)