git.iko.soy/elk
on da346ea help sign in
elk/compiler/Type/Type.hs
338 lines 10.0 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 :: Map.Map String [TermN a] -> TermN a -> TermN a
29record fs rec = TermN (Record1 fs rec)
31type Type = TermN Variable
32type Variable = UF.Point Descriptor
34type SchemeName = String
35type TypeName = String
37data Constraint a b
38 = CTrue
39 | CSaveEnv
40 | CEqual a a
41 | CAnd [Constraint a b]
42 | CLet [Scheme a b] (Constraint a b)
43 | CInstance SchemeName a
44 deriving Show
46data Scheme a b = Scheme {
47 rigidQuantifiers :: [b],
48 flexibleQuantifiers :: [b],
49 constraint :: Constraint a b,
50 header :: Map.Map String a
51} deriving Show
53type TypeConstraint = Constraint Type Variable
54type TypeScheme = Scheme Type Variable
56monoscheme headers = Scheme [] [] CTrue headers
58infixl 8 /\
60(/\) :: Constraint a b -> Constraint a b -> Constraint a b
61a /\ CTrue = a
62CTrue /\ b = b
63a /\ b = CAnd [a,b]
65(===) :: Type -> Type -> TypeConstraint
66(===) = CEqual
68(<?) :: SchemeName -> Type -> TypeConstraint
69x <? t = CInstance x t
71infixr 9 ==>
72(==>) :: Type -> Type -> Type
73a ==> b = TermN (Fun1 a b)
75f <| a = TermN (App1 f a)
77data Descriptor = Descriptor {
78 structure :: Maybe (Term1 Variable),
79 rank :: Int,
80 flex :: Flex,
81 name :: Maybe TypeName,
82 copy :: Maybe Variable,
83 mark :: Int
84} deriving Show
86noRank = -1
87outermostRank = 0 :: Int
89noMark = 0
90initialMark = 1
92data Flex = Rigid | Flexible | Constant | Is SuperType
93 deriving (Show, Eq)
95data SuperType = Number | Comparable | Appendable
96 deriving (Show, Eq)
98namedVar flex name = UF.fresh $ Descriptor {
99 structure = Nothing,
100 rank = noRank,
101 flex = flex,
102 name = Just name,
103 copy = Nothing,
104 mark = noMark
105 }
107var flex = UF.fresh $ Descriptor {
108 structure = Nothing,
109 rank = noRank,
110 flex = flex,
111 name = Nothing,
112 copy = Nothing,
113 mark = noMark
114 }
116structuredVar structure = UF.fresh $ Descriptor {
117 structure = Just structure,
118 rank = noRank,
119 flex = Flexible,
120 name = Nothing,
121 copy = Nothing,
122 mark = noMark
123 }
126-- ex qs constraint == exists qs. constraint
127ex :: [Variable] -> TypeConstraint -> TypeConstraint
128ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
130-- fl qs constraint == forall qs. constraint
131fl :: [Variable] -> TypeConstraint -> TypeConstraint
132fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
134exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
135exists f = do
136 v <- var Flexible
137 ex [v] <$> f (VarN v)
140instance Show a => Show (UF.Point a) where
141 show point = unsafePerformIO $ fmap show (UF.descriptor point)
144instance PrettyType a => PrettyType (UF.Point a) where
145 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
148instance PrettyType a => PrettyType (Term1 a) where
149 pretty when term =
150 let prty = pretty Never in
151 case term of
152 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
153 | otherwise -> parensIf needed (px <+> pretty App x)
154 where
155 px = prty f
156 needed = case when of
157 App -> True
158 _ -> False
160 Fun1 arg body ->
161 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
162 where
163 needed = case when of
164 Never -> False
165 _ -> True
167 Var1 x -> prty x
169 EmptyRecord1 -> P.braces P.empty
171 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
172 where
173 prettyExt = prty ext
174 extend | P.render prettyExt == "{}" = P.empty
175 | otherwise = prettyExt <+> P.text "|"
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, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
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, 0, 0, 0)
261 return value
262 where
263 getNames desc state@(vars, a, b, c) =
264 let name' = name desc in
265 case name' of
266 Just var -> (name', (var:vars, a, b, c))
267 Nothing -> (name', state)
269 rename desc state@(vars, a, b, c) =
270 case name desc of
271 Just var -> (Just var, state)
272 Nothing ->
273 case flex desc of
274 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
275 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
276 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
277 _ -> (Just $ head vars, (tail vars, a, b, c))
280type CrawlState = ([String], Int, Int, Int)
282-- Code for traversing all the type data-structures and giving
283-- names to the variables embedded deep in there.
284class Crawl t where
285 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
286 -> t
287 -> StateT CrawlState IO t
289instance (Crawl t, Crawl v) => Crawl (Constraint t v) where
290 crawl nextState constraint =
291 let rnm = crawl nextState in
292 case constraint of
293 CTrue -> return CTrue
294 CSaveEnv -> return CSaveEnv
295 CEqual a b -> CEqual <$> rnm a <*> rnm b
296 CAnd cs -> CAnd <$> crawl nextState cs
297 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
298 CInstance name tipe -> CInstance name <$> rnm tipe
300instance Crawl a => Crawl [a] where
301 crawl nextState list = mapM (crawl nextState) list
303instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
304 crawl nextState (Scheme rqs fqs c headers) =
305 let rnm = crawl nextState in
306 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
308instance Crawl t => Crawl (TermN t) where
309 crawl nextState tipe =
310 case tipe of
311 VarN x -> VarN <$> crawl nextState x
312 TermN term -> TermN <$> crawl nextState term
314instance Crawl t => Crawl (Term1 t) where
315 crawl nextState term =
316 let rnm = crawl nextState in
317 case term of
318 App1 a b -> App1 <$> rnm a <*> rnm b
319 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
320 Var1 a -> Var1 <$> rnm a
321 EmptyRecord1 -> return EmptyRecord1
322 Record1 fields ext ->
323 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
325instance Crawl a => Crawl (UF.Point a) where
326 crawl nextState point = do
327 desc <- liftIO $ UF.descriptor point
328 desc' <- crawl nextState desc
329 liftIO $ UF.setDescriptor point desc'
330 return point
332instance Crawl Descriptor where
333 crawl nextState desc = do
334 state <- get
335 let (name', state') = nextState desc state
336 structure' <- traverse (crawl nextState) (structure desc)
337 put state'
338 return $ desc { name = name', structure = structure' }