git.iko.soy/elk
on 8036fca help sign in
elk/src/Type/Type.hs
597 lines 15 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
20-- CONCRETE TYPES
22type Type = TermN Variable
24type Variable = UF.Point Descriptor
26type TypeConstraint = Constraint Type Variable
28type TypeScheme = Scheme Type Variable
30type Alias a = Maybe (Var.Canonical, [(String,a)])
33-- TYPE PRIMITIVES
35data Term1 a
36 = App1 a a
37 | Fun1 a a
38 | Var1 a
39 | EmptyRecord1
40 | Record1 (Map.Map String [a]) a
43data TermN a
44 = PlaceHolder String
45 | VarN (Alias (TermN a)) a
46 | TermN (Alias (TermN a)) (Term1 (TermN a))
49varN :: a -> TermN a
50varN =
51 VarN Nothing
54termN :: (Term1 (TermN a)) -> TermN a
55termN =
56 TermN Nothing
59record :: Map.Map String [TermN a] -> TermN a -> TermN a
60record fs rec =
61 termN (Record1 fs rec)
64-- DESCRIPTORS
66data Descriptor = Descriptor
67 { structure :: Maybe (Term1 Variable)
68 , rank :: Int
69 , flex :: Flex
70 , name :: Maybe TypeName
71 , copy :: Maybe Variable
72 , mark :: Int
73 , alias :: Alias Variable
74 }
76noRank :: Int
77noRank = -1
79outermostRank :: Int
80outermostRank = 0
82noMark :: Int
83noMark = 0
85initialMark :: Int
86initialMark = 1
88data Flex
89 = Rigid
90 | Flexible
91 | Constant
92 | Is SuperType
93 deriving (Eq)
95data SuperType
96 = Number
97 | Comparable
98 | Appendable
99 deriving (Eq)
102-- CONSTRAINTS
104type Constraint a b =
105 Located (BasicConstraint a b)
107data BasicConstraint a b
108 = CTrue
109 | CSaveEnv
110 | CEqual a a
111 | CAnd [Constraint a b]
112 | CLet [Scheme a b] (Constraint a b)
113 | CInstance SchemeName a
115type SchemeName = String
117type TypeName = Var.Canonical
119data Scheme a b = Scheme
120 { rigidQuantifiers :: [b]
121 , flexibleQuantifiers :: [b]
122 , constraint :: Constraint a b
123 , header :: Map.Map String a
124 }
127-- TYPE HELPERS
129infixr 9 ==>
131(==>) :: Type -> Type -> Type
132(==>) a b =
133 termN (Fun1 a b)
136(<|) :: TermN a -> TermN a -> TermN a
137(<|) f a =
138 termN (App1 f a)
141-- VARIABLE HELPERS
143namedVar :: Flex -> Var.Canonical -> IO Variable
144namedVar flex name = UF.fresh $ Descriptor
145 { structure = Nothing
146 , rank = noRank
147 , flex = flex
148 , name = Just name
149 , copy = Nothing
150 , mark = noMark
151 , alias = Nothing
152 }
155variable :: Flex -> IO Variable
156variable flex = UF.fresh $ Descriptor
157 { structure = Nothing
158 , rank = noRank
159 , flex = flex
160 , name = Nothing
161 , copy = Nothing
162 , mark = noMark
163 , alias = Nothing
164 }
167-- CONSTRAINT HELPERS
169monoscheme :: Map.Map String a -> Scheme a b
170monoscheme headers =
171 Scheme [] [] (noneNoDocs CTrue) headers
174infixl 8 /\
176(/\) :: Constraint a b -> Constraint a b -> Constraint a b
177(/\) a@(A _ c1) b@(A _ c2) =
178 case (c1, c2) of
179 (CTrue, _) -> b
180 (_, CTrue) -> a
181 _ -> mergeOldDocs a b (CAnd [a,b])
184-- ex qs constraint == exists qs. constraint
185ex :: [Variable] -> TypeConstraint -> TypeConstraint
186ex fqs constraint@(A ann _) =
187 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
190-- fl qs constraint == forall qs. constraint
191fl :: [Variable] -> TypeConstraint -> TypeConstraint
192fl rqs constraint@(A ann _) =
193 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
196exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
197exists f =
198 do v <- liftIO $ variable Flexible
199 ex [v] <$> f (varN v)
202existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
203existsNumber f =
204 do v <- liftIO $ variable (Is Number)
205 ex [v] <$> f (varN v)
208-- TYPES TO PRETTY STRINGS
210instance PrettyType a => PrettyType (UF.Point a) where
211 pretty when point =
212 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
215instance PrettyType t => PrettyType (Annotated a t) where
216 pretty when (A _ e) =
217 pretty when e
220instance PrettyType a => PrettyType (Term1 a) where
221 pretty when term =
222 let prty = pretty Never in
223 case term of
224 App1 f x ->
225 parensIf needed (px <+> pretty App x)
226 where
227 px = prty f
228 needed =
229 case when of
230 App -> True
231 _ -> False
233 Fun1 arg body ->
234 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
235 where
236 needed =
237 case when of
238 Never -> False
239 _ -> True
241 Var1 x ->
242 prty x
244 EmptyRecord1 ->
245 P.braces P.empty
247 Record1 fields ext ->
248 P.braces (extend <+> commaSep prettyFields)
249 where
250 prettyExt = prty ext
252 extend
253 | P.render prettyExt == "{}" =
254 P.empty
255 | otherwise =
256 prettyExt <+> P.text "|"
258 mkPretty f t =
259 P.text f <+> P.text ":" <+> prty t
261 prettyFields =
262 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
265instance PrettyType a => PrettyType (TermN a) where
266 pretty when term =
267 case term of
268 PlaceHolder _ ->
269 error "problem prettifying type, probably indicates a bigger problem"
271 VarN alias x ->
272 either alias (pretty when x)
274 TermN alias t1 ->
275 either alias (pretty when t1)
276 where
277 either maybeAlias doc =
278 case maybeAlias of
279 Nothing -> doc
280 Just (name, args) ->
281 P.hang (PP.pretty name) 2 (P.sep (map (pretty App . snd) args))
284instance PrettyType Descriptor where
285 pretty when desc =
286 case (alias desc, structure desc, name desc) of
287 (Just (name, args), _, _) ->
288 P.hang (PP.pretty name) 4 (P.sep (map (pretty App . snd) args))
290 (_, Just term, _) ->
291 pretty when term
293 (_, _, Just name)
294 | Var.isTuple name ->
295 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
296 | otherwise ->
297 P.text (Var.toString name)
299 _ -> P.text "?"
302instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
303 pretty _ constraint =
304 let prty = pretty Never in
305 case constraint of
306 CTrue -> P.text "True"
307 CSaveEnv -> P.text "SaveTheEnvironment!!!"
308 CEqual a b -> prty a <+> P.text "=" <+> prty b
309 CAnd [] -> P.text "True"
311 CAnd cs ->
312 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
314 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
315 P.sep [ binder, pretty Never c ]
316 where
317 mergeExists vs (A _ c) =
318 case c of
319 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
320 _ -> (vs, c)
322 (fqs', c) = mergeExists fqs constraint
324 binder = if null fqs' then P.empty else
325 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
327 CLet schemes constraint ->
328 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
329 , P.text "in", pretty Never constraint ]
331 CInstance name tipe ->
332 P.text name <+> P.text "<" <+> prty tipe
335instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
336 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
337 P.sep [ forall, cs, headers' ]
338 where
339 prty = pretty Never
341 forall = if null rqs && null fqs then P.empty else
342 P.text "\x2200" <+> frees <+> rigids
344 frees = P.hsep $ map prty fqs
345 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
347 cs = case constraint of
348 CTrue -> P.empty
349 CAnd [] -> P.empty
350 _ -> P.brackets (pretty Never constraint)
352 headers' = if Map.size headers > 0 then dict else P.empty
353 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
354 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
357extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
358extraPretty t =
359 pretty Never <$> addNames t
362-- ADDING NAMES TO TYPES
364addNames :: (Crawl t) => t -> IO t
365addNames value =
366 do (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
368 let vars = map head . List.group $ List.sort rawVars
370 let suffix s = map (++s) (map (:[]) ['a'..'z'])
372 let allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
374 let okayVars = filter (`notElem` vars) allVars
376 runStateT (crawl rename value) (okayVars, 0, 0, 0)
378 return value
379 where
380 getNames desc state@(vars, a, b, c) =
381 let name' = name desc in
382 case name' of
383 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
384 _ -> (name', state)
386 rename desc state@(vars, a, b, c) =
387 case name desc of
388 Just var -> (Just var, state)
389 Nothing ->
390 case flex desc of
391 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
392 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
393 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
394 _ -> (local $ head vars, (tail vars, a, b, c))
395 where
396 local v = Just (Var.local v)
399-- CRAWLING OVER TYPES
401type CrawlState = ([String], Int, Int, Int)
404-- Code for traversing all the type data-structures and giving
405-- names to the variables embedded deep in there.
406class Crawl t where
407 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
408 -> t
409 -> StateT CrawlState IO t
412instance Crawl e => Crawl (Annotated a e) where
413 crawl nextState (A ann e) =
414 A ann <$> crawl nextState e
417instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
418 crawl nextState constraint =
419 let rnm = crawl nextState in
420 case constraint of
421 CTrue -> return CTrue
422 CSaveEnv -> return CSaveEnv
423 CEqual a b -> CEqual <$> rnm a <*> rnm b
424 CAnd cs -> CAnd <$> crawl nextState cs
425 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
426 CInstance name tipe -> CInstance name <$> rnm tipe
429instance Crawl a => Crawl [a] where
430 crawl nextState list =
431 mapM (crawl nextState) list
434instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
435 crawl nextState (Scheme rqs fqs c headers) =
436 let rnm = crawl nextState
437 in
438 Scheme
439 <$> rnm rqs
440 <*> rnm fqs
441 <*> crawl nextState c
442 <*> return headers
445instance Crawl t => Crawl (TermN t) where
446 crawl nextState tipe =
447 case tipe of
448 PlaceHolder name ->
449 return (PlaceHolder name)
451 VarN a x ->
452 VarN a <$> crawl nextState x
454 TermN a term ->
455 TermN a <$> crawl nextState term
458instance Crawl t => Crawl (Term1 t) where
459 crawl nextState term =
460 let rnm = crawl nextState in
461 case term of
462 App1 a b ->
463 App1 <$> rnm a <*> rnm b
465 Fun1 a b ->
466 Fun1 <$> rnm a <*> rnm b
468 Var1 a ->
469 Var1 <$> rnm a
471 EmptyRecord1 ->
472 return EmptyRecord1
474 Record1 fields ext ->
475 Record1
476 <$> traverse (mapM rnm) fields
477 <*> rnm ext
480instance Crawl a => Crawl (UF.Point a) where
481 crawl nextState point =
482 do desc <- liftIO $ UF.descriptor point
483 desc' <- crawl nextState desc
484 liftIO $ UF.setDescriptor point desc'
485 return point
488instance Crawl Descriptor where
489 crawl nextState desc =
490 do state <- get
491 let (name', state') = nextState desc state
492 structure' <- traverse (crawl nextState) (structure desc)
493 put state'
494 return $ desc { name = name', structure = structure' }
497-- TODO: Attach resulting type to the descriptor so that you
498-- never have to do extra work, particularly nice for aliased types
499toSrcType :: Variable -> IO T.CanonicalType
500toSrcType var =
501 go =<< addNames var
502 where
503 go v =
504 do desc <- UF.descriptor v
505 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
506 case alias desc of
507 Nothing ->
508 return srcType
510 Just (name, args) ->
511 do args' <- mapM (\(arg,tvar) -> (,) arg <$> go tvar) args
512 return (T.Aliased name args' srcType)
514 backupSrcType :: Descriptor -> IO T.CanonicalType
515 backupSrcType desc =
516 case name desc of
517 Just v@(Var.Canonical _ x@(c:_))
518 | Char.isLower c ->
519 return (T.Var x)
520 | otherwise ->
521 return $ T.Type v
523 _ ->
524 error $
525 concat
526 [ "Problem converting the following type "
527 , "from a type-checker type to a source-syntax type:"
528 , P.render (pretty Never var)
529 ]
531 termToSrcType :: Term1 Variable -> IO T.CanonicalType
532 termToSrcType term =
533 case term of
534 App1 a b ->
535 do a' <- go a
536 b' <- go b
537 case a' of
538 T.App f args ->
539 return $ T.App f (args ++ [b'])
540 _ ->
541 return $ T.App a' [b']
543 Fun1 a b ->
544 T.Lambda <$> go a <*> go b
546 Var1 a ->
547 go a
549 EmptyRecord1 ->
550 return $ T.Record [] Nothing
552 Record1 tfields extension ->
553 do fields' <- traverse (mapM go) tfields
554 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
555 ext' <- dealias <$> go extension
556 return $
557 case ext' of
558 T.Record fs ext -> T.Record (fs ++ fields) ext
559 T.Var _ -> T.Record fields (Just ext')
560 _ -> error "Used toSrcType on a type that is not well-formed"
562 dealias :: T.CanonicalType -> T.CanonicalType
563 dealias tipe =
564 case tipe of
565 T.Aliased _ args tipe' ->
566 T.dealias args tipe'
567 _ ->
568 tipe
571data AppStructure
572 = List Variable
573 | Tuple [Variable]
574 | Other
577collectApps :: Variable -> IO AppStructure
578collectApps var =
579 go [] var
580 where
581 go vars var = do
582 desc <- UF.descriptor var
583 case (structure desc, vars) of
584 (Nothing, [v]) ->
585 case name desc of
586 Just n | Var.isList n -> return (List v)
587 _ -> return Other
589 (Nothing, vs) ->
590 case name desc of
591 Just n | Var.isTuple n -> return (Tuple vs)
592 _ -> return Other
594 (Just term, _) ->
595 case term of
596 App1 a b -> go (vars ++ [b]) a
597 _ -> return Other