diff options
author | Péter Diviánszky <divipp@gmail.com> | 2016-01-26 12:01:56 +0100 |
---|---|---|
committer | Péter Diviánszky <divipp@gmail.com> | 2016-01-26 12:01:56 +0100 |
commit | 723e6a391eb5a93036048c74ac94a17fca12c02a (patch) | |
tree | b4000efa9ada7e734d08e7e645062c7855ae4c12 /src | |
parent | 44c351c677c3361271862b461a9ab10220575ea0 (diff) |
refactoring: move ESC handling to Pretty.hs
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler/Driver.hs | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Infer.hs | 86 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Pretty.hs | 45 |
3 files changed, 71 insertions, 62 deletions
diff --git a/src/LambdaCube/Compiler/Driver.hs b/src/LambdaCube/Compiler/Driver.hs index 6d54393c..e6e6cd76 100644 --- a/src/LambdaCube/Compiler/Driver.hs +++ b/src/LambdaCube/Compiler/Driver.hs | |||
@@ -42,7 +42,7 @@ import qualified Data.Text.IO as TIO | |||
42 | 42 | ||
43 | import IR | 43 | import IR |
44 | import LambdaCube.Compiler.Pretty hiding ((</>)) | 44 | import LambdaCube.Compiler.Pretty hiding ((</>)) |
45 | import LambdaCube.Compiler.Infer (Infos, listInfos, ErrorMsg(..), showRange, PolyEnv(..), Export(..), ModuleR(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_, removeEscs, ImportItems (..)) | 45 | import LambdaCube.Compiler.Infer (Infos, listInfos, ErrorMsg(..), showRange, PolyEnv(..), Export(..), ModuleR(..), ErrorT, throwErrorTCM, parseLC, joinPolyEnvs, filterPolyEnv, inference_, ImportItems (..)) |
46 | import LambdaCube.Compiler.CoreToIR | 46 | import LambdaCube.Compiler.CoreToIR |
47 | 47 | ||
48 | type EName = String | 48 | type EName = String |
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs index b3c0fbf6..9aa53226 100644 --- a/src/LambdaCube/Compiler/Infer.hs +++ b/src/LambdaCube/Compiler/Infer.hs | |||
@@ -10,12 +10,13 @@ | |||
10 | {-# LANGUAGE RecursiveDo #-} | 10 | {-# LANGUAGE RecursiveDo #-} |
11 | {-# LANGUAGE RankNTypes #-} | 11 | {-# LANGUAGE RankNTypes #-} |
12 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} | 12 | {-# LANGUAGE GeneralizedNewtypeDeriving #-} |
13 | {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-} -- TODO: remove | ||
13 | {-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove | 14 | {-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove |
14 | {-# OPTIONS_GHC -fno-warn-orphans #-} -- instance NFData SourcePos | 15 | {-# OPTIONS_GHC -fno-warn-orphans #-} -- instance NFData SourcePos |
15 | module LambdaCube.Compiler.Infer | 16 | module LambdaCube.Compiler.Infer |
16 | ( Binder (..), SName, Lit(..), Visibility(..), FunName(..), CaseFunName(..), ConName(..), TyConName(..), Export(..), ModuleR(..) | 17 | ( Binder (..), SName, Lit(..), Visibility(..), FunName(..), CaseFunName(..), ConName(..), TyConName(..), Export(..), ModuleR(..) |
17 | , Exp (..), GlobalEnv | 18 | , Exp (..), GlobalEnv |
18 | , pattern Var, pattern Fun, pattern CaseFun, pattern TyCaseFun, pattern App, pattern FunN, pattern ConN, pattern PMLabel, pattern FixLabel | 19 | , pattern Var, pattern Fun, pattern CaseFun, pattern TyCaseFun, pattern App, pattern PMLabel, pattern FixLabel |
19 | , pattern Con, pattern TyCon, pattern Lam, pattern Pi | 20 | , pattern Con, pattern TyCon, pattern Lam, pattern Pi |
20 | , downE | 21 | , downE |
21 | , litType | 22 | , litType |
@@ -52,8 +53,6 @@ import Text.Parsec.Pos | |||
52 | import Text.Parsec.Indentation hiding (Any) | 53 | import Text.Parsec.Indentation hiding (Any) |
53 | import Text.Parsec.Indentation.Char | 54 | import Text.Parsec.Indentation.Char |
54 | 55 | ||
55 | import Debug.Trace | ||
56 | |||
57 | import qualified LambdaCube.Compiler.Pretty as P | 56 | import qualified LambdaCube.Compiler.Pretty as P |
58 | import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) | 57 | import LambdaCube.Compiler.Pretty hiding (Doc, braces, parens) |
59 | import LambdaCube.Compiler.Token | 58 | import LambdaCube.Compiler.Token |
@@ -62,6 +61,10 @@ import LambdaCube.Compiler.Token | |||
62 | 61 | ||
63 | (<&>) = flip (<$>) | 62 | (<&>) = flip (<$>) |
64 | 63 | ||
64 | dropNth i xs = take i xs ++ drop (i+1) xs | ||
65 | iterateN n f e = iterate f e !! n | ||
66 | holes xs = [(as, x, bs) | (as, x: bs) <- zip (inits xs) (tails xs)] | ||
67 | mtrace s = trace_ s $ return () | ||
65 | 68 | ||
66 | -------------------------------------------------------------------------------- source data | 69 | -------------------------------------------------------------------------------- source data |
67 | 70 | ||
@@ -140,7 +143,7 @@ instance Monoid SI where | |||
140 | 143 | ||
141 | data SExp | 144 | data SExp |
142 | = SGlobal SIName | 145 | = SGlobal SIName |
143 | | SBind SI Binder SIName{-parameter's name-} SExp SExp | 146 | | SBind SI Binder (SData SIName{-parameter's name-}) SExp SExp |
144 | | SApp SI Visibility SExp SExp | 147 | | SApp SI Visibility SExp SExp |
145 | | SLet LI SExp SExp -- let x = e in f --> SLet e f{-x is Var 0-} | 148 | | SLet LI SExp SExp -- let x = e in f --> SLet e f{-x is Var 0-} |
146 | | SVar_ (SData SIName) !Int | 149 | | SVar_ (SData SIName) !Int |
@@ -171,22 +174,20 @@ data Visibility = Hidden | Visible | |||
171 | sLit a = STyped mempty (ELit a, litType a) | 174 | sLit a = STyped mempty (ELit a, litType a) |
172 | pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined" | 175 | pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined" |
173 | pattern SType <- STyped _ (TType, TType) where SType = STyped (debugSI "pattern SType") (TType, TType) | 176 | pattern SType <- STyped _ (TType, TType) where SType = STyped (debugSI "pattern SType") (TType, TType) |
174 | pattern SPi h a b <- SBind _ (BPi h) _ a b where SPi h a b = sBind (BPi h) (debugSI "patternSPi2", "pattern_spi_name") a b | 177 | pattern SPi h a b <- SBind _ (BPi h) _ a b where SPi h a b = sBind (BPi h) (SData (debugSI "patternSPi2", "pattern_spi_name")) a b |
175 | pattern SLam h a b <- SBind _ (BLam h) _ a b where SLam h a b = sBind (BLam h) (debugSI "patternSLam2", "pattern_slam_name") a b | 178 | pattern SLam h a b <- SBind _ (BLam h) _ a b where SLam h a b = sBind (BLam h) (SData (debugSI "patternSLam2", "pattern_slam_name")) a b |
176 | pattern Wildcard t <- SBind _ BMeta _ t (SVar _ 0) where Wildcard t = sBind BMeta (debugSI "pattern Wildcard2", "pattern_wildcard_name") t (SVar (debugSI "pattern Wildcard2", ".wc") 0) | 179 | pattern Wildcard t <- SBind _ BMeta _ t (SVar _ 0) where Wildcard t = sBind BMeta (SData (debugSI "pattern Wildcard2", "pattern_wildcard_name")) t (SVar (debugSI "pattern Wildcard2", ".wc") 0) |
177 | pattern Wildcard_ si t <- SBind _ BMeta _ t (SVar (si, _) 0) | 180 | pattern Wildcard_ si t <- SBind _ BMeta _ t (SVar (si, _) 0) |
178 | pattern SAppH a b <- SApp _ Hidden a b where SAppH a b = sApp Hidden a b | 181 | pattern SAppH a b <- SApp _ Hidden a b where SAppH a b = sApp Hidden a b |
179 | pattern SAppV a b <- SApp _ Visible a b where SAppV a b = sApp Visible a b | 182 | pattern SAppV a b <- SApp _ Visible a b where SAppV a b = sApp Visible a b |
183 | pattern SAppV2 f a b = f `SAppV` a `SAppV` b | ||
180 | pattern SLamV a = SLam Visible (Wildcard SType) a | 184 | pattern SLamV a = SLam Visible (Wildcard SType) a |
181 | pattern SAnn a t <- STyped _ (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a -- a :: t ~~> id t a | 185 | pattern SAnn a t <- STyped _ (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a -- a :: t ~~> id t a |
182 | where SAnn a t = STyped (debugSI "pattern SAnn") (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a | 186 | where SAnn a t = STyped (debugSI "pattern SAnn") (Lam Visible TType (Lam Visible (Var 0) (Var 0)), TType :~> Var 0 :~> Var 1) `SAppV` t `SAppV` a |
183 | pattern TyType a <- STyped _ (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a | 187 | pattern TyType a <- STyped _ (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a |
184 | where TyType a = STyped mempty (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a | 188 | where TyType a = STyped mempty (Lam Visible TType (Var 0), TType :~> TType) `SAppV` a |
185 | -- same as (a :: TType) -- a :: TType ~~> (\(x :: TType) -> x) a | 189 | -- same as (a :: TType) -- a :: TType ~~> (\(x :: TType) -> x) a |
186 | pattern SCstr a b = SBuiltin "'EqCT" `SAppV` SType `SAppV` a `SAppV` b -- a ~ b | ||
187 | pattern SParEval a b = SBuiltin "parEval" `SAppV` Wildcard SType `SAppV` a `SAppV` b | ||
188 | pattern SLabelEnd a = SBuiltin "labelend" `SAppV` a | 190 | pattern SLabelEnd a = SBuiltin "labelend" `SAppV` a |
189 | pattern ST2 a b = SBuiltin "'T2" `SAppV` a `SAppV` b | ||
190 | 191 | ||
191 | pattern SBuiltin s <- SGlobal (_, s) where SBuiltin s = SGlobal (debugSI $ "builtin " ++ s, s) | 192 | pattern SBuiltin s <- SGlobal (_, s) where SBuiltin s = SGlobal (debugSI $ "builtin " ++ s, s) |
192 | 193 | ||
@@ -311,8 +312,8 @@ pattern ParEval t a b = TFun "parEval" (TType :~> Var 0 :~> Var 1 :~> Var 2) [t, | |||
311 | pattern Undef t = TFun "undefined" (Pi Hidden TType (Var 0)) [t] | 312 | pattern Undef t = TFun "undefined" (Pi Hidden TType (Var 0)) [t] |
312 | 313 | ||
313 | pattern ConN s a <- Con (ConName s _ _ _) a | 314 | pattern ConN s a <- Con (ConName s _ _ _) a |
314 | pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a | ||
315 | pattern TCon s i t a <- Con (ConName s _ i t) a where TCon s i t a = Con (ConName s Nothing i t) a -- todo: don't match on type | 315 | pattern TCon s i t a <- Con (ConName s _ i t) a where TCon s i t a = Con (ConName s Nothing i t) a -- todo: don't match on type |
316 | pattern TyConN s a <- TyCon (TyConName s _ _ _ _ _) a | ||
316 | pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ error "TTyCon") a | 317 | pattern TTyCon s t a <- TyCon (TyConName s _ _ t _ _) a where TTyCon s t a = TyCon (TyConName s Nothing (error "todo: inum") t (error "todo: tcn cons 2") $ error "TTyCon") a |
317 | pattern TTyCon0 s <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = TyCon (TyConName s Nothing (error "todo: inum2") TType (error "todo: tcn cons 3") $ error "TTyCon0") [] | 318 | pattern TTyCon0 s <- TyCon (TyConName s _ _ TType _ _) [] where TTyCon0 s = TyCon (TyConName s Nothing (error "todo: inum2") TType (error "todo: tcn cons 3") $ error "TTyCon0") [] |
318 | pattern Sigma a b <- TyConN "Sigma" [a, Lam' b] where Sigma a b = TTyCon "Sigma" (error "sigmatype") [a, Lam Visible a{-todo: don't duplicate-} b] | 319 | pattern Sigma a b <- TyConN "Sigma" [a, Lam' b] where Sigma a b = TTyCon "Sigma" (error "sigmatype") [a, Lam Visible a{-todo: don't duplicate-} b] |
@@ -334,8 +335,8 @@ pattern Succ n = TCon "Succ" 1 (TNat :~> TNat) [n] | |||
334 | --pattern TVec a b = TTyCon "'Vec" (TNat :~> TType :~> TType) [a, b] | 335 | --pattern TVec a b = TTyCon "'Vec" (TNat :~> TType :~> TType) [a, b] |
335 | pattern TVec a b = TTyCon "'VecS" (TType :~> TNat :~> TType) [b, a] | 336 | pattern TVec a b = TTyCon "'VecS" (TType :~> TNat :~> TType) [b, a] |
336 | pattern TFrameBuffer a b = TTyCon "'FrameBuffer" (TNat :~> TType :~> TType) [a, b] | 337 | pattern TFrameBuffer a b = TTyCon "'FrameBuffer" (TNat :~> TType :~> TType) [a, b] |
337 | pattern Tuple2 a b c d = TCon "Tuple2" 0 Tuple2Type [a, b, c, d] | 338 | --pattern Tuple2 a b c d = TCon "Tuple2" 0 Tuple2Type [a, b, c, d] |
338 | pattern Tuple0 = TCon "Tuple0" 0 TTuple0 [] | 339 | --pattern Tuple0 = TCon "Tuple0" 0 TTuple0 [] |
339 | pattern CSplit a b c <- FunN "'Split" [a, b, c] | 340 | pattern CSplit a b c <- FunN "'Split" [a, b, c] |
340 | pattern TInterpolated a = TTyCon "'Interpolated" (TType :~> TType) [a] | 341 | pattern TInterpolated a = TTyCon "'Interpolated" (TType :~> TType) [a] |
341 | 342 | ||
@@ -1818,7 +1819,7 @@ compileFunAlts par ulend lend ds xs = asks fst >>= \ge -> case xs of | |||
1818 | [Instance{}] -> return [] | 1819 | [Instance{}] -> return [] |
1819 | [Class n ps ms] -> compileFunAlts' SLabelEnd $ | 1820 | [Class n ps ms] -> compileFunAlts' SLabelEnd $ |
1820 | [ TypeAnn n $ foldr (SPi Visible) SType ps ] | 1821 | [ TypeAnn n $ foldr (SPi Visible) SType ps ] |
1821 | ++ [ FunAlt n (map noTA ps) $ Right $ foldr ST2 (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] | 1822 | ++ [ FunAlt n (map noTA ps) $ Right $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'Unit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ] |
1822 | ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] | 1823 | ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")] |
1823 | ++ concat | 1824 | ++ concat |
1824 | [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ upS t) | 1825 | [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ upS t) |
@@ -1856,7 +1857,7 @@ compileFunAlts par ulend lend ds xs = asks fst >>= \ge -> case xs of | |||
1856 | noTA x = ((Visible, Wildcard SType), x) | 1857 | noTA x = ((Visible, Wildcard SType), x) |
1857 | 1858 | ||
1858 | compileGuardTrees False ulend lend ge alts = compileGuardTree ulend lend ge $ Alts alts | 1859 | compileGuardTrees False ulend lend ge alts = compileGuardTree ulend lend ge $ Alts alts |
1859 | compileGuardTrees True ulend lend ge alts = foldr1 SParEval $ compileGuardTree ulend lend ge <$> alts | 1860 | compileGuardTrees True ulend lend ge alts = foldr1 (SAppV2 $ SBuiltin "parEval" `SAppV` Wildcard SType) $ compileGuardTree ulend lend ge <$> alts |
1860 | 1861 | ||
1861 | parseDefs lend = many parseDef >>= compileFunAlts' lend . concat | 1862 | parseDefs lend = many parseDef >>= compileFunAlts' lend . concat |
1862 | 1863 | ||
@@ -1902,8 +1903,8 @@ parseDef = | |||
1902 | (nps, ts) <- telescope (Just SType) | 1903 | (nps, ts) <- telescope (Just SType) |
1903 | t <- dbf' nps <$> parseType (Just SType) | 1904 | t <- dbf' nps <$> parseType (Just SType) |
1904 | option {-open type family-}[TypeFamily x ts t] $ do | 1905 | option {-open type family-}[TypeFamily x ts t] $ do |
1905 | cs <- reserved "where" *> localIndentation Ge (localAbsoluteIndentation $ many $ | 1906 | reserved "where" |
1906 | funAltDef (upperCase >>= \x' -> guard (snd x == x') >> return x')) | 1907 | cs <- localIndentation Ge $ localAbsoluteIndentation $ many $ funAltDef $ mfilter (== snd x) upperCase |
1907 | -- closed type family desugared here | 1908 | -- closed type family desugared here |
1908 | compileFunAlts False id SLabelEnd [TypeAnn x $ addParamsS ts t] cs | 1909 | compileFunAlts False id SLabelEnd [TypeAnn x $ addParamsS ts t] cs |
1909 | <|> do indentation (reserved "type") $ typeNS $ do | 1910 | <|> do indentation (reserved "type") $ typeNS $ do |
@@ -2001,7 +2002,7 @@ parseTerm prec = withRange setSI $ case prec of | |||
2001 | <|> asks (\ge -> compileGuardTree id id (fst ge) . Alts) <*> parseSomeGuards (const True) | 2002 | <|> asks (\ge -> compileGuardTree id id (fst ge) . Alts) <*> parseSomeGuards (const True) |
2002 | <|> do t <- parseTerm PrecEq | 2003 | <|> do t <- parseTerm PrecEq |
2003 | option t $ mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam | 2004 | option t $ mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> parseTTerm PrecLam |
2004 | PrecEq -> parseTerm PrecAnn >>= \t -> option t $ SCstr t <$ reservedOp "~" <*> parseTTerm PrecAnn | 2005 | PrecEq -> parseTerm PrecAnn >>= \t -> option t $ SAppV2 (SBuiltin "'EqCT" `SAppV` SType) t <$ reservedOp "~" <*> parseTTerm PrecAnn |
2005 | PrecAnn -> parseTerm PrecOp >>= \t -> option t $ SAnn t <$> parseType Nothing | 2006 | PrecAnn -> parseTerm PrecOp >>= \t -> option t $ SAnn t <$> parseType Nothing |
2006 | PrecOp -> asks (calculatePrecs . fst) <*> p' where | 2007 | PrecOp -> asks (calculatePrecs . fst) <*> p' where |
2007 | p' = getNS (\ns -> (\si (t, xs) -> (mkNat ns 0, (SBuiltin "-", t): xs)) `withRange` (reservedOp "-" *> p_)) | 2008 | p' = getNS (\ns -> (\si (t, xs) -> (mkNat ns 0, (SBuiltin "-", t): xs)) `withRange` (reservedOp "-" *> p_)) |
@@ -2032,7 +2033,7 @@ parseTerm prec = withRange setSI $ case prec of | |||
2032 | <|> mkDotDot <$> try "dotdot expression" (reservedOp "[" *> parseTerm PrecLam <* reservedOp ".." ) <*> parseTerm PrecLam <* reservedOp "]" | 2033 | <|> mkDotDot <$> try "dotdot expression" (reservedOp "[" *> parseTerm PrecLam <* reservedOp ".." ) <*> parseTerm PrecLam <* reservedOp "]" |
2033 | <|> listCompr | 2034 | <|> listCompr |
2034 | <|> getNS' mkList <*> brackets (commaSep $ parseTerm PrecLam) | 2035 | <|> getNS' mkList <*> brackets (commaSep $ parseTerm PrecLam) |
2035 | <|> mkLeftSection <$> try "left section"{-todo: better try-} (parens $ (,) <$> withSI (guardM (/= "-") operatorT) <*> parseTerm PrecLam) | 2036 | <|> mkLeftSection <$> try "left section"{-todo: better try-} (parens $ (,) <$> withSI (mfilter (/= "-") operatorT) <*> parseTerm PrecLam) |
2036 | <|> mkRightSection <$> try "right section"{-todo: better try!-} (parens $ (,) <$> parseTerm PrecApp <*> withSI operatorT) | 2037 | <|> mkRightSection <$> try "right section"{-todo: better try!-} (parens $ (,) <$> parseTerm PrecApp <*> withSI operatorT) |
2037 | <|> getNS' mkTuple <*> parens (commaSep $ parseTerm PrecLam) | 2038 | <|> getNS' mkTuple <*> parens (commaSep $ parseTerm PrecLam) |
2038 | <|> mkRecord <$> braces (commaSep $ (,) <$> lowerCase <* colon <*> parseTerm PrecLam) | 2039 | <|> mkRecord <$> braces (commaSep $ (,) <$> lowerCase <* colon <*> parseTerm PrecLam) |
@@ -2273,7 +2274,7 @@ instance SourceInfo Pat where | |||
2273 | instance SourceInfo SExp where | 2274 | instance SourceInfo SExp where |
2274 | sourceInfo = \case | 2275 | sourceInfo = \case |
2275 | SGlobal (si, _) -> si | 2276 | SGlobal (si, _) -> si |
2276 | SBind si _ (si', _) e1 e2 -> si | 2277 | SBind si _ _ e1 e2 -> si |
2277 | SApp si _ e1 e2 -> si | 2278 | SApp si _ e1 e2 -> si |
2278 | SLet _ e1 e2 -> sourceInfo e1 <> sourceInfo e2 | 2279 | SLet _ e1 e2 -> sourceInfo e1 <> sourceInfo e2 |
2279 | SVar (si, _) _ -> si | 2280 | SVar (si, _) _ -> si |
@@ -2647,6 +2648,9 @@ shCstr x y = prec PrecEq $ lpar x <> " ~ " <> rpar y | |||
2647 | shLet' x y | isAtom x && isAtom y = shAtom' $ str x <> ":=" <> str y | 2648 | shLet' x y | isAtom x && isAtom y = shAtom' $ str x <> ":=" <> str y |
2648 | shLet' x y = prec PrecLet $ lpar x <> " := " <> rpar y | 2649 | shLet' x y = prec PrecLet $ lpar x <> " := " <> rpar y |
2649 | shLam' x y | PrecLam <- getPrec y = prec PrecLam $ "\\" <> lpar x <> " " <> pure (dropC $ str y) | 2650 | shLam' x y | PrecLam <- getPrec y = prec PrecLam $ "\\" <> lpar x <> " " <> pure (dropC $ str y) |
2651 | where | ||
2652 | dropC (ESC s (dropC -> x)) = ESC s x | ||
2653 | dropC (x: xs) = xs | ||
2650 | shLam' x y | isAtom x && isAtom y = shAtom' $ "\\" <> str x <> "->" <> str y | 2654 | shLam' x y | isAtom x && isAtom y = shAtom' $ "\\" <> str x <> "->" <> str y |
2651 | shLam' x y = prec PrecLam $ "\\" <> lpar x <> " -> " <> rpar y | 2655 | shLam' x y = prec PrecLam $ "\\" <> lpar x <> " -> " <> rpar y |
2652 | brace s = shAtom $ "{" <> str s <> "}" | 2656 | brace s = shAtom $ "{" <> str s <> "}" |
@@ -2654,43 +2658,10 @@ cpar s | isAtom' s = s -- TODO: replace with lpar, rpar | |||
2654 | cpar s = shAtom $ par True $ str s | 2658 | cpar s = shAtom $ par True $ str s |
2655 | epar = fmap underlined | 2659 | epar = fmap underlined |
2656 | 2660 | ||
2657 | dropC (ESC s (dropC -> x)) = ESC s x | 2661 | instance IsString (Prec -> String) where fromString = const |
2658 | dropC (x: xs) = xs | ||
2659 | |||
2660 | pattern ESC a b <- (splitESC -> Just (a, b)) where ESC a b | 'm' `notElem` a = "\ESC[" ++ a ++ "m" ++ b | ||
2661 | 2662 | ||
2662 | splitESC ('\ESC':'[': (span (/='m') -> (a, c: b))) | c == 'm' = Just (a, b) | ||
2663 | splitESC _ = Nothing | ||
2664 | 2663 | ||
2665 | instance IsString (Prec -> String) where fromString = const | ||
2666 | 2664 | ||
2667 | inGreen = withEsc 32 | ||
2668 | inBlue = withEsc 34 | ||
2669 | inRed = withEsc 31 | ||
2670 | underlined = withEsc 47 | ||
2671 | withEsc i s = ESC (show i) $ s ++ ESC "" "" | ||
2672 | |||
2673 | removeEscs (ESC _ cs) = removeEscs cs | ||
2674 | removeEscs (c: cs) = c: removeEscs cs | ||
2675 | removeEscs [] = [] | ||
2676 | |||
2677 | correctEscs = (++ "\ESC[K") . f ["39","49"] where | ||
2678 | f acc (ESC i@(_:_) cs) = ESC i $ f (i:acc) cs | ||
2679 | f (a: acc) (ESC "" cs) = ESC (compOld (cType a) acc) $ f acc cs | ||
2680 | f acc (c: cs) = c: f acc cs | ||
2681 | f acc [] = [] | ||
2682 | |||
2683 | compOld x xs = head $ filter ((== x) . cType) xs | ||
2684 | |||
2685 | cType n | ||
2686 | | "30" <= n && n <= "39" = 0 | ||
2687 | | "40" <= n && n <= "49" = 1 | ||
2688 | | otherwise = 2 | ||
2689 | |||
2690 | putStrLn_ = putStrLn . correctEscs | ||
2691 | error_ = error . correctEscs | ||
2692 | trace_ = trace . correctEscs | ||
2693 | throwError_ = throwError . correctEscs | ||
2694 | traceD x = if debug then trace_ x else id | 2665 | traceD x = if debug then trace_ x else id |
2695 | 2666 | ||
2696 | -------------------------------------------------------------------------------- main | 2667 | -------------------------------------------------------------------------------- main |
@@ -2736,11 +2707,4 @@ inference_ (PolyEnv pe is) m = ff $ runWriter $ runExceptT $ mdo | |||
2736 | tell is | 2707 | tell is |
2737 | return $ PolyEnv ge is | 2708 | return $ PolyEnv ge is |
2738 | 2709 | ||
2739 | -------------------------------------------------------------------------------- utils | ||
2740 | |||
2741 | dropNth i xs = take i xs ++ drop (i+1) xs | ||
2742 | iterateN n f e = iterate f e !! n | ||
2743 | holes xs = [(as, x, bs) | (as, x: bs) <- zip (inits xs) (tails xs)] | ||
2744 | mtrace s = trace_ s $ return () | ||
2745 | guardM p m = m >>= \x -> if p x then return x else fail "guardM" | ||
2746 | 2710 | ||
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs index 416e844d..5eee2067 100644 --- a/src/LambdaCube/Compiler/Pretty.hs +++ b/src/LambdaCube/Compiler/Pretty.hs | |||
@@ -1,6 +1,9 @@ | |||
1 | {-# LANGUAGE OverloadedStrings #-} | 1 | {-# LANGUAGE OverloadedStrings #-} |
2 | {-# LANGUAGE NoMonomorphismRestriction #-} | 2 | {-# LANGUAGE NoMonomorphismRestriction #-} |
3 | {-# LANGUAGE LambdaCase #-} | 3 | {-# LANGUAGE LambdaCase #-} |
4 | {-# LANGUAGE PatternSynonyms #-} | ||
5 | {-# LANGUAGE ViewPatterns #-} | ||
6 | {-# LANGUAGE FlexibleContexts #-} | ||
4 | module LambdaCube.Compiler.Pretty | 7 | module LambdaCube.Compiler.Pretty |
5 | ( module LambdaCube.Compiler.Pretty | 8 | ( module LambdaCube.Compiler.Pretty |
6 | , Doc | 9 | , Doc |
@@ -15,6 +18,8 @@ import Data.Set (Set) | |||
15 | import qualified Data.Set as Set | 18 | import qualified Data.Set as Set |
16 | import Data.Map (Map) | 19 | import Data.Map (Map) |
17 | import qualified Data.Map as Map | 20 | import qualified Data.Map as Map |
21 | import Control.Monad.Except | ||
22 | import Debug.Trace | ||
18 | 23 | ||
19 | import Text.PrettyPrint.Compact | 24 | import Text.PrettyPrint.Compact |
20 | 25 | ||
@@ -98,3 +103,43 @@ instance PShow Integer where pShowPrec _ = integer | |||
98 | instance PShow Double where pShowPrec _ = double | 103 | instance PShow Double where pShowPrec _ = double |
99 | instance PShow Char where pShowPrec _ = char | 104 | instance PShow Char where pShowPrec _ = char |
100 | instance PShow () where pShowPrec _ _ = "()" | 105 | instance PShow () where pShowPrec _ _ = "()" |
106 | |||
107 | |||
108 | -------------------------------------------------------------------------------- ANSI terminal colors | ||
109 | |||
110 | pattern ESC a b <- (splitESC -> Just (a, b)) where ESC a b | 'm' `notElem` a = "\ESC[" ++ a ++ "m" ++ b | ||
111 | |||
112 | splitESC ('\ESC':'[': (span (/='m') -> (a, c: b))) | c == 'm' = Just (a, b) | ||
113 | splitESC _ = Nothing | ||
114 | |||
115 | withEsc i s = ESC (show i) $ s ++ ESC "" "" | ||
116 | |||
117 | inGreen = withEsc 32 | ||
118 | inBlue = withEsc 34 | ||
119 | inRed = withEsc 31 | ||
120 | underlined = withEsc 47 | ||
121 | |||
122 | removeEscs :: String -> String | ||
123 | removeEscs (ESC _ cs) = removeEscs cs | ||
124 | removeEscs (c: cs) = c: removeEscs cs | ||
125 | removeEscs [] = [] | ||
126 | |||
127 | correctEscs :: String -> String | ||
128 | correctEscs = (++ "\ESC[K") . f ["39","49"] where | ||
129 | f acc (ESC i@(_:_) cs) = ESC i $ f (i:acc) cs | ||
130 | f (a: acc) (ESC "" cs) = ESC (compOld (cType a) acc) $ f acc cs | ||
131 | f acc (c: cs) = c: f acc cs | ||
132 | f acc [] = [] | ||
133 | |||
134 | compOld x xs = head $ filter ((== x) . cType) xs | ||
135 | |||
136 | cType n | ||
137 | | "30" <= n && n <= "39" = 0 | ||
138 | | "40" <= n && n <= "49" = 1 | ||
139 | | otherwise = 2 | ||
140 | |||
141 | putStrLn_ = putStrLn . correctEscs | ||
142 | error_ = error . correctEscs | ||
143 | trace_ = trace . correctEscs | ||
144 | throwError_ = throwError . correctEscs | ||
145 | |||