git.iko.soy/elk
on edfca84 help sign in
elk/src/Type/Type.hs
513 lines 14 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 (StateT, get, put, execStateT, runStateT)
12import Control.Monad.Error (ErrorT, Error, liftIO)
13import Data.Traversable (traverse)
14import AST.Annotation
15import qualified AST.PrettyPrint as PP
16import qualified AST.Type as T
17import 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
28data TermN a
29 = VarN (Maybe Var.Canonical) a
30 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
33varN :: a -> TermN a
34varN = VarN Nothing
37termN :: (Term1 (TermN a)) -> TermN a
38termN = TermN Nothing
41record :: Map.Map String [TermN a] -> TermN a -> TermN a
42record fs rec = termN (Record1 fs rec)
45type Type = TermN Variable
48type Variable = UF.Point Descriptor
51type SchemeName = String
54type TypeName = Var.Canonical
57type Constraint a b = Located (BasicConstraint a b)
60data BasicConstraint a b
61 = CTrue
62 | CSaveEnv
63 | CEqual a a
64 | CAnd [Constraint a b]
65 | CLet [Scheme a b] (Constraint a b)
66 | CInstance SchemeName a
69data Scheme a b = Scheme
70 { rigidQuantifiers :: [b]
71 , flexibleQuantifiers :: [b]
72 , constraint :: Constraint a b
73 , header :: Map.Map String a
74 }
77type TypeConstraint = Constraint Type Variable
79type TypeScheme = Scheme Type Variable
82monoscheme :: Map.Map String a -> Scheme a b
83monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
86infixl 8 /\
88(/\) :: Constraint a b -> Constraint a b -> Constraint a b
89a@(A _ c1) /\ b@(A _ c2) =
90 case (c1, c2) of
91 (CTrue, _) -> b
92 (_, CTrue) -> a
93 _ -> mergeOldDocs a b (CAnd [a,b])
96infixr 9 ==>
98(==>) :: Type -> Type -> Type
99a ==> b = termN (Fun1 a b)
102(<|) :: TermN a -> TermN a -> TermN a
103f <| a = termN (App1 f a)
106data Descriptor = Descriptor
107 { structure :: Maybe (Term1 Variable)
108 , rank :: Int
109 , flex :: Flex
110 , name :: Maybe TypeName
111 , copy :: Maybe Variable
112 , mark :: Int
113 , alias :: Maybe Var.Canonical
114 }
117noRank :: Int
118noRank = -1
121outermostRank :: Int
122outermostRank = 0
125noMark :: Int
126noMark = 0
129initialMark :: Int
130initialMark = 1
133data Flex
134 = Rigid
135 | Flexible
136 | Constant
137 | Is SuperType
138 deriving (Eq)
141data SuperType
142 = Number
143 | Comparable
144 | Appendable
145 deriving (Eq)
148namedVar :: Flex -> Var.Canonical -> IO Variable
149namedVar flex name = UF.fresh $ Descriptor
150 { structure = Nothing
151 , rank = noRank
152 , flex = flex
153 , name = Just name
154 , copy = Nothing
155 , mark = noMark
156 , alias = Nothing
157 }
160variable :: Flex -> IO Variable
161variable flex = UF.fresh $ Descriptor
162 { structure = Nothing
163 , rank = noRank
164 , flex = flex
165 , name = Nothing
166 , copy = Nothing
167 , mark = noMark
168 , alias = Nothing
169 }
172-- ex qs constraint == exists qs. constraint
173ex :: [Variable] -> TypeConstraint -> TypeConstraint
174ex fqs constraint@(A ann _) =
175 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
178-- fl qs constraint == forall qs. constraint
179fl :: [Variable] -> TypeConstraint -> TypeConstraint
180fl rqs constraint@(A ann _) =
181 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
184exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
185exists f =
186 do v <- liftIO $ variable Flexible
187 ex [v] <$> f (varN v)
190existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
191existsNumber f =
192 do v <- liftIO $ variable (Is Number)
193 ex [v] <$> f (varN v)
196-- TYPES TO PRETTY STRINGS
198instance PrettyType a => PrettyType (UF.Point a) where
199 pretty when point =
200 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
203instance PrettyType t => PrettyType (Annotated a t) where
204 pretty when (A _ e) =
205 pretty when e
208instance PrettyType a => PrettyType (Term1 a) where
209 pretty when term =
210 let prty = pretty Never in
211 case term of
212 App1 f x ->
213 parensIf needed (px <+> pretty App x)
214 where
215 px = prty f
216 needed = case when of
217 App -> True
218 _ -> False
220 Fun1 arg body ->
221 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
222 where
223 needed = case when of
224 Never -> False
225 _ -> True
227 Var1 x -> prty x
229 EmptyRecord1 -> P.braces P.empty
231 Record1 fields ext ->
232 P.braces (extend <+> commaSep prettyFields)
233 where
234 prettyExt = prty ext
235 extend | P.render prettyExt == "{}" = P.empty
236 | otherwise = prettyExt <+> P.text "|"
237 mkPretty f t = P.text f <+> P.text ":" <+> prty t
238 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
241instance PrettyType a => PrettyType (TermN a) where
242 pretty when term =
243 case term of
244 VarN alias x -> either alias (pretty when x)
245 TermN alias t1 -> either alias (pretty when t1)
246 where
247 either maybeAlias doc =
248 case maybeAlias of
249 Just alias -> PP.pretty alias
250 Nothing -> doc
253instance PrettyType Descriptor where
254 pretty when desc = do
255 case (alias desc, structure desc, name desc) of
256 (Just name, _, _) -> PP.pretty name
257 (_, Just term, _) -> pretty when term
258 (_, _, Just name)
259 | Var.isTuple name ->
260 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
261 | otherwise ->
262 P.text (Var.toString name)
264 _ -> P.text "?"
267instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
268 pretty _ constraint =
269 let prty = pretty Never in
270 case constraint of
271 CTrue -> P.text "True"
272 CSaveEnv -> P.text "SaveTheEnvironment!!!"
273 CEqual a b -> prty a <+> P.text "=" <+> prty b
274 CAnd [] -> P.text "True"
276 CAnd cs ->
277 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
279 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
280 P.sep [ binder, pretty Never c ]
281 where
282 mergeExists vs (A _ c) =
283 case c of
284 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
285 _ -> (vs, c)
287 (fqs', c) = mergeExists fqs constraint
289 binder = if null fqs' then P.empty else
290 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
292 CLet schemes constraint ->
293 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
294 , P.text "in", pretty Never constraint ]
296 CInstance name tipe ->
297 P.text name <+> P.text "<" <+> prty tipe
300instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
301 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
302 P.sep [ forall, cs, headers' ]
303 where
304 prty = pretty Never
306 forall = if null rqs && null fqs then P.empty else
307 P.text "\x2200" <+> frees <+> rigids
309 frees = P.hsep $ map prty fqs
310 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
312 cs = case constraint of
313 CTrue -> P.empty
314 CAnd [] -> P.empty
315 _ -> P.brackets (pretty Never constraint)
317 headers' = if Map.size headers > 0 then dict else P.empty
318 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
319 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
322extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
323extraPretty t = pretty Never <$> addNames t
326-- ADDING NAMES TO TYPES
328addNames :: (Crawl t) => t -> IO t
329addNames value = do
330 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
331 let vars = map head . List.group $ List.sort rawVars
332 suffix s = map (++s) (map (:[]) ['a'..'z'])
333 allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
334 okayVars = filter (`notElem` vars) allVars
335 runStateT (crawl rename value) (okayVars, 0, 0, 0)
336 return value
337 where
338 getNames desc state@(vars, a, b, c) =
339 let name' = name desc in
340 case name' of
341 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
342 _ -> (name', state)
344 rename desc state@(vars, a, b, c) =
345 case name desc of
346 Just var -> (Just var, state)
347 Nothing ->
348 case flex desc of
349 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
350 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
351 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
352 _ -> (local $ head vars, (tail vars, a, b, c))
353 where
354 local v = Just (Var.local v)
357-- CRAWLING OVER TYPES
359type CrawlState = ([String], Int, Int, Int)
362-- Code for traversing all the type data-structures and giving
363-- names to the variables embedded deep in there.
364class Crawl t where
365 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
366 -> t
367 -> StateT CrawlState IO t
370instance Crawl e => Crawl (Annotated a e) where
371 crawl nextState (A ann e) = A ann <$> crawl nextState e
374instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
375 crawl nextState constraint =
376 let rnm = crawl nextState in
377 case constraint of
378 CTrue -> return CTrue
379 CSaveEnv -> return CSaveEnv
380 CEqual a b -> CEqual <$> rnm a <*> rnm b
381 CAnd cs -> CAnd <$> crawl nextState cs
382 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
383 CInstance name tipe -> CInstance name <$> rnm tipe
386instance Crawl a => Crawl [a] where
387 crawl nextState list = mapM (crawl nextState) list
390instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
391 crawl nextState (Scheme rqs fqs c headers) =
392 let rnm = crawl nextState
393 in
394 Scheme
395 <$> rnm rqs
396 <*> rnm fqs
397 <*> crawl nextState c
398 <*> return headers
401instance Crawl t => Crawl (TermN t) where
402 crawl nextState tipe =
403 case tipe of
404 VarN a x ->
405 VarN a <$> crawl nextState x
407 TermN a term ->
408 TermN a <$> crawl nextState term
411instance Crawl t => Crawl (Term1 t) where
412 crawl nextState term =
413 let rnm = crawl nextState in
414 case term of
415 App1 a b -> App1 <$> rnm a <*> rnm b
416 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
417 Var1 a -> Var1 <$> rnm a
418 EmptyRecord1 -> return EmptyRecord1
419 Record1 fields ext ->
420 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
423instance Crawl a => Crawl (UF.Point a) where
424 crawl nextState point =
425 do desc <- liftIO $ UF.descriptor point
426 desc' <- crawl nextState desc
427 liftIO $ UF.setDescriptor point desc'
428 return point
431instance Crawl Descriptor where
432 crawl nextState desc =
433 do state <- get
434 let (name', state') = nextState desc state
435 structure' <- traverse (crawl nextState) (structure desc)
436 put state'
437 return $ desc { name = name', structure = structure' }
440toSrcType :: Variable -> IO T.CanonicalType
441toSrcType var =
442 go =<< addNames var
443 where
444 go v =
445 do desc <- UF.descriptor v
446 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
447 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
449 backupSrcType desc =
450 case name desc of
451 Just v@(Var.Canonical _ x@(c:_))
452 | Char.isLower c -> return (T.Var x)
453 | otherwise -> return $ T.Type v
455 _ -> error $ concat
456 [ "Problem converting the following type "
457 , "from a type-checker type to a source-syntax type:"
458 , P.render (pretty Never var) ]
460 termToSrcType term =
461 case term of
462 App1 a b -> do
463 a' <- go a
464 b' <- go b
465 case a' of
466 T.App f args -> return $ T.App f (args ++ [b'])
467 _ -> return $ T.App a' [b']
469 Fun1 a b -> T.Lambda <$> go a <*> go b
471 Var1 a -> go a
473 EmptyRecord1 -> return $ T.Record [] Nothing
475 Record1 tfields extension -> do
476 fields' <- traverse (mapM go) tfields
477 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
478 ext' <- dealias <$> go extension
479 return $ case ext' of
480 T.Record fs ext -> T.Record (fs ++ fields) ext
481 T.Var _ -> T.Record fields (Just ext')
482 _ -> error "Used toSrcType on a type that is not well-formed"
484 dealias :: T.CanonicalType -> T.CanonicalType
485 dealias t =
486 case t of
487 T.Aliased _ t' -> t'
488 _ -> t
491data AppStructure = List Variable | Tuple [Variable] | Other
494collectApps :: Variable -> IO AppStructure
495collectApps var = go [] var
496 where
497 go vars var = do
498 desc <- UF.descriptor var
499 case (structure desc, vars) of
500 (Nothing, [v]) ->
501 case name desc of
502 Just n | Var.isList n -> return (List v)
503 _ -> return Other
505 (Nothing, vs) ->
506 case name desc of
507 Just n | Var.isTuple n -> return (Tuple vs)
508 _ -> return Other
510 (Just term, _) ->
511 case term of
512 App1 a b -> go (vars ++ [b]) a
513 _ -> return Other