git.iko.soy/elk
on ab53fac help sign in
elk/compiler/Type/Type.hs
394 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 Control.Monad.Error
13import Data.Traversable (traverse)
14import SourceSyntax.Location
15import SourceSyntax.Helpers (isTuple)
16import qualified SourceSyntax.Type as Src
18data Term1 a
19 = App1 a a
20 | Fun1 a a
21 | Var1 a
22 | EmptyRecord1
23 | Record1 (Map.Map String [a]) a
24 deriving Show
26data TermN a
27 = VarN a
28 | TermN (Term1 (TermN a))
29 deriving Show
31record :: Map.Map String [TermN a] -> TermN a -> TermN a
32record fs rec = TermN (Record1 fs rec)
34type Type = TermN Variable
35type Variable = UF.Point Descriptor
37type SchemeName = String
38type TypeName = String
40type Constraint a b = Located (BasicConstraint a b)
41data BasicConstraint a b
42 = CTrue
43 | CSaveEnv
44 | CEqual a a
45 | CAnd [Constraint a b]
46 | CLet [Scheme a b] (Constraint a b)
47 | CInstance SchemeName a
48 deriving Show
50data Scheme a b = Scheme {
51 rigidQuantifiers :: [b],
52 flexibleQuantifiers :: [b],
53 constraint :: Constraint a b,
54 header :: Map.Map String a
55} deriving Show
57type TypeConstraint = Constraint Type Variable
58type TypeScheme = Scheme Type Variable
60monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
62infixl 8 /\
64(/\) :: Constraint a b -> Constraint a b -> Constraint a b
65a@(L s1 c1) /\ b@(L s2 c2) =
66 case (c1, c2) of
67 (CTrue, _) -> b
68 (_, CTrue) -> a
69 _ -> mergeOldDocs a b (CAnd [a,b])
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@(L s _) = L s $ CLet [Scheme [] fqs constraint Map.empty] (L s CTrue)
130-- fl qs constraint == forall qs. constraint
131fl :: [Variable] -> TypeConstraint -> TypeConstraint
132fl rqs constraint@(L s _) = L s $ CLet [Scheme rqs [] constraint Map.empty] (L s CTrue)
134exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
135exists f = do
136 v <- liftIO $ 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 (Located a) where
149 pretty when (L _ e) = pretty when e
152instance PrettyType a => PrettyType (Term1 a) where
153 pretty when term =
154 let prty = pretty Never in
155 case term of
156 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
157 | otherwise -> parensIf needed (px <+> pretty App x)
158 where
159 px = prty f
160 needed = case when of
161 App -> True
162 _ -> False
164 Fun1 arg body ->
165 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
166 where
167 needed = case when of
168 Never -> False
169 _ -> True
171 Var1 x -> prty x
173 EmptyRecord1 -> P.braces P.empty
175 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
176 where
177 prettyExt = prty ext
178 extend | P.render prettyExt == "{}" = P.empty
179 | otherwise = prettyExt <+> P.text "|"
180 mkPretty f t = P.text (reprime f) <+> P.text ":" <+> prty t
181 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
184instance PrettyType a => PrettyType (TermN a) where
185 pretty when term =
186 case term of
187 VarN x -> pretty when x
188 TermN t1 -> pretty when t1
191instance PrettyType Descriptor where
192 pretty when desc =
193 case (structure desc, name desc) of
194 (Just term, _) -> pretty when term
195 (_, Just name) -> if not (isTuple name) then P.text (reprime name) else
196 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
197 _ -> P.text "?"
200instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
201 pretty _ constraint =
202 let prty = pretty Never in
203 case constraint of
204 CTrue -> P.text "True"
205 CSaveEnv -> P.text "SaveTheEnvironment!!!"
206 CEqual a b -> prty a <+> P.text "=" <+> prty b
207 CAnd [] -> P.text "True"
209 CAnd cs ->
210 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
212 CLet [Scheme [] fqs constraint header] (L _ CTrue) | Map.null header ->
213 P.sep [ binder, pretty Never c ]
214 where
215 mergeExists vs (L _ c) =
216 case c of
217 CLet [Scheme [] fqs' c' _] (L _ CTrue) -> mergeExists (vs ++ fqs') c'
218 _ -> (vs, c)
220 (fqs', c) = mergeExists fqs constraint
222 binder = if null fqs' then P.empty else
223 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
225 CLet schemes constraint ->
226 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
227 , P.text "in", pretty Never constraint ]
229 CInstance name tipe ->
230 P.text name <+> P.text "<" <+> prty tipe
232instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
233 pretty _ (Scheme rqs fqs (L _ constraint) headers) =
234 P.sep [ forall, cs, headers' ]
235 where
236 prty = pretty Never
238 forall = if null rqs && null fqs then P.empty else
239 P.text "\x2200" <+> frees <+> rigids
241 frees = P.hsep $ map prty fqs
242 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
244 cs = case constraint of
245 CTrue -> P.empty
246 CAnd [] -> P.empty
247 _ -> P.brackets (pretty Never constraint)
249 headers' = if Map.size headers > 0 then dict else P.empty
250 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
251 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
254extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
255extraPretty t = pretty Never <$> addNames t
257addNames :: (Crawl t) => t -> IO t
258addNames value = do
259 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
260 let vars = map head . List.group $ List.sort rawVars
261 suffix s = map (++s) (map (:[]) ['a'..'z'])
262 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
263 okayVars = filter (`notElem` vars) allVars
264 runStateT (crawl rename value) (okayVars, 0, 0, 0)
265 return value
266 where
267 getNames desc state@(vars, a, b, c) =
268 let name' = name desc in
269 case name' of
270 Just var -> (name', (var:vars, a, b, c))
271 Nothing -> (name', state)
273 rename desc state@(vars, a, b, c) =
274 case name desc of
275 Just var -> (Just var, state)
276 Nothing ->
277 case flex desc of
278 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
279 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
280 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
281 other -> (Just $ head vars, (tail vars, a, b, c))
282 where mark = case other of
283 Flexible -> ""
284 Rigid -> "!"
285 Constant -> "#"
288type CrawlState = ([String], Int, Int, Int)
290-- Code for traversing all the type data-structures and giving
291-- names to the variables embedded deep in there.
292class Crawl t where
293 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
294 -> t
295 -> StateT CrawlState IO t
297instance Crawl a => Crawl (Located a) where
298 crawl nextState (L s e) = L s <$> crawl nextState e
300instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
301 crawl nextState constraint =
302 let rnm = crawl nextState in
303 case constraint of
304 CTrue -> return CTrue
305 CSaveEnv -> return CSaveEnv
306 CEqual a b -> CEqual <$> rnm a <*> rnm b
307 CAnd cs -> CAnd <$> crawl nextState cs
308 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
309 CInstance name tipe -> CInstance name <$> rnm tipe
311instance Crawl a => Crawl [a] where
312 crawl nextState list = mapM (crawl nextState) list
314instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
315 crawl nextState (Scheme rqs fqs c headers) =
316 let rnm = crawl nextState in
317 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
319instance Crawl t => Crawl (TermN t) where
320 crawl nextState tipe =
321 case tipe of
322 VarN x -> VarN <$> crawl nextState x
323 TermN term -> TermN <$> crawl nextState term
325instance Crawl t => Crawl (Term1 t) where
326 crawl nextState term =
327 let rnm = crawl nextState in
328 case term of
329 App1 a b -> App1 <$> rnm a <*> rnm b
330 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
331 Var1 a -> Var1 <$> rnm a
332 EmptyRecord1 -> return EmptyRecord1
333 Record1 fields ext ->
334 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
336instance Crawl a => Crawl (UF.Point a) where
337 crawl nextState point = do
338 desc <- liftIO $ UF.descriptor point
339 desc' <- crawl nextState desc
340 liftIO $ UF.setDescriptor point desc'
341 return point
343instance Crawl Descriptor where
344 crawl nextState desc = do
345 state <- get
346 let (name', state') = nextState desc state
347 structure' <- traverse (crawl nextState) (structure desc)
348 put state'
349 return $ desc { name = name', structure = structure' }
352toSrcType :: Variable -> IO Src.Type
353toSrcType variable = do
354 desc <- UF.descriptor =<< addNames variable
355 case structure desc of
356 Just term ->
357 case term of
358 App1 a b -> do
359 Src.Data name ts <- toSrcType a
360 b' <- toSrcType b
361 return (Src.Data name (ts ++ [b']))
362 Fun1 a b -> Src.Lambda <$> toSrcType a <*> toSrcType b
363 Var1 a -> toSrcType a
364 EmptyRecord1 -> return Src.EmptyRecord
365 Record1 fs ext -> do
366 fs' <- traverse (mapM toSrcType) fs
367 let fs'' = concat [ map ((,) name) ts | (name,ts) <- Map.toList fs' ]
368 Src.Record fs'' <$> toSrcType ext
369 Nothing ->
370 case name desc of
371 Just x@(c:cs) | Char.isLower c -> return (Src.Var x)
372 | otherwise -> return (Src.Data x [])
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) ]
378data AppStructure = List Variable | Tuple [Variable] | Other
380collectApps :: Variable -> IO AppStructure
381collectApps variable = go [] variable
382 where
383 go vars variable = do
384 desc <- UF.descriptor variable
385 case (structure desc, vars) of
386 (Nothing, [v] ) -> case name desc of
387 Just "_List" -> return (List v)
388 _ -> return Other
389 (Nothing, vs ) -> case name desc of
390 Just ctor | isTuple ctor -> return (Tuple vs)
391 _ -> return Other
392 (Just term, vs) -> case term of
393 App1 a b -> go (vars ++ [b]) a
394 _ -> return Other