git.iko.soy/elk
on 003ebfd help sign in
elk/compiler/Type/Type.hs
288 lines 8.4 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 SourceSyntax.PrettyPrint
7import Text.PrettyPrint as P
8import System.IO.Unsafe
9import Control.Applicative ((<$>),(<*>))
10import Control.Monad.State
11import Data.Traversable (traverse)
13data Term1 a
14 = App1 a a
15 | Fun1 a a
16 | Var1 a
17 | EmptyRecord1
18 | Record1 (Map.Map String [a]) a
19 deriving Show
21data TermN a
22 = VarN a
23 | TermN (Term1 (TermN a))
24 deriving Show
26record fs rec = TermN (Record1 fs rec)
28type SchemeName = String
29type TypeName = String
31data Constraint a b
32 = CTrue
33 | CEqual a a
34 | CAnd [Constraint a b]
35 | CLet [Scheme a b] (Constraint a b)
36 | CInstance SchemeName a
37 deriving Show
39data Scheme a b = Scheme {
40 rigidQuantifiers :: [b],
41 flexibleQuantifiers :: [b],
42 constraint :: Constraint a b,
43 header :: Map.Map String a
44} deriving Show
46monoscheme headers = Scheme [] [] CTrue headers
48data Descriptor = Descriptor {
49 structure :: Maybe (Term1 Variable),
50 rank :: Int,
51 flex :: Flex,
52 name :: Maybe TypeName,
53 copy :: Maybe Variable,
54 mark :: Int
55} deriving Show
57noRank = -1
58outermostRank = 0 :: Int
60noMark = 0
61initialMark = 1
63data Flex = Rigid | Flexible | Constant
64 deriving (Show, Eq)
66type Variable = UF.Point Descriptor
68type Type = TermN Variable
69type TypeConstraint = Constraint Type Variable
70type TypeScheme = Scheme Type Variable
72infixl 8 /\
74(/\) :: Constraint a b -> Constraint a b -> Constraint a b
75a /\ b = CAnd [a,b]
77(===) :: Type -> Type -> TypeConstraint
78(===) = CEqual
80(<?) :: SchemeName -> Type -> TypeConstraint
81x <? t = CInstance x t
83infixr 9 ==>
84(==>) :: Type -> Type -> Type
85a ==> b = TermN (Fun1 a b)
87namedVar name = UF.fresh $ Descriptor {
88 structure = Nothing,
89 rank = noRank,
90 flex = Constant,
91 name = Just name,
92 copy = Nothing,
93 mark = noMark
94 }
96flexibleVar = UF.fresh $ Descriptor {
97 structure = Nothing,
98 rank = noRank,
99 flex = Flexible,
100 name = Nothing,
101 copy = Nothing,
102 mark = noMark
103 }
105rigidVar = UF.fresh $ Descriptor {
106 structure = Nothing,
107 rank = noRank,
108 flex = Rigid,
109 name = Nothing,
110 copy = Nothing,
111 mark = noMark
112 }
114-- ex qs constraint == exists qs. constraint
115ex :: [Variable] -> TypeConstraint -> TypeConstraint
116ex fqs constraint = CLet [Scheme [] fqs constraint Map.empty] CTrue
118-- fl qs constraint == forall qs. constraint
119fl :: [Variable] -> TypeConstraint -> TypeConstraint
120fl rqs constraint = CLet [Scheme rqs [] constraint Map.empty] CTrue
122exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
123exists f = do
124 v <- flexibleVar
125 ex [v] <$> f (VarN v)
127instance Show a => Show (UF.Point a) where
128 show point = unsafePerformIO $ fmap show (UF.descriptor point)
130instance Pretty a => Pretty (UF.Point a) where
131 pretty point = unsafePerformIO $ fmap pretty (UF.descriptor point)
133instance Pretty a => Pretty (Term1 a) where
134 pretty term =
135 case term of
136 App1 f x -> pretty f <+> pretty x
137 Fun1 arg body -> formattedArg <+> P.text "->" <+> pretty body
138 where
139 prettyArg = pretty arg
140 formattedArg = parensIf ("->" `List.isInfixOf` P.render prettyArg) prettyArg
141 Var1 x -> pretty x
142 EmptyRecord1 -> P.braces P.empty
143 Record1 fields ext ->
144 P.braces (pretty ext <+> P.text "|" <+> P.sep (P.punctuate P.comma prettyFields))
145 where
146 mkPretty f t = P.text f <+> P.text ":" <+> pretty t
147 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
149instance Pretty a => Pretty (TermN a) where
150 pretty term =
151 case term of
152 VarN x -> pretty x
153 TermN t1 -> pretty t1
155instance Pretty Descriptor where
156 pretty desc =
157 case (structure desc, name desc) of
158 (Just term, _) -> pretty term
159 (_, Just name) -> P.text name
160 _ -> P.text "?"
162instance (Pretty a, Pretty b) => Pretty (Constraint a b) where
163 pretty constraint =
164 case constraint of
165 CTrue -> P.text "True"
166 CEqual a b -> pretty a <+> P.text "=" <+> pretty b
167 CAnd [] -> P.text "True"
169 CAnd cs ->
170 P.parens . P.sep $ P.punctuate (P.text " and") (map pretty cs)
172 CLet [Scheme [] fqs constraint header] CTrue | Map.null header ->
173 P.sep [ binder, pretty c ]
174 where
175 mergeExists vs c =
176 case c of
177 CLet [Scheme [] fqs' c' _] CTrue -> mergeExists (vs ++ fqs') c'
178 _ -> (vs, c)
180 (fqs', c) = mergeExists fqs constraint
182 binder = if null fqs' then P.empty else
183 P.text "exists" <+> P.hsep (map pretty fqs') <> P.text "."
185 CLet schemes constraint ->
186 P.fsep [ P.hang (P.text "let") 4 (P.brackets . P.sep . P.punctuate P.comma $ map pretty schemes)
187 , P.text "in", pretty constraint ]
189 CInstance name tipe ->
190 P.text name <+> P.text "<" <+> pretty tipe
192instance (Pretty a, Pretty b) => Pretty (Scheme a b) where
193 pretty (Scheme rqs fqs constraint headers) =
194 P.sep [ forall, cs, headers' ]
195 where
196 forall = if null rqs && null fqs then P.empty else
197 P.text "forall" <+> frees <+> rigids
199 frees = P.hsep $ map pretty fqs
200 rigids = if null rqs then P.empty else P.braces . P.hsep $ map pretty rqs
202 cs = case constraint of
203 CTrue -> P.empty
204 CAnd [] -> P.empty
205 _ -> P.brackets (pretty constraint)
207 headers' = if Map.size headers > 0 then dict else P.empty
208 dict = P.parens . P.sep . P.punctuate P.comma . map prettyPair $ Map.toList headers
209 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty t
211extraPretty :: (Pretty t, Crawl t) => t -> IO Doc
212extraPretty value = do
213 (_, rawVars) <- runStateT (crawl getNames value) []
214 let vars = map head . List.group $ List.sort rawVars
215 letters = map (:[]) ['a'..'z']
216 suffix s = map (++s)
217 allVars = letters ++ suffix "'" letters ++ concatMap (\n -> suffix (show n) letters) [0..]
218 okayVars = filter (`notElem` vars) allVars
219 runStateT (crawl rename value) okayVars
220 return (pretty value)
221 where
222 getNames name vars =
223 case name of
224 Just var -> (name, var:vars)
225 Nothing -> (name, vars)
227 rename name vars =
228 case name of
229 Just var -> (name, vars)
230 Nothing -> (Just (head vars), tail vars)
233-- Code for traversing all the type data-structures and giving
234-- names to the variables embedded deep in there.
235class Crawl t where
236 crawl :: (Maybe TypeName -> [String] -> (Maybe TypeName, [String]))
237 -> t
238 -> StateT [String] IO t
240instance (Crawl t, Crawl v) => Crawl (Constraint t v) where
241 crawl nextState constraint =
242 let rnm = crawl nextState in
243 case constraint of
244 CTrue -> return CTrue
245 CEqual a b -> CEqual <$> rnm a <*> rnm b
246 CAnd cs -> CAnd <$> crawl nextState cs
247 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
248 CInstance name tipe -> CInstance name <$> rnm tipe
250instance Crawl a => Crawl [a] where
251 crawl nextState list = mapM (crawl nextState) list
253instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
254 crawl nextState (Scheme rqs fqs c headers) =
255 let rnm = crawl nextState in
256 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
258instance Crawl t => Crawl (TermN t) where
259 crawl nextState tipe =
260 case tipe of
261 VarN x -> VarN <$> crawl nextState x
262 TermN term -> TermN <$> crawl nextState term
264instance Crawl t => Crawl (Term1 t) where
265 crawl nextState term =
266 let rnm = crawl nextState in
267 case term of
268 App1 a b -> App1 <$> rnm a <*> rnm b
269 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
270 Var1 a -> Var1 <$> rnm a
271 EmptyRecord1 -> return EmptyRecord1
272 Record1 fields ext ->
273 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
275instance Crawl a => Crawl (UF.Point a) where
276 crawl nextState point = do
277 desc <- liftIO $ UF.descriptor point
278 desc' <- crawl nextState desc
279 liftIO $ UF.setDescriptor point desc'
280 return point
282instance Crawl Descriptor where
283 crawl nextState desc = do
284 state <- get
285 let (name', state') = nextState (name desc) state
286 structure' <- traverse (crawl nextState) (structure desc)
287 put state'
288 return $ desc { name = name', structure = structure' }