git.iko.soy/elk
on 4e7ef5f help sign in
elk/compiler/Type/Type.hs
330 lines 9.4 kB history raw
1module Type.Type where
3import qualified Data.List as List
4import qualified Data.Map as Map
5import qualified Data.UnionFind.IO as UF
6import Type.PrettyPrint
7import Text.PrettyPrint as P
8import System.IO.Unsafe
9import Control.Applicative ((<$>),(<*>))
10import Control.Monad.State
11import Data.Traversable (traverse)
12import SourceSyntax.Helpers (isTuple)
13import qualified SourceSyntax.Type as Src
15data Term1 a
16 = App1 a a
17 | Fun1 a a
18 | Var1 a
19 | EmptyRecord1
20 | Record1 (Map.Map String [a]) a
21 deriving Show
23data TermN a
24 = VarN a
25 | TermN (Term1 (TermN a))
26 deriving Show
28record fs rec = TermN (Record1 fs rec)
30type Type = TermN Variable
31type Variable = UF.Point Descriptor
33type SchemeName = String
34type TypeName = String
36data Constraint a b
37 = CTrue
38 | CSaveEnv
39 | CEqual a a
40 | CAnd [Constraint a b]
41 | CLet [Scheme a b] (Constraint a b)
42 | CInstance SchemeName a
43 deriving Show
45data Scheme a b = Scheme {
46 rigidQuantifiers :: [b],
47 flexibleQuantifiers :: [b],
48 constraint :: Constraint a b,
49 header :: Map.Map String a
50} deriving Show
52type TypeConstraint = Constraint Type Variable
53type TypeScheme = Scheme Type Variable
55monoscheme headers = Scheme [] [] CTrue headers
57infixl 8 /\
59(/\) :: Constraint a b -> Constraint a b -> Constraint a b
60a /\ CTrue = a
61CTrue /\ b = b
62a /\ b = CAnd [a,b]
64(===) :: Type -> Type -> TypeConstraint
65(===) = CEqual
67(<?) :: SchemeName -> Type -> TypeConstraint
68x <? t = CInstance x t
70infixr 9 ==>
71(==>) :: Type -> Type -> Type
72a ==> b = TermN (Fun1 a b)
74f <| a = TermN (App1 f a)
76data Descriptor = Descriptor {
77 structure :: Maybe (Term1 Variable),
78 rank :: Int,
79 flex :: Flex,
80 name :: Maybe TypeName,
81 copy :: Maybe Variable,
82 mark :: Int
83} deriving Show
85noRank = -1
86outermostRank = 0 :: Int
88noMark = 0
89initialMark = 1
91data Flex = Rigid | Flexible | Constant | IsIn SuperType
92 deriving (Show, Eq)
94data SuperType = Number | Comparable | Appendable
95 deriving (Show, Eq)
97number = namedVar (IsIn Number) "number"
98comparable = namedVar (IsIn Comparable) "comparable"
99appendable = namedVar (IsIn Appendable) "appendable"
101namedVar flex name = UF.fresh $ Descriptor {
102 structure = Nothing,
103 rank = noRank,
104 flex = flex,
105 name = Just name,
106 copy = Nothing,
107 mark = noMark
108 }
110flexibleVar = UF.fresh $ Descriptor {
111 structure = Nothing,
112 rank = noRank,
113 flex = Flexible,
114 name = Nothing,
115 copy = Nothing,
116 mark = noMark
117 }
119rigidVar = UF.fresh $ Descriptor {
120 structure = Nothing,
121 rank = noRank,
122 flex = Rigid,
123 name = Nothing,
124 copy = Nothing,
125 mark = noMark
126 }
128-- ex qs constraint == exists qs. constraint
129ex :: [Variable] -> TypeConstraint -> TypeConstraint
130ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
132-- fl qs constraint == forall qs. constraint
133fl :: [Variable] -> TypeConstraint -> TypeConstraint
134fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
136exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
137exists f = do
138 v <- flexibleVar
139 ex [v] <$> f (VarN v)
142instance Show a => Show (UF.Point a) where
143 show point = unsafePerformIO $ fmap show (UF.descriptor point)
146instance PrettyType a => PrettyType (UF.Point a) where
147 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
150instance PrettyType a => PrettyType (Term1 a) where
151 pretty when term =
152 let prty = pretty Never in
153 case term of
154 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
155 | otherwise -> parensIf needed (px <+> pretty App x)
156 where
157 px = prty f
158 needed = case when of
159 App -> True
160 _ -> False
162 Fun1 arg body ->
163 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
164 where
165 needed = case when of
166 Never -> False
167 _ -> True
169 Var1 x -> prty x
171 EmptyRecord1 -> P.braces P.empty
173 Record1 fields ext ->
174 P.braces (prty ext <+> P.text "|" <+> commaSep prettyFields)
175 where
176 mkPretty f t = P.text f <+> P.text ":" <+> prty t
177 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
180instance PrettyType a => PrettyType (TermN a) where
181 pretty when term =
182 case term of
183 VarN x -> pretty when x
184 TermN t1 -> pretty when t1
187instance PrettyType Descriptor where
188 pretty when desc =
189 case (structure desc, name desc) of
190 (Just term, _) -> pretty when term
191 (_, Just name) -> if not (isTuple name) then P.text name else
192 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
193 _ -> P.text "?"
196instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
197 pretty _ constraint =
198 let prty = pretty Never in
199 case constraint of
200 CTrue -> P.text "True"
201 CSaveEnv -> P.text "SaveTheEnvironment!!!"
202 CEqual a b -> prty a <+> P.text "=" <+> prty b
203 CAnd [] -> P.text "True"
205 CAnd cs ->
206 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
208 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
209 P.sep [ binder, pretty Never c ]
210 where
211 mergeExists vs c =
212 case c of
213 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
214 _ -> (vs, c)
216 (fqs', c) = mergeExists fqs constraint
218 binder = if null fqs' then P.empty else
219 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
221 CLet schemes constraint ->
222 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
223 , P.text "in", pretty Never constraint ]
225 CInstance name tipe ->
226 P.text name <+> P.text "<" <+> prty tipe
228instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
229 pretty _ (Scheme rqs fqs constraint headers) =
230 P.sep [ forall, cs, headers' ]
231 where
232 prty = pretty Never
234 forall = if null rqs && null fqs then P.empty else
235 P.text "\x2200" <+> frees <+> rigids
237 frees = P.hsep $ map prty fqs
238 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
240 cs = case constraint of
241 CTrue -> P.empty
242 CAnd [] -> P.empty
243 _ -> P.brackets (pretty Never constraint)
245 headers' = if Map.size headers > 0 then dict else P.empty
246 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
247 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
250extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
251extraPretty t = pretty Never <$> addNames t
253addNames :: (Crawl t) => t -> IO t
254addNames value = do
255 (_, rawVars) <- runStateT (crawl getNames value) []
256 let vars = map head . List.group $ List.sort rawVars
257 suffix s = map (++s) (map (:[]) ['a'..'z'])
258 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
259 okayVars = filter (`notElem` vars) allVars
260 runStateT (crawl rename value) okayVars
261 return value
262 where
263 getNames name vars =
264 case name of
265 Just var -> (name, var:vars)
266 Nothing -> (name, vars)
268 rename name vars =
269 case name of
270 Just var -> (name, vars)
271 Nothing -> (Just (head vars), tail vars)
274-- Code for traversing all the type data-structures and giving
275-- names to the variables embedded deep in there.
276class Crawl t where
277 crawl :: (Maybe TypeName -> [String] -> (Maybe TypeName, [String]))
278 -> t
279 -> StateT [String] IO t
281instance (Crawl t, Crawl v) => Crawl (Constraint t v) where
282 crawl nextState constraint =
283 let rnm = crawl nextState in
284 case constraint of
285 CTrue -> return CTrue
286 CSaveEnv -> return CSaveEnv
287 CEqual a b -> CEqual <$> rnm a <*> rnm b
288 CAnd cs -> CAnd <$> crawl nextState cs
289 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
290 CInstance name tipe -> CInstance name <$> rnm tipe
292instance Crawl a => Crawl [a] where
293 crawl nextState list = mapM (crawl nextState) list
295instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
296 crawl nextState (Scheme rqs fqs c headers) =
297 let rnm = crawl nextState in
298 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
300instance Crawl t => Crawl (TermN t) where
301 crawl nextState tipe =
302 case tipe of
303 VarN x -> VarN <$> crawl nextState x
304 TermN term -> TermN <$> crawl nextState term
306instance Crawl t => Crawl (Term1 t) where
307 crawl nextState term =
308 let rnm = crawl nextState in
309 case term of
310 App1 a b -> App1 <$> rnm a <*> rnm b
311 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
312 Var1 a -> Var1 <$> rnm a
313 EmptyRecord1 -> return EmptyRecord1
314 Record1 fields ext ->
315 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
317instance Crawl a => Crawl (UF.Point a) where
318 crawl nextState point = do
319 desc <- liftIO $ UF.descriptor point
320 desc' <- crawl nextState desc
321 liftIO $ UF.setDescriptor point desc'
322 return point
324instance Crawl Descriptor where
325 crawl nextState desc = do
326 state <- get
327 let (name', state') = nextState (name desc) state
328 structure' <- traverse (crawl nextState) (structure desc)
329 put state'
330 return $ desc { name = name', structure = structure' }