git.iko.soy/elk
on b10c2ea help sign in
elk/src/Type/Type.hs
577 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
20-- CONCRETE TYPES
22type Type = TermN Variable
24type Variable = UF.Point Descriptor
26type TypeConstraint = Constraint Type Variable
28type TypeScheme = Scheme Type Variable
31-- TYPE PRIMITIVES
33data Term1 a
34 = App1 a a
35 | Fun1 a a
36 | Var1 a
37 | EmptyRecord1
38 | Record1 (Map.Map String [a]) a
41data TermN a
42 = VarN (Maybe Var.Canonical) a
43 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
46varN :: a -> TermN a
47varN =
48 VarN Nothing
51termN :: (Term1 (TermN a)) -> TermN a
52termN =
53 TermN Nothing
56record :: Map.Map String [TermN a] -> TermN a -> TermN a
57record fs rec =
58 termN (Record1 fs rec)
61-- DESCRIPTORS
63data Descriptor = Descriptor
64 { structure :: Maybe (Term1 Variable)
65 , rank :: Int
66 , flex :: Flex
67 , name :: Maybe TypeName
68 , copy :: Maybe Variable
69 , mark :: Int
70 , alias :: Maybe Var.Canonical
71 }
73noRank :: Int
74noRank = -1
76outermostRank :: Int
77outermostRank = 0
79noMark :: Int
80noMark = 0
82initialMark :: Int
83initialMark = 1
85data Flex
86 = Rigid
87 | Flexible
88 | Constant
89 | Is SuperType
90 deriving (Eq)
92data SuperType
93 = Number
94 | Comparable
95 | Appendable
96 deriving (Eq)
99-- CONSTRAINTS
101type Constraint a b =
102 Located (BasicConstraint a b)
104data BasicConstraint a b
105 = CTrue
106 | CSaveEnv
107 | CEqual a a
108 | CAnd [Constraint a b]
109 | CLet [Scheme a b] (Constraint a b)
110 | CInstance SchemeName a
112type SchemeName = String
114type TypeName = Var.Canonical
116data Scheme a b = Scheme
117 { rigidQuantifiers :: [b]
118 , flexibleQuantifiers :: [b]
119 , constraint :: Constraint a b
120 , header :: Map.Map String a
121 }
124-- TYPE HELPERS
126infixr 9 ==>
128(==>) :: Type -> Type -> Type
129(==>) a b =
130 termN (Fun1 a b)
133(<|) :: TermN a -> TermN a -> TermN a
134(<|) f a =
135 termN (App1 f a)
138-- VARIABLE HELPERS
140namedVar :: Flex -> Var.Canonical -> IO Variable
141namedVar flex name = UF.fresh $ Descriptor
142 { structure = Nothing
143 , rank = noRank
144 , flex = flex
145 , name = Just name
146 , copy = Nothing
147 , mark = noMark
148 , alias = Nothing
149 }
152variable :: Flex -> IO Variable
153variable flex = UF.fresh $ Descriptor
154 { structure = Nothing
155 , rank = noRank
156 , flex = flex
157 , name = Nothing
158 , copy = Nothing
159 , mark = noMark
160 , alias = Nothing
161 }
164-- CONSTRAINT HELPERS
166monoscheme :: Map.Map String a -> Scheme a b
167monoscheme headers =
168 Scheme [] [] (noneNoDocs CTrue) headers
171infixl 8 /\
173(/\) :: Constraint a b -> Constraint a b -> Constraint a b
174(/\) a@(A _ c1) b@(A _ c2) =
175 case (c1, c2) of
176 (CTrue, _) -> b
177 (_, CTrue) -> a
178 _ -> mergeOldDocs a b (CAnd [a,b])
181-- ex qs constraint == exists qs. constraint
182ex :: [Variable] -> TypeConstraint -> TypeConstraint
183ex fqs constraint@(A ann _) =
184 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
187-- fl qs constraint == forall qs. constraint
188fl :: [Variable] -> TypeConstraint -> TypeConstraint
189fl rqs constraint@(A ann _) =
190 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
193exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
194exists f =
195 do v <- liftIO $ variable Flexible
196 ex [v] <$> f (varN v)
199existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
200existsNumber f =
201 do v <- liftIO $ variable (Is Number)
202 ex [v] <$> f (varN v)
205-- TYPES TO PRETTY STRINGS
207instance PrettyType a => PrettyType (UF.Point a) where
208 pretty when point =
209 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
212instance PrettyType t => PrettyType (Annotated a t) where
213 pretty when (A _ e) =
214 pretty when e
217instance PrettyType a => PrettyType (Term1 a) where
218 pretty when term =
219 let prty = pretty Never in
220 case term of
221 App1 f x ->
222 parensIf needed (px <+> pretty App x)
223 where
224 px = prty f
225 needed =
226 case when of
227 App -> True
228 _ -> False
230 Fun1 arg body ->
231 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
232 where
233 needed =
234 case when of
235 Never -> False
236 _ -> True
238 Var1 x ->
239 prty x
241 EmptyRecord1 ->
242 P.braces P.empty
244 Record1 fields ext ->
245 P.braces (extend <+> commaSep prettyFields)
246 where
247 prettyExt = prty ext
249 extend
250 | P.render prettyExt == "{}" =
251 P.empty
252 | otherwise =
253 prettyExt <+> P.text "|"
255 mkPretty f t =
256 P.text f <+> P.text ":" <+> prty t
258 prettyFields =
259 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
262instance PrettyType a => PrettyType (TermN a) where
263 pretty when term =
264 case term of
265 VarN alias x ->
266 either alias (pretty when x)
268 TermN alias t1 ->
269 either alias (pretty when t1)
270 where
271 either maybeAlias doc =
272 case maybeAlias of
273 Just alias -> PP.pretty alias
274 Nothing -> doc
277instance PrettyType Descriptor where
278 pretty when desc =
279 case (alias desc, structure desc, name desc) of
280 (Just name, _, _) ->
281 PP.pretty name
283 (_, Just term, _) ->
284 pretty when term
286 (_, _, Just name)
287 | Var.isTuple name ->
288 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
289 | otherwise ->
290 P.text (Var.toString name)
292 _ -> P.text "?"
295instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
296 pretty _ constraint =
297 let prty = pretty Never in
298 case constraint of
299 CTrue -> P.text "True"
300 CSaveEnv -> P.text "SaveTheEnvironment!!!"
301 CEqual a b -> prty a <+> P.text "=" <+> prty b
302 CAnd [] -> P.text "True"
304 CAnd cs ->
305 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
307 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
308 P.sep [ binder, pretty Never c ]
309 where
310 mergeExists vs (A _ c) =
311 case c of
312 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
313 _ -> (vs, c)
315 (fqs', c) = mergeExists fqs constraint
317 binder = if null fqs' then P.empty else
318 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
320 CLet schemes constraint ->
321 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
322 , P.text "in", pretty Never constraint ]
324 CInstance name tipe ->
325 P.text name <+> P.text "<" <+> prty tipe
328instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
329 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
330 P.sep [ forall, cs, headers' ]
331 where
332 prty = pretty Never
334 forall = if null rqs && null fqs then P.empty else
335 P.text "\x2200" <+> frees <+> rigids
337 frees = P.hsep $ map prty fqs
338 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
340 cs = case constraint of
341 CTrue -> P.empty
342 CAnd [] -> P.empty
343 _ -> P.brackets (pretty Never constraint)
345 headers' = if Map.size headers > 0 then dict else P.empty
346 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
347 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
350extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
351extraPretty t =
352 pretty Never <$> addNames t
355-- ADDING NAMES TO TYPES
357addNames :: (Crawl t) => t -> IO t
358addNames value =
359 do (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
361 let vars = map head . List.group $ List.sort rawVars
363 let suffix s = map (++s) (map (:[]) ['a'..'z'])
365 let allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
367 let okayVars = filter (`notElem` vars) allVars
369 runStateT (crawl rename value) (okayVars, 0, 0, 0)
371 return value
372 where
373 getNames desc state@(vars, a, b, c) =
374 let name' = name desc in
375 case name' of
376 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
377 _ -> (name', state)
379 rename desc state@(vars, a, b, c) =
380 case name desc of
381 Just var -> (Just var, state)
382 Nothing ->
383 case flex desc of
384 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
385 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
386 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
387 _ -> (local $ head vars, (tail vars, a, b, c))
388 where
389 local v = Just (Var.local v)
392-- CRAWLING OVER TYPES
394type CrawlState = ([String], Int, Int, Int)
397-- Code for traversing all the type data-structures and giving
398-- names to the variables embedded deep in there.
399class Crawl t where
400 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
401 -> t
402 -> StateT CrawlState IO t
405instance Crawl e => Crawl (Annotated a e) where
406 crawl nextState (A ann e) =
407 A ann <$> crawl nextState e
410instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
411 crawl nextState constraint =
412 let rnm = crawl nextState in
413 case constraint of
414 CTrue -> return CTrue
415 CSaveEnv -> return CSaveEnv
416 CEqual a b -> CEqual <$> rnm a <*> rnm b
417 CAnd cs -> CAnd <$> crawl nextState cs
418 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
419 CInstance name tipe -> CInstance name <$> rnm tipe
422instance Crawl a => Crawl [a] where
423 crawl nextState list =
424 mapM (crawl nextState) list
427instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
428 crawl nextState (Scheme rqs fqs c headers) =
429 let rnm = crawl nextState
430 in
431 Scheme
432 <$> rnm rqs
433 <*> rnm fqs
434 <*> crawl nextState c
435 <*> return headers
438instance Crawl t => Crawl (TermN t) where
439 crawl nextState tipe =
440 case tipe of
441 VarN a x ->
442 VarN a <$> crawl nextState x
444 TermN a term ->
445 TermN a <$> crawl nextState term
448instance Crawl t => Crawl (Term1 t) where
449 crawl nextState term =
450 let rnm = crawl nextState in
451 case term of
452 App1 a b ->
453 App1 <$> rnm a <*> rnm b
455 Fun1 a b ->
456 Fun1 <$> rnm a <*> rnm b
458 Var1 a ->
459 Var1 <$> rnm a
461 EmptyRecord1 ->
462 return EmptyRecord1
464 Record1 fields ext ->
465 Record1
466 <$> traverse (mapM rnm) fields
467 <*> rnm ext
470instance Crawl a => Crawl (UF.Point a) where
471 crawl nextState point =
472 do desc <- liftIO $ UF.descriptor point
473 desc' <- crawl nextState desc
474 liftIO $ UF.setDescriptor point desc'
475 return point
478instance Crawl Descriptor where
479 crawl nextState desc =
480 do state <- get
481 let (name', state') = nextState desc state
482 structure' <- traverse (crawl nextState) (structure desc)
483 put state'
484 return $ desc { name = name', structure = structure' }
487toSrcType :: Variable -> IO T.CanonicalType
488toSrcType var =
489 go =<< addNames var
490 where
491 go v =
492 do desc <- UF.descriptor v
493 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
494 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
496 backupSrcType :: Descriptor -> IO T.CanonicalType
497 backupSrcType desc =
498 case name desc of
499 Just v@(Var.Canonical _ x@(c:_))
500 | Char.isLower c ->
501 return (T.Var x)
502 | otherwise ->
503 return $ T.Type v
505 _ ->
506 error $
507 concat
508 [ "Problem converting the following type "
509 , "from a type-checker type to a source-syntax type:"
510 , P.render (pretty Never var)
511 ]
513 termToSrcType :: Term1 Variable -> IO T.CanonicalType
514 termToSrcType term =
515 case term of
516 App1 a b ->
517 do a' <- go a
518 b' <- go b
519 case a' of
520 T.App f args ->
521 return $ T.App f (args ++ [b'])
522 _ ->
523 return $ T.App a' [b']
525 Fun1 a b ->
526 T.Lambda <$> go a <*> go b
528 Var1 a ->
529 go a
531 EmptyRecord1 ->
532 return $ T.Record [] Nothing
534 Record1 tfields extension ->
535 do fields' <- traverse (mapM go) tfields
536 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
537 ext' <- dealias <$> go extension
538 return $
539 case ext' of
540 T.Record fs ext -> T.Record (fs ++ fields) ext
541 T.Var _ -> T.Record fields (Just ext')
542 _ -> error "Used toSrcType on a type that is not well-formed"
544 dealias :: T.CanonicalType -> T.CanonicalType
545 dealias t =
546 case t of
547 T.Aliased _ t' -> t'
548 _ -> t
551data AppStructure
552 = List Variable
553 | Tuple [Variable]
554 | Other
557collectApps :: Variable -> IO AppStructure
558collectApps var =
559 go [] var
560 where
561 go vars var = do
562 desc <- UF.descriptor var
563 case (structure desc, vars) of
564 (Nothing, [v]) ->
565 case name desc of
566 Just n | Var.isList n -> return (List v)
567 _ -> return Other
569 (Nothing, vs) ->
570 case name desc of
571 Just n | Var.isTuple n -> return (Tuple vs)
572 _ -> return Other
574 (Just term, _) ->
575 case term of
576 App1 a b -> go (vars ++ [b]) a
577 _ -> return Other