git.iko.soy/elk
on defb40c help sign in
elk/src/Type/Type.hs
621 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 Control.Monad.Error (ErrorT, Error, liftIO)
7import qualified Data.Char as Char
8import qualified Data.Map as Map
9import qualified Data.Set as Set
10import qualified Data.Traversable as Traverse (traverse)
11import qualified Data.UnionFind.IO as UF
12import Text.PrettyPrint as P
13import System.IO.Unsafe
15import AST.Annotation
16import qualified AST.PrettyPrint as PP
17import qualified AST.Type as T
18import qualified AST.Variable as Var
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
106type Constraint a b =
107 Located (BasicConstraint a b)
109data BasicConstraint a b
110 = CTrue
111 | CSaveEnv
112 | CEqual a a
113 | CAnd [Constraint a b]
114 | CLet [Scheme a b] (Constraint a b)
115 | CInstance SchemeName a
117type SchemeName = String
119type TypeName = Var.Canonical
121data Scheme a b = Scheme
122 { rigidQuantifiers :: [b]
123 , flexibleQuantifiers :: [b]
124 , constraint :: Constraint a b
125 , header :: Map.Map String a
126 }
129-- TYPE HELPERS
131infixr 9 ==>
133(==>) :: Type -> Type -> Type
134(==>) a b =
135 termN (Fun1 a b)
138(<|) :: TermN a -> TermN a -> TermN a
139(<|) f a =
140 termN (App1 f a)
143-- VARIABLE HELPERS
145namedVar :: Flex -> Var.Canonical -> IO Variable
146namedVar flex name = UF.fresh $ Descriptor
147 { structure = Nothing
148 , rank = noRank
149 , flex = flex
150 , name = Just name
151 , copy = Nothing
152 , mark = noMark
153 , alias = Nothing
154 }
157variable :: Flex -> IO Variable
158variable flex = UF.fresh $ Descriptor
159 { structure = Nothing
160 , rank = noRank
161 , flex = flex
162 , name = Nothing
163 , copy = Nothing
164 , mark = noMark
165 , alias = Nothing
166 }
169-- CONSTRAINT HELPERS
171monoscheme :: Map.Map String a -> Scheme a b
172monoscheme headers =
173 Scheme [] [] (noneNoDocs CTrue) headers
176infixl 8 /\
178(/\) :: Constraint a b -> Constraint a b -> Constraint a b
179(/\) a@(A _ c1) b@(A _ c2) =
180 case (c1, c2) of
181 (CTrue, _) -> b
182 (_, CTrue) -> a
183 _ -> mergeOldDocs a b (CAnd [a,b])
186-- ex qs constraint == exists qs. constraint
187ex :: [Variable] -> TypeConstraint -> TypeConstraint
188ex fqs constraint@(A ann _) =
189 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
192-- fl qs constraint == forall qs. constraint
193fl :: [Variable] -> TypeConstraint -> TypeConstraint
194fl rqs constraint@(A ann _) =
195 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
198exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
199exists f =
200 do v <- liftIO $ variable Flexible
201 ex [v] <$> f (varN v)
204existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
205existsNumber f =
206 do v <- liftIO $ variable (Is Number)
207 ex [v] <$> f (varN v)
210-- TYPES TO PRETTY STRINGS
212instance PrettyType a => PrettyType (UF.Point a) where
213 pretty when point =
214 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
217instance PrettyType t => PrettyType (Annotated a t) where
218 pretty when (A _ e) =
219 pretty when e
222instance PrettyType a => PrettyType (Term1 a) where
223 pretty when term =
224 let prty = pretty Never in
225 case term of
226 App1 f x ->
227 parensIf needed (px <+> pretty App x)
228 where
229 px = prty f
230 needed =
231 case when of
232 App -> True
233 _ -> False
235 Fun1 arg body ->
236 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
237 where
238 needed =
239 case when of
240 Never -> False
241 _ -> True
243 Var1 x ->
244 prty x
246 EmptyRecord1 ->
247 P.braces P.empty
249 Record1 fields ext ->
250 P.braces (extend <+> commaSep prettyFields)
251 where
252 prettyExt = prty ext
254 extend
255 | P.render prettyExt == "{}" =
256 P.empty
257 | otherwise =
258 prettyExt <+> P.text "|"
260 mkPretty f t =
261 P.text f <+> P.text ":" <+> prty t
263 prettyFields =
264 concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
267instance PrettyType a => PrettyType (TermN a) where
268 pretty when term =
269 case term of
270 PlaceHolder _ ->
271 error "problem prettifying type, probably indicates a bigger problem"
273 VarN alias x ->
274 either alias (pretty when x)
276 TermN alias t1 ->
277 either alias (pretty when t1)
278 where
279 either maybeAlias doc =
280 case maybeAlias of
281 Nothing -> doc
282 Just (name, args) ->
283 P.hang (PP.pretty name) 2 (P.sep (map (pretty App . snd) args))
286instance PrettyType Descriptor where
287 pretty when desc =
288 case (alias desc, structure desc, name desc) of
289 (Just (name, args), _, _) ->
290 P.hang (PP.pretty name) 4 (P.sep (map (pretty App . snd) args))
292 (_, Just term, _) ->
293 pretty when term
295 (_, _, Just name)
296 | Var.isTuple name ->
297 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
298 | otherwise ->
299 P.text (Var.toString name)
301 _ -> P.text "?"
304instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
305 pretty _ constraint =
306 let prty = pretty Never in
307 case constraint of
308 CTrue -> P.text "True"
309 CSaveEnv -> P.text "SaveTheEnvironment!!!"
310 CEqual a b -> prty a <+> P.text "=" <+> prty b
311 CAnd [] -> P.text "True"
313 CAnd cs ->
314 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
316 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
317 P.sep [ binder, pretty Never c ]
318 where
319 mergeExists vs (A _ c) =
320 case c of
321 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
322 _ -> (vs, c)
324 (fqs', c) = mergeExists fqs constraint
326 binder = if null fqs' then P.empty else
327 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
329 CLet schemes constraint ->
330 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
331 , P.text "in", pretty Never constraint ]
333 CInstance name tipe ->
334 P.text name <+> P.text "<" <+> prty tipe
337instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
338 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
339 P.sep [ forall, cs, headers' ]
340 where
341 prty = pretty Never
343 forall = if null rqs && null fqs then P.empty else
344 P.text "\x2200" <+> frees <+> rigids
346 frees = P.hsep $ map prty fqs
347 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
349 cs = case constraint of
350 CTrue -> P.empty
351 CAnd [] -> P.empty
352 _ -> P.brackets (pretty Never constraint)
354 headers' = if Map.size headers > 0 then dict else P.empty
355 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
356 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
359-- CONVERT TO SOURCE TYPES
361-- TODO: Attach resulting type to the descriptor so that you
362-- never have to do extra work, particularly nice for aliased types
363toSrcType :: Variable -> IO T.CanonicalType
364toSrcType variable =
365 do addNames variable
366 variableToSrcType variable variable
369variableToSrcType :: Variable -> Variable -> IO T.CanonicalType
370variableToSrcType rootVariable variable =
371 do desc <- UF.descriptor variable
372 srcType <- maybe (backupSrcType desc) (termToSrcType rootVariable) (structure desc)
373 case alias desc of
374 Nothing ->
375 return srcType
377 Just (name, args) ->
378 case srcType of
379 T.Type (Var.Canonical Var.BuiltIn _) ->
380 return srcType
382 _ ->
383 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
384 return (T.Aliased name args' (T.Filled srcType))
385 where
386 backupSrcType :: Descriptor -> IO T.CanonicalType
387 backupSrcType desc =
388 case name desc of
389 Just v@(Var.Canonical _ x@(c:_))
390 | Char.isLower c ->
391 return (T.Var x)
392 | otherwise ->
393 return $ T.Type v
395 _ ->
396 error $
397 concat
398 [ "Problem converting the following type "
399 , "from a type-checker type to a source-syntax type:"
400 , P.render (pretty Never rootVariable)
401 ]
404termToSrcType :: Variable -> Term1 Variable -> IO T.CanonicalType
405termToSrcType rootVariable term =
406 let go = variableToSrcType rootVariable in
407 case term of
408 App1 a b ->
409 do a' <- go a
410 b' <- go b
411 case a' of
412 T.App f args ->
413 return $ T.App f (args ++ [b'])
414 _ ->
415 return $ T.App a' [b']
417 Fun1 a b ->
418 T.Lambda <$> go a <*> go b
420 Var1 a ->
421 go a
423 EmptyRecord1 ->
424 return $ T.Record [] Nothing
426 Record1 tfields extension ->
427 do fields' <- Traverse.traverse (mapM go) tfields
428 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
429 ext' <- dealias <$> go extension
430 return $
431 case ext' of
432 T.Record fs ext -> T.Record (fs ++ fields) ext
433 T.Var _ -> T.Record fields (Just ext')
434 _ -> error "Used toSrcType on a type that is not well-formed"
435 where
436 dealias :: T.CanonicalType -> T.CanonicalType
437 dealias tipe =
438 case tipe of
439 T.Aliased _ args tipe' ->
440 T.dealias args tipe'
441 _ ->
442 tipe
445-- ADD NAMES TO TYPES
447addNames :: Variable -> IO ()
448addNames variable =
449 do usedNames <- getVarNames variable
450 let freeNames = makeFreeNames usedNames
451 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
452 return ()
455makeFreeNames :: Set.Set String -> [String]
456makeFreeNames usedNames =
457 let makeName suffix =
458 map (:suffix) ['a'..'z']
460 allNames =
461 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
462 in
463 filter (\name -> Set.notMember name usedNames) allNames
466data NameState = NameState
467 { freeNames :: [String]
468 , numberPrimes :: Int
469 , comparablePrimes :: Int
470 , appendablePrimes :: Int
471 }
474varAddNames :: Variable -> StateT NameState IO ()
475varAddNames var =
476 do desc <- liftIO (UF.descriptor var)
477 case alias desc of
478 Nothing ->
479 return ()
481 Just (_name, args) ->
482 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
484 case structure desc of
485 Just term ->
486 termAddNames term
488 Nothing ->
489 case name desc of
490 Just _ -> return ()
491 Nothing ->
492 do name' <- createName desc
493 liftIO $ UF.modifyDescriptor var $ \desc ->
494 desc { name = Just (Var.local name') }
497termAddNames :: Term1 Variable -> StateT NameState IO ()
498termAddNames term =
499 case term of
500 App1 a b ->
501 do varAddNames a
502 varAddNames b
504 Fun1 a b ->
505 do varAddNames a
506 varAddNames b
508 Var1 a ->
509 varAddNames a
511 EmptyRecord1 ->
512 return ()
514 Record1 fields extension ->
515 do mapM_ varAddNames (concat (Map.elems fields))
516 varAddNames extension
519createName :: (Monad m) => Descriptor -> StateT NameState m String
520createName desc =
521 case flex desc of
522 Is Number ->
523 do primes <- State.gets numberPrimes
524 State.modify (\state -> state { numberPrimes = primes + 1 })
525 return ("number" ++ replicate primes '\'')
527 Is Comparable ->
528 do primes <- State.gets comparablePrimes
529 State.modify (\state -> state { comparablePrimes = primes + 1 })
530 return ("comparable" ++ replicate primes '\'')
532 Is Appendable ->
533 do primes <- State.gets appendablePrimes
534 State.modify (\state -> state { appendablePrimes = primes + 1 })
535 return ("appendable" ++ replicate primes '\'')
537 _ ->
538 do names <- State.gets freeNames
539 State.modify (\state -> state { freeNames = tail names })
540 return (head names)
543-- GET ALL VARIABLE NAMES
545getVarNames :: Variable -> IO (Set.Set String)
546getVarNames var =
547 do desc <- UF.descriptor var
549 let baseSet =
550 case name desc of
551 Just var -> Set.singleton (Var.toString var)
552 Nothing -> Set.empty
554 structureSet <-
555 case structure desc of
556 Nothing -> return Set.empty
557 Just term -> getVarNamesTerm term
559 aliasSet <-
560 case alias desc of
561 Nothing ->
562 return Set.empty
564 Just (_name, args) ->
565 do let set = Set.fromList (map fst args)
566 sets <- mapM (getVarNames . snd) args
567 return (Set.unions (set : sets))
569 return (Set.unions [ baseSet, structureSet, aliasSet ])
572getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
573getVarNamesTerm term =
574 let go = getVarNames in
575 case term of
576 App1 a b ->
577 Set.union <$> go a <*> go b
579 Fun1 a b ->
580 Set.union <$> go a <*> go b
582 Var1 a ->
583 go a
585 EmptyRecord1 ->
586 return Set.empty
588 Record1 fields extension ->
589 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
590 Set.union fieldVars <$> go extension
593-- COLLECT APPLICATIONS
595data AppStructure
596 = List Variable
597 | Tuple [Variable]
598 | Other
601collectApps :: Variable -> IO AppStructure
602collectApps var =
603 go [] var
604 where
605 go vars var = do
606 desc <- UF.descriptor var
607 case (structure desc, vars) of
608 (Nothing, [v]) ->
609 case name desc of
610 Just n | Var.isList n -> return (List v)
611 _ -> return Other
613 (Nothing, vs) ->
614 case name desc of
615 Just n | Var.isTuple n -> return (Tuple vs)
616 _ -> return Other
618 (Just term, _) ->
619 case term of
620 App1 a b -> go (vars ++ [b]) a
621 _ -> return Other