git.iko.soy/elk
on a268421 help sign in
elk/compiler/Type/Type.hs
391 lines 12 kB history raw
1module Type.Type where
3import qualified Data.Char as Char
4import qualified Data.List as List
5import qualified Data.Map as Map
6import qualified Data.UnionFind.IO as UF
7import Type.PrettyPrint
8import Text.PrettyPrint as P
9import System.IO.Unsafe
10import Control.Applicative ((<$>),(<*>))
11import Control.Monad.State
12import Data.Traversable (traverse)
13import SourceSyntax.Location
14import SourceSyntax.Helpers (isTuple)
15import qualified SourceSyntax.Type as Src
17data Term1 a
18 = App1 a a
19 | Fun1 a a
20 | Var1 a
21 | EmptyRecord1
22 | Record1 (Map.Map String [a]) a
23 deriving Show
25data TermN a
26 = VarN a
27 | TermN (Term1 (TermN a))
28 deriving Show
30record :: Map.Map String [TermN a] -> TermN a -> TermN a
31record fs rec = TermN (Record1 fs rec)
33type Type = TermN Variable
34type Variable = UF.Point Descriptor
36type SchemeName = String
37type TypeName = String
39type Constraint a b = Located (BasicConstraint a b)
40data BasicConstraint a b
41 = CTrue
42 | CSaveEnv
43 | CEqual a a
44 | CAnd [Constraint a b]
45 | CLet [Scheme a b] (Constraint a b)
46 | CInstance SchemeName a
47 deriving Show
49data Scheme a b = Scheme {
50 rigidQuantifiers :: [b],
51 flexibleQuantifiers :: [b],
52 constraint :: Constraint a b,
53 header :: Map.Map String a
54} deriving Show
56type TypeConstraint = Constraint Type Variable
57type TypeScheme = Scheme Type Variable
59monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
61infixl 8 /\
63(/\) :: Constraint a b -> Constraint a b -> Constraint a b
64a@(L s1 c1) /\ b@(L s2 c2) =
65 case (c1, c2) of
66 (CTrue, _) -> b
67 (_, CTrue) -> a
68 _ -> mergeOldDocs a b (CAnd [a,b])
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 | Is SuperType
92 deriving (Show, Eq)
94data SuperType = Number | Comparable | Appendable
95 deriving (Show, Eq)
97namedVar flex name = UF.fresh $ Descriptor {
98 structure = Nothing,
99 rank = noRank,
100 flex = flex,
101 name = Just name,
102 copy = Nothing,
103 mark = noMark
104 }
106var flex = UF.fresh $ Descriptor {
107 structure = Nothing,
108 rank = noRank,
109 flex = flex,
110 name = Nothing,
111 copy = Nothing,
112 mark = noMark
113 }
115structuredVar structure = UF.fresh $ Descriptor {
116 structure = Just structure,
117 rank = noRank,
118 flex = Flexible,
119 name = Nothing,
120 copy = Nothing,
121 mark = noMark
122 }
125-- ex qs constraint == exists qs. constraint
126ex :: [Variable] -> TypeConstraint -> TypeConstraint
127ex fqs constraint@(L s _) = L s $ CLet [Scheme [] fqs constraint Map.empty] (L s CTrue)
129-- fl qs constraint == forall qs. constraint
130fl :: [Variable] -> TypeConstraint -> TypeConstraint
131fl rqs constraint@(L s _) = L s $ CLet [Scheme rqs [] constraint Map.empty] (L s CTrue)
133exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
134exists f = do
135 v <- var Flexible
136 ex [v] <$> f (VarN v)
139instance Show a => Show (UF.Point a) where
140 show point = unsafePerformIO $ fmap show (UF.descriptor point)
143instance PrettyType a => PrettyType (UF.Point a) where
144 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
147instance PrettyType a => PrettyType (Located a) where
148 pretty when (L _ e) = pretty when e
151instance PrettyType a => PrettyType (Term1 a) where
152 pretty when term =
153 let prty = pretty Never in
154 case term of
155 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
156 | otherwise -> parensIf needed (px <+> pretty App x)
157 where
158 px = prty f
159 needed = case when of
160 App -> True
161 _ -> False
163 Fun1 arg body ->
164 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
165 where
166 needed = case when of
167 Never -> False
168 _ -> True
170 Var1 x -> prty x
172 EmptyRecord1 -> P.braces P.empty
174 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
175 where
176 prettyExt = prty ext
177 extend | P.render prettyExt == "{}" = P.empty
178 | otherwise = prettyExt <+> P.text "|"
179 mkPretty f t = P.text f <+> P.text ":" <+> prty t
180 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
183instance PrettyType a => PrettyType (TermN a) where
184 pretty when term =
185 case term of
186 VarN x -> pretty when x
187 TermN t1 -> pretty when t1
190instance PrettyType Descriptor where
191 pretty when desc =
192 case (structure desc, name desc) of
193 (Just term, _) -> pretty when term
194 (_, Just name) -> if not (isTuple name) then P.text name else
195 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
196 _ -> P.text "?"
199instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
200 pretty _ constraint =
201 let prty = pretty Never in
202 case constraint of
203 CTrue -> P.text "True"
204 CSaveEnv -> P.text "SaveTheEnvironment!!!"
205 CEqual a b -> prty a <+> P.text "=" <+> prty b
206 CAnd [] -> P.text "True"
208 CAnd cs ->
209 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
211 CLet [Scheme [] fqs constraint header] (L _ CTrue) | Map.null header ->
212 P.sep [ binder, pretty Never c ]
213 where
214 mergeExists vs (L _ c) =
215 case c of
216 CLet [Scheme [] fqs' c' _] (L _ CTrue) -> mergeExists (vs ++ fqs') c'
217 _ -> (vs, c)
219 (fqs', c) = mergeExists fqs constraint
221 binder = if null fqs' then P.empty else
222 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
224 CLet schemes constraint ->
225 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
226 , P.text "in", pretty Never constraint ]
228 CInstance name tipe ->
229 P.text name <+> P.text "<" <+> prty tipe
231instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
232 pretty _ (Scheme rqs fqs (L _ constraint) headers) =
233 P.sep [ forall, cs, headers' ]
234 where
235 prty = pretty Never
237 forall = if null rqs && null fqs then P.empty else
238 P.text "\x2200" <+> frees <+> rigids
240 frees = P.hsep $ map prty fqs
241 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
243 cs = case constraint of
244 CTrue -> P.empty
245 CAnd [] -> P.empty
246 _ -> P.brackets (pretty Never constraint)
248 headers' = if Map.size headers > 0 then dict else P.empty
249 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
250 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
253extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
254extraPretty t = pretty Never <$> addNames t
256addNames :: (Crawl t) => t -> IO t
257addNames value = do
258 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
259 let vars = map head . List.group $ List.sort rawVars
260 suffix s = map (++s) (map (:[]) ['a'..'z'])
261 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
262 okayVars = filter (`notElem` vars) allVars
263 runStateT (crawl rename value) (okayVars, 0, 0, 0)
264 return value
265 where
266 getNames desc state@(vars, a, b, c) =
267 let name' = name desc in
268 case name' of
269 Just var -> (name', (var:vars, a, b, c))
270 Nothing -> (name', state)
272 rename desc state@(vars, a, b, c) =
273 case name desc of
274 Just var -> (Just var, state)
275 Nothing ->
276 case flex desc of
277 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
278 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
279 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
280 _ -> (Just $ head vars, (tail vars, a, b, c))
283type CrawlState = ([String], Int, Int, Int)
285-- Code for traversing all the type data-structures and giving
286-- names to the variables embedded deep in there.
287class Crawl t where
288 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
289 -> t
290 -> StateT CrawlState IO t
292instance Crawl a => Crawl (Located a) where
293 crawl nextState (L s e) = L s <$> crawl nextState e
295instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
296 crawl nextState constraint =
297 let rnm = crawl nextState in
298 case constraint of
299 CTrue -> return CTrue
300 CSaveEnv -> return CSaveEnv
301 CEqual a b -> CEqual <$> rnm a <*> rnm b
302 CAnd cs -> CAnd <$> crawl nextState cs
303 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
304 CInstance name tipe -> CInstance name <$> rnm tipe
306instance Crawl a => Crawl [a] where
307 crawl nextState list = mapM (crawl nextState) list
309instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
310 crawl nextState (Scheme rqs fqs c headers) =
311 let rnm = crawl nextState in
312 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
314instance Crawl t => Crawl (TermN t) where
315 crawl nextState tipe =
316 case tipe of
317 VarN x -> VarN <$> crawl nextState x
318 TermN term -> TermN <$> crawl nextState term
320instance Crawl t => Crawl (Term1 t) where
321 crawl nextState term =
322 let rnm = crawl nextState in
323 case term of
324 App1 a b -> App1 <$> rnm a <*> rnm b
325 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
326 Var1 a -> Var1 <$> rnm a
327 EmptyRecord1 -> return EmptyRecord1
328 Record1 fields ext ->
329 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
331instance Crawl a => Crawl (UF.Point a) where
332 crawl nextState point = do
333 desc <- liftIO $ UF.descriptor point
334 desc' <- crawl nextState desc
335 liftIO $ UF.setDescriptor point desc'
336 return point
338instance Crawl Descriptor where
339 crawl nextState desc = do
340 state <- get
341 let (name', state') = nextState desc state
342 structure' <- traverse (crawl nextState) (structure desc)
343 put state'
344 return $ desc { name = name', structure = structure' }
347toSrcType :: Variable -> IO Src.Type
348toSrcType variable = do
349 desc <- UF.descriptor =<< addNames variable
350 case structure desc of
351 Just term ->
352 case term of
353 App1 a b -> do
354 Src.Data name ts <- toSrcType a
355 b' <- toSrcType b
356 return (Src.Data name (ts ++ [b']))
357 Fun1 a b -> Src.Lambda <$> toSrcType a <*> toSrcType b
358 Var1 a -> toSrcType a
359 EmptyRecord1 -> return Src.EmptyRecord
360 Record1 fs ext -> do
361 fs' <- traverse (mapM toSrcType) fs
362 let fs'' = concat [ map ((,) name) ts | (name,ts) <- Map.toList fs' ]
363 Src.Record fs'' <$> toSrcType ext
364 Nothing ->
365 case name desc of
366 Just x@(c:cs) | Char.isLower c -> return (Src.Var x)
367 | otherwise -> return (Src.Data x [])
368 Nothing ->
369 error $ concat
370 [ "Problem converting the following type "
371 , "from a type-checker type to a source-syntax type:"
372 , P.render (pretty Never variable) ]
375data AppStructure = List Variable | Tuple [Variable] | Other
377collectApps :: Variable -> IO AppStructure
378collectApps variable = go [] variable
379 where
380 go vars variable = do
381 desc <- UF.descriptor variable
382 case (structure desc, vars) of
383 (Nothing, [v] ) -> case name desc of
384 Just "_List" -> return (List v)
385 _ -> return Other
386 (Nothing, vs ) -> case name desc of
387 Just ctor | isTuple ctor -> return (Tuple vs)
388 _ -> return Other
389 (Just term, vs) -> case term of
390 App1 a b -> go (vars ++ [b]) a
391 _ -> return Other