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