git.iko.soy/elk
on b614df2 help sign in
elk/src/Type/Type.hs
649 lines 16 kB history raw
1module Type.Type where
3import Control.Monad.State (StateT)
4import qualified Control.Monad.State as State
5import qualified Data.Char as Char
6import qualified Data.Map as Map
7import qualified Data.Set as Set
8import qualified Data.Traversable as Traverse (traverse)
9import qualified Data.UnionFind.IO as UF
10import Text.PrettyPrint as P
11import System.IO.Unsafe
13import qualified AST.Type as T
14import qualified AST.Variable as Var
15import qualified Reporting.Annotation as A
16import qualified Reporting.Error.Type as Error
17import qualified Reporting.Region as R
18import Type.PrettyPrint
21-- CONCRETE TYPES
23type Type = TermN Variable
25type Variable = UF.Point Descriptor
27type TypeConstraint = Constraint Type Variable
29type TypeScheme = Scheme Type Variable
31type Alias a = Maybe (Var.Canonical, [(String,a)])
34-- TYPE PRIMITIVES
36data Term1 a
37 = App1 a a
38 | Fun1 a a
39 | Var1 a
40 | EmptyRecord1
41 | Record1 (Map.Map String [a]) a
44data TermN a
45 = PlaceHolder String
46 | VarN (Alias (TermN a)) a
47 | TermN (Alias (TermN a)) (Term1 (TermN a))
50varN :: a -> TermN a
51varN =
52 VarN Nothing
55termN :: (Term1 (TermN a)) -> TermN a
56termN =
57 TermN Nothing
60record :: Map.Map String [TermN a] -> TermN a -> TermN a
61record fs rec =
62 termN (Record1 fs rec)
65-- DESCRIPTORS
67data Descriptor = Descriptor
68 { structure :: Maybe (Term1 Variable)
69 , rank :: Int
70 , flex :: Flex
71 , name :: Maybe TypeName
72 , copy :: Maybe Variable
73 , mark :: Int
74 , alias :: Alias Variable
75 }
77noRank :: Int
78noRank = -1
80outermostRank :: Int
81outermostRank = 0
83noMark :: Int
84noMark = 0
86initialMark :: Int
87initialMark = 1
89data Flex
90 = Rigid
91 | Flexible
92 | Constant
93 | Is SuperType
94 | Error
95 deriving (Eq)
97data SuperType
98 = Number
99 | Comparable
100 | Appendable
101 deriving (Eq)
104-- CONSTRAINTS
106data Constraint a b
107 = CTrue
108 | CSaveEnv
109 | CEqual Error.Hint R.Region a a
110 | CAnd [Constraint a b]
111 | CLet [Scheme a b] (Constraint a b)
112 | CInstance R.Region SchemeName a
114type SchemeName = String
116type TypeName = Var.Canonical
118data Scheme a b = Scheme
119 { rigidQuantifiers :: [b]
120 , flexibleQuantifiers :: [b]
121 , constraint :: Constraint a b
122 , header :: Map.Map String (A.Located a)
123 }
126-- TYPE HELPERS
128infixr 9 ==>
130(==>) :: Type -> Type -> Type
131(==>) a b =
132 termN (Fun1 a b)
135(<|) :: TermN a -> TermN a -> TermN a
136(<|) f a =
137 termN (App1 f a)
140-- VARIABLE HELPERS
142namedVar :: Flex -> Var.Canonical -> IO Variable
143namedVar flex name = UF.fresh $ Descriptor
144 { structure = Nothing
145 , rank = noRank
146 , flex = flex
147 , name = Just name
148 , copy = Nothing
149 , mark = noMark
150 , alias = Nothing
151 }
154variable :: Flex -> IO Variable
155variable flex =
156 UF.fresh (descriptor flex)
159descriptor :: Flex -> Descriptor
160descriptor flex =
161 Descriptor
162 { structure = Nothing
163 , rank = noRank
164 , flex = flex
165 , name = Nothing
166 , copy = Nothing
167 , mark = noMark
168 , alias = Nothing
169 }
172-- CONSTRAINT HELPERS
174monoscheme :: Map.Map String (A.Located a) -> Scheme a b
175monoscheme headers =
176 Scheme [] [] CTrue headers
179infixl 8 /\
181(/\) :: Constraint a b -> Constraint a b -> Constraint a b
182(/\) c1 c2 =
183 case (c1, c2) of
184 (CTrue, _) -> c2
185 (_, CTrue) -> c1
186 _ -> CAnd [c1,c2]
189-- ex qs constraint == exists qs. constraint
190ex :: [Variable] -> TypeConstraint -> TypeConstraint
191ex fqs constraint =
192 CLet [Scheme [] fqs constraint Map.empty] CTrue
195-- fl qs constraint == forall qs. constraint
196fl :: [Variable] -> TypeConstraint -> TypeConstraint
197fl rqs constraint =
198 CLet [Scheme rqs [] constraint Map.empty] CTrue
201exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
202exists f =
203 do v <- variable Flexible
204 ex [v] <$> f (varN v)
207existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
208existsNumber f =
209 do v <- variable (Is Number)
210 ex [v] <$> f (varN v)
213-- TYPES TO PRETTY STRINGS
215instance PrettyType a => PrettyType (UF.Point a) where
216 pretty when point =
217 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
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
282 (P.text (Var.toString name))
283 2
284 (P.sep (map (pretty App . snd) args))
287instance PrettyType Descriptor where
288 pretty when desc =
289 case (alias desc, structure desc, name desc) of
290 (Just (name, args), _, _) ->
291 P.hang
292 (P.text (Var.toString name))
293 4
294 (P.sep (map (pretty App . snd) args))
296 (_, Just term, _) ->
297 pretty when term
299 (_, _, Just name)
300 | Var.isTuple name ->
301 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
302 | otherwise ->
303 P.text (Var.toString name)
305 _ -> P.text "?"
308instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
309 pretty _ constraint =
310 let prty = pretty Never in
311 case constraint of
312 CTrue ->
313 P.text "True"
315 CSaveEnv ->
316 P.text "SaveTheEnvironment!!!"
318 CEqual _ _ a b ->
319 prty a <+> P.text "=" <+> prty b
321 CAnd [] ->
322 P.text "True"
324 CAnd cs ->
325 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
327 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
328 P.sep [ binder, pretty Never c ]
329 where
330 mergeExists vs c =
331 case c of
332 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
333 _ -> (vs, c)
335 (fqs', c) = mergeExists fqs constraint
337 binder =
338 if null fqs'
339 then P.empty
340 else
341 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
343 CLet schemes constraint ->
344 P.fsep
345 [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
346 , P.text "in", pretty Never constraint
347 ]
349 CInstance _region name tipe ->
350 P.text name <+> P.text "<" <+> prty tipe
353instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
354 pretty _ (Scheme rqs fqs constraint headers) =
355 P.sep [ forall, cs, headers' ]
356 where
357 prty = pretty Never
359 forall =
360 if null rqs && null fqs
361 then P.empty
362 else P.text "\x2200" <+> frees <+> rigids
364 frees = P.hsep (map prty fqs)
366 rigids =
367 if null rqs
368 then P.empty
369 else P.braces . P.hsep $ map prty rqs
371 cs =
372 case constraint of
373 CTrue -> P.empty
374 CAnd [] -> P.empty
375 _ -> P.brackets (pretty Never constraint)
377 headers' =
378 if Map.size headers > 0 then dict else P.empty
380 dict =
381 P.parens . commaSep . map prettyPair $ Map.toList headers
383 prettyPair (fieldName, A.A _ tipe) =
384 P.text fieldName <+> P.text ":" <+> pretty Never tipe
387-- CONVERT TO SOURCE TYPES
389-- TODO: Attach resulting type to the descriptor so that you
390-- never have to do extra work, particularly nice for aliased types
391toSrcType :: Variable -> IO T.Canonical
392toSrcType variable =
393 do addNames variable
394 variableToSrcType variable variable
397variableToSrcType :: Variable -> Variable -> IO T.Canonical
398variableToSrcType rootVariable variable =
399 do desc <- UF.descriptor variable
400 srcType <- maybe (backupSrcType desc) (termToSrcType rootVariable) (structure desc)
401 case alias desc of
402 Nothing ->
403 return srcType
405 Just (name, args) ->
406 case srcType of
407 T.Type (Var.Canonical Var.BuiltIn _) ->
408 return srcType
410 _ ->
411 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
412 return (T.Aliased name args' (T.Filled srcType))
413 where
414 backupSrcType :: Descriptor -> IO T.Canonical
415 backupSrcType desc =
416 case name desc of
417 Just v@(Var.Canonical _ x@(c:_))
418 | Char.isLower c ->
419 return (T.Var x)
420 | otherwise ->
421 return $ T.Type v
423 _ ->
424 error $
425 concat
426 [ "Problem converting the following type "
427 , "from a type-checker type to a source-syntax type:"
428 , P.render (pretty Never rootVariable)
429 ]
432termToSrcType :: Variable -> Term1 Variable -> IO T.Canonical
433termToSrcType rootVariable term =
434 let go = variableToSrcType rootVariable in
435 case term of
436 App1 a b ->
437 do a' <- go a
438 b' <- go b
439 case a' of
440 T.App f args ->
441 return $ T.App f (args ++ [b'])
442 _ ->
443 return $ T.App a' [b']
445 Fun1 a b ->
446 T.Lambda <$> go a <*> go b
448 Var1 a ->
449 go a
451 EmptyRecord1 ->
452 return $ T.Record [] Nothing
454 Record1 tfields extension ->
455 do fields' <- Traverse.traverse (mapM go) tfields
456 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
457 ext' <- dealias <$> go extension
458 return $
459 case ext' of
460 T.Record fs ext -> T.Record (fs ++ fields) ext
461 T.Var _ -> T.Record fields (Just ext')
462 _ -> error "Used toSrcType on a type that is not well-formed"
463 where
464 dealias :: T.Canonical -> T.Canonical
465 dealias tipe =
466 case tipe of
467 T.Aliased _ args tipe' ->
468 T.dealias args tipe'
469 _ ->
470 tipe
473-- ADD NAMES TO TYPES
475addNames :: Variable -> IO ()
476addNames variable =
477 do usedNames <- getVarNames variable
478 let freeNames = makeFreeNames usedNames
479 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
480 return ()
483makeFreeNames :: Set.Set String -> [String]
484makeFreeNames usedNames =
485 let makeName suffix =
486 map (:suffix) ['a'..'z']
488 allNames =
489 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
490 in
491 filter (\name -> Set.notMember name usedNames) allNames
494data NameState = NameState
495 { freeNames :: [String]
496 , numberPrimes :: Int
497 , comparablePrimes :: Int
498 , appendablePrimes :: Int
499 }
502varAddNames :: Variable -> StateT NameState IO ()
503varAddNames var =
504 do desc <- State.liftIO (UF.descriptor var)
505 case alias desc of
506 Nothing ->
507 return ()
509 Just (_name, args) ->
510 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
512 case structure desc of
513 Just term ->
514 termAddNames term
516 Nothing ->
517 case name desc of
518 Just _ -> return ()
519 Nothing ->
520 do name' <- createName desc
521 State.liftIO $ UF.modifyDescriptor var $ \desc ->
522 desc { name = Just (Var.local name') }
525termAddNames :: Term1 Variable -> StateT NameState IO ()
526termAddNames term =
527 case term of
528 App1 a b ->
529 do varAddNames a
530 varAddNames b
532 Fun1 a b ->
533 do varAddNames a
534 varAddNames b
536 Var1 a ->
537 varAddNames a
539 EmptyRecord1 ->
540 return ()
542 Record1 fields extension ->
543 do mapM_ varAddNames (concat (Map.elems fields))
544 varAddNames extension
547createName :: (Monad m) => Descriptor -> StateT NameState m String
548createName desc =
549 case flex desc of
550 Is Number ->
551 do primes <- State.gets numberPrimes
552 State.modify (\state -> state { numberPrimes = primes + 1 })
553 return ("number" ++ replicate primes '\'')
555 Is Comparable ->
556 do primes <- State.gets comparablePrimes
557 State.modify (\state -> state { comparablePrimes = primes + 1 })
558 return ("comparable" ++ replicate primes '\'')
560 Is Appendable ->
561 do primes <- State.gets appendablePrimes
562 State.modify (\state -> state { appendablePrimes = primes + 1 })
563 return ("appendable" ++ replicate primes '\'')
565 _ ->
566 do names <- State.gets freeNames
567 State.modify (\state -> state { freeNames = tail names })
568 return (head names)
571-- GET ALL VARIABLE NAMES
573getVarNames :: Variable -> IO (Set.Set String)
574getVarNames var =
575 do desc <- UF.descriptor var
577 let baseSet =
578 case name desc of
579 Just var -> Set.singleton (Var.toString var)
580 Nothing -> Set.empty
582 structureSet <-
583 case structure desc of
584 Nothing -> return Set.empty
585 Just term -> getVarNamesTerm term
587 aliasSet <-
588 case alias desc of
589 Nothing ->
590 return Set.empty
592 Just (_name, args) ->
593 do let set = Set.fromList (map fst args)
594 sets <- mapM (getVarNames . snd) args
595 return (Set.unions (set : sets))
597 return (Set.unions [ baseSet, structureSet, aliasSet ])
600getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
601getVarNamesTerm term =
602 let go = getVarNames in
603 case term of
604 App1 a b ->
605 Set.union <$> go a <*> go b
607 Fun1 a b ->
608 Set.union <$> go a <*> go b
610 Var1 a ->
611 go a
613 EmptyRecord1 ->
614 return Set.empty
616 Record1 fields extension ->
617 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
618 Set.union fieldVars <$> go extension
621-- COLLECT APPLICATIONS
623data AppStructure
624 = List Variable
625 | Tuple [Variable]
626 | Other
629collectApps :: Variable -> IO AppStructure
630collectApps var =
631 go [] var
632 where
633 go vars var = do
634 desc <- UF.descriptor var
635 case (structure desc, vars) of
636 (Nothing, [v]) ->
637 case name desc of
638 Just n | Var.isList n -> return (List v)
639 _ -> return Other
641 (Nothing, vs) ->
642 case name desc of
643 Just n | Var.isTuple n -> return (Tuple vs)
644 _ -> return Other
646 (Just term, _) ->
647 case term of
648 App1 a b -> go (vars ++ [b]) a
649 _ -> return Other