git.iko.soy/elk
on 8a87749 help sign in
elk/src/Type/Type.hs
616 lines 15 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 do args' <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType rootVariable tvar) args
379 return (T.Aliased name args' (T.Filled srcType))
380 where
381 backupSrcType :: Descriptor -> IO T.CanonicalType
382 backupSrcType desc =
383 case name desc of
384 Just v@(Var.Canonical _ x@(c:_))
385 | Char.isLower c ->
386 return (T.Var x)
387 | otherwise ->
388 return $ T.Type v
390 _ ->
391 error $
392 concat
393 [ "Problem converting the following type "
394 , "from a type-checker type to a source-syntax type:"
395 , P.render (pretty Never rootVariable)
396 ]
399termToSrcType :: Variable -> Term1 Variable -> IO T.CanonicalType
400termToSrcType rootVariable term =
401 let go = variableToSrcType rootVariable in
402 case term of
403 App1 a b ->
404 do a' <- go a
405 b' <- go b
406 case a' of
407 T.App f args ->
408 return $ T.App f (args ++ [b'])
409 _ ->
410 return $ T.App a' [b']
412 Fun1 a b ->
413 T.Lambda <$> go a <*> go b
415 Var1 a ->
416 go a
418 EmptyRecord1 ->
419 return $ T.Record [] Nothing
421 Record1 tfields extension ->
422 do fields' <- Traverse.traverse (mapM go) tfields
423 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
424 ext' <- dealias <$> go extension
425 return $
426 case ext' of
427 T.Record fs ext -> T.Record (fs ++ fields) ext
428 T.Var _ -> T.Record fields (Just ext')
429 _ -> error "Used toSrcType on a type that is not well-formed"
430 where
431 dealias :: T.CanonicalType -> T.CanonicalType
432 dealias tipe =
433 case tipe of
434 T.Aliased _ args tipe' ->
435 T.dealias args tipe'
436 _ ->
437 tipe
440-- ADD NAMES TO TYPES
442addNames :: Variable -> IO ()
443addNames variable =
444 do usedNames <- getVarNames variable
445 let freeNames = makeFreeNames usedNames
446 State.runStateT (varAddNames variable) (NameState freeNames 0 0 0)
447 return ()
450makeFreeNames :: Set.Set String -> [String]
451makeFreeNames usedNames =
452 let makeName suffix =
453 map (:suffix) ['a'..'z']
455 allNames =
456 concatMap makeName ("" : "'" : "_" : map show [ (0 :: Int) .. ])
457 in
458 filter (\name -> Set.notMember name usedNames) allNames
461data NameState = NameState
462 { freeNames :: [String]
463 , numberPrimes :: Int
464 , comparablePrimes :: Int
465 , appendablePrimes :: Int
466 }
469varAddNames :: Variable -> StateT NameState IO ()
470varAddNames var =
471 do desc <- liftIO (UF.descriptor var)
472 case alias desc of
473 Nothing ->
474 return ()
476 Just (_name, args) ->
477 mapM_ (\(v,t) -> (,) v <$> varAddNames t) args
479 case structure desc of
480 Just term ->
481 termAddNames term
483 Nothing ->
484 case name desc of
485 Just _ -> return ()
486 Nothing ->
487 do name' <- createName desc
488 liftIO $ UF.modifyDescriptor var $ \desc ->
489 desc { name = Just (Var.local name') }
492termAddNames :: Term1 Variable -> StateT NameState IO ()
493termAddNames term =
494 case term of
495 App1 a b ->
496 do varAddNames a
497 varAddNames b
499 Fun1 a b ->
500 do varAddNames a
501 varAddNames b
503 Var1 a ->
504 varAddNames a
506 EmptyRecord1 ->
507 return ()
509 Record1 fields extension ->
510 do mapM_ varAddNames (concat (Map.elems fields))
511 varAddNames extension
514createName :: (Monad m) => Descriptor -> StateT NameState m String
515createName desc =
516 case flex desc of
517 Is Number ->
518 do primes <- State.gets numberPrimes
519 State.modify (\state -> state { numberPrimes = primes + 1 })
520 return ("number" ++ replicate primes '\'')
522 Is Comparable ->
523 do primes <- State.gets comparablePrimes
524 State.modify (\state -> state { comparablePrimes = primes + 1 })
525 return ("comparable" ++ replicate primes '\'')
527 Is Appendable ->
528 do primes <- State.gets appendablePrimes
529 State.modify (\state -> state { appendablePrimes = primes + 1 })
530 return ("appendable" ++ replicate primes '\'')
532 _ ->
533 do names <- State.gets freeNames
534 State.modify (\state -> state { freeNames = tail names })
535 return (head names)
538-- GET ALL VARIABLE NAMES
540getVarNames :: Variable -> IO (Set.Set String)
541getVarNames var =
542 do desc <- UF.descriptor var
544 let baseSet =
545 case name desc of
546 Just var -> Set.singleton (Var.toString var)
547 Nothing -> Set.empty
549 structureSet <-
550 case structure desc of
551 Nothing -> return Set.empty
552 Just term -> getVarNamesTerm term
554 aliasSet <-
555 case alias desc of
556 Nothing ->
557 return Set.empty
559 Just (_name, args) ->
560 do let set = Set.fromList (map fst args)
561 sets <- mapM (getVarNames . snd) args
562 return (Set.unions (set : sets))
564 return (Set.unions [ baseSet, structureSet, aliasSet ])
567getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
568getVarNamesTerm term =
569 let go = getVarNames in
570 case term of
571 App1 a b ->
572 Set.union <$> go a <*> go b
574 Fun1 a b ->
575 Set.union <$> go a <*> go b
577 Var1 a ->
578 go a
580 EmptyRecord1 ->
581 return Set.empty
583 Record1 fields extension ->
584 do fieldVars <- Set.unions <$> mapM go (concat (Map.elems fields))
585 Set.union fieldVars <$> go extension
588-- COLLECT APPLICATIONS
590data AppStructure
591 = List Variable
592 | Tuple [Variable]
593 | Other
596collectApps :: Variable -> IO AppStructure
597collectApps var =
598 go [] var
599 where
600 go vars var = do
601 desc <- UF.descriptor var
602 case (structure desc, vars) of
603 (Nothing, [v]) ->
604 case name desc of
605 Just n | Var.isList n -> return (List v)
606 _ -> return Other
608 (Nothing, vs) ->
609 case name desc of
610 Just n | Var.isTuple n -> return (Tuple vs)
611 _ -> return Other
613 (Just term, _) ->
614 case term of
615 App1 a b -> go (vars ++ [b]) a
616 _ -> return Other