git.iko.soy/elk
on 357dedf help sign in
elk/src/Type/Type.hs
641 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.Region as R
17import Type.PrettyPrint
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
104data Constraint a b
105 = CTrue
106 | CSaveEnv
107 | CEqual R.Region a a
108 | CAnd [Constraint a b]
109 | CLet [Scheme a b] (Constraint a b)
110 | CInstance R.Region 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 [] [] CTrue headers
171infixl 8 /\
173(/\) :: Constraint a b -> Constraint a b -> Constraint a b
174(/\) c1 c2 =
175 case (c1, c2) of
176 (CTrue, _) -> c2
177 (_, CTrue) -> c1
178 _ -> CAnd [c1,c2]
181-- ex qs constraint == exists qs. constraint
182ex :: [Variable] -> TypeConstraint -> TypeConstraint
183ex fqs constraint =
184 CLet [Scheme [] fqs constraint Map.empty] CTrue
187-- fl qs constraint == forall qs. constraint
188fl :: [Variable] -> TypeConstraint -> TypeConstraint
189fl rqs constraint =
190 CLet [Scheme rqs [] constraint Map.empty] CTrue
193exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
194exists f =
195 do v <- variable Flexible
196 ex [v] <$> f (varN v)
199existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
200existsNumber f =
201 do v <- 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 a => PrettyType (Term1 a) where
213 pretty when term =
214 let prty = pretty Never in
215 case term of
216 App1 f x ->
217 parensIf needed (px <+> pretty App x)
218 where
219 px = prty f
220 needed =
221 case when of
222 App -> True
223 _ -> False
225 Fun1 arg body ->
226 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
227 where
228 needed =
229 case when of
230 Never -> False
231 _ -> True
233 Var1 x ->
234 prty x
236 EmptyRecord1 ->
237 P.braces P.empty
239 Record1 fields ext ->
240 P.braces (extend <+> commaSep prettyFields)
241 where
242 prettyExt = prty ext
244 extend
245 | P.render prettyExt == "{}" =
246 P.empty
247 | otherwise =
248 prettyExt <+> P.text "|"
250 mkPretty f t =
251 P.text f <+> P.text ":" <+> prty t
253 prettyFields =
254 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
257instance PrettyType a => PrettyType (TermN a) where
258 pretty when term =
259 case term of
260 PlaceHolder _ ->
261 error "problem prettifying type, probably indicates a bigger problem"
263 VarN alias x ->
264 either alias (pretty when x)
266 TermN alias t1 ->
267 either alias (pretty when t1)
268 where
269 either maybeAlias doc =
270 case maybeAlias of
271 Nothing -> doc
272 Just (name, args) ->
273 P.hang
274 (P.text (Var.toString name))
275 2
276 (P.sep (map (pretty App . snd) args))
279instance PrettyType Descriptor where
280 pretty when desc =
281 case (alias desc, structure desc, name desc) of
282 (Just (name, args), _, _) ->
283 P.hang
284 (P.text (Var.toString name))
285 4
286 (P.sep (map (pretty App . snd) args))
288 (_, Just term, _) ->
289 pretty when term
291 (_, _, Just name)
292 | Var.isTuple name ->
293 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
294 | otherwise ->
295 P.text (Var.toString name)
297 _ -> P.text "?"
300instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
301 pretty _ constraint =
302 let prty = pretty Never in
303 case constraint of
304 CTrue ->
305 P.text "True"
307 CSaveEnv ->
308 P.text "SaveTheEnvironment!!!"
310 CEqual _region a b ->
311 prty a <+> P.text "=" <+> prty b
313 CAnd [] ->
314 P.text "True"
316 CAnd cs ->
317 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
319 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
320 P.sep [ binder, pretty Never c ]
321 where
322 mergeExists vs c =
323 case c of
324 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
325 _ -> (vs, c)
327 (fqs', c) = mergeExists fqs constraint
329 binder =
330 if null fqs'
331 then P.empty
332 else
333 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
335 CLet schemes constraint ->
336 P.fsep
337 [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
338 , P.text "in", pretty Never constraint
339 ]
341 CInstance _region name tipe ->
342 P.text name <+> P.text "<" <+> prty tipe
345instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
346 pretty _ (Scheme rqs fqs constraint headers) =
347 P.sep [ forall, cs, headers' ]
348 where
349 prty = pretty Never
351 forall =
352 if null rqs && null fqs
353 then P.empty
354 else P.text "\x2200" <+> frees <+> rigids
356 frees = P.hsep (map prty fqs)
358 rigids =
359 if null rqs
360 then P.empty
361 else P.braces . P.hsep $ map prty rqs
363 cs =
364 case constraint of
365 CTrue -> P.empty
366 CAnd [] -> P.empty
367 _ -> P.brackets (pretty Never constraint)
369 headers' =
370 if Map.size headers > 0 then dict else P.empty
372 dict =
373 P.parens . commaSep . map prettyPair $ Map.toList headers
375 prettyPair (n,t) =
376 P.text n <+> P.text ":" <+> pretty Never t
379-- CONVERT TO SOURCE TYPES
381-- TODO: Attach resulting type to the descriptor so that you
382-- never have to do extra work, particularly nice for aliased types
383toSrcType :: Variable -> IO T.Canonical
384toSrcType variable =
385 do addNames variable
386 variableToSrcType variable variable
389variableToSrcType :: Variable -> Variable -> IO T.Canonical
390variableToSrcType rootVariable variable =
391 do desc <- UF.descriptor variable
392 srcType <- maybe (backupSrcType desc) (termToSrcType rootVariable) (structure desc)
393 case alias desc of
394 Nothing ->
395 return srcType
397 Just (name, args) ->
398 case srcType of
399 T.Type (Var.Canonical Var.BuiltIn _) ->
400 return srcType
402 _ ->
403 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
404 return (T.Aliased name args' (T.Filled srcType))
405 where
406 backupSrcType :: Descriptor -> IO T.Canonical
407 backupSrcType desc =
408 case name desc of
409 Just v@(Var.Canonical _ x@(c:_))
410 | Char.isLower c ->
411 return (T.Var x)
412 | otherwise ->
413 return $ T.Type v
415 _ ->
416 error $
417 concat
418 [ "Problem converting the following type "
419 , "from a type-checker type to a source-syntax type:"
420 , P.render (pretty Never rootVariable)
421 ]
424termToSrcType :: Variable -> Term1 Variable -> IO T.Canonical
425termToSrcType rootVariable term =
426 let go = variableToSrcType rootVariable in
427 case term of
428 App1 a b ->
429 do a' <- go a
430 b' <- go b
431 case a' of
432 T.App f args ->
433 return $ T.App f (args ++ [b'])
434 _ ->
435 return $ T.App a' [b']
437 Fun1 a b ->
438 T.Lambda <$> go a <*> go b
440 Var1 a ->
441 go a
443 EmptyRecord1 ->
444 return $ T.Record [] Nothing
446 Record1 tfields extension ->
447 do fields' <- Traverse.traverse (mapM go) tfields
448 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
449 ext' <- dealias <$> go extension
450 return $
451 case ext' of
452 T.Record fs ext -> T.Record (fs ++ fields) ext
453 T.Var _ -> T.Record fields (Just ext')
454 _ -> error "Used toSrcType on a type that is not well-formed"
455 where
456 dealias :: T.Canonical -> T.Canonical
457 dealias tipe =
458 case tipe of
459 T.Aliased _ args tipe' ->
460 T.dealias args tipe'
461 _ ->
462 tipe
465-- ADD NAMES TO TYPES
467addNames :: Variable -> IO ()
468addNames variable =
469 do usedNames <- getVarNames variable
470 let freeNames = makeFreeNames usedNames
471 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
472 return ()
475makeFreeNames :: Set.Set String -> [String]
476makeFreeNames usedNames =
477 let makeName suffix =
478 map (:suffix) ['a'..'z']
480 allNames =
481 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
482 in
483 filter (\name -> Set.notMember name usedNames) allNames
486data NameState = NameState
487 { freeNames :: [String]
488 , numberPrimes :: Int
489 , comparablePrimes :: Int
490 , appendablePrimes :: Int
491 }
494varAddNames :: Variable -> StateT NameState IO ()
495varAddNames var =
496 do desc <- State.liftIO (UF.descriptor var)
497 case alias desc of
498 Nothing ->
499 return ()
501 Just (_name, args) ->
502 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
504 case structure desc of
505 Just term ->
506 termAddNames term
508 Nothing ->
509 case name desc of
510 Just _ -> return ()
511 Nothing ->
512 do name' <- createName desc
513 State.liftIO $ UF.modifyDescriptor var $ \desc ->
514 desc { name = Just (Var.local name') }
517termAddNames :: Term1 Variable -> StateT NameState IO ()
518termAddNames term =
519 case term of
520 App1 a b ->
521 do varAddNames a
522 varAddNames b
524 Fun1 a b ->
525 do varAddNames a
526 varAddNames b
528 Var1 a ->
529 varAddNames a
531 EmptyRecord1 ->
532 return ()
534 Record1 fields extension ->
535 do mapM_ varAddNames (concat (Map.elems fields))
536 varAddNames extension
539createName :: (Monad m) => Descriptor -> StateT NameState m String
540createName desc =
541 case flex desc of
542 Is Number ->
543 do primes <- State.gets numberPrimes
544 State.modify (\state -> state { numberPrimes = primes + 1 })
545 return ("number" ++ replicate primes '\'')
547 Is Comparable ->
548 do primes <- State.gets comparablePrimes
549 State.modify (\state -> state { comparablePrimes = primes + 1 })
550 return ("comparable" ++ replicate primes '\'')
552 Is Appendable ->
553 do primes <- State.gets appendablePrimes
554 State.modify (\state -> state { appendablePrimes = primes + 1 })
555 return ("appendable" ++ replicate primes '\'')
557 _ ->
558 do names <- State.gets freeNames
559 State.modify (\state -> state { freeNames = tail names })
560 return (head names)
563-- GET ALL VARIABLE NAMES
565getVarNames :: Variable -> IO (Set.Set String)
566getVarNames var =
567 do desc <- UF.descriptor var
569 let baseSet =
570 case name desc of
571 Just var -> Set.singleton (Var.toString var)
572 Nothing -> Set.empty
574 structureSet <-
575 case structure desc of
576 Nothing -> return Set.empty
577 Just term -> getVarNamesTerm term
579 aliasSet <-
580 case alias desc of
581 Nothing ->
582 return Set.empty
584 Just (_name, args) ->
585 do let set = Set.fromList (map fst args)
586 sets <- mapM (getVarNames . snd) args
587 return (Set.unions (set : sets))
589 return (Set.unions [ baseSet, structureSet, aliasSet ])
592getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
593getVarNamesTerm term =
594 let go = getVarNames in
595 case term of
596 App1 a b ->
597 Set.union <$> go a <*> go b
599 Fun1 a b ->
600 Set.union <$> go a <*> go b
602 Var1 a ->
603 go a
605 EmptyRecord1 ->
606 return Set.empty
608 Record1 fields extension ->
609 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
610 Set.union fieldVars <$> go extension
613-- COLLECT APPLICATIONS
615data AppStructure
616 = List Variable
617 | Tuple [Variable]
618 | Other
621collectApps :: Variable -> IO AppStructure
622collectApps var =
623 go [] var
624 where
625 go vars var = do
626 desc <- UF.descriptor var
627 case (structure desc, vars) of
628 (Nothing, [v]) ->
629 case name desc of
630 Just n | Var.isList n -> return (List v)
631 _ -> return Other
633 (Nothing, vs) ->
634 case name desc of
635 Just n | Var.isTuple n -> return (Tuple vs)
636 _ -> return Other
638 (Just term, _) ->
639 case term of
640 App1 a b -> go (vars ++ [b]) a
641 _ -> return Other