From 9e232c77ee6d0948f7dd5727d3ec568bbedf4316 Mon Sep 17 00:00:00 2001 From: Péter Diviánszky Date: Thu, 5 May 2016 17:55:01 +0200 Subject: improve pretty printing & try to fix local function handling --- src/LambdaCube/Compiler/Core.hs | 18 ++--------- src/LambdaCube/Compiler/CoreToIR.hs | 23 ++++++-------- src/LambdaCube/Compiler/DesugaredSource.hs | 19 +++++++----- src/LambdaCube/Compiler/Infer.hs | 22 +++++++------- src/LambdaCube/Compiler/Pretty.hs | 48 +++++++++++++++++++++++++----- 5 files changed, 74 insertions(+), 56 deletions(-) (limited to 'src') diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs index 5e2b4136..a75beb60 100644 --- a/src/LambdaCube/Compiler/Core.hs +++ b/src/LambdaCube/Compiler/Core.hs @@ -21,7 +21,7 @@ import Control.Arrow hiding ((<+>)) --import LambdaCube.Compiler.Utils import LambdaCube.Compiler.DeBruijn import LambdaCube.Compiler.Pretty hiding (braces, parens) -import LambdaCube.Compiler.DesugaredSource hiding (getList) +import LambdaCube.Compiler.DesugaredSource -------------------------------------------------------------------------------- De-Bruijn limit @@ -509,8 +509,7 @@ instance MkDoc Exp where Pi h TType b -> shLam_ (usedVar 0 b) (BPi h) Nothing (f b) Pi h a b -> shLam (usedVar 0 b) (BPi h) (f a) (f b) ENat n -> pShow n - (getTTup -> Just xs) -> shTuple $ f <$> xs - (getTup -> Just xs) -> shTuple $ f <$> xs + ConN FHCons [_, _, x, xs] -> foldl DApp (text "HCons") (f <$> [x, xs]) Con s _ xs -> foldl DApp (pShow s) (f <$> xs) TyConN s xs -> foldl DApp (pShow s) (f <$> xs) TType -> text "Type" @@ -533,17 +532,6 @@ instance MkDoc Neutral where TyCaseFun_ s [m, t, f] n -> foldl DApp (pShow s) (g <$> [m, t, Neut n, f]) TyCaseFun_ s _ n -> error $ "mkDoc TyCaseFun" -getTup (hnf -> ConN FHCons [_, _, x, xs]) = (x:) <$> getTup xs -getTup (hnf -> ConN FHNil []) = Just [] -getTup _ = Nothing - -getTTup (hnf -> TyConN FHList [xs]) = getList xs -getTTup _ = Nothing - -getList (hnf -> ConN FCons [x, xs]) = (x:) <$> getList xs -getList (hnf -> ConN FNil []) = Just [] -getList _ = Nothing - -------------------------------------------------------------------------------- reduction {- todo: generate @@ -686,7 +674,7 @@ cstr = f [] f_ [] typ a@Neut{} a' = CstrT typ a a' f_ [] typ a a'@Neut{} = CstrT typ a a' - f_ ns typ a a' = CEmpty $ unlines [ "can not unify", ppShow a, "with", ppShow a' ] + f_ ns typ a a' = CEmpty $ simpleShow $ nest 2 ("can not unify" <$$> DTypeNamespace True (pShow a)) <$$> nest 2 ("with" <$$> DTypeNamespace True (pShow a')) ff _ _ [] = CUnit ff ns tt@(Pi v t _) ((t1, t2'): ts) = t2 (f ns t t1 t2') $ ff ns (appTy tt t1) ts diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs index 303f1156..f65b543d 100644 --- a/src/LambdaCube/Compiler/CoreToIR.hs +++ b/src/LambdaCube/Compiler/CoreToIR.hs @@ -865,7 +865,7 @@ mkLam _ = Nothing mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs) mkCon (ExpTV (I.TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs) -mkCon (ExpTV (I.Neut (I.Fun s (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs) +mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ 0 _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs) mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n]) mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f]) mkCon _ = Nothing @@ -874,7 +874,13 @@ mkApp (ExpTV (I.Neut (I.App_ a b)) et vs) = Just (ExpTV (I.Neut a) t vs, head $ where t = neutType' (mkEnv vs) a mkApp _ = Nothing -mkFunc r@(ExpTV (IFunc (show -> n) def nt xs) ty vs) | all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n +removeRHS 0 (I.RHS x) = Just x +removeRHS n (I.Lam x) | n > 0 = I.Lam <$> removeRHS (n-1) x +removeRHS _ _ = Nothing + +mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) 0 (I.ExpDef def_) nt) xs I.RHS{})) ty vs) + | Just def <- removeRHS (length xs) def_ + , all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n = Just (untick n +++ intercalate "_" (filter (/="TT") $ map (filter isAlphaNum . plainShow) hs), toExp $ I.ET (foldl I.app_ def hs) (foldl I.appTy nt hs), tyOf r, xs') where a +++ [] = a @@ -897,21 +903,10 @@ unLab' (I.RHS x) = unLab' x -- TODO: remove unLab' x = x unFunc' (I.Reduced x) = unFunc' x -- todo: remove? -unFunc' (UFL x) = unFunc' x +unFunc' (I.Neut (I.Fun (I.FunName _ _ I.ExpDef{} _) _ y)) = unFunc' y unFunc' (I.RHS x) = unFunc' x -- TODO: remove unFunc' x = x -pattern UFL y <- I.Neut (I.Fun (I.FunName _ _ I.ExpDef{} _) _ y) - -pattern IFunc n def ty xs <- (mkIFunc -> Just (n, def, ty, xs)) - -mkIFunc (I.Neut (I.Fun (I.FunName n 0 (I.ExpDef def) ty) xs I.RHS{})) | Just def' <- removeRHS (length xs) def = Just (n, def', ty, xs) -mkIFunc _ = Nothing - -removeRHS 0 (I.RHS x) = Just x -removeRHS n (I.Lam x) | n > 0 = I.Lam <$> removeRHS (n-1) x -removeRHS _ _ = Nothing - instance Subst I.Exp ExpTV where subst_ i0 dx x (ExpTV a at vs) = ExpTV (subst_ i0 dx x a) (subst_ i0 dx x at) (zipWith (\i -> subst_ (i0+i) (I.upDB i dx) $ up i x{-todo: review-}) [1..] vs) diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs index 271c678e..074e0299 100644 --- a/src/LambdaCube/Compiler/DesugaredSource.hs +++ b/src/LambdaCube/Compiler/DesugaredSource.hs @@ -235,7 +235,6 @@ instance PShow FName where pShow (CFName _ (SData s)) = pShow s pShow s = maybe (error "show") text' $ lookup s $ map (\(a, b) -> (b, a)) fntable where - text' "Nil" = "[]" text' ":" = pShow ConsName text' s = text s @@ -468,7 +467,10 @@ shApp Hidden a b = DApp a (DAt b) shLam usedVar h a b = shLam_ usedVar h (Just a) b -shLam_ False (BPi Hidden) (Just (DText "'CW" `DApp` a)) b = DFreshName False $ showContext (DUp 0 a) b +simpleFo (DExpand x _) = x +simpleFo x = x + +shLam_ False (BPi Hidden) (Just ((simpleFo -> DText "'CW") `DApp` a)) b = DFreshName False $ showContext (DUp 0 a) b where showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d showContext x (DParContext xs y) = DParContext (DComma x xs) y @@ -500,18 +502,19 @@ shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b showForall s x (DForall s' xs y) | s == s' = DForall s (DSep (InfixR 11) x xs) y showForall s x y = DForall s x y - -- TODO: use other sign instead of (=>) - showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d - showContext x (DParContext xs y) = DParContext (DComma x xs) y - showContext x (DContext xs y) = DParContext (DComma x xs) y - showContext x y = DContext x y + showContext x y = DContext' x y showLam x (DFreshName u d) = DFreshName u $ showLam (DUp 0 x) d showLam x (DLam xs y) = DLam (DSep (InfixR 11) x xs) y showLam x y = DLam x y shLet i a b = DLet' (DLet "=" (blue $ shVar i) $ DUp i a) (DUp i b) -shLet_ a b = DFreshName True $ DLet' (DLet "=" (shVar 0) $ DUp 0 a) b + +showLet x (DFreshName u d) = DFreshName u $ showLet (DUp 0 x) d +showLet x (DLet' xs y) = DLet' (DSemi x xs) y +showLet x y = DLet' x y + +shLet_ a b = DFreshName True $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b -------------------------------------------------------------------------------- statement diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index b511d9c0..1cb528ea 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs @@ -51,17 +51,21 @@ varType err n_ env = f n_ env where mkELet n x xt env = {-(if null vs then id else trace_ $ "mkELet " ++ show (length vs) ++ " " ++ show n)-} term where - vs = sort $ Set.toList $ join grow $ free x <> free xt + vs = sort $ Set.toList $ grow mempty $ free x <> free xt nloc = length vs - fn = FunName (mkFName n) nloc (ExpDef $ addLams 0 vs x) (addPis 0 vs xt) + fn = FunName (mkFName n) nloc (ExpDef $ addLams vs x) (addPis vs xt) term = mkFun fn (Var <$> reverse vs) $ getFix x 0 - addLams l [] x = x - addLams l (v: vs) x = Lam $ rMove v l $ addLams (l+1) vs x + getFix (Lam z) i = Lam $ getFix z (i+1) + getFix (DFun FprimFix _ [t, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f + getFix x _ = x - addPis l [] x = x - addPis l (v: vs) x = Pi Visible (snd $ varType "mkELet" v env) $ rMove v l $ addPis (l+1) vs x + addLams [] x = x + addLams (v: vs) x = Lam $ rMove v 0 $ addLams vs x + + addPis [] x = x + addPis (v: vs) x = Pi Visible (snd $ varType "mkELet" v env) $ rMove v 0 $ addPis vs x grow acc s | Set.null s = acc @@ -69,12 +73,6 @@ mkELet n x xt env = {-(if null vs then id else trace_ $ "mkELet " ++ show (lengt where s' = mconcat (free . snd . flip (varType "mkELet2") env <$> Set.toList s) - getFix (Lam z) i = Lam $ getFix z (i+1) - getFix (DFun FprimFix _ [t, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f - getFix x _ = x - - - instance PShow (CEnv Exp) where pShow = mkDoc False diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs index f9702b94..db31ee2e 100644 --- a/src/LambdaCube/Compiler/Pretty.hs +++ b/src/LambdaCube/Compiler/Pretty.hs @@ -16,6 +16,7 @@ module LambdaCube.Compiler.Pretty import Data.Maybe import Data.String import Data.Char +import Data.Monoid --import qualified Data.Set as Set --import qualified Data.Map as Map import Control.Applicative @@ -153,8 +154,22 @@ renderDoc showVarA (SimpleAtom s) = pure $ SimpleAtom s showVarA (ComplexAtom s i d a) = ComplexAtom s i <$> showVars d <*> showVarA a + getTup (DText "HCons" `DApp` x `DApp` (getTup -> Just xs)) = Just $ x: xs + getTup (DText "HNil") = Just [] + getTup _ = Nothing + + getList (DOp0 ":" _ `DApp` x `DApp` (getList -> Just xs)) = Just $ x: xs + getList (DText "Nil") = Just [] + getList _ = Nothing + + shTick True = DPreOp 20 (SimpleAtom "'") + shTick False = id + namespace :: Bool -> Doc -> Doc namespace tn x = case x of + (getTup -> Just xs) -> shTick tn $ namespace tn $ shTuple xs + (getList -> Just xs) -> shTick tn $ namespace tn $ shList xs + DText "'HList" `DApp` (getList -> Just xs) -> shTick (not tn) $ namespace tn $ shTuple xs DAtom x -> DAtom $ namespaceA x DText "'List" `DApp` x -> namespace tn $ DBracket x DInfix pr' x op y -> DInfix pr' (namespace tn x) (namespaceA op) (namespace tn y) @@ -198,25 +213,39 @@ renderDoc getApps (DApp (getApps -> (n, xs)) x) = (n, x: xs) getApps x = (x, []) + getSemis (DSemi x (getSemis -> (xs, n))) = (x: xs, n) + getSemis x = ([], x) + + getCommas (DComma x (getCommas -> xs)) = x: xs + getCommas x = [x] + render :: Doc -> P.Doc render = snd . render' where render' = \case - DText "Nil" -> rtext "[]" - DText "'Nil" -> rtext "'[]" DAtom x -> renderA x DFormat c x -> second c $ render' x DDocOp f d -> (('\0', '\0'), f $ render <$> d) - DPreOp _ op y -> renderA op <++> render' y + DPreOp _ op y -> renderA' op <++> render' y DSep (InfixR 11) a b -> gr $ render' a <+++> render' b x@DApp{} -> case getApps x of (n, reverse -> xs) -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.nest 2 . P.sep) (unzip $ render' n: (render' <$> xs)) + x@DComma{} -> case getCommas x of + x: xs -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.cat) (unzip $ render' x: (second ("," P.<+>) . render' <$> xs)) + x@DSemi{} -> case getSemis x of + (xs, n) -> ((\xs -> (fst $ head xs, snd $ last xs)) *** P.sep) (unzip $ (second (<> ";") . render' <$> xs) ++ [render' n]) DInfix _ x op y -> gr $ render' x <+++> renderA op <++> render' y + renderA' (SimpleAtom s) = rtext s + renderA' x = gr $ renderA'' x + + renderA'' (SimpleAtom s) = rtext s + renderA'' (ComplexAtom s _ d a) = rtext s <+++> render' d <+++> renderA'' a + renderA (SimpleAtom s) = rtext s renderA (ComplexAtom s _ d a) = rtext s <++> render' d <++> renderA a - gr = second (P.nest 2. P.group) + gr = second (P.nest 2 . P.group) rtext "" = (('\0', '\0'), mempty) rtext s@(h:_) = ((h, last s), P.text s) @@ -224,12 +253,12 @@ renderDoc ((lx, rx), x) <++> ((ly, ry), y) = ((lx, ry), z) where z | sep rx ly = x P.<+> y - | otherwise = x P.<> y + | otherwise = x <> y ((lx, rx), x) <+++> ((ly, ry), y) = ((lx, ry), z) where - z | sep rx ly = x P.<> P.line P.<> y - | otherwise = x P.<> y + z | sep rx ly = x <> P.line <> y + | otherwise = x <> y sep x y | x == '\0' || y == '\0' = False @@ -291,6 +320,7 @@ infixl 4 `DApp` pattern DAt x = DGlue (InfixR 20) (DText "@") x pattern DApp x y = DSep (InfixL 10) x y +pattern DSemi x y = DOp ";" (InfixR (-19)) x y pattern DArr_ s x y = DOp s (InfixR (-1)) x y -- -> => . pattern DCstr x y = DOp "~" (Infix (-2)) x y pattern DAnn x y = DOp "::" (Infix (-3)) x (DTypeNamespace True y) @@ -317,12 +347,16 @@ shTuple [] = "()" shTuple [x] = DParen $ DParen x shTuple xs = DParen $ foldr1 DComma xs +shList [] = "[]" +shList xs = DBracket $ foldr1 DComma xs + shAnn = DAnn shArr = DArr pattern DForall s vs e = DArr_ s (DPreOp 10 (SimpleAtom "forall") vs) e +pattern DContext' vs e = DArr_ "->" (DAt vs) e pattern DContext vs e = DArr_ "=>" vs e pattern DParContext vs e = DContext (DParen vs) e pattern DLam vs e = DPreOp (-10) (ComplexAtom "\\" 11 vs (SimpleAtom "->")) e -- cgit v1.2.3