git.iko.soy/elk
on 080eb08 help sign in
elk/compiler/Type/Type.hs
403 lines 13 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
12import Control.Monad.Error
13import Data.Traversable (traverse)
14import SourceSyntax.Annotation
15import SourceSyntax.Helpers (isTuple)
16import qualified SourceSyntax.Type as Src
18data Term1 a
19 = App1 a a
20 | Fun1 a a
21 | Var1 a
22 | EmptyRecord1
23 | Record1 (Map.Map String [a]) a
24 deriving Show
26data TermN a
27 = VarN a
28 | TermN (Term1 (TermN a))
29 deriving Show
31record :: Map.Map String [TermN a] -> TermN a -> TermN a
32record fs rec = TermN (Record1 fs rec)
34type Type = TermN Variable
35type Variable = UF.Point Descriptor
37type SchemeName = String
38type TypeName = String
40type Constraint a b = Located (BasicConstraint a b)
41data BasicConstraint a b
42 = CTrue
43 | CSaveEnv
44 | CEqual a a
45 | CAnd [Constraint a b]
46 | CLet [Scheme a b] (Constraint a b)
47 | CInstance SchemeName a
48 deriving Show
50data Scheme a b = Scheme {
51 rigidQuantifiers :: [b],
52 flexibleQuantifiers :: [b],
53 constraint :: Constraint a b,
54 header :: Map.Map String a
55} deriving Show
57type TypeConstraint = Constraint Type Variable
58type TypeScheme = Scheme Type Variable
60monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
62infixl 8 /\
64(/\) :: Constraint a b -> Constraint a b -> Constraint a b
65a@(A _ c1) /\ b@(A _ c2) =
66 case (c1, c2) of
67 (CTrue, _) -> b
68 (_, CTrue) -> a
69 _ -> mergeOldDocs a b (CAnd [a,b])
71infixr 9 ==>
72(==>) :: Type -> Type -> Type
73a ==> b = TermN (Fun1 a b)
75f <| a = TermN (App1 f a)
77data Descriptor = Descriptor {
78 structure :: Maybe (Term1 Variable),
79 rank :: Int,
80 flex :: Flex,
81 name :: Maybe TypeName,
82 copy :: Maybe Variable,
83 mark :: Int
84} deriving Show
86noRank = -1
87outermostRank = 0 :: Int
89noMark = 0
90initialMark = 1
92data Flex = Rigid | Flexible | Constant | Is SuperType
93 deriving (Show, Eq)
95data SuperType = Number | Comparable | Appendable
96 deriving (Show, Eq)
98namedVar :: Flex -> String -> IO Variable
99namedVar flex name = UF.fresh $ Descriptor {
100 structure = Nothing,
101 rank = noRank,
102 flex = flex,
103 name = Just name,
104 copy = Nothing,
105 mark = noMark
106 }
108var :: Flex -> IO Variable
109var flex = UF.fresh $ Descriptor {
110 structure = Nothing,
111 rank = noRank,
112 flex = flex,
113 name = Nothing,
114 copy = Nothing,
115 mark = noMark
116 }
118structuredVar :: Term1 Variable -> IO Variable
119structuredVar structure = UF.fresh $ Descriptor {
120 structure = Just structure,
121 rank = noRank,
122 flex = Flexible,
123 name = Nothing,
124 copy = Nothing,
125 mark = noMark
126 }
129-- ex qs constraint == exists qs. constraint
130ex :: [Variable] -> TypeConstraint -> TypeConstraint
131ex fqs constraint@(A ann _) =
132 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
134-- fl qs constraint == forall qs. constraint
135fl :: [Variable] -> TypeConstraint -> TypeConstraint
136fl rqs constraint@(A ann _) =
137 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
139exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
140exists f = do
141 v <- liftIO $ var Flexible
142 ex [v] <$> f (VarN v)
145instance Show a => Show (UF.Point a) where
146 show point = unsafePerformIO $ fmap show (UF.descriptor point)
149instance PrettyType a => PrettyType (UF.Point a) where
150 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
153instance PrettyType t => PrettyType (Annotated a t) where
154 pretty when (A _ e) = pretty when e
157instance PrettyType a => PrettyType (Term1 a) where
158 pretty when term =
159 let prty = pretty Never in
160 case term of
161 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
162 | otherwise -> parensIf needed (px <+> pretty App x)
163 where
164 px = prty f
165 needed = case when of
166 App -> True
167 _ -> False
169 Fun1 arg body ->
170 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
171 where
172 needed = case when of
173 Never -> False
174 _ -> True
176 Var1 x -> prty x
178 EmptyRecord1 -> P.braces P.empty
180 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
181 where
182 prettyExt = prty ext
183 extend | P.render prettyExt == "{}" = P.empty
184 | otherwise = prettyExt <+> P.text "|"
185 mkPretty f t = P.text (reprime f) <+> P.text ":" <+> prty t
186 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
189instance PrettyType a => PrettyType (TermN a) where
190 pretty when term =
191 case term of
192 VarN x -> pretty when x
193 TermN t1 -> pretty when t1
196instance PrettyType Descriptor where
197 pretty when desc =
198 case (structure desc, name desc) of
199 (Just term, _) -> pretty when term
200 (_, Just name) -> if not (isTuple name) then P.text (reprime name) else
201 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
202 _ -> P.text "?"
205instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
206 pretty _ constraint =
207 let prty = pretty Never in
208 case constraint of
209 CTrue -> P.text "True"
210 CSaveEnv -> P.text "SaveTheEnvironment!!!"
211 CEqual a b -> prty a <+> P.text "=" <+> prty b
212 CAnd [] -> P.text "True"
214 CAnd cs ->
215 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
217 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
218 P.sep [ binder, pretty Never c ]
219 where
220 mergeExists vs (A _ c) =
221 case c of
222 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
223 _ -> (vs, c)
225 (fqs', c) = mergeExists fqs constraint
227 binder = if null fqs' then P.empty else
228 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
230 CLet schemes constraint ->
231 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
232 , P.text "in", pretty Never constraint ]
234 CInstance name tipe ->
235 P.text name <+> P.text "<" <+> prty tipe
237instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
238 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
239 P.sep [ forall, cs, headers' ]
240 where
241 prty = pretty Never
243 forall = if null rqs && null fqs then P.empty else
244 P.text "\x2200" <+> frees <+> rigids
246 frees = P.hsep $ map prty fqs
247 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
249 cs = case constraint of
250 CTrue -> P.empty
251 CAnd [] -> P.empty
252 _ -> P.brackets (pretty Never constraint)
254 headers' = if Map.size headers > 0 then dict else P.empty
255 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
256 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
259extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
260extraPretty t = pretty Never <$> addNames t
262addNames :: (Crawl t) => t -> IO t
263addNames value = do
264 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
265 let vars = map head . List.group $ List.sort rawVars
266 suffix s = map (++s) (map (:[]) ['a'..'z'])
267 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
268 okayVars = filter (`notElem` vars) allVars
269 runStateT (crawl rename value) (okayVars, 0, 0, 0)
270 return value
271 where
272 getNames desc state@(vars, a, b, c) =
273 let name' = name desc in
274 case name' of
275 Just var -> (name', (var:vars, a, b, c))
276 Nothing -> (name', state)
278 rename desc state@(vars, a, b, c) =
279 case name desc of
280 Just var -> (Just var, state)
281 Nothing ->
282 case flex desc of
283 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
284 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
285 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
286 other -> (Just $ head vars, (tail vars, a, b, c))
287 where mark = case other of
288 Flexible -> ""
289 Rigid -> "!"
290 Constant -> "#"
293type CrawlState = ([String], Int, Int, Int)
295-- Code for traversing all the type data-structures and giving
296-- names to the variables embedded deep in there.
297class Crawl t where
298 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
299 -> t
300 -> StateT CrawlState IO t
302instance Crawl e => Crawl (Annotated a e) where
303 crawl nextState (A ann e) = A ann <$> crawl nextState e
305instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
306 crawl nextState constraint =
307 let rnm = crawl nextState in
308 case constraint of
309 CTrue -> return CTrue
310 CSaveEnv -> return CSaveEnv
311 CEqual a b -> CEqual <$> rnm a <*> rnm b
312 CAnd cs -> CAnd <$> crawl nextState cs
313 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
314 CInstance name tipe -> CInstance name <$> rnm tipe
316instance Crawl a => Crawl [a] where
317 crawl nextState list = mapM (crawl nextState) list
319instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
320 crawl nextState (Scheme rqs fqs c headers) =
321 let rnm = crawl nextState in
322 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
324instance Crawl t => Crawl (TermN t) where
325 crawl nextState tipe =
326 case tipe of
327 VarN x -> VarN <$> crawl nextState x
328 TermN term -> TermN <$> crawl nextState term
330instance Crawl t => Crawl (Term1 t) where
331 crawl nextState term =
332 let rnm = crawl nextState in
333 case term of
334 App1 a b -> App1 <$> rnm a <*> rnm b
335 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
336 Var1 a -> Var1 <$> rnm a
337 EmptyRecord1 -> return EmptyRecord1
338 Record1 fields ext ->
339 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
341instance Crawl a => Crawl (UF.Point a) where
342 crawl nextState point = do
343 desc <- liftIO $ UF.descriptor point
344 desc' <- crawl nextState desc
345 liftIO $ UF.setDescriptor point desc'
346 return point
348instance Crawl Descriptor where
349 crawl nextState desc = do
350 state <- get
351 let (name', state') = nextState desc state
352 structure' <- traverse (crawl nextState) (structure desc)
353 put state'
354 return $ desc { name = name', structure = structure' }
357toSrcType :: Variable -> IO Src.Type
358toSrcType variable = do
359 desc <- UF.descriptor =<< addNames variable
360 case structure desc of
361 Just term ->
362 case term of
363 App1 a b -> do
364 Src.Data name ts <- toSrcType a
365 b' <- toSrcType b
366 return (Src.Data name (ts ++ [b']))
367 Fun1 a b -> Src.Lambda <$> toSrcType a <*> toSrcType b
368 Var1 a -> toSrcType a
369 EmptyRecord1 -> return $ Src.Record [] Nothing
370 Record1 tfields extension -> do
371 fields' <- traverse (mapM toSrcType) tfields
372 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
373 ext' <- toSrcType extension
374 return $ case ext' of
375 Src.Record fs ext -> Src.Record (fs ++ fields) ext
376 Src.Var x -> Src.Record fields (Just x)
377 _ -> error "Used toSrcType on a type that is not well-formed"
378 Nothing ->
379 case name desc of
380 Just x@(c:_) | Char.isLower c -> return (Src.Var x)
381 | otherwise -> return (Src.Data x [])
382 _ -> error $ concat
383 [ "Problem converting the following type "
384 , "from a type-checker type to a source-syntax type:"
385 , P.render (pretty Never variable) ]
387data AppStructure = List Variable | Tuple [Variable] | Other
389collectApps :: Variable -> IO AppStructure
390collectApps variable = go [] variable
391 where
392 go vars variable = do
393 desc <- UF.descriptor variable
394 case (structure desc, vars) of
395 (Nothing, [v]) -> case name desc of
396 Just "_List" -> return (List v)
397 _ -> return Other
398 (Nothing, vs) -> case name desc of
399 Just ctor | isTuple ctor -> return (Tuple vs)
400 _ -> return Other
401 (Just term, _) -> case term of
402 App1 a b -> go (vars ++ [b]) a
403 _ -> return Other