git.iko.soy/elk
on dfdf96d help sign in
elk/compiler/Type/Type.hs
419 lines 13 kB history raw
1{-# OPTIONS_GHC -W #-}
2module Type.Type where
4import qualified Data.Char as Char
5import qualified Data.List as List
6import qualified Data.Map as Map
7import qualified Data.UnionFind.IO as UF
8import Type.PrettyPrint
9import Text.PrettyPrint as P
10import System.IO.Unsafe
11import Control.Applicative ((<$>),(<*>))
12import Control.Monad.State
13import Control.Monad.Error
14import Data.Traversable (traverse)
15import AST.Annotation
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 = Var.Canonical
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 -> Var.Canonical -> 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 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)
207 | Var.isTuple name ->
208 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
209 | otherwise ->
210 P.text (Var.toString name)
212 _ -> P.text "?"
215instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
216 pretty _ constraint =
217 let prty = pretty Never in
218 case constraint of
219 CTrue -> P.text "True"
220 CSaveEnv -> P.text "SaveTheEnvironment!!!"
221 CEqual a b -> prty a <+> P.text "=" <+> prty b
222 CAnd [] -> P.text "True"
224 CAnd cs ->
225 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
227 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
228 P.sep [ binder, pretty Never c ]
229 where
230 mergeExists vs (A _ c) =
231 case c of
232 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
233 _ -> (vs, c)
235 (fqs', c) = mergeExists fqs constraint
237 binder = if null fqs' then P.empty else
238 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
240 CLet schemes constraint ->
241 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
242 , P.text "in", pretty Never constraint ]
244 CInstance name tipe ->
245 P.text name <+> P.text "<" <+> prty tipe
247instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
248 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
249 P.sep [ forall, cs, headers' ]
250 where
251 prty = pretty Never
253 forall = if null rqs && null fqs then P.empty else
254 P.text "\x2200" <+> frees <+> rigids
256 frees = P.hsep $ map prty fqs
257 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
259 cs = case constraint of
260 CTrue -> P.empty
261 CAnd [] -> P.empty
262 _ -> P.brackets (pretty Never constraint)
264 headers' = if Map.size headers > 0 then dict else P.empty
265 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
266 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
269extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
270extraPretty t = pretty Never <$> addNames t
272addNames :: (Crawl t) => t -> IO t
273addNames value = do
274 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
275 let vars = map head . List.group $ List.sort rawVars
276 suffix s = map (++s) (map (:[]) ['a'..'z'])
277 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
278 okayVars = filter (`notElem` vars) allVars
279 runStateT (crawl rename value) (okayVars, 0, 0, 0)
280 return value
281 where
282 getNames desc state@(vars, a, b, c) =
283 let name' = name desc in
284 case name' of
285 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
286 _ -> (name', state)
288 rename desc state@(vars, a, b, c) =
289 case name desc of
290 Just var -> (Just var, state)
291 Nothing ->
292 case flex desc of
293 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
294 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
295 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
296 _ -> (local $ head vars, (tail vars, a, b, c))
297 where
298 local v = Just (Var.local v)
300type CrawlState = ([String], Int, Int, Int)
302-- Code for traversing all the type data-structures and giving
303-- names to the variables embedded deep in there.
304class Crawl t where
305 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
306 -> t
307 -> StateT CrawlState IO t
309instance Crawl e => Crawl (Annotated a e) where
310 crawl nextState (A ann e) = A ann <$> crawl nextState e
312instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
313 crawl nextState constraint =
314 let rnm = crawl nextState in
315 case constraint of
316 CTrue -> return CTrue
317 CSaveEnv -> return CSaveEnv
318 CEqual a b -> CEqual <$> rnm a <*> rnm b
319 CAnd cs -> CAnd <$> crawl nextState cs
320 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
321 CInstance name tipe -> CInstance name <$> rnm tipe
323instance Crawl a => Crawl [a] where
324 crawl nextState list = mapM (crawl nextState) list
326instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
327 crawl nextState (Scheme rqs fqs c headers) =
328 let rnm = crawl nextState in
329 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
331instance Crawl t => Crawl (TermN t) where
332 crawl nextState tipe =
333 case tipe of
334 VarN x -> VarN <$> crawl nextState x
335 TermN term -> TermN <$> crawl nextState term
337instance Crawl t => Crawl (Term1 t) where
338 crawl nextState term =
339 let rnm = crawl nextState in
340 case term of
341 App1 a b -> App1 <$> rnm a <*> rnm b
342 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
343 Var1 a -> Var1 <$> rnm a
344 EmptyRecord1 -> return EmptyRecord1
345 Record1 fields ext ->
346 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
348instance Crawl a => Crawl (UF.Point a) where
349 crawl nextState point = do
350 desc <- liftIO $ UF.descriptor point
351 desc' <- crawl nextState desc
352 liftIO $ UF.setDescriptor point desc'
353 return point
355instance Crawl Descriptor where
356 crawl nextState desc = do
357 state <- get
358 let (name', state') = nextState desc state
359 structure' <- traverse (crawl nextState) (structure desc)
360 put state'
361 return $ desc { name = name', structure = structure' }
364toSrcType :: Variable -> IO T.CanonicalType
365toSrcType variable = do
366 desc <- UF.descriptor =<< addNames variable
367 case structure desc of
368 Just term ->
369 case term of
370 App1 a b -> do
371 a' <- toSrcType a
372 b' <- toSrcType b
373 case a' of
374 T.App f args -> return $ T.App f (args ++ [b'])
375 _ -> return $ T.App a' [b']
377 Fun1 a b -> T.Lambda <$> toSrcType a <*> toSrcType b
379 Var1 a -> toSrcType a
381 EmptyRecord1 -> return $ T.Record [] Nothing
383 Record1 tfields extension -> do
384 fields' <- traverse (mapM toSrcType) tfields
385 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
386 ext' <- toSrcType extension
387 return $ case ext' of
388 T.Record fs ext -> T.Record (fs ++ fields) ext
389 T.Var _ -> T.Record fields (Just ext')
390 _ -> error "Used toSrcType on a type that is not well-formed"
392 Nothing ->
393 case name desc of
394 Just var@(Var.Canonical _ x@(c:_))
395 | Char.isLower c -> return (T.Var x)
396 | otherwise -> return $ T.Type var
398 _ -> error $ concat
399 [ "Problem converting the following type "
400 , "from a type-checker type to a source-syntax type:"
401 , P.render (pretty Never variable) ]
403data AppStructure = List Variable | Tuple [Variable] | Other
405collectApps :: Variable -> IO AppStructure
406collectApps variable = go [] variable
407 where
408 go vars variable = do
409 desc <- UF.descriptor variable
410 case (structure desc, vars) of
411 (Nothing, [v]) -> case name desc of
412 Just n | Var.isList n -> return (List v)
413 _ -> return Other
414 (Nothing, vs) -> case name desc of
415 Just n | Var.isTuple n -> return (Tuple vs)
416 _ -> return Other
417 (Just term, _) -> case term of
418 App1 a b -> go (vars ++ [b]) a
419 _ -> return Other