git.iko.soy/elk
on ab17521 help sign in
elk/compiler/Type/Type.hs
409 lines 13 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 AST.Annotation
15import AST.Helpers (isTuple)
16import qualified AST.Type as T
17import qualified AST.Variable as Var
19data Term1 a
20 = App1 a a
21 | Fun1 a a
22 | Var1 a
23 | EmptyRecord1
24 | Record1 (Map.Map String [a]) a
25 deriving Show
27data TermN a
28 = VarN a
29 | TermN (Term1 (TermN a))
30 deriving Show
32record :: Map.Map String [TermN a] -> TermN a -> TermN a
33record fs rec = TermN (Record1 fs rec)
35type Type = TermN Variable
36type Variable = UF.Point Descriptor
38type SchemeName = String
39type TypeName = String
41type Constraint a b = Located (BasicConstraint a b)
42data BasicConstraint a b
43 = CTrue
44 | CSaveEnv
45 | CEqual a a
46 | CAnd [Constraint a b]
47 | CLet [Scheme a b] (Constraint a b)
48 | CInstance SchemeName a
49 deriving Show
51data Scheme a b = Scheme {
52 rigidQuantifiers :: [b],
53 flexibleQuantifiers :: [b],
54 constraint :: Constraint a b,
55 header :: Map.Map String a
56} deriving Show
58type TypeConstraint = Constraint Type Variable
59type TypeScheme = Scheme Type Variable
61monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
63infixl 8 /\
65(/\) :: Constraint a b -> Constraint a b -> Constraint a b
66a@(A _ c1) /\ b@(A _ c2) =
67 case (c1, c2) of
68 (CTrue, _) -> b
69 (_, CTrue) -> a
70 _ -> mergeOldDocs a b (CAnd [a,b])
72infixr 9 ==>
73(==>) :: Type -> Type -> Type
74a ==> b = TermN (Fun1 a b)
76f <| a = TermN (App1 f a)
78data Descriptor = Descriptor {
79 structure :: Maybe (Term1 Variable),
80 rank :: Int,
81 flex :: Flex,
82 name :: Maybe TypeName,
83 copy :: Maybe Variable,
84 mark :: Int
85} deriving Show
87noRank = -1
88outermostRank = 0 :: Int
90noMark = 0
91initialMark = 1
93data Flex = Rigid | Flexible | Constant | Is SuperType
94 deriving (Show, Eq)
96data SuperType = Number | Comparable | Appendable
97 deriving (Show, Eq)
99namedVar :: Flex -> String -> IO Variable
100namedVar flex name = UF.fresh $ Descriptor {
101 structure = Nothing,
102 rank = noRank,
103 flex = flex,
104 name = Just name,
105 copy = Nothing,
106 mark = noMark
107 }
109var :: Flex -> IO Variable
110var flex = UF.fresh $ Descriptor {
111 structure = Nothing,
112 rank = noRank,
113 flex = flex,
114 name = Nothing,
115 copy = Nothing,
116 mark = noMark
117 }
119structuredVar :: Term1 Variable -> IO Variable
120structuredVar structure = UF.fresh $ Descriptor {
121 structure = Just structure,
122 rank = noRank,
123 flex = Flexible,
124 name = Nothing,
125 copy = Nothing,
126 mark = noMark
127 }
130-- ex qs constraint == exists qs. constraint
131ex :: [Variable] -> TypeConstraint -> TypeConstraint
132ex fqs constraint@(A ann _) =
133 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
135-- fl qs constraint == forall qs. constraint
136fl :: [Variable] -> TypeConstraint -> TypeConstraint
137fl rqs constraint@(A ann _) =
138 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
140exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
141exists f = do
142 v <- liftIO $ var Flexible
143 ex [v] <$> f (VarN v)
145existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
146existsNumber f = do
147 v <- liftIO $ var (Is Number)
148 ex [v] <$> f (VarN v)
151instance Show a => Show (UF.Point a) where
152 show point = unsafePerformIO $ fmap show (UF.descriptor point)
155instance PrettyType a => PrettyType (UF.Point a) where
156 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
159instance PrettyType t => PrettyType (Annotated a t) where
160 pretty when (A _ e) = pretty when e
163instance PrettyType a => PrettyType (Term1 a) where
164 pretty when term =
165 let prty = pretty Never in
166 case term of
167 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
168 | otherwise -> parensIf needed (px <+> pretty App x)
169 where
170 px = prty f
171 needed = case when of
172 App -> True
173 _ -> False
175 Fun1 arg body ->
176 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
177 where
178 needed = case when of
179 Never -> False
180 _ -> True
182 Var1 x -> prty x
184 EmptyRecord1 -> P.braces P.empty
186 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
187 where
188 prettyExt = prty ext
189 extend | P.render prettyExt == "{}" = P.empty
190 | otherwise = prettyExt <+> P.text "|"
191 mkPretty f t = P.text (reprime f) <+> P.text ":" <+> prty t
192 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
195instance PrettyType a => PrettyType (TermN a) where
196 pretty when term =
197 case term of
198 VarN x -> pretty when x
199 TermN t1 -> pretty when t1
202instance PrettyType Descriptor where
203 pretty when desc =
204 case (structure desc, name desc) of
205 (Just term, _) -> pretty when term
206 (_, Just name) -> if not (isTuple name) then P.text (reprime name) else
207 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
208 _ -> P.text "?"
211instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
212 pretty _ constraint =
213 let prty = pretty Never in
214 case constraint of
215 CTrue -> P.text "True"
216 CSaveEnv -> P.text "SaveTheEnvironment!!!"
217 CEqual a b -> prty a <+> P.text "=" <+> prty b
218 CAnd [] -> P.text "True"
220 CAnd cs ->
221 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
223 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
224 P.sep [ binder, pretty Never c ]
225 where
226 mergeExists vs (A _ c) =
227 case c of
228 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
229 _ -> (vs, c)
231 (fqs', c) = mergeExists fqs constraint
233 binder = if null fqs' then P.empty else
234 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
236 CLet schemes constraint ->
237 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
238 , P.text "in", pretty Never constraint ]
240 CInstance name tipe ->
241 P.text name <+> P.text "<" <+> prty tipe
243instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
244 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
245 P.sep [ forall, cs, headers' ]
246 where
247 prty = pretty Never
249 forall = if null rqs && null fqs then P.empty else
250 P.text "\x2200" <+> frees <+> rigids
252 frees = P.hsep $ map prty fqs
253 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
255 cs = case constraint of
256 CTrue -> P.empty
257 CAnd [] -> P.empty
258 _ -> P.brackets (pretty Never constraint)
260 headers' = if Map.size headers > 0 then dict else P.empty
261 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
262 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
265extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
266extraPretty t = pretty Never <$> addNames t
268addNames :: (Crawl t) => t -> IO t
269addNames value = do
270 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
271 let vars = map head . List.group $ List.sort rawVars
272 suffix s = map (++s) (map (:[]) ['a'..'z'])
273 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
274 okayVars = filter (`notElem` vars) allVars
275 runStateT (crawl rename value) (okayVars, 0, 0, 0)
276 return value
277 where
278 getNames desc state@(vars, a, b, c) =
279 let name' = name desc in
280 case name' of
281 Just var -> (name', (var:vars, a, b, c))
282 Nothing -> (name', state)
284 rename desc state@(vars, a, b, c) =
285 case name desc of
286 Just var -> (Just var, state)
287 Nothing ->
288 case flex desc of
289 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
290 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
291 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
292 other -> (Just $ head vars, (tail vars, a, b, c))
293 where mark = case other of
294 Flexible -> ""
295 Rigid -> "!"
296 Constant -> "#"
299type CrawlState = ([String], Int, Int, Int)
301-- Code for traversing all the type data-structures and giving
302-- names to the variables embedded deep in there.
303class Crawl t where
304 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
305 -> t
306 -> StateT CrawlState IO t
308instance Crawl e => Crawl (Annotated a e) where
309 crawl nextState (A ann e) = A ann <$> crawl nextState e
311instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
312 crawl nextState constraint =
313 let rnm = crawl nextState in
314 case constraint of
315 CTrue -> return CTrue
316 CSaveEnv -> return CSaveEnv
317 CEqual a b -> CEqual <$> rnm a <*> rnm b
318 CAnd cs -> CAnd <$> crawl nextState cs
319 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
320 CInstance name tipe -> CInstance name <$> rnm tipe
322instance Crawl a => Crawl [a] where
323 crawl nextState list = mapM (crawl nextState) list
325instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
326 crawl nextState (Scheme rqs fqs c headers) =
327 let rnm = crawl nextState in
328 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
330instance Crawl t => Crawl (TermN t) where
331 crawl nextState tipe =
332 case tipe of
333 VarN x -> VarN <$> crawl nextState x
334 TermN term -> TermN <$> crawl nextState term
336instance Crawl t => Crawl (Term1 t) where
337 crawl nextState term =
338 let rnm = crawl nextState in
339 case term of
340 App1 a b -> App1 <$> rnm a <*> rnm b
341 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
342 Var1 a -> Var1 <$> rnm a
343 EmptyRecord1 -> return EmptyRecord1
344 Record1 fields ext ->
345 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
347instance Crawl a => Crawl (UF.Point a) where
348 crawl nextState point = do
349 desc <- liftIO $ UF.descriptor point
350 desc' <- crawl nextState desc
351 liftIO $ UF.setDescriptor point desc'
352 return point
354instance Crawl Descriptor where
355 crawl nextState desc = do
356 state <- get
357 let (name', state') = nextState desc state
358 structure' <- traverse (crawl nextState) (structure desc)
359 put state'
360 return $ desc { name = name', structure = structure' }
363toSrcType :: Variable -> IO T.CanonicalType
364toSrcType variable = do
365 desc <- UF.descriptor =<< addNames variable
366 case structure desc of
367 Just term ->
368 case term of
369 App1 a b -> do
370 T.Data name ts <- toSrcType a
371 b' <- toSrcType b
372 return (T.Data name (ts ++ [b']))
373 Fun1 a b -> T.Lambda <$> toSrcType a <*> toSrcType b
374 Var1 a -> toSrcType a
375 EmptyRecord1 -> return $ T.Record [] Nothing
376 Record1 tfields extension -> do
377 fields' <- traverse (mapM toSrcType) tfields
378 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
379 ext' <- toSrcType extension
380 return $ case ext' of
381 T.Record fs ext -> T.Record (fs ++ fields) ext
382 T.Var x -> T.Record fields (Just ext')
383 _ -> error "Used toSrcType on a type that is not well-formed"
384 Nothing ->
385 case name desc of
386 Just x@(c:_) | Char.isLower c -> return (T.Var x)
387 | otherwise -> return (T.Data (Var.Canonical (error "did not finish converting toSrcType") x) [])
388 _ -> error $ concat
389 [ "Problem converting the following type "
390 , "from a type-checker type to a source-syntax type:"
391 , P.render (pretty Never variable) ]
393data AppStructure = List Variable | Tuple [Variable] | Other
395collectApps :: Variable -> IO AppStructure
396collectApps variable = go [] variable
397 where
398 go vars variable = do
399 desc <- UF.descriptor variable
400 case (structure desc, vars) of
401 (Nothing, [v]) -> case name desc of
402 Just "_List" -> return (List v)
403 _ -> return Other
404 (Nothing, vs) -> case name desc of
405 Just ctor | isTuple ctor -> return (Tuple vs)
406 _ -> return Other
407 (Just term, _) -> case term of
408 App1 a b -> go (vars ++ [b]) a
409 _ -> return Other