git.iko.soy/elk
on c19ccfe help sign in
elk/compiler/Type/Type.hs
326 lines 9.6 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
57infixl 8 /\
59(/\) :: Constraint a b -> Constraint a b -> Constraint a b
60a /\ CTrue = a
61CTrue /\ b = b
62a /\ b = CAnd [a,b]
64(===) :: Type -> Type -> TypeConstraint
65(===) = CEqual
67(<?) :: SchemeName -> Type -> TypeConstraint
68x <? t = CInstance x t
70infixr 9 ==>
71(==>) :: Type -> Type -> Type
72a ==> b = TermN (Fun1 a b)
74f <| a = TermN (App1 f a)
76data Descriptor = Descriptor {
77 structure :: Maybe (Term1 Variable),
78 rank :: Int,
79 flex :: Flex,
80 name :: Maybe TypeName,
81 copy :: Maybe Variable,
82 mark :: Int
83} deriving Show
85noRank = -1
86outermostRank = 0 :: Int
88noMark = 0
89initialMark = 1
91data Flex = Rigid | Flexible | Constant | Is SuperType
92 deriving (Show, Eq)
94data SuperType = Number | Comparable | Appendable
95 deriving (Show, Eq)
97namedVar flex name = UF.fresh $ Descriptor {
98 structure = Nothing,
99 rank = noRank,
100 flex = flex,
101 name = Just name,
102 copy = Nothing,
103 mark = noMark
104 }
106var flex = UF.fresh $ Descriptor {
107 structure = Nothing,
108 rank = noRank,
109 flex = flex,
110 name = Nothing,
111 copy = Nothing,
112 mark = noMark
113 }
116-- ex qs constraint == exists qs. constraint
117ex :: [Variable] -> TypeConstraint -> TypeConstraint
118ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
120-- fl qs constraint == forall qs. constraint
121fl :: [Variable] -> TypeConstraint -> TypeConstraint
122fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
124exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
125exists f = do
126 v <- var Flexible
127 ex [v] <$> f (VarN v)
130instance Show a => Show (UF.Point a) where
131 show point = unsafePerformIO $ fmap show (UF.descriptor point)
134instance PrettyType a => PrettyType (UF.Point a) where
135 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
138instance PrettyType a => PrettyType (Term1 a) where
139 pretty when term =
140 let prty = pretty Never in
141 case term of
142 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
143 | otherwise -> parensIf needed (px <+> pretty App x)
144 where
145 px = prty f
146 needed = case when of
147 App -> True
148 _ -> False
150 Fun1 arg body ->
151 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
152 where
153 needed = case when of
154 Never -> False
155 _ -> True
157 Var1 x -> prty x
159 EmptyRecord1 -> P.braces P.empty
161 Record1 fields ext ->
162 P.braces (prty ext <+> P.text "|" <+> commaSep prettyFields)
163 where
164 mkPretty f t = P.text f <+> P.text ":" <+> prty t
165 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
168instance PrettyType a => PrettyType (TermN a) where
169 pretty when term =
170 case term of
171 VarN x -> pretty when x
172 TermN t1 -> pretty when t1
175instance PrettyType Descriptor where
176 pretty when desc =
177 case (structure desc, name desc) of
178 (Just term, _) -> pretty when term
179 (_, Just name) -> if not (isTuple name) then P.text name else
180 P.parens . P.text $ replicate (read (drop 6 name) - 1) ','
181 _ -> P.text "?"
184instance (PrettyType a, PrettyType b) => PrettyType (Constraint a b) where
185 pretty _ constraint =
186 let prty = pretty Never in
187 case constraint of
188 CTrue -> P.text "True"
189 CSaveEnv -> P.text "SaveTheEnvironment!!!"
190 CEqual a b -> prty a <+> P.text "=" <+> prty b
191 CAnd [] -> P.text "True"
193 CAnd cs ->
194 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
196 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
197 P.sep [ binder, pretty Never c ]
198 where
199 mergeExists vs c =
200 case c of
201 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
202 _ -> (vs, c)
204 (fqs', c) = mergeExists fqs constraint
206 binder = if null fqs' then P.empty else
207 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
209 CLet schemes constraint ->
210 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
211 , P.text "in", pretty Never constraint ]
213 CInstance name tipe ->
214 P.text name <+> P.text "<" <+> prty tipe
216instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
217 pretty _ (Scheme rqs fqs constraint headers) =
218 P.sep [ forall, cs, headers' ]
219 where
220 prty = pretty Never
222 forall = if null rqs && null fqs then P.empty else
223 P.text "\x2200" <+> frees <+> rigids
225 frees = P.hsep $ map prty fqs
226 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
228 cs = case constraint of
229 CTrue -> P.empty
230 CAnd [] -> P.empty
231 _ -> P.brackets (pretty Never constraint)
233 headers' = if Map.size headers > 0 then dict else P.empty
234 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
235 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
238extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
239extraPretty t = pretty Never <$> addNames t
241addNames :: (Crawl t) => t -> IO t
242addNames value = do
243 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
244 let vars = map head . List.group $ List.sort rawVars
245 suffix s = map (++s) (map (:[]) ['a'..'z'])
246 allVars = concatMap suffix $ ["","'","_"] ++ map show [0..]
247 okayVars = filter (`notElem` vars) allVars
248 runStateT (crawl rename value) (okayVars, 0, 0, 0)
249 return value
250 where
251 getNames desc state@(vars, a, b, c) =
252 let name' = name desc in
253 case name' of
254 Just var -> (name', (var:vars, a, b, c))
255 Nothing -> (name', state)
257 rename desc state@(vars, a, b, c) =
258 case name desc of
259 Just var -> (Just var, state)
260 Nothing ->
261 case flex desc of
262 Is Number -> (Just $ "number" ++ replicate a '\'', (vars, a+1, b, c))
263 Is Comparable -> (Just $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
264 Is Appendable -> (Just $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
265 _ -> (Just $ head vars, (tail vars, a, b, c))
268type CrawlState = ([String], Int, Int, Int)
270-- Code for traversing all the type data-structures and giving
271-- names to the variables embedded deep in there.
272class Crawl t where
273 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
274 -> t
275 -> StateT CrawlState IO t
277instance (Crawl t, Crawl v) => Crawl (Constraint t v) where
278 crawl nextState constraint =
279 let rnm = crawl nextState in
280 case constraint of
281 CTrue -> return CTrue
282 CSaveEnv -> return CSaveEnv
283 CEqual a b -> CEqual <$> rnm a <*> rnm b
284 CAnd cs -> CAnd <$> crawl nextState cs
285 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
286 CInstance name tipe -> CInstance name <$> rnm tipe
288instance Crawl a => Crawl [a] where
289 crawl nextState list = mapM (crawl nextState) list
291instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
292 crawl nextState (Scheme rqs fqs c headers) =
293 let rnm = crawl nextState in
294 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
296instance Crawl t => Crawl (TermN t) where
297 crawl nextState tipe =
298 case tipe of
299 VarN x -> VarN <$> crawl nextState x
300 TermN term -> TermN <$> crawl nextState term
302instance Crawl t => Crawl (Term1 t) where
303 crawl nextState term =
304 let rnm = crawl nextState in
305 case term of
306 App1 a b -> App1 <$> rnm a <*> rnm b
307 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
308 Var1 a -> Var1 <$> rnm a
309 EmptyRecord1 -> return EmptyRecord1
310 Record1 fields ext ->
311 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
313instance Crawl a => Crawl (UF.Point a) where
314 crawl nextState point = do
315 desc <- liftIO $ UF.descriptor point
316 desc' <- crawl nextState desc
317 liftIO $ UF.setDescriptor point desc'
318 return point
320instance Crawl Descriptor where
321 crawl nextState desc = do
322 state <- get
323 let (name', state') = nextState desc state
324 structure' <- traverse (crawl nextState) (structure desc)
325 put state'
326 return $ desc { name = name', structure = structure' }