git.iko.soy/elk
on 2d29699 help sign in
elk/src/Type/Type.hs
650 lines 16 kB history raw
1module Type.Type where
3import Control.Applicative ((<$>),(<*>))
4import Control.Monad.State (StateT)
5import qualified Control.Monad.State as State
6import qualified Data.Char as Char
7import qualified Data.Map as Map
8import qualified Data.Set as Set
9import qualified Data.Traversable as Traverse (traverse)
10import qualified Data.UnionFind.IO as UF
11import Text.PrettyPrint as P
12import System.IO.Unsafe
14import qualified AST.Type as T
15import qualified AST.Variable as Var
16import qualified Reporting.Annotation as A
17import qualified Reporting.Error.Type as Error
18import qualified Reporting.Region as R
19import Type.PrettyPrint
22-- CONCRETE TYPES
24type Type = TermN Variable
26type Variable = UF.Point Descriptor
28type TypeConstraint = Constraint Type Variable
30type TypeScheme = Scheme Type Variable
32type Alias a = Maybe (Var.Canonical, [(String,a)])
35-- TYPE PRIMITIVES
37data Term1 a
38 = App1 a a
39 | Fun1 a a
40 | Var1 a
41 | EmptyRecord1
42 | Record1 (Map.Map String [a]) a
45data TermN a
46 = PlaceHolder String
47 | VarN (Alias (TermN a)) a
48 | TermN (Alias (TermN a)) (Term1 (TermN a))
51varN :: a -> TermN a
52varN =
53 VarN Nothing
56termN :: (Term1 (TermN a)) -> TermN a
57termN =
58 TermN Nothing
61record :: Map.Map String [TermN a] -> TermN a -> TermN a
62record fs rec =
63 termN (Record1 fs rec)
66-- DESCRIPTORS
68data Descriptor = Descriptor
69 { structure :: Maybe (Term1 Variable)
70 , rank :: Int
71 , flex :: Flex
72 , name :: Maybe TypeName
73 , copy :: Maybe Variable
74 , mark :: Int
75 , alias :: Alias Variable
76 }
78noRank :: Int
79noRank = -1
81outermostRank :: Int
82outermostRank = 0
84noMark :: Int
85noMark = 0
87initialMark :: Int
88initialMark = 1
90data Flex
91 = Rigid
92 | Flexible
93 | Constant
94 | Is SuperType
95 | Error
96 deriving (Eq)
98data SuperType
99 = Number
100 | Comparable
101 | Appendable
102 deriving (Eq)
105-- CONSTRAINTS
107data Constraint a b
108 = CTrue
109 | CSaveEnv
110 | CEqual Error.Hint R.Region a a
111 | CAnd [Constraint a b]
112 | CLet [Scheme a b] (Constraint a b)
113 | CInstance R.Region 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.Located 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 =
157 UF.fresh (descriptor flex)
160descriptor :: Flex -> Descriptor
161descriptor flex =
162 Descriptor
163 { structure = Nothing
164 , rank = noRank
165 , flex = flex
166 , name = Nothing
167 , copy = Nothing
168 , mark = noMark
169 , alias = Nothing
170 }
173-- CONSTRAINT HELPERS
175monoscheme :: Map.Map String (A.Located a) -> Scheme a b
176monoscheme headers =
177 Scheme [] [] CTrue headers
180infixl 8 /\
182(/\) :: Constraint a b -> Constraint a b -> Constraint a b
183(/\) c1 c2 =
184 case (c1, c2) of
185 (CTrue, _) -> c2
186 (_, CTrue) -> c1
187 _ -> CAnd [c1,c2]
190-- ex qs constraint == exists qs. constraint
191ex :: [Variable] -> TypeConstraint -> TypeConstraint
192ex fqs constraint =
193 CLet [Scheme [] fqs constraint Map.empty] CTrue
196-- fl qs constraint == forall qs. constraint
197fl :: [Variable] -> TypeConstraint -> TypeConstraint
198fl rqs constraint =
199 CLet [Scheme rqs [] constraint Map.empty] CTrue
202exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
203exists f =
204 do v <- variable Flexible
205 ex [v] <$> f (varN v)
208existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
209existsNumber f =
210 do v <- variable (Is Number)
211 ex [v] <$> f (varN v)
214-- TYPES TO PRETTY STRINGS
216instance PrettyType a => PrettyType (UF.Point a) where
217 pretty when point =
218 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
221instance PrettyType a => PrettyType (Term1 a) where
222 pretty when term =
223 let prty = pretty Never in
224 case term of
225 App1 f x ->
226 parensIf needed (px <+> pretty App x)
227 where
228 px = prty f
229 needed =
230 case when of
231 App -> True
232 _ -> False
234 Fun1 arg body ->
235 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
236 where
237 needed =
238 case when of
239 Never -> False
240 _ -> True
242 Var1 x ->
243 prty x
245 EmptyRecord1 ->
246 P.braces P.empty
248 Record1 fields ext ->
249 P.braces (extend <+> commaSep prettyFields)
250 where
251 prettyExt = prty ext
253 extend
254 | P.render prettyExt == "{}" =
255 P.empty
256 | otherwise =
257 prettyExt <+> P.text "|"
259 mkPretty f t =
260 P.text f <+> P.text ":" <+> prty t
262 prettyFields =
263 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
266instance PrettyType a => PrettyType (TermN a) where
267 pretty when term =
268 case term of
269 PlaceHolder _ ->
270 error "problem prettifying type, probably indicates a bigger problem"
272 VarN alias x ->
273 either alias (pretty when x)
275 TermN alias t1 ->
276 either alias (pretty when t1)
277 where
278 either maybeAlias doc =
279 case maybeAlias of
280 Nothing -> doc
281 Just (name, args) ->
282 P.hang
283 (P.text (Var.toString name))
284 2
285 (P.sep (map (pretty App . snd) args))
288instance PrettyType Descriptor where
289 pretty when desc =
290 case (alias desc, structure desc, name desc) of
291 (Just (name, args), _, _) ->
292 P.hang
293 (P.text (Var.toString name))
294 4
295 (P.sep (map (pretty App . snd) args))
297 (_, Just term, _) ->
298 pretty when term
300 (_, _, Just name)
301 | Var.isTuple name ->
302 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
303 | otherwise ->
304 P.text (Var.toString name)
306 _ -> P.text "?"
309instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
310 pretty _ constraint =
311 let prty = pretty Never in
312 case constraint of
313 CTrue ->
314 P.text "True"
316 CSaveEnv ->
317 P.text "SaveTheEnvironment!!!"
319 CEqual _ _ a b ->
320 prty a <+> P.text "=" <+> prty b
322 CAnd [] ->
323 P.text "True"
325 CAnd cs ->
326 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
328 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
329 P.sep [ binder, pretty Never c ]
330 where
331 mergeExists vs c =
332 case c of
333 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
334 _ -> (vs, c)
336 (fqs', c) = mergeExists fqs constraint
338 binder =
339 if null fqs'
340 then P.empty
341 else
342 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
344 CLet schemes constraint ->
345 P.fsep
346 [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
347 , P.text "in", pretty Never constraint
348 ]
350 CInstance _region name tipe ->
351 P.text name <+> P.text "<" <+> prty tipe
354instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
355 pretty _ (Scheme rqs fqs constraint headers) =
356 P.sep [ forall, cs, headers' ]
357 where
358 prty = pretty Never
360 forall =
361 if null rqs && null fqs
362 then P.empty
363 else P.text "\x2200" <+> frees <+> rigids
365 frees = P.hsep (map prty fqs)
367 rigids =
368 if null rqs
369 then P.empty
370 else P.braces . P.hsep $ map prty rqs
372 cs =
373 case constraint of
374 CTrue -> P.empty
375 CAnd [] -> P.empty
376 _ -> P.brackets (pretty Never constraint)
378 headers' =
379 if Map.size headers > 0 then dict else P.empty
381 dict =
382 P.parens . commaSep . map prettyPair $ Map.toList headers
384 prettyPair (fieldName, A.A _ tipe) =
385 P.text fieldName <+> P.text ":" <+> pretty Never tipe
388-- CONVERT TO SOURCE TYPES
390-- TODO: Attach resulting type to the descriptor so that you
391-- never have to do extra work, particularly nice for aliased types
392toSrcType :: Variable -> IO T.Canonical
393toSrcType variable =
394 do addNames variable
395 variableToSrcType variable variable
398variableToSrcType :: Variable -> Variable -> IO T.Canonical
399variableToSrcType rootVariable variable =
400 do desc <- UF.descriptor variable
401 srcType <- maybe (backupSrcType desc) (termToSrcType rootVariable) (structure desc)
402 case alias desc of
403 Nothing ->
404 return srcType
406 Just (name, args) ->
407 case srcType of
408 T.Type (Var.Canonical Var.BuiltIn _) ->
409 return srcType
411 _ ->
412 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
413 return (T.Aliased name args' (T.Filled srcType))
414 where
415 backupSrcType :: Descriptor -> IO T.Canonical
416 backupSrcType desc =
417 case name desc of
418 Just v@(Var.Canonical _ x@(c:_))
419 | Char.isLower c ->
420 return (T.Var x)
421 | otherwise ->
422 return $ T.Type v
424 _ ->
425 error $
426 concat
427 [ "Problem converting the following type "
428 , "from a type-checker type to a source-syntax type:"
429 , P.render (pretty Never rootVariable)
430 ]
433termToSrcType :: Variable -> Term1 Variable -> IO T.Canonical
434termToSrcType rootVariable term =
435 let go = variableToSrcType rootVariable in
436 case term of
437 App1 a b ->
438 do a' <- go a
439 b' <- go b
440 case a' of
441 T.App f args ->
442 return $ T.App f (args ++ [b'])
443 _ ->
444 return $ T.App a' [b']
446 Fun1 a b ->
447 T.Lambda <$> go a <*> go b
449 Var1 a ->
450 go a
452 EmptyRecord1 ->
453 return $ T.Record [] Nothing
455 Record1 tfields extension ->
456 do fields' <- Traverse.traverse (mapM go) tfields
457 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
458 ext' <- dealias <$> go extension
459 return $
460 case ext' of
461 T.Record fs ext -> T.Record (fs ++ fields) ext
462 T.Var _ -> T.Record fields (Just ext')
463 _ -> error "Used toSrcType on a type that is not well-formed"
464 where
465 dealias :: T.Canonical -> T.Canonical
466 dealias tipe =
467 case tipe of
468 T.Aliased _ args tipe' ->
469 T.dealias args tipe'
470 _ ->
471 tipe
474-- ADD NAMES TO TYPES
476addNames :: Variable -> IO ()
477addNames variable =
478 do usedNames <- getVarNames variable
479 let freeNames = makeFreeNames usedNames
480 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
481 return ()
484makeFreeNames :: Set.Set String -> [String]
485makeFreeNames usedNames =
486 let makeName suffix =
487 map (:suffix) ['a'..'z']
489 allNames =
490 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
491 in
492 filter (\name -> Set.notMember name usedNames) allNames
495data NameState = NameState
496 { freeNames :: [String]
497 , numberPrimes :: Int
498 , comparablePrimes :: Int
499 , appendablePrimes :: Int
500 }
503varAddNames :: Variable -> StateT NameState IO ()
504varAddNames var =
505 do desc <- State.liftIO (UF.descriptor var)
506 case alias desc of
507 Nothing ->
508 return ()
510 Just (_name, args) ->
511 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
513 case structure desc of
514 Just term ->
515 termAddNames term
517 Nothing ->
518 case name desc of
519 Just _ -> return ()
520 Nothing ->
521 do name' <- createName desc
522 State.liftIO $ UF.modifyDescriptor var $ \desc ->
523 desc { name = Just (Var.local name') }
526termAddNames :: Term1 Variable -> StateT NameState IO ()
527termAddNames term =
528 case term of
529 App1 a b ->
530 do varAddNames a
531 varAddNames b
533 Fun1 a b ->
534 do varAddNames a
535 varAddNames b
537 Var1 a ->
538 varAddNames a
540 EmptyRecord1 ->
541 return ()
543 Record1 fields extension ->
544 do mapM_ varAddNames (concat (Map.elems fields))
545 varAddNames extension
548createName :: (Monad m) => Descriptor -> StateT NameState m String
549createName desc =
550 case flex desc of
551 Is Number ->
552 do primes <- State.gets numberPrimes
553 State.modify (\state -> state { numberPrimes = primes + 1 })
554 return ("number" ++ replicate primes '\'')
556 Is Comparable ->
557 do primes <- State.gets comparablePrimes
558 State.modify (\state -> state { comparablePrimes = primes + 1 })
559 return ("comparable" ++ replicate primes '\'')
561 Is Appendable ->
562 do primes <- State.gets appendablePrimes
563 State.modify (\state -> state { appendablePrimes = primes + 1 })
564 return ("appendable" ++ replicate primes '\'')
566 _ ->
567 do names <- State.gets freeNames
568 State.modify (\state -> state { freeNames = tail names })
569 return (head names)
572-- GET ALL VARIABLE NAMES
574getVarNames :: Variable -> IO (Set.Set String)
575getVarNames var =
576 do desc <- UF.descriptor var
578 let baseSet =
579 case name desc of
580 Just var -> Set.singleton (Var.toString var)
581 Nothing -> Set.empty
583 structureSet <-
584 case structure desc of
585 Nothing -> return Set.empty
586 Just term -> getVarNamesTerm term
588 aliasSet <-
589 case alias desc of
590 Nothing ->
591 return Set.empty
593 Just (_name, args) ->
594 do let set = Set.fromList (map fst args)
595 sets <- mapM (getVarNames . snd) args
596 return (Set.unions (set : sets))
598 return (Set.unions [ baseSet, structureSet, aliasSet ])
601getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
602getVarNamesTerm term =
603 let go = getVarNames in
604 case term of
605 App1 a b ->
606 Set.union <$> go a <*> go b
608 Fun1 a b ->
609 Set.union <$> go a <*> go b
611 Var1 a ->
612 go a
614 EmptyRecord1 ->
615 return Set.empty
617 Record1 fields extension ->
618 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
619 Set.union fieldVars <$> go extension
622-- COLLECT APPLICATIONS
624data AppStructure
625 = List Variable
626 | Tuple [Variable]
627 | Other
630collectApps :: Variable -> IO AppStructure
631collectApps var =
632 go [] var
633 where
634 go vars var = do
635 desc <- UF.descriptor var
636 case (structure desc, vars) of
637 (Nothing, [v]) ->
638 case name desc of
639 Just n | Var.isList n -> return (List v)
640 _ -> return Other
642 (Nothing, vs) ->
643 case name desc of
644 Just n | Var.isTuple n -> return (Tuple vs)
645 _ -> return Other
647 (Just term, _) ->
648 case term of
649 App1 a b -> go (vars ++ [b]) a
650 _ -> return Other