git.iko.soy/elk
on ff9acf5 help sign in
elk/src/Type/Type.hs
523 lines 14 kB history raw
1module Type.Type where
3import qualified Data.Char as Char
4import qualified Data.List as List
5import qualified Data.Map as Map
6import qualified Data.UnionFind.IO as UF
7import Type.PrettyPrint
8import Text.PrettyPrint as P
9import System.IO.Unsafe
10import Control.Applicative ((<$>),(<*>))
11import Control.Monad.State (StateT, get, put, execStateT, runStateT)
12import Control.Monad.Error (ErrorT, Error, liftIO)
13import Data.Traversable (traverse)
14import AST.Annotation
15import qualified AST.PrettyPrint as PP
16import qualified AST.Type as T
17import qualified AST.Variable as Var
20data Term1 a
21 = App1 a a
22 | Fun1 a a
23 | Var1 a
24 | EmptyRecord1
25 | Record1 (Map.Map String [a]) a
26 deriving Show
29data TermN a
30 = VarN (Maybe Var.Canonical) a
31 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
32 deriving Show
35varN :: a -> TermN a
36varN = VarN Nothing
39termN :: (Term1 (TermN a)) -> TermN a
40termN = TermN Nothing
43record :: Map.Map String [TermN a] -> TermN a -> TermN a
44record fs rec = termN (Record1 fs rec)
47type Type = TermN Variable
50type Variable = UF.Point Descriptor
53type SchemeName = String
56type TypeName = Var.Canonical
59type Constraint a b = Located (BasicConstraint a b)
62data BasicConstraint a b
63 = CTrue
64 | CSaveEnv
65 | CEqual a a
66 | CAnd [Constraint a b]
67 | CLet [Scheme a b] (Constraint a b)
68 | CInstance SchemeName a
69 deriving Show
72data Scheme a b = Scheme
73 { rigidQuantifiers :: [b]
74 , flexibleQuantifiers :: [b]
75 , constraint :: Constraint a b
76 , header :: Map.Map String a
77 }
78 deriving Show
81type TypeConstraint = Constraint Type Variable
83type TypeScheme = Scheme Type Variable
86monoscheme :: Map.Map String a -> Scheme a b
87monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
90infixl 8 /\
92(/\) :: Constraint a b -> Constraint a b -> Constraint a b
93a@(A _ c1) /\ b@(A _ c2) =
94 case (c1, c2) of
95 (CTrue, _) -> b
96 (_, CTrue) -> a
97 _ -> mergeOldDocs a b (CAnd [a,b])
100infixr 9 ==>
102(==>) :: Type -> Type -> Type
103a ==> b = termN (Fun1 a b)
106(<|) :: TermN a -> TermN a -> TermN a
107f <| a = termN (App1 f a)
110data Descriptor = Descriptor
111 { structure :: Maybe (Term1 Variable)
112 , rank :: Int
113 , flex :: Flex
114 , name :: Maybe TypeName
115 , copy :: Maybe Variable
116 , mark :: Int
117 , alias :: Maybe Var.Canonical
118 }
119 deriving Show
122noRank :: Int
123noRank = -1
126outermostRank :: Int
127outermostRank = 0
130noMark :: Int
131noMark = 0
134initialMark :: Int
135initialMark = 1
138data Flex
139 = Rigid
140 | Flexible
141 | Constant
142 | Is SuperType
143 deriving (Show, Eq)
146data SuperType
147 = Number
148 | Comparable
149 | Appendable
150 deriving (Show, Eq)
153namedVar :: Flex -> Var.Canonical -> IO Variable
154namedVar flex name = UF.fresh $ Descriptor
155 { structure = Nothing
156 , rank = noRank
157 , flex = flex
158 , name = Just name
159 , copy = Nothing
160 , mark = noMark
161 , alias = Nothing
162 }
165variable :: Flex -> IO Variable
166variable flex = UF.fresh $ Descriptor
167 { structure = Nothing
168 , rank = noRank
169 , flex = flex
170 , name = Nothing
171 , copy = Nothing
172 , mark = noMark
173 , alias = Nothing
174 }
177-- ex qs constraint == exists qs. constraint
178ex :: [Variable] -> TypeConstraint -> TypeConstraint
179ex fqs constraint@(A ann _) =
180 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
183-- fl qs constraint == forall qs. constraint
184fl :: [Variable] -> TypeConstraint -> TypeConstraint
185fl rqs constraint@(A ann _) =
186 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
189exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
190exists f =
191 do v <- liftIO $ variable Flexible
192 ex [v] <$> f (varN v)
195existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
196existsNumber f =
197 do v <- liftIO $ variable (Is Number)
198 ex [v] <$> f (varN v)
201-- TYPES TO PRETTY STRINGS
203instance Show a => Show (UF.Point a) where
204 show point =
205 unsafePerformIO $ fmap show (UF.descriptor point)
208instance PrettyType a => PrettyType (UF.Point a) where
209 pretty when point =
210 unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
213instance PrettyType t => PrettyType (Annotated a t) where
214 pretty when (A _ e) =
215 pretty when e
218instance PrettyType a => PrettyType (Term1 a) where
219 pretty when term =
220 let prty = pretty Never in
221 case term of
222 App1 f x ->
223 parensIf needed (px <+> pretty App x)
224 where
225 px = prty f
226 needed = case when of
227 App -> True
228 _ -> False
230 Fun1 arg body ->
231 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
232 where
233 needed = case when of
234 Never -> False
235 _ -> True
237 Var1 x -> prty x
239 EmptyRecord1 -> P.braces P.empty
241 Record1 fields ext ->
242 P.braces (extend <+> commaSep prettyFields)
243 where
244 prettyExt = prty ext
245 extend | P.render prettyExt == "{}" = P.empty
246 | otherwise = prettyExt <+> P.text "|"
247 mkPretty f t = P.text f <+> P.text ":" <+> prty t
248 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
251instance PrettyType a => PrettyType (TermN a) where
252 pretty when term =
253 case term of
254 VarN alias x -> either alias (pretty when x)
255 TermN alias t1 -> either alias (pretty when t1)
256 where
257 either maybeAlias doc =
258 case maybeAlias of
259 Just alias -> PP.pretty alias
260 Nothing -> doc
263instance PrettyType Descriptor where
264 pretty when desc = do
265 case (alias desc, structure desc, name desc) of
266 (Just name, _, _) -> PP.pretty name
267 (_, Just term, _) -> pretty when term
268 (_, _, Just name)
269 | Var.isTuple name ->
270 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
271 | otherwise ->
272 P.text (Var.toString name)
274 _ -> P.text "?"
277instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
278 pretty _ constraint =
279 let prty = pretty Never in
280 case constraint of
281 CTrue -> P.text "True"
282 CSaveEnv -> P.text "SaveTheEnvironment!!!"
283 CEqual a b -> prty a <+> P.text "=" <+> prty b
284 CAnd [] -> P.text "True"
286 CAnd cs ->
287 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
289 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
290 P.sep [ binder, pretty Never c ]
291 where
292 mergeExists vs (A _ c) =
293 case c of
294 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
295 _ -> (vs, c)
297 (fqs', c) = mergeExists fqs constraint
299 binder = if null fqs' then P.empty else
300 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
302 CLet schemes constraint ->
303 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
304 , P.text "in", pretty Never constraint ]
306 CInstance name tipe ->
307 P.text name <+> P.text "<" <+> prty tipe
310instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
311 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
312 P.sep [ forall, cs, headers' ]
313 where
314 prty = pretty Never
316 forall = if null rqs && null fqs then P.empty else
317 P.text "\x2200" <+> frees <+> rigids
319 frees = P.hsep $ map prty fqs
320 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
322 cs = case constraint of
323 CTrue -> P.empty
324 CAnd [] -> P.empty
325 _ -> P.brackets (pretty Never constraint)
327 headers' = if Map.size headers > 0 then dict else P.empty
328 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
329 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
332extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
333extraPretty t = pretty Never <$> addNames t
336-- ADDING NAMES TO TYPES
338addNames :: (Crawl t) => t -> IO t
339addNames value = do
340 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
341 let vars = map head . List.group $ List.sort rawVars
342 suffix s = map (++s) (map (:[]) ['a'..'z'])
343 allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
344 okayVars = filter (`notElem` vars) allVars
345 runStateT (crawl rename value) (okayVars, 0, 0, 0)
346 return value
347 where
348 getNames desc state@(vars, a, b, c) =
349 let name' = name desc in
350 case name' of
351 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
352 _ -> (name', state)
354 rename desc state@(vars, a, b, c) =
355 case name desc of
356 Just var -> (Just var, state)
357 Nothing ->
358 case flex desc of
359 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
360 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
361 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
362 _ -> (local $ head vars, (tail vars, a, b, c))
363 where
364 local v = Just (Var.local v)
367-- CRAWLING OVER TYPES
369type CrawlState = ([String], Int, Int, Int)
372-- Code for traversing all the type data-structures and giving
373-- names to the variables embedded deep in there.
374class Crawl t where
375 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
376 -> t
377 -> StateT CrawlState IO t
380instance Crawl e => Crawl (Annotated a e) where
381 crawl nextState (A ann e) = A ann <$> crawl nextState e
384instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
385 crawl nextState constraint =
386 let rnm = crawl nextState in
387 case constraint of
388 CTrue -> return CTrue
389 CSaveEnv -> return CSaveEnv
390 CEqual a b -> CEqual <$> rnm a <*> rnm b
391 CAnd cs -> CAnd <$> crawl nextState cs
392 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
393 CInstance name tipe -> CInstance name <$> rnm tipe
396instance Crawl a => Crawl [a] where
397 crawl nextState list = mapM (crawl nextState) list
400instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
401 crawl nextState (Scheme rqs fqs c headers) =
402 let rnm = crawl nextState
403 in
404 Scheme
405 <$> rnm rqs
406 <*> rnm fqs
407 <*> crawl nextState c
408 <*> return headers
411instance Crawl t => Crawl (TermN t) where
412 crawl nextState tipe =
413 case tipe of
414 VarN a x ->
415 VarN a <$> crawl nextState x
417 TermN a term ->
418 TermN a <$> crawl nextState term
421instance Crawl t => Crawl (Term1 t) where
422 crawl nextState term =
423 let rnm = crawl nextState in
424 case term of
425 App1 a b -> App1 <$> rnm a <*> rnm b
426 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
427 Var1 a -> Var1 <$> rnm a
428 EmptyRecord1 -> return EmptyRecord1
429 Record1 fields ext ->
430 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
433instance Crawl a => Crawl (UF.Point a) where
434 crawl nextState point =
435 do desc <- liftIO $ UF.descriptor point
436 desc' <- crawl nextState desc
437 liftIO $ UF.setDescriptor point desc'
438 return point
441instance Crawl Descriptor where
442 crawl nextState desc =
443 do state <- get
444 let (name', state') = nextState desc state
445 structure' <- traverse (crawl nextState) (structure desc)
446 put state'
447 return $ desc { name = name', structure = structure' }
450toSrcType :: Variable -> IO T.CanonicalType
451toSrcType var =
452 go =<< addNames var
453 where
454 go v =
455 do desc <- UF.descriptor v
456 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
457 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
459 backupSrcType desc =
460 case name desc of
461 Just v@(Var.Canonical _ x@(c:_))
462 | Char.isLower c -> return (T.Var x)
463 | otherwise -> return $ T.Type v
465 _ -> error $ concat
466 [ "Problem converting the following type "
467 , "from a type-checker type to a source-syntax type:"
468 , P.render (pretty Never var) ]
470 termToSrcType term =
471 case term of
472 App1 a b -> do
473 a' <- go a
474 b' <- go b
475 case a' of
476 T.App f args -> return $ T.App f (args ++ [b'])
477 _ -> return $ T.App a' [b']
479 Fun1 a b -> T.Lambda <$> go a <*> go b
481 Var1 a -> go a
483 EmptyRecord1 -> return $ T.Record [] Nothing
485 Record1 tfields extension -> do
486 fields' <- traverse (mapM go) tfields
487 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
488 ext' <- dealias <$> go extension
489 return $ case ext' of
490 T.Record fs ext -> T.Record (fs ++ fields) ext
491 T.Var _ -> T.Record fields (Just ext')
492 _ -> error "Used toSrcType on a type that is not well-formed"
494 dealias :: T.CanonicalType -> T.CanonicalType
495 dealias t =
496 case t of
497 T.Aliased _ t' -> t'
498 _ -> t
501data AppStructure = List Variable | Tuple [Variable] | Other
504collectApps :: Variable -> IO AppStructure
505collectApps var = go [] var
506 where
507 go vars var = do
508 desc <- UF.descriptor var
509 case (structure desc, vars) of
510 (Nothing, [v]) ->
511 case name desc of
512 Just n | Var.isList n -> return (List v)
513 _ -> return Other
515 (Nothing, vs) ->
516 case name desc of
517 Just n | Var.isTuple n -> return (Tuple vs)
518 _ -> return Other
520 (Just term, _) ->
521 case term of
522 App1 a b -> go (vars ++ [b]) a
523 _ -> return Other