git.iko.soy/elk
on e123780 help sign in
elk/compiler/Type/Type.hs
408 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)
144existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
145existsNumber f = do
146 v <- liftIO $ var (Is Number)
147 ex [v] <$> f (VarN v)
150instance Show a => Show (UF.Point a) where
151 show point = unsafePerformIO $ fmap show (UF.descriptor point)
154instance PrettyType a => PrettyType (UF.Point a) where
155 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
158instance PrettyType t => PrettyType (Annotated a t) where
159 pretty when (A _ e) = pretty when e
162instance PrettyType a => PrettyType (Term1 a) where
163 pretty when term =
164 let prty = pretty Never in
165 case term of
166 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
167 | otherwise -> parensIf needed (px <+> pretty App x)
168 where
169 px = prty f
170 needed = case when of
171 App -> True
172 _ -> False
174 Fun1 arg body ->
175 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
176 where
177 needed = case when of
178 Never -> False
179 _ -> True
181 Var1 x -> prty x
183 EmptyRecord1 -> P.braces P.empty
185 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
186 where
187 prettyExt = prty ext
188 extend | P.render prettyExt == "{}" = P.empty
189 | otherwise = prettyExt <+> P.text "|"
190 mkPretty f t = P.text (reprime f) <+> P.text ":" <+> prty t
191 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
194instance PrettyType a => PrettyType (TermN a) where
195 pretty when term =
196 case term of
197 VarN x -> pretty when x
198 TermN t1 -> pretty when t1
201instance PrettyType Descriptor where
202 pretty when desc =
203 case (structure desc, name desc) of
204 (Just term, _) -> pretty when term
205 (_, Just name) -> if not (isTuple name) then P.text (reprime name) else
206 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
207 _ -> P.text "?"
210instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
211 pretty _ constraint =
212 let prty = pretty Never in
213 case constraint of
214 CTrue -> P.text "True"
215 CSaveEnv -> P.text "SaveTheEnvironment!!!"
216 CEqual a b -> prty a <+> P.text "=" <+> prty b
217 CAnd [] -> P.text "True"
219 CAnd cs ->
220 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
222 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
223 P.sep [ binder, pretty Never c ]
224 where
225 mergeExists vs (A _ c) =
226 case c of
227 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
228 _ -> (vs, c)
230 (fqs', c) = mergeExists fqs constraint
232 binder = if null fqs' then P.empty else
233 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
235 CLet schemes constraint ->
236 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
237 , P.text "in", pretty Never constraint ]
239 CInstance name tipe ->
240 P.text name <+> P.text "<" <+> prty tipe
242instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
243 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
244 P.sep [ forall, cs, headers' ]
245 where
246 prty = pretty Never
248 forall = if null rqs && null fqs then P.empty else
249 P.text "\x2200" <+> frees <+> rigids
251 frees = P.hsep $ map prty fqs
252 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
254 cs = case constraint of
255 CTrue -> P.empty
256 CAnd [] -> P.empty
257 _ -> P.brackets (pretty Never constraint)
259 headers' = if Map.size headers > 0 then dict else P.empty
260 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
261 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
264extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
265extraPretty t = pretty Never <$> addNames t
267addNames :: (Crawl t) => t -> IO t
268addNames value = do
269 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
270 let vars = map head . List.group $ List.sort rawVars
271 suffix s = map (++s) (map (:[]) ['a'..'z'])
272 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
273 okayVars = filter (`notElem` vars) allVars
274 runStateT (crawl rename value) (okayVars, 0, 0, 0)
275 return value
276 where
277 getNames desc state@(vars, a, b, c) =
278 let name' = name desc in
279 case name' of
280 Just var -> (name', (var:vars, a, b, c))
281 Nothing -> (name', state)
283 rename desc state@(vars, a, b, c) =
284 case name desc of
285 Just var -> (Just var, state)
286 Nothing ->
287 case flex desc of
288 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
289 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
290 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
291 other -> (Just $ head vars, (tail vars, a, b, c))
292 where mark = case other of
293 Flexible -> ""
294 Rigid -> "!"
295 Constant -> "#"
298type CrawlState = ([String], Int, Int, Int)
300-- Code for traversing all the type data-structures and giving
301-- names to the variables embedded deep in there.
302class Crawl t where
303 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
304 -> t
305 -> StateT CrawlState IO t
307instance Crawl e => Crawl (Annotated a e) where
308 crawl nextState (A ann e) = A ann <$> crawl nextState e
310instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
311 crawl nextState constraint =
312 let rnm = crawl nextState in
313 case constraint of
314 CTrue -> return CTrue
315 CSaveEnv -> return CSaveEnv
316 CEqual a b -> CEqual <$> rnm a <*> rnm b
317 CAnd cs -> CAnd <$> crawl nextState cs
318 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
319 CInstance name tipe -> CInstance name <$> rnm tipe
321instance Crawl a => Crawl [a] where
322 crawl nextState list = mapM (crawl nextState) list
324instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
325 crawl nextState (Scheme rqs fqs c headers) =
326 let rnm = crawl nextState in
327 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
329instance Crawl t => Crawl (TermN t) where
330 crawl nextState tipe =
331 case tipe of
332 VarN x -> VarN <$> crawl nextState x
333 TermN term -> TermN <$> crawl nextState term
335instance Crawl t => Crawl (Term1 t) where
336 crawl nextState term =
337 let rnm = crawl nextState in
338 case term of
339 App1 a b -> App1 <$> rnm a <*> rnm b
340 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
341 Var1 a -> Var1 <$> rnm a
342 EmptyRecord1 -> return EmptyRecord1
343 Record1 fields ext ->
344 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
346instance Crawl a => Crawl (UF.Point a) where
347 crawl nextState point = do
348 desc <- liftIO $ UF.descriptor point
349 desc' <- crawl nextState desc
350 liftIO $ UF.setDescriptor point desc'
351 return point
353instance Crawl Descriptor where
354 crawl nextState desc = do
355 state <- get
356 let (name', state') = nextState desc state
357 structure' <- traverse (crawl nextState) (structure desc)
358 put state'
359 return $ desc { name = name', structure = structure' }
362toSrcType :: Variable -> IO Src.Type
363toSrcType variable = do
364 desc <- UF.descriptor =<< addNames variable
365 case structure desc of
366 Just term ->
367 case term of
368 App1 a b -> do
369 Src.Data name ts <- toSrcType a
370 b' <- toSrcType b
371 return (Src.Data name (ts ++ [b']))
372 Fun1 a b -> Src.Lambda <$> toSrcType a <*> toSrcType b
373 Var1 a -> toSrcType a
374 EmptyRecord1 -> return $ Src.Record [] Nothing
375 Record1 tfields extension -> do
376 fields' <- traverse (mapM toSrcType) tfields
377 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
378 ext' <- toSrcType extension
379 return $ case ext' of
380 Src.Record fs ext -> Src.Record (fs ++ fields) ext
381 Src.Var x -> Src.Record fields (Just x)
382 _ -> error "Used toSrcType on a type that is not well-formed"
383 Nothing ->
384 case name desc of
385 Just x@(c:_) | Char.isLower c -> return (Src.Var x)
386 | otherwise -> return (Src.Data x [])
387 _ -> error $ concat
388 [ "Problem converting the following type "
389 , "from a type-checker type to a source-syntax type:"
390 , P.render (pretty Never variable) ]
392data AppStructure = List Variable | Tuple [Variable] | Other
394collectApps :: Variable -> IO AppStructure
395collectApps variable = go [] variable
396 where
397 go vars variable = do
398 desc <- UF.descriptor variable
399 case (structure desc, vars) of
400 (Nothing, [v]) -> case name desc of
401 Just "_List" -> return (List v)
402 _ -> return Other
403 (Nothing, vs) -> case name desc of
404 Just ctor | isTuple ctor -> return (Tuple vs)
405 _ -> return Other
406 (Just term, _) -> case term of
407 App1 a b -> go (vars ++ [b]) a
408 _ -> return Other