git.iko.soy/elk
on eaa751d help sign in
elk/compiler/Type/Type.hs
324 lines 9.2 kB history raw
1module Type.Type where
3import qualified Data.List as List
4import qualified Data.Map as Map
5import qualified Data.UnionFind.IO as UF
6import Type.PrettyPrint
7import Text.PrettyPrint as P
8import System.IO.Unsafe
9import Control.Applicative ((<$>),(<*>))
10import Control.Monad.State
11import Data.Traversable (traverse)
12import SourceSyntax.Helpers (isTuple)
13import qualified SourceSyntax.Type as Src
15data Term1 a
16 = App1 a a
17 | Fun1 a a
18 | Var1 a
19 | EmptyRecord1
20 | Record1 (Map.Map String [a]) a
21 deriving Show
23data TermN a
24 = VarN a
25 | TermN (Term1 (TermN a))
26 deriving Show
28record fs rec = TermN (Record1 fs rec)
30type Type = TermN Variable
31type Variable = UF.Point Descriptor
33type SchemeName = String
34type TypeName = String
36data Constraint a b
37 = CTrue
38 | CSaveEnv
39 | CEqual a a
40 | CAnd [Constraint a b]
41 | CLet [Scheme a b] (Constraint a b)
42 | CInstance SchemeName a
43 deriving Show
45data Scheme a b = Scheme {
46 rigidQuantifiers :: [b],
47 flexibleQuantifiers :: [b],
48 constraint :: Constraint a b,
49 header :: Map.Map String a
50} deriving Show
52type TypeConstraint = Constraint Type Variable
53type TypeScheme = Scheme Type Variable
55monoscheme headers = Scheme [] [] CTrue headers
57data Descriptor = Descriptor {
58 structure :: Maybe (Term1 Variable),
59 rank :: Int,
60 flex :: Flex,
61 name :: Maybe TypeName,
62 copy :: Maybe Variable,
63 mark :: Int
64} deriving Show
66noRank = -1
67outermostRank = 0 :: Int
69noMark = 0
70initialMark = 1
72data Flex = Rigid | Flexible | Constant
73 deriving (Show, Eq)
75infixl 8 /\
77(/\) :: Constraint a b -> Constraint a b -> Constraint a b
78a /\ CTrue = a
79CTrue /\ b = b
80a /\ b = CAnd [a,b]
82(===) :: Type -> Type -> TypeConstraint
83(===) = CEqual
85(<?) :: SchemeName -> Type -> TypeConstraint
86x <? t = CInstance x t
88infixr 9 ==>
89(==>) :: Type -> Type -> Type
90a ==> b = TermN (Fun1 a b)
92f <| a = TermN (App1 f a)
95namedVar flex name = UF.fresh $ Descriptor {
96 structure = Nothing,
97 rank = noRank,
98 flex = flex,
99 name = Just name,
100 copy = Nothing,
101 mark = noMark
102 }
104flexibleVar = UF.fresh $ Descriptor {
105 structure = Nothing,
106 rank = noRank,
107 flex = Flexible,
108 name = Nothing,
109 copy = Nothing,
110 mark = noMark
111 }
113rigidVar = UF.fresh $ Descriptor {
114 structure = Nothing,
115 rank = noRank,
116 flex = Rigid,
117 name = Nothing,
118 copy = Nothing,
119 mark = noMark
120 }
122-- ex qs constraint == exists qs. constraint
123ex :: [Variable] -> TypeConstraint -> TypeConstraint
124ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
126-- fl qs constraint == forall qs. constraint
127fl :: [Variable] -> TypeConstraint -> TypeConstraint
128fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
130exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
131exists f = do
132 v <- flexibleVar
133 ex [v] <$> f (VarN v)
136instance Show a => Show (UF.Point a) where
137 show point = unsafePerformIO $ fmap show (UF.descriptor point)
140instance PrettyType a => PrettyType (UF.Point a) where
141 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
144instance PrettyType a => PrettyType (Term1 a) where
145 pretty when term =
146 let prty = pretty Never in
147 case term of
148 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
149 | otherwise -> parensIf needed (px <+> pretty App x)
150 where
151 px = prty f
152 needed = case when of
153 App -> True
154 _ -> False
156 Fun1 arg body ->
157 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
158 where
159 needed = case when of
160 Never -> False
161 _ -> True
163 Var1 x -> prty x
165 EmptyRecord1 -> P.braces P.empty
167 Record1 fields ext ->
168 P.braces (prty ext <+> P.text "|" <+> commaSep prettyFields)
169 where
170 mkPretty f t = P.text f <+> P.text ":" <+> prty t
171 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
174instance PrettyType a => PrettyType (TermN a) where
175 pretty when term =
176 case term of
177 VarN x -> pretty when x
178 TermN t1 -> pretty when t1
181instance PrettyType Descriptor where
182 pretty when desc =
183 case (structure desc, name desc) of
184 (Just term, _) -> pretty when term
185 (_, Just name) -> if not (isTuple name) then P.text name else
186 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
187 _ -> P.text "?"
190instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
191 pretty _ constraint =
192 let prty = pretty Never in
193 case constraint of
194 CTrue -> P.text "True"
195 CSaveEnv -> P.text "SaveTheEnvironment!!!"
196 CEqual a b -> prty a <+> P.text "=" <+> prty b
197 CAnd [] -> P.text "True"
199 CAnd cs ->
200 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
202 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
203 P.sep [ binder, pretty Never c ]
204 where
205 mergeExists vs c =
206 case c of
207 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
208 _ -> (vs, c)
210 (fqs', c) = mergeExists fqs constraint
212 binder = if null fqs' then P.empty else
213 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
215 CLet schemes constraint ->
216 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
217 , P.text "in", pretty Never constraint ]
219 CInstance name tipe ->
220 P.text name <+> P.text "<" <+> prty tipe
222instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
223 pretty _ (Scheme rqs fqs constraint headers) =
224 P.sep [ forall, cs, headers' ]
225 where
226 prty = pretty Never
228 forall = if null rqs && null fqs then P.empty else
229 P.text "\x2200" <+> frees <+> rigids
231 frees = P.hsep $ map prty fqs
232 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
234 cs = case constraint of
235 CTrue -> P.empty
236 CAnd [] -> P.empty
237 _ -> P.brackets (pretty Never constraint)
239 headers' = if Map.size headers > 0 then dict else P.empty
240 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
241 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
244extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
245extraPretty t = pretty Never <$> addNames t
247addNames :: (Crawl t) => t -> IO t
248addNames value = do
249 (_, rawVars) <- runStateT (crawl getNames value) []
250 let vars = map head . List.group $ List.sort rawVars
251 suffix s = map (++s) (map (:[]) ['a'..'z'])
252 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
253 okayVars = filter (`notElem` vars) allVars
254 runStateT (crawl rename value) okayVars
255 return value
256 where
257 getNames name vars =
258 case name of
259 Just var -> (name, var:vars)
260 Nothing -> (name, vars)
262 rename name vars =
263 case name of
264 Just var -> (name, vars)
265 Nothing -> (Just (head vars), tail vars)
268-- Code for traversing all the type data-structures and giving
269-- names to the variables embedded deep in there.
270class Crawl t where
271 crawl :: (Maybe TypeName -> [String] -> (Maybe TypeName, [String]))
272 -> t
273 -> StateT [String] IO t
275instance (Crawl t, Crawl v) => Crawl (Constraint t v) where
276 crawl nextState constraint =
277 let rnm = crawl nextState in
278 case constraint of
279 CTrue -> return CTrue
280 CSaveEnv -> return CSaveEnv
281 CEqual a b -> CEqual <$> rnm a <*> rnm b
282 CAnd cs -> CAnd <$> crawl nextState cs
283 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
284 CInstance name tipe -> CInstance name <$> rnm tipe
286instance Crawl a => Crawl [a] where
287 crawl nextState list = mapM (crawl nextState) list
289instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
290 crawl nextState (Scheme rqs fqs c headers) =
291 let rnm = crawl nextState in
292 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
294instance Crawl t => Crawl (TermN t) where
295 crawl nextState tipe =
296 case tipe of
297 VarN x -> VarN <$> crawl nextState x
298 TermN term -> TermN <$> crawl nextState term
300instance Crawl t => Crawl (Term1 t) where
301 crawl nextState term =
302 let rnm = crawl nextState in
303 case term of
304 App1 a b -> App1 <$> rnm a <*> rnm b
305 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
306 Var1 a -> Var1 <$> rnm a
307 EmptyRecord1 -> return EmptyRecord1
308 Record1 fields ext ->
309 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
311instance Crawl a => Crawl (UF.Point a) where
312 crawl nextState point = do
313 desc <- liftIO $ UF.descriptor point
314 desc' <- crawl nextState desc
315 liftIO $ UF.setDescriptor point desc'
316 return point
318instance Crawl Descriptor where
319 crawl nextState desc = do
320 state <- get
321 let (name', state') = nextState (name desc) state
322 structure' <- traverse (crawl nextState) (structure desc)
323 put state'
324 return $ desc { name = name', structure = structure' }