git.iko.soy/elk
on 396fd33 help sign in
elk/src/Type/Type.hs
443 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
19data Term1 a
20 = App1 a a
21 | Fun1 a a
22 | Var1 a
23 | EmptyRecord1
24 | Record1 (Map.Map String [a]) a
25 deriving Show
27data TermN a
28 = VarN (Maybe Var.Canonical) a
29 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
30 deriving Show
32varN :: a -> TermN a
33varN = VarN Nothing
35termN :: (Term1 (TermN a)) -> TermN a
36termN = TermN Nothing
38record :: Map.Map String [TermN a] -> TermN a -> TermN a
39record fs rec = termN (Record1 fs rec)
41type Type = TermN Variable
42type Variable = UF.Point Descriptor
44type SchemeName = String
45type TypeName = Var.Canonical
47type Constraint a b = Located (BasicConstraint a b)
48data BasicConstraint a b
49 = CTrue
50 | CSaveEnv
51 | CEqual a a
52 | CAnd [Constraint a b]
53 | CLet [Scheme a b] (Constraint a b)
54 | CInstance SchemeName a
55 deriving Show
57data Scheme a b = Scheme {
58 rigidQuantifiers :: [b],
59 flexibleQuantifiers :: [b],
60 constraint :: Constraint a b,
61 header :: Map.Map String a
62} deriving Show
64type TypeConstraint = Constraint Type Variable
65type TypeScheme = Scheme Type Variable
67monoscheme :: Map.Map String a -> Scheme a b
68monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
70infixl 8 /\
72(/\) :: Constraint a b -> Constraint a b -> Constraint a b
73a@(A _ c1) /\ b@(A _ c2) =
74 case (c1, c2) of
75 (CTrue, _) -> b
76 (_, CTrue) -> a
77 _ -> mergeOldDocs a b (CAnd [a,b])
79infixr 9 ==>
80(==>) :: Type -> Type -> Type
81a ==> b = termN (Fun1 a b)
83(<|) :: TermN a -> TermN a -> TermN a
84f <| a = termN (App1 f a)
86data Descriptor = Descriptor
87 { structure :: Maybe (Term1 Variable)
88 , rank :: Int
89 , flex :: Flex
90 , name :: Maybe TypeName
91 , copy :: Maybe Variable
92 , mark :: Int
93 , alias :: Maybe Var.Canonical
94 } deriving Show
96noRank :: Int
97noRank = -1
99outermostRank :: Int
100outermostRank = 0
102noMark :: Int
103noMark = 0
105initialMark :: Int
106initialMark = 1
108data Flex = Rigid | Flexible | Constant | Is SuperType
109 deriving (Show, Eq)
111data SuperType = Number | Comparable | Appendable
112 deriving (Show, Eq)
114namedVar :: Flex -> Var.Canonical -> IO Variable
115namedVar flex name = UF.fresh $ Descriptor
116 { structure = Nothing
117 , rank = noRank
118 , flex = flex
119 , name = Just name
120 , copy = Nothing
121 , mark = noMark
122 , alias = Nothing
123 }
125variable :: Flex -> IO Variable
126variable flex = UF.fresh $ Descriptor
127 { structure = Nothing
128 , rank = noRank
129 , flex = flex
130 , name = Nothing
131 , copy = Nothing
132 , mark = noMark
133 , alias = Nothing
134 }
137-- ex qs constraint == exists qs. constraint
138ex :: [Variable] -> TypeConstraint -> TypeConstraint
139ex fqs constraint@(A ann _) =
140 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
142-- fl qs constraint == forall qs. constraint
143fl :: [Variable] -> TypeConstraint -> TypeConstraint
144fl rqs constraint@(A ann _) =
145 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
147exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
148exists f = do
149 v <- liftIO $ variable Flexible
150 ex [v] <$> f (varN v)
152existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
153existsNumber f = do
154 v <- liftIO $ variable (Is Number)
155 ex [v] <$> f (varN v)
158instance Show a => Show (UF.Point a) where
159 show point = unsafePerformIO $ fmap show (UF.descriptor point)
162instance PrettyType a => PrettyType (UF.Point a) where
163 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
166instance PrettyType t => PrettyType (Annotated a t) where
167 pretty when (A _ e) = pretty when e
170instance PrettyType a => PrettyType (Term1 a) where
171 pretty when term =
172 let prty = pretty Never in
173 case term of
174 App1 f x ->
175 parensIf needed (px <+> pretty App x)
176 where
177 px = prty f
178 needed = case when of
179 App -> True
180 _ -> False
182 Fun1 arg body ->
183 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
184 where
185 needed = case when of
186 Never -> False
187 _ -> True
189 Var1 x -> prty x
191 EmptyRecord1 -> P.braces P.empty
193 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
194 where
195 prettyExt = prty ext
196 extend | P.render prettyExt == "{}" = P.empty
197 | otherwise = prettyExt <+> P.text "|"
198 mkPretty f t = P.text f <+> P.text ":" <+> prty t
199 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
202instance PrettyType a => PrettyType (TermN a) where
203 pretty when term =
204 case term of
205 VarN alias x -> either alias (pretty when x)
206 TermN alias t1 -> either alias (pretty when t1)
207 where
208 either maybeAlias doc =
209 case maybeAlias of
210 Just alias -> PP.pretty alias
211 Nothing -> doc
213instance PrettyType Descriptor where
214 pretty when desc = do
215 case (alias desc, structure desc, name desc) of
216 (Just name, _, _) -> PP.pretty name
217 (_, Just term, _) -> pretty when term
218 (_, _, Just name)
219 | Var.isTuple name ->
220 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
221 | otherwise ->
222 P.text (Var.toString name)
224 _ -> P.text "?"
227instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
228 pretty _ constraint =
229 let prty = pretty Never in
230 case constraint of
231 CTrue -> P.text "True"
232 CSaveEnv -> P.text "SaveTheEnvironment!!!"
233 CEqual a b -> prty a <+> P.text "=" <+> prty b
234 CAnd [] -> P.text "True"
236 CAnd cs ->
237 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
239 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
240 P.sep [ binder, pretty Never c ]
241 where
242 mergeExists vs (A _ c) =
243 case c of
244 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
245 _ -> (vs, c)
247 (fqs', c) = mergeExists fqs constraint
249 binder = if null fqs' then P.empty else
250 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
252 CLet schemes constraint ->
253 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
254 , P.text "in", pretty Never constraint ]
256 CInstance name tipe ->
257 P.text name <+> P.text "<" <+> prty tipe
259instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
260 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
261 P.sep [ forall, cs, headers' ]
262 where
263 prty = pretty Never
265 forall = if null rqs && null fqs then P.empty else
266 P.text "\x2200" <+> frees <+> rigids
268 frees = P.hsep $ map prty fqs
269 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
271 cs = case constraint of
272 CTrue -> P.empty
273 CAnd [] -> P.empty
274 _ -> P.brackets (pretty Never constraint)
276 headers' = if Map.size headers > 0 then dict else P.empty
277 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
278 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
281extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
282extraPretty t = pretty Never <$> addNames t
284addNames :: (Crawl t) => t -> IO t
285addNames value = do
286 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
287 let vars = map head . List.group $ List.sort rawVars
288 suffix s = map (++s) (map (:[]) ['a'..'z'])
289 allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
290 okayVars = filter (`notElem` vars) allVars
291 runStateT (crawl rename value) (okayVars, 0, 0, 0)
292 return value
293 where
294 getNames desc state@(vars, a, b, c) =
295 let name' = name desc in
296 case name' of
297 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
298 _ -> (name', state)
300 rename desc state@(vars, a, b, c) =
301 case name desc of
302 Just var -> (Just var, state)
303 Nothing ->
304 case flex desc of
305 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
306 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
307 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
308 _ -> (local $ head vars, (tail vars, a, b, c))
309 where
310 local v = Just (Var.local v)
312type CrawlState = ([String], Int, Int, Int)
314-- Code for traversing all the type data-structures and giving
315-- names to the variables embedded deep in there.
316class Crawl t where
317 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
318 -> t
319 -> StateT CrawlState IO t
321instance Crawl e => Crawl (Annotated a e) where
322 crawl nextState (A ann e) = A ann <$> crawl nextState e
324instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
325 crawl nextState constraint =
326 let rnm = crawl nextState in
327 case constraint of
328 CTrue -> return CTrue
329 CSaveEnv -> return CSaveEnv
330 CEqual a b -> CEqual <$> rnm a <*> rnm b
331 CAnd cs -> CAnd <$> crawl nextState cs
332 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
333 CInstance name tipe -> CInstance name <$> rnm tipe
335instance Crawl a => Crawl [a] where
336 crawl nextState list = mapM (crawl nextState) list
338instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
339 crawl nextState (Scheme rqs fqs c headers) =
340 let rnm = crawl nextState in
341 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
343instance Crawl t => Crawl (TermN t) where
344 crawl nextState tipe =
345 case tipe of
346 VarN a x -> VarN a <$> crawl nextState x
347 TermN a term -> TermN a <$> crawl nextState term
349instance Crawl t => Crawl (Term1 t) where
350 crawl nextState term =
351 let rnm = crawl nextState in
352 case term of
353 App1 a b -> App1 <$> rnm a <*> rnm b
354 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
355 Var1 a -> Var1 <$> rnm a
356 EmptyRecord1 -> return EmptyRecord1
357 Record1 fields ext ->
358 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
360instance Crawl a => Crawl (UF.Point a) where
361 crawl nextState point = do
362 desc <- liftIO $ UF.descriptor point
363 desc' <- crawl nextState desc
364 liftIO $ UF.setDescriptor point desc'
365 return point
367instance Crawl Descriptor where
368 crawl nextState desc = do
369 state <- get
370 let (name', state') = nextState desc state
371 structure' <- traverse (crawl nextState) (structure desc)
372 put state'
373 return $ desc { name = name', structure = structure' }
376toSrcType :: Variable -> IO T.CanonicalType
377toSrcType var =
378 go =<< addNames var
379 where
380 go v = do
381 desc <- UF.descriptor v
382 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
383 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
385 backupSrcType desc =
386 case name desc of
387 Just v@(Var.Canonical _ x@(c:_))
388 | Char.isLower c -> return (T.Var x)
389 | otherwise -> return $ T.Type v
391 _ -> error $ concat
392 [ "Problem converting the following type "
393 , "from a type-checker type to a source-syntax type:"
394 , P.render (pretty Never var) ]
396 termToSrcType term =
397 case term of
398 App1 a b -> do
399 a' <- go a
400 b' <- go b
401 case a' of
402 T.App f args -> return $ T.App f (args ++ [b'])
403 _ -> return $ T.App a' [b']
405 Fun1 a b -> T.Lambda <$> go a <*> go b
407 Var1 a -> go a
409 EmptyRecord1 -> return $ T.Record [] Nothing
411 Record1 tfields extension -> do
412 fields' <- traverse (mapM go) tfields
413 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
414 ext' <- dealias <$> go extension
415 return $ case ext' of
416 T.Record fs ext -> T.Record (fs ++ fields) ext
417 T.Var _ -> T.Record fields (Just ext')
418 _ -> error "Used toSrcType on a type that is not well-formed"
420 dealias :: T.CanonicalType -> T.CanonicalType
421 dealias t =
422 case t of
423 T.Aliased _ t' -> t'
424 _ -> t
427data AppStructure = List Variable | Tuple [Variable] | Other
429collectApps :: Variable -> IO AppStructure
430collectApps var = go [] var
431 where
432 go vars var = do
433 desc <- UF.descriptor var
434 case (structure desc, vars) of
435 (Nothing, [v]) -> case name desc of
436 Just n | Var.isList n -> return (List v)
437 _ -> return Other
438 (Nothing, vs) -> case name desc of
439 Just n | Var.isTuple n -> return (Tuple vs)
440 _ -> return Other
441 (Just term, _) -> case term of
442 App1 a b -> go (vars ++ [b]) a
443 _ -> return Other