git.iko.soy/elk
on 446c784 help sign in
elk/src/Type/Type.hs
643 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 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 = UF.fresh $ Descriptor
156 { structure = Nothing
157 , rank = noRank
158 , flex = flex
159 , name = Nothing
160 , copy = Nothing
161 , mark = noMark
162 , alias = Nothing
163 }
166-- CONSTRAINT HELPERS
168monoscheme :: Map.Map String (A.Located a) -> Scheme a b
169monoscheme headers =
170 Scheme [] [] CTrue headers
173infixl 8 /\
175(/\) :: Constraint a b -> Constraint a b -> Constraint a b
176(/\) c1 c2 =
177 case (c1, c2) of
178 (CTrue, _) -> c2
179 (_, CTrue) -> c1
180 _ -> CAnd [c1,c2]
183-- ex qs constraint == exists qs. constraint
184ex :: [Variable] -> TypeConstraint -> TypeConstraint
185ex fqs constraint =
186 CLet [Scheme [] fqs constraint Map.empty] CTrue
189-- fl qs constraint == forall qs. constraint
190fl :: [Variable] -> TypeConstraint -> TypeConstraint
191fl rqs constraint =
192 CLet [Scheme rqs [] constraint Map.empty] CTrue
195exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
196exists f =
197 do v <- variable Flexible
198 ex [v] <$> f (varN v)
201existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
202existsNumber f =
203 do v <- variable (Is Number)
204 ex [v] <$> f (varN v)
207-- TYPES TO PRETTY STRINGS
209instance PrettyType a => PrettyType (UF.Point a) where
210 pretty when point =
211 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
214instance PrettyType a => PrettyType (Term1 a) where
215 pretty when term =
216 let prty = pretty Never in
217 case term of
218 App1 f x ->
219 parensIf needed (px <+> pretty App x)
220 where
221 px = prty f
222 needed =
223 case when of
224 App -> True
225 _ -> False
227 Fun1 arg body ->
228 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
229 where
230 needed =
231 case when of
232 Never -> False
233 _ -> True
235 Var1 x ->
236 prty x
238 EmptyRecord1 ->
239 P.braces P.empty
241 Record1 fields ext ->
242 P.braces (extend <+> commaSep prettyFields)
243 where
244 prettyExt = prty ext
246 extend
247 | P.render prettyExt == "{}" =
248 P.empty
249 | otherwise =
250 prettyExt <+> P.text "|"
252 mkPretty f t =
253 P.text f <+> P.text ":" <+> prty t
255 prettyFields =
256 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
259instance PrettyType a => PrettyType (TermN a) where
260 pretty when term =
261 case term of
262 PlaceHolder _ ->
263 error "problem prettifying type, probably indicates a bigger problem"
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 Nothing -> doc
274 Just (name, args) ->
275 P.hang
276 (P.text (Var.toString name))
277 2
278 (P.sep (map (pretty App . snd) args))
281instance PrettyType Descriptor where
282 pretty when desc =
283 case (alias desc, structure desc, name desc) of
284 (Just (name, args), _, _) ->
285 P.hang
286 (P.text (Var.toString name))
287 4
288 (P.sep (map (pretty App . snd) args))
290 (_, Just term, _) ->
291 pretty when term
293 (_, _, Just name)
294 | Var.isTuple name ->
295 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
296 | otherwise ->
297 P.text (Var.toString name)
299 _ -> P.text "?"
302instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
303 pretty _ constraint =
304 let prty = pretty Never in
305 case constraint of
306 CTrue ->
307 P.text "True"
309 CSaveEnv ->
310 P.text "SaveTheEnvironment!!!"
312 CEqual _ _ a b ->
313 prty a <+> P.text "=" <+> prty b
315 CAnd [] ->
316 P.text "True"
318 CAnd cs ->
319 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
321 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
322 P.sep [ binder, pretty Never c ]
323 where
324 mergeExists vs c =
325 case c of
326 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
327 _ -> (vs, c)
329 (fqs', c) = mergeExists fqs constraint
331 binder =
332 if null fqs'
333 then P.empty
334 else
335 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
337 CLet schemes constraint ->
338 P.fsep
339 [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
340 , P.text "in", pretty Never constraint
341 ]
343 CInstance _region name tipe ->
344 P.text name <+> P.text "<" <+> prty tipe
347instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
348 pretty _ (Scheme rqs fqs constraint headers) =
349 P.sep [ forall, cs, headers' ]
350 where
351 prty = pretty Never
353 forall =
354 if null rqs && null fqs
355 then P.empty
356 else P.text "\x2200" <+> frees <+> rigids
358 frees = P.hsep (map prty fqs)
360 rigids =
361 if null rqs
362 then P.empty
363 else P.braces . P.hsep $ map prty rqs
365 cs =
366 case constraint of
367 CTrue -> P.empty
368 CAnd [] -> P.empty
369 _ -> P.brackets (pretty Never constraint)
371 headers' =
372 if Map.size headers > 0 then dict else P.empty
374 dict =
375 P.parens . commaSep . map prettyPair $ Map.toList headers
377 prettyPair (fieldName, A.A _ tipe) =
378 P.text fieldName <+> P.text ":" <+> pretty Never tipe
381-- CONVERT TO SOURCE TYPES
383-- TODO: Attach resulting type to the descriptor so that you
384-- never have to do extra work, particularly nice for aliased types
385toSrcType :: Variable -> IO T.Canonical
386toSrcType variable =
387 do addNames variable
388 variableToSrcType variable variable
391variableToSrcType :: Variable -> Variable -> IO T.Canonical
392variableToSrcType rootVariable variable =
393 do desc <- UF.descriptor variable
394 srcType <- maybe (backupSrcType desc) (termToSrcType rootVariable) (structure desc)
395 case alias desc of
396 Nothing ->
397 return srcType
399 Just (name, args) ->
400 case srcType of
401 T.Type (Var.Canonical Var.BuiltIn _) ->
402 return srcType
404 _ ->
405 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
406 return (T.Aliased name args' (T.Filled srcType))
407 where
408 backupSrcType :: Descriptor -> IO T.Canonical
409 backupSrcType desc =
410 case name desc of
411 Just v@(Var.Canonical _ x@(c:_))
412 | Char.isLower c ->
413 return (T.Var x)
414 | otherwise ->
415 return $ T.Type v
417 _ ->
418 error $
419 concat
420 [ "Problem converting the following type "
421 , "from a type-checker type to a source-syntax type:"
422 , P.render (pretty Never rootVariable)
423 ]
426termToSrcType :: Variable -> Term1 Variable -> IO T.Canonical
427termToSrcType rootVariable term =
428 let go = variableToSrcType rootVariable in
429 case term of
430 App1 a b ->
431 do a' <- go a
432 b' <- go b
433 case a' of
434 T.App f args ->
435 return $ T.App f (args ++ [b'])
436 _ ->
437 return $ T.App a' [b']
439 Fun1 a b ->
440 T.Lambda <$> go a <*> go b
442 Var1 a ->
443 go a
445 EmptyRecord1 ->
446 return $ T.Record [] Nothing
448 Record1 tfields extension ->
449 do fields' <- Traverse.traverse (mapM go) tfields
450 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
451 ext' <- dealias <$> go extension
452 return $
453 case ext' of
454 T.Record fs ext -> T.Record (fs ++ fields) ext
455 T.Var _ -> T.Record fields (Just ext')
456 _ -> error "Used toSrcType on a type that is not well-formed"
457 where
458 dealias :: T.Canonical -> T.Canonical
459 dealias tipe =
460 case tipe of
461 T.Aliased _ args tipe' ->
462 T.dealias args tipe'
463 _ ->
464 tipe
467-- ADD NAMES TO TYPES
469addNames :: Variable -> IO ()
470addNames variable =
471 do usedNames <- getVarNames variable
472 let freeNames = makeFreeNames usedNames
473 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
474 return ()
477makeFreeNames :: Set.Set String -> [String]
478makeFreeNames usedNames =
479 let makeName suffix =
480 map (:suffix) ['a'..'z']
482 allNames =
483 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
484 in
485 filter (\name -> Set.notMember name usedNames) allNames
488data NameState = NameState
489 { freeNames :: [String]
490 , numberPrimes :: Int
491 , comparablePrimes :: Int
492 , appendablePrimes :: Int
493 }
496varAddNames :: Variable -> StateT NameState IO ()
497varAddNames var =
498 do desc <- State.liftIO (UF.descriptor var)
499 case alias desc of
500 Nothing ->
501 return ()
503 Just (_name, args) ->
504 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
506 case structure desc of
507 Just term ->
508 termAddNames term
510 Nothing ->
511 case name desc of
512 Just _ -> return ()
513 Nothing ->
514 do name' <- createName desc
515 State.liftIO $ UF.modifyDescriptor var $ \desc ->
516 desc { name = Just (Var.local name') }
519termAddNames :: Term1 Variable -> StateT NameState IO ()
520termAddNames term =
521 case term of
522 App1 a b ->
523 do varAddNames a
524 varAddNames b
526 Fun1 a b ->
527 do varAddNames a
528 varAddNames b
530 Var1 a ->
531 varAddNames a
533 EmptyRecord1 ->
534 return ()
536 Record1 fields extension ->
537 do mapM_ varAddNames (concat (Map.elems fields))
538 varAddNames extension
541createName :: (Monad m) => Descriptor -> StateT NameState m String
542createName desc =
543 case flex desc of
544 Is Number ->
545 do primes <- State.gets numberPrimes
546 State.modify (\state -> state { numberPrimes = primes + 1 })
547 return ("number" ++ replicate primes '\'')
549 Is Comparable ->
550 do primes <- State.gets comparablePrimes
551 State.modify (\state -> state { comparablePrimes = primes + 1 })
552 return ("comparable" ++ replicate primes '\'')
554 Is Appendable ->
555 do primes <- State.gets appendablePrimes
556 State.modify (\state -> state { appendablePrimes = primes + 1 })
557 return ("appendable" ++ replicate primes '\'')
559 _ ->
560 do names <- State.gets freeNames
561 State.modify (\state -> state { freeNames = tail names })
562 return (head names)
565-- GET ALL VARIABLE NAMES
567getVarNames :: Variable -> IO (Set.Set String)
568getVarNames var =
569 do desc <- UF.descriptor var
571 let baseSet =
572 case name desc of
573 Just var -> Set.singleton (Var.toString var)
574 Nothing -> Set.empty
576 structureSet <-
577 case structure desc of
578 Nothing -> return Set.empty
579 Just term -> getVarNamesTerm term
581 aliasSet <-
582 case alias desc of
583 Nothing ->
584 return Set.empty
586 Just (_name, args) ->
587 do let set = Set.fromList (map fst args)
588 sets <- mapM (getVarNames . snd) args
589 return (Set.unions (set : sets))
591 return (Set.unions [ baseSet, structureSet, aliasSet ])
594getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
595getVarNamesTerm term =
596 let go = getVarNames in
597 case term of
598 App1 a b ->
599 Set.union <$> go a <*> go b
601 Fun1 a b ->
602 Set.union <$> go a <*> go b
604 Var1 a ->
605 go a
607 EmptyRecord1 ->
608 return Set.empty
610 Record1 fields extension ->
611 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
612 Set.union fieldVars <$> go extension
615-- COLLECT APPLICATIONS
617data AppStructure
618 = List Variable
619 | Tuple [Variable]
620 | Other
623collectApps :: Variable -> IO AppStructure
624collectApps var =
625 go [] var
626 where
627 go vars var = do
628 desc <- UF.descriptor var
629 case (structure desc, vars) of
630 (Nothing, [v]) ->
631 case name desc of
632 Just n | Var.isList n -> return (List v)
633 _ -> return Other
635 (Nothing, vs) ->
636 case name desc of
637 Just n | Var.isTuple n -> return (Tuple vs)
638 _ -> return Other
640 (Just term, _) ->
641 case term of
642 App1 a b -> go (vars ++ [b]) a
643 _ -> return Other