git.iko.soy/elk
on 476e87f help sign in
elk/compiler/Type/Type.hs
395 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 (reprime 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 (reprime 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 other -> (Just $ head vars, (tail vars, a, b, c))
281 where mark = case other of
282 Flexible -> ""
283 Rigid -> "!"
284 Constant -> "#"
287type CrawlState = ([String], Int, Int, Int)
289-- Code for traversing all the type data-structures and giving
290-- names to the variables embedded deep in there.
291class Crawl t where
292 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
293 -> t
294 -> StateT CrawlState IO t
296instance Crawl a => Crawl (Located a) where
297 crawl nextState (L s e) = L s <$> crawl nextState e
299instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
300 crawl nextState constraint =
301 let rnm = crawl nextState in
302 case constraint of
303 CTrue -> return CTrue
304 CSaveEnv -> return CSaveEnv
305 CEqual a b -> CEqual <$> rnm a <*> rnm b
306 CAnd cs -> CAnd <$> crawl nextState cs
307 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
308 CInstance name tipe -> CInstance name <$> rnm tipe
310instance Crawl a => Crawl [a] where
311 crawl nextState list = mapM (crawl nextState) list
313instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
314 crawl nextState (Scheme rqs fqs c headers) =
315 let rnm = crawl nextState in
316 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
318instance Crawl t => Crawl (TermN t) where
319 crawl nextState tipe =
320 case tipe of
321 VarN x -> VarN <$> crawl nextState x
322 TermN term -> TermN <$> crawl nextState term
324instance Crawl t => Crawl (Term1 t) where
325 crawl nextState term =
326 let rnm = crawl nextState in
327 case term of
328 App1 a b -> App1 <$> rnm a <*> rnm b
329 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
330 Var1 a -> Var1 <$> rnm a
331 EmptyRecord1 -> return EmptyRecord1
332 Record1 fields ext ->
333 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
335instance Crawl a => Crawl (UF.Point a) where
336 crawl nextState point = do
337 desc <- liftIO $ UF.descriptor point
338 desc' <- crawl nextState desc
339 liftIO $ UF.setDescriptor point desc'
340 return point
342instance Crawl Descriptor where
343 crawl nextState desc = do
344 state <- get
345 let (name', state') = nextState desc state
346 structure' <- traverse (crawl nextState) (structure desc)
347 put state'
348 return $ desc { name = name', structure = structure' }
351toSrcType :: Variable -> IO Src.Type
352toSrcType variable = do
353 desc <- UF.descriptor =<< addNames variable
354 case structure desc of
355 Just term ->
356 case term of
357 App1 a b -> do
358 Src.Data name ts <- toSrcType a
359 b' <- toSrcType b
360 return (Src.Data name (ts ++ [b']))
361 Fun1 a b -> Src.Lambda <$> toSrcType a <*> toSrcType b
362 Var1 a -> toSrcType a
363 EmptyRecord1 -> return Src.EmptyRecord
364 Record1 fs ext -> do
365 fs' <- traverse (mapM toSrcType) fs
366 let fs'' = concat [ map ((,) name) ts | (name,ts) <- Map.toList fs' ]
367 Src.Record fs'' <$> toSrcType ext
368 Nothing ->
369 case name desc of
370 Just x@(c:cs) | Char.isLower c -> return (Src.Var x)
371 | otherwise -> return (Src.Data x [])
372 Nothing ->
373 error $ concat
374 [ "Problem converting the following type "
375 , "from a type-checker type to a source-syntax type:"
376 , P.render (pretty Never variable) ]
379data AppStructure = List Variable | Tuple [Variable] | Other
381collectApps :: Variable -> IO AppStructure
382collectApps variable = go [] variable
383 where
384 go vars variable = do
385 desc <- UF.descriptor variable
386 case (structure desc, vars) of
387 (Nothing, [v] ) -> case name desc of
388 Just "_List" -> return (List v)
389 _ -> return Other
390 (Nothing, vs ) -> case name desc of
391 Just ctor | isTuple ctor -> return (Tuple vs)
392 _ -> return Other
393 (Just term, vs) -> case term of
394 App1 a b -> go (vars ++ [b]) a
395 _ -> return Other