git.iko.soy/elk
on fb08d70 help sign in
elk/src/Type/Type.hs
642 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.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 deriving (Eq)
96data SuperType
97 = Number
98 | Comparable
99 | Appendable
100 deriving (Eq)
103-- CONSTRAINTS
105data Constraint a b
106 = CTrue
107 | CSaveEnv
108 | CEqual Error.Hint R.Region a a
109 | CAnd [Constraint a b]
110 | CLet [Scheme a b] (Constraint a b)
111 | CInstance R.Region SchemeName a
113type SchemeName = String
115type TypeName = Var.Canonical
117data Scheme a b = Scheme
118 { rigidQuantifiers :: [b]
119 , flexibleQuantifiers :: [b]
120 , constraint :: Constraint a b
121 , header :: Map.Map String a
122 }
125-- TYPE HELPERS
127infixr 9 ==>
129(==>) :: Type -> Type -> Type
130(==>) a b =
131 termN (Fun1 a b)
134(<|) :: TermN a -> TermN a -> TermN a
135(<|) f a =
136 termN (App1 f a)
139-- VARIABLE HELPERS
141namedVar :: Flex -> Var.Canonical -> IO Variable
142namedVar flex name = UF.fresh $ Descriptor
143 { structure = Nothing
144 , rank = noRank
145 , flex = flex
146 , name = Just name
147 , copy = Nothing
148 , mark = noMark
149 , alias = Nothing
150 }
153variable :: Flex -> IO Variable
154variable flex = UF.fresh $ Descriptor
155 { structure = Nothing
156 , rank = noRank
157 , flex = flex
158 , name = Nothing
159 , copy = Nothing
160 , mark = noMark
161 , alias = Nothing
162 }
165-- CONSTRAINT HELPERS
167monoscheme :: Map.Map String a -> Scheme a b
168monoscheme headers =
169 Scheme [] [] CTrue headers
172infixl 8 /\
174(/\) :: Constraint a b -> Constraint a b -> Constraint a b
175(/\) c1 c2 =
176 case (c1, c2) of
177 (CTrue, _) -> c2
178 (_, CTrue) -> c1
179 _ -> CAnd [c1,c2]
182-- ex qs constraint == exists qs. constraint
183ex :: [Variable] -> TypeConstraint -> TypeConstraint
184ex fqs constraint =
185 CLet [Scheme [] fqs constraint Map.empty] CTrue
188-- fl qs constraint == forall qs. constraint
189fl :: [Variable] -> TypeConstraint -> TypeConstraint
190fl rqs constraint =
191 CLet [Scheme rqs [] constraint Map.empty] CTrue
194exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
195exists f =
196 do v <- variable Flexible
197 ex [v] <$> f (varN v)
200existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
201existsNumber f =
202 do v <- variable (Is Number)
203 ex [v] <$> f (varN v)
206-- TYPES TO PRETTY STRINGS
208instance PrettyType a => PrettyType (UF.Point a) where
209 pretty when point =
210 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
213instance PrettyType a => PrettyType (Term1 a) where
214 pretty when term =
215 let prty = pretty Never in
216 case term of
217 App1 f x ->
218 parensIf needed (px <+> pretty App x)
219 where
220 px = prty f
221 needed =
222 case when of
223 App -> True
224 _ -> False
226 Fun1 arg body ->
227 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
228 where
229 needed =
230 case when of
231 Never -> False
232 _ -> True
234 Var1 x ->
235 prty x
237 EmptyRecord1 ->
238 P.braces P.empty
240 Record1 fields ext ->
241 P.braces (extend <+> commaSep prettyFields)
242 where
243 prettyExt = prty ext
245 extend
246 | P.render prettyExt == "{}" =
247 P.empty
248 | otherwise =
249 prettyExt <+> P.text "|"
251 mkPretty f t =
252 P.text f <+> P.text ":" <+> prty t
254 prettyFields =
255 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
258instance PrettyType a => PrettyType (TermN a) where
259 pretty when term =
260 case term of
261 PlaceHolder _ ->
262 error "problem prettifying type, probably indicates a bigger problem"
264 VarN alias x ->
265 either alias (pretty when x)
267 TermN alias t1 ->
268 either alias (pretty when t1)
269 where
270 either maybeAlias doc =
271 case maybeAlias of
272 Nothing -> doc
273 Just (name, args) ->
274 P.hang
275 (P.text (Var.toString name))
276 2
277 (P.sep (map (pretty App . snd) args))
280instance PrettyType Descriptor where
281 pretty when desc =
282 case (alias desc, structure desc, name desc) of
283 (Just (name, args), _, _) ->
284 P.hang
285 (P.text (Var.toString name))
286 4
287 (P.sep (map (pretty App . snd) args))
289 (_, Just term, _) ->
290 pretty when term
292 (_, _, Just name)
293 | Var.isTuple name ->
294 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
295 | otherwise ->
296 P.text (Var.toString name)
298 _ -> P.text "?"
301instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
302 pretty _ constraint =
303 let prty = pretty Never in
304 case constraint of
305 CTrue ->
306 P.text "True"
308 CSaveEnv ->
309 P.text "SaveTheEnvironment!!!"
311 CEqual _ _ a b ->
312 prty a <+> P.text "=" <+> prty b
314 CAnd [] ->
315 P.text "True"
317 CAnd cs ->
318 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
320 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
321 P.sep [ binder, pretty Never c ]
322 where
323 mergeExists vs c =
324 case c of
325 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
326 _ -> (vs, c)
328 (fqs', c) = mergeExists fqs constraint
330 binder =
331 if null fqs'
332 then P.empty
333 else
334 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
336 CLet schemes constraint ->
337 P.fsep
338 [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
339 , P.text "in", pretty Never constraint
340 ]
342 CInstance _region name tipe ->
343 P.text name <+> P.text "<" <+> prty tipe
346instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
347 pretty _ (Scheme rqs fqs constraint headers) =
348 P.sep [ forall, cs, headers' ]
349 where
350 prty = pretty Never
352 forall =
353 if null rqs && null fqs
354 then P.empty
355 else P.text "\x2200" <+> frees <+> rigids
357 frees = P.hsep (map prty fqs)
359 rigids =
360 if null rqs
361 then P.empty
362 else P.braces . P.hsep $ map prty rqs
364 cs =
365 case constraint of
366 CTrue -> P.empty
367 CAnd [] -> P.empty
368 _ -> P.brackets (pretty Never constraint)
370 headers' =
371 if Map.size headers > 0 then dict else P.empty
373 dict =
374 P.parens . commaSep . map prettyPair $ Map.toList headers
376 prettyPair (n,t) =
377 P.text n <+> P.text ":" <+> pretty Never t
380-- CONVERT TO SOURCE TYPES
382-- TODO: Attach resulting type to the descriptor so that you
383-- never have to do extra work, particularly nice for aliased types
384toSrcType :: Variable -> IO T.Canonical
385toSrcType variable =
386 do addNames variable
387 variableToSrcType variable variable
390variableToSrcType :: Variable -> Variable -> IO T.Canonical
391variableToSrcType rootVariable variable =
392 do desc <- UF.descriptor variable
393 srcType <- maybe (backupSrcType desc) (termToSrcType rootVariable) (structure desc)
394 case alias desc of
395 Nothing ->
396 return srcType
398 Just (name, args) ->
399 case srcType of
400 T.Type (Var.Canonical Var.BuiltIn _) ->
401 return srcType
403 _ ->
404 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
405 return (T.Aliased name args' (T.Filled srcType))
406 where
407 backupSrcType :: Descriptor -> IO T.Canonical
408 backupSrcType desc =
409 case name desc of
410 Just v@(Var.Canonical _ x@(c:_))
411 | Char.isLower c ->
412 return (T.Var x)
413 | otherwise ->
414 return $ T.Type v
416 _ ->
417 error $
418 concat
419 [ "Problem converting the following type "
420 , "from a type-checker type to a source-syntax type:"
421 , P.render (pretty Never rootVariable)
422 ]
425termToSrcType :: Variable -> Term1 Variable -> IO T.Canonical
426termToSrcType rootVariable term =
427 let go = variableToSrcType rootVariable in
428 case term of
429 App1 a b ->
430 do a' <- go a
431 b' <- go b
432 case a' of
433 T.App f args ->
434 return $ T.App f (args ++ [b'])
435 _ ->
436 return $ T.App a' [b']
438 Fun1 a b ->
439 T.Lambda <$> go a <*> go b
441 Var1 a ->
442 go a
444 EmptyRecord1 ->
445 return $ T.Record [] Nothing
447 Record1 tfields extension ->
448 do fields' <- Traverse.traverse (mapM go) tfields
449 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
450 ext' <- dealias <$> go extension
451 return $
452 case ext' of
453 T.Record fs ext -> T.Record (fs ++ fields) ext
454 T.Var _ -> T.Record fields (Just ext')
455 _ -> error "Used toSrcType on a type that is not well-formed"
456 where
457 dealias :: T.Canonical -> T.Canonical
458 dealias tipe =
459 case tipe of
460 T.Aliased _ args tipe' ->
461 T.dealias args tipe'
462 _ ->
463 tipe
466-- ADD NAMES TO TYPES
468addNames :: Variable -> IO ()
469addNames variable =
470 do usedNames <- getVarNames variable
471 let freeNames = makeFreeNames usedNames
472 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
473 return ()
476makeFreeNames :: Set.Set String -> [String]
477makeFreeNames usedNames =
478 let makeName suffix =
479 map (:suffix) ['a'..'z']
481 allNames =
482 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
483 in
484 filter (\name -> Set.notMember name usedNames) allNames
487data NameState = NameState
488 { freeNames :: [String]
489 , numberPrimes :: Int
490 , comparablePrimes :: Int
491 , appendablePrimes :: Int
492 }
495varAddNames :: Variable -> StateT NameState IO ()
496varAddNames var =
497 do desc <- State.liftIO (UF.descriptor var)
498 case alias desc of
499 Nothing ->
500 return ()
502 Just (_name, args) ->
503 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
505 case structure desc of
506 Just term ->
507 termAddNames term
509 Nothing ->
510 case name desc of
511 Just _ -> return ()
512 Nothing ->
513 do name' <- createName desc
514 State.liftIO $ UF.modifyDescriptor var $ \desc ->
515 desc { name = Just (Var.local name') }
518termAddNames :: Term1 Variable -> StateT NameState IO ()
519termAddNames term =
520 case term of
521 App1 a b ->
522 do varAddNames a
523 varAddNames b
525 Fun1 a b ->
526 do varAddNames a
527 varAddNames b
529 Var1 a ->
530 varAddNames a
532 EmptyRecord1 ->
533 return ()
535 Record1 fields extension ->
536 do mapM_ varAddNames (concat (Map.elems fields))
537 varAddNames extension
540createName :: (Monad m) => Descriptor -> StateT NameState m String
541createName desc =
542 case flex desc of
543 Is Number ->
544 do primes <- State.gets numberPrimes
545 State.modify (\state -> state { numberPrimes = primes + 1 })
546 return ("number" ++ replicate primes '\'')
548 Is Comparable ->
549 do primes <- State.gets comparablePrimes
550 State.modify (\state -> state { comparablePrimes = primes + 1 })
551 return ("comparable" ++ replicate primes '\'')
553 Is Appendable ->
554 do primes <- State.gets appendablePrimes
555 State.modify (\state -> state { appendablePrimes = primes + 1 })
556 return ("appendable" ++ replicate primes '\'')
558 _ ->
559 do names <- State.gets freeNames
560 State.modify (\state -> state { freeNames = tail names })
561 return (head names)
564-- GET ALL VARIABLE NAMES
566getVarNames :: Variable -> IO (Set.Set String)
567getVarNames var =
568 do desc <- UF.descriptor var
570 let baseSet =
571 case name desc of
572 Just var -> Set.singleton (Var.toString var)
573 Nothing -> Set.empty
575 structureSet <-
576 case structure desc of
577 Nothing -> return Set.empty
578 Just term -> getVarNamesTerm term
580 aliasSet <-
581 case alias desc of
582 Nothing ->
583 return Set.empty
585 Just (_name, args) ->
586 do let set = Set.fromList (map fst args)
587 sets <- mapM (getVarNames . snd) args
588 return (Set.unions (set : sets))
590 return (Set.unions [ baseSet, structureSet, aliasSet ])
593getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
594getVarNamesTerm term =
595 let go = getVarNames in
596 case term of
597 App1 a b ->
598 Set.union <$> go a <*> go b
600 Fun1 a b ->
601 Set.union <$> go a <*> go b
603 Var1 a ->
604 go a
606 EmptyRecord1 ->
607 return Set.empty
609 Record1 fields extension ->
610 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
611 Set.union fieldVars <$> go extension
614-- COLLECT APPLICATIONS
616data AppStructure
617 = List Variable
618 | Tuple [Variable]
619 | Other
622collectApps :: Variable -> IO AppStructure
623collectApps var =
624 go [] var
625 where
626 go vars var = do
627 desc <- UF.descriptor var
628 case (structure desc, vars) of
629 (Nothing, [v]) ->
630 case name desc of
631 Just n | Var.isList n -> return (List v)
632 _ -> return Other
634 (Nothing, vs) ->
635 case name desc of
636 Just n | Var.isTuple n -> return (Tuple vs)
637 _ -> return Other
639 (Just term, _) ->
640 case term of
641 App1 a b -> go (vars ++ [b]) a
642 _ -> return Other