git.iko.soy/elk
on eaea367 help sign in
elk/compiler/Type/Type.hs
434 lines 14 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 (StateT, get, put, execStateT, runStateT)
13import Control.Monad.Error (ErrorT, Error, liftIO)
14import Data.Traversable (traverse)
15import AST.Annotation
16import qualified AST.PrettyPrint as PP
17import qualified AST.Type as T
18import qualified AST.Variable as Var
20data Term1 a
21 = App1 a a
22 | Fun1 a a
23 | Var1 a
24 | EmptyRecord1
25 | Record1 (Map.Map String [a]) a
26 deriving Show
28data TermN a
29 = VarN (Maybe Var.Canonical) a
30 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
31 deriving Show
33varN :: a -> TermN a
34varN = VarN Nothing
36termN :: (Term1 (TermN a)) -> TermN a
37termN = TermN Nothing
39record :: Map.Map String [TermN a] -> TermN a -> TermN a
40record fs rec = termN (Record1 fs rec)
42type Type = TermN Variable
43type Variable = UF.Point Descriptor
45type SchemeName = String
46type TypeName = Var.Canonical
48type Constraint a b = Located (BasicConstraint a b)
49data BasicConstraint a b
50 = CTrue
51 | CSaveEnv
52 | CEqual a a
53 | CAnd [Constraint a b]
54 | CLet [Scheme a b] (Constraint a b)
55 | CInstance SchemeName a
56 deriving Show
58data Scheme a b = Scheme {
59 rigidQuantifiers :: [b],
60 flexibleQuantifiers :: [b],
61 constraint :: Constraint a b,
62 header :: Map.Map String a
63} deriving Show
65type TypeConstraint = Constraint Type Variable
66type TypeScheme = Scheme Type Variable
68monoscheme :: Map.Map String a -> Scheme a b
69monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
71infixl 8 /\
73(/\) :: Constraint a b -> Constraint a b -> Constraint a b
74a@(A _ c1) /\ b@(A _ c2) =
75 case (c1, c2) of
76 (CTrue, _) -> b
77 (_, CTrue) -> a
78 _ -> mergeOldDocs a b (CAnd [a,b])
80infixr 9 ==>
81(==>) :: Type -> Type -> Type
82a ==> b = termN (Fun1 a b)
84(<|) :: TermN a -> TermN a -> TermN a
85f <| a = termN (App1 f a)
87data Descriptor = Descriptor
88 { structure :: Maybe (Term1 Variable)
89 , rank :: Int
90 , flex :: Flex
91 , name :: Maybe TypeName
92 , copy :: Maybe Variable
93 , mark :: Int
94 , alias :: Maybe Var.Canonical
95 } deriving Show
97noRank :: Int
98noRank = -1
100outermostRank :: Int
101outermostRank = 0
103noMark :: Int
104noMark = 0
106initialMark :: Int
107initialMark = 1
109data Flex = Rigid | Flexible | Constant | Is SuperType
110 deriving (Show, Eq)
112data SuperType = Number | Comparable | Appendable
113 deriving (Show, Eq)
115namedVar :: Flex -> Var.Canonical -> IO Variable
116namedVar flex name = UF.fresh $ Descriptor
117 { structure = Nothing
118 , rank = noRank
119 , flex = flex
120 , name = Just name
121 , copy = Nothing
122 , mark = noMark
123 , alias = Nothing
124 }
126variable :: Flex -> IO Variable
127variable flex = UF.fresh $ Descriptor
128 { structure = Nothing
129 , rank = noRank
130 , flex = flex
131 , name = Nothing
132 , copy = Nothing
133 , mark = noMark
134 , alias = Nothing
135 }
138-- ex qs constraint == exists qs. constraint
139ex :: [Variable] -> TypeConstraint -> TypeConstraint
140ex fqs constraint@(A ann _) =
141 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
143-- fl qs constraint == forall qs. constraint
144fl :: [Variable] -> TypeConstraint -> TypeConstraint
145fl rqs constraint@(A ann _) =
146 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
148exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
149exists f = do
150 v <- liftIO $ variable Flexible
151 ex [v] <$> f (varN v)
153existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
154existsNumber f = do
155 v <- liftIO $ variable (Is Number)
156 ex [v] <$> f (varN v)
159instance Show a => Show (UF.Point a) where
160 show point = unsafePerformIO $ fmap show (UF.descriptor point)
163instance PrettyType a => PrettyType (UF.Point a) where
164 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
167instance PrettyType t => PrettyType (Annotated a t) where
168 pretty when (A _ e) = pretty when e
171instance PrettyType a => PrettyType (Term1 a) where
172 pretty when term =
173 let prty = pretty Never in
174 case term of
175 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
176 | otherwise -> parensIf needed (px <+> pretty App x)
177 where
178 px = prty f
179 needed = case when of
180 App -> True
181 _ -> False
183 Fun1 arg body ->
184 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
185 where
186 needed = case when of
187 Never -> False
188 _ -> True
190 Var1 x -> prty x
192 EmptyRecord1 -> P.braces P.empty
194 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
195 where
196 prettyExt = prty ext
197 extend | P.render prettyExt == "{}" = P.empty
198 | otherwise = prettyExt <+> P.text "|"
199 mkPretty f t = P.text f <+> P.text ":" <+> prty t
200 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
203instance PrettyType a => PrettyType (TermN a) where
204 pretty when term =
205 case term of
206 VarN alias x -> either alias (pretty when x)
207 TermN alias t1 -> either alias (pretty when t1)
208 where
209 either maybeAlias doc =
210 case maybeAlias of
211 Just alias -> PP.pretty alias
212 Nothing -> doc
214instance PrettyType Descriptor where
215 pretty when desc =
216 case (structure desc, name desc) of
217 (Just term, _) -> pretty when term
218 (_, Just name)
219 | Var.isTuple name ->
220 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
221 | otherwise ->
222 P.text (Var.toString name)
224 _ -> P.text "?"
227instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
228 pretty _ constraint =
229 let prty = pretty Never in
230 case constraint of
231 CTrue -> P.text "True"
232 CSaveEnv -> P.text "SaveTheEnvironment!!!"
233 CEqual a b -> prty a <+> P.text "=" <+> prty b
234 CAnd [] -> P.text "True"
236 CAnd cs ->
237 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
239 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
240 P.sep [ binder, pretty Never c ]
241 where
242 mergeExists vs (A _ c) =
243 case c of
244 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
245 _ -> (vs, c)
247 (fqs', c) = mergeExists fqs constraint
249 binder = if null fqs' then P.empty else
250 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
252 CLet schemes constraint ->
253 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
254 , P.text "in", pretty Never constraint ]
256 CInstance name tipe ->
257 P.text name <+> P.text "<" <+> prty tipe
259instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
260 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
261 P.sep [ forall, cs, headers' ]
262 where
263 prty = pretty Never
265 forall = if null rqs && null fqs then P.empty else
266 P.text "\x2200" <+> frees <+> rigids
268 frees = P.hsep $ map prty fqs
269 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
271 cs = case constraint of
272 CTrue -> P.empty
273 CAnd [] -> P.empty
274 _ -> P.brackets (pretty Never constraint)
276 headers' = if Map.size headers > 0 then dict else P.empty
277 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
278 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
281extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
282extraPretty t = pretty Never <$> addNames t
284addNames :: (Crawl t) => t -> IO t
285addNames value = do
286 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
287 let vars = map head . List.group $ List.sort rawVars
288 suffix s = map (++s) (map (:[]) ['a'..'z'])
289 allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
290 okayVars = filter (`notElem` vars) allVars
291 runStateT (crawl rename value) (okayVars, 0, 0, 0)
292 return value
293 where
294 getNames desc state@(vars, a, b, c) =
295 let name' = name desc in
296 case name' of
297 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
298 _ -> (name', state)
300 rename desc state@(vars, a, b, c) =
301 case name desc of
302 Just var -> (Just var, state)
303 Nothing ->
304 case flex desc of
305 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
306 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
307 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
308 _ -> (local $ head vars, (tail vars, a, b, c))
309 where
310 local v = Just (Var.local v)
312type CrawlState = ([String], Int, Int, Int)
314-- Code for traversing all the type data-structures and giving
315-- names to the variables embedded deep in there.
316class Crawl t where
317 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
318 -> t
319 -> StateT CrawlState IO t
321instance Crawl e => Crawl (Annotated a e) where
322 crawl nextState (A ann e) = A ann <$> crawl nextState e
324instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
325 crawl nextState constraint =
326 let rnm = crawl nextState in
327 case constraint of
328 CTrue -> return CTrue
329 CSaveEnv -> return CSaveEnv
330 CEqual a b -> CEqual <$> rnm a <*> rnm b
331 CAnd cs -> CAnd <$> crawl nextState cs
332 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
333 CInstance name tipe -> CInstance name <$> rnm tipe
335instance Crawl a => Crawl [a] where
336 crawl nextState list = mapM (crawl nextState) list
338instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
339 crawl nextState (Scheme rqs fqs c headers) =
340 let rnm = crawl nextState in
341 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
343instance Crawl t => Crawl (TermN t) where
344 crawl nextState tipe =
345 case tipe of
346 VarN a x -> VarN a <$> crawl nextState x
347 TermN a term -> TermN a <$> crawl nextState term
349instance Crawl t => Crawl (Term1 t) where
350 crawl nextState term =
351 let rnm = crawl nextState in
352 case term of
353 App1 a b -> App1 <$> rnm a <*> rnm b
354 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
355 Var1 a -> Var1 <$> rnm a
356 EmptyRecord1 -> return EmptyRecord1
357 Record1 fields ext ->
358 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
360instance Crawl a => Crawl (UF.Point a) where
361 crawl nextState point = do
362 desc <- liftIO $ UF.descriptor point
363 desc' <- crawl nextState desc
364 liftIO $ UF.setDescriptor point desc'
365 return point
367instance Crawl Descriptor where
368 crawl nextState desc = do
369 state <- get
370 let (name', state') = nextState desc state
371 structure' <- traverse (crawl nextState) (structure desc)
372 put state'
373 return $ desc { name = name', structure = structure' }
376toSrcType :: Variable -> IO T.CanonicalType
377toSrcType var =
378 do desc <- UF.descriptor =<< addNames var
379 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
380 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
381 where
382 backupSrcType desc =
383 case name desc of
384 Just v@(Var.Canonical _ x@(c:_))
385 | Char.isLower c -> return (T.Var x)
386 | otherwise -> return $ T.Type v
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 var) ]
393 termToSrcType term =
394 case term of
395 App1 a b -> do
396 a' <- toSrcType a
397 b' <- toSrcType b
398 case a' of
399 T.App f args -> return $ T.App f (args ++ [b'])
400 _ -> return $ T.App a' [b']
402 Fun1 a b -> T.Lambda <$> toSrcType a <*> toSrcType b
404 Var1 a -> toSrcType a
406 EmptyRecord1 -> return $ T.Record [] Nothing
408 Record1 tfields extension -> do
409 fields' <- traverse (mapM toSrcType) tfields
410 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
411 ext' <- toSrcType extension
412 return $ case ext' of
413 T.Record fs ext -> T.Record (fs ++ fields) ext
414 T.Var _ -> T.Record fields (Just ext')
415 _ -> error "Used toSrcType on a type that is not well-formed"
418data AppStructure = List Variable | Tuple [Variable] | Other
420collectApps :: Variable -> IO AppStructure
421collectApps var = go [] var
422 where
423 go vars var = do
424 desc <- UF.descriptor var
425 case (structure desc, vars) of
426 (Nothing, [v]) -> case name desc of
427 Just n | Var.isList n -> return (List v)
428 _ -> return Other
429 (Nothing, vs) -> case name desc of
430 Just n | Var.isTuple n -> return (Tuple vs)
431 _ -> return Other
432 (Just term, _) -> case term of
433 App1 a b -> go (vars ++ [b]) a
434 _ -> return Other