git.iko.soy/elk
on bdfaa69 help sign in
elk/src/Type/Type.hs
444 lines 14 kB history raw
1{-# OPTIONS_GHC -W #-}
2module Type.Type where
4import qualified Data.Char as Char
5import qualified Data.List as List
6import qualified Data.Map as Map
7import qualified Data.UnionFind.IO as UF
8import Type.PrettyPrint
9import Text.PrettyPrint as P
10import System.IO.Unsafe
11import Control.Applicative ((<$>),(<*>))
12import Control.Monad.State (StateT, get, put, execStateT, runStateT)
13import Control.Monad.Error (ErrorT, Error, liftIO)
14import Data.Traversable (traverse)
15import AST.Annotation
16import qualified AST.PrettyPrint as PP
17import qualified AST.Type as T
18import qualified AST.Variable as Var
20data Term1 a
21 = App1 a a
22 | Fun1 a a
23 | Var1 a
24 | EmptyRecord1
25 | Record1 (Map.Map String [a]) a
26 deriving Show
28data TermN a
29 = VarN (Maybe Var.Canonical) a
30 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
31 deriving Show
33varN :: a -> TermN a
34varN = VarN Nothing
36termN :: (Term1 (TermN a)) -> TermN a
37termN = TermN Nothing
39record :: Map.Map String [TermN a] -> TermN a -> TermN a
40record fs rec = termN (Record1 fs rec)
42type Type = TermN Variable
43type Variable = UF.Point Descriptor
45type SchemeName = String
46type TypeName = Var.Canonical
48type Constraint a b = Located (BasicConstraint a b)
49data BasicConstraint a b
50 = CTrue
51 | CSaveEnv
52 | CEqual a a
53 | CAnd [Constraint a b]
54 | CLet [Scheme a b] (Constraint a b)
55 | CInstance SchemeName a
56 deriving Show
58data Scheme a b = Scheme {
59 rigidQuantifiers :: [b],
60 flexibleQuantifiers :: [b],
61 constraint :: Constraint a b,
62 header :: Map.Map String a
63} deriving Show
65type TypeConstraint = Constraint Type Variable
66type TypeScheme = Scheme Type Variable
68monoscheme :: Map.Map String a -> Scheme a b
69monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
71infixl 8 /\
73(/\) :: Constraint a b -> Constraint a b -> Constraint a b
74a@(A _ c1) /\ b@(A _ c2) =
75 case (c1, c2) of
76 (CTrue, _) -> b
77 (_, CTrue) -> a
78 _ -> mergeOldDocs a b (CAnd [a,b])
80infixr 9 ==>
81(==>) :: Type -> Type -> Type
82a ==> b = termN (Fun1 a b)
84(<|) :: TermN a -> TermN a -> TermN a
85f <| a = termN (App1 f a)
87data Descriptor = Descriptor
88 { structure :: Maybe (Term1 Variable)
89 , rank :: Int
90 , flex :: Flex
91 , name :: Maybe TypeName
92 , copy :: Maybe Variable
93 , mark :: Int
94 , alias :: Maybe Var.Canonical
95 } deriving Show
97noRank :: Int
98noRank = -1
100outermostRank :: Int
101outermostRank = 0
103noMark :: Int
104noMark = 0
106initialMark :: Int
107initialMark = 1
109data Flex = Rigid | Flexible | Constant | Is SuperType
110 deriving (Show, Eq)
112data SuperType = Number | Comparable | Appendable
113 deriving (Show, Eq)
115namedVar :: Flex -> Var.Canonical -> IO Variable
116namedVar flex name = UF.fresh $ Descriptor
117 { structure = Nothing
118 , rank = noRank
119 , flex = flex
120 , name = Just name
121 , copy = Nothing
122 , mark = noMark
123 , alias = Nothing
124 }
126variable :: Flex -> IO Variable
127variable flex = UF.fresh $ Descriptor
128 { structure = Nothing
129 , rank = noRank
130 , flex = flex
131 , name = Nothing
132 , copy = Nothing
133 , mark = noMark
134 , alias = Nothing
135 }
138-- ex qs constraint == exists qs. constraint
139ex :: [Variable] -> TypeConstraint -> TypeConstraint
140ex fqs constraint@(A ann _) =
141 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
143-- fl qs constraint == forall qs. constraint
144fl :: [Variable] -> TypeConstraint -> TypeConstraint
145fl rqs constraint@(A ann _) =
146 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
148exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
149exists f = do
150 v <- liftIO $ variable Flexible
151 ex [v] <$> f (varN v)
153existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
154existsNumber f = do
155 v <- liftIO $ variable (Is Number)
156 ex [v] <$> f (varN v)
159instance Show a => Show (UF.Point a) where
160 show point = unsafePerformIO $ fmap show (UF.descriptor point)
163instance PrettyType a => PrettyType (UF.Point a) where
164 pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
167instance PrettyType t => PrettyType (Annotated a t) where
168 pretty when (A _ e) = pretty when e
171instance PrettyType a => PrettyType (Term1 a) where
172 pretty when term =
173 let prty = pretty Never in
174 case term of
175 App1 f x | P.render px == "_List" -> P.brackets (pretty Never x)
176 | otherwise -> parensIf needed (px <+> pretty App x)
177 where
178 px = prty f
179 needed = case when of
180 App -> True
181 _ -> False
183 Fun1 arg body ->
184 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
185 where
186 needed = case when of
187 Never -> False
188 _ -> True
190 Var1 x -> prty x
192 EmptyRecord1 -> P.braces P.empty
194 Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
195 where
196 prettyExt = prty ext
197 extend | P.render prettyExt == "{}" = P.empty
198 | otherwise = prettyExt <+> P.text "|"
199 mkPretty f t = P.text f <+> P.text ":" <+> prty t
200 prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
203instance PrettyType a => PrettyType (TermN a) where
204 pretty when term =
205 case term of
206 VarN alias x -> either alias (pretty when x)
207 TermN alias t1 -> either alias (pretty when t1)
208 where
209 either maybeAlias doc =
210 case maybeAlias of
211 Just alias -> PP.pretty alias
212 Nothing -> doc
214instance PrettyType Descriptor where
215 pretty when desc = do
216 case (alias desc, structure desc, name desc) of
217 (Just name, _, _) -> PP.pretty name
218 (_, Just term, _) -> pretty when term
219 (_, _, Just name)
220 | Var.isTuple name ->
221 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
222 | otherwise ->
223 P.text (Var.toString name)
225 _ -> P.text "?"
228instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
229 pretty _ constraint =
230 let prty = pretty Never in
231 case constraint of
232 CTrue -> P.text "True"
233 CSaveEnv -> P.text "SaveTheEnvironment!!!"
234 CEqual a b -> prty a <+> P.text "=" <+> prty b
235 CAnd [] -> P.text "True"
237 CAnd cs ->
238 P.parens . P.sep $ P.punctuate (P.text " and") (map (pretty Never) cs)
240 CLet [Scheme [] fqs constraint header] (A _ CTrue) | Map.null header ->
241 P.sep [ binder, pretty Never c ]
242 where
243 mergeExists vs (A _ c) =
244 case c of
245 CLet [Scheme [] fqs' c' _] (A _ CTrue) -> mergeExists (vs ++ fqs') c'
246 _ -> (vs, c)
248 (fqs', c) = mergeExists fqs constraint
250 binder = if null fqs' then P.empty else
251 P.text "\x2203" <+> P.hsep (map (pretty Never) fqs') <> P.text "."
253 CLet schemes constraint ->
254 P.fsep [ P.hang (P.text "let") 4 (P.brackets . commaSep $ map (pretty Never) schemes)
255 , P.text "in", pretty Never constraint ]
257 CInstance name tipe ->
258 P.text name <+> P.text "<" <+> prty tipe
260instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
261 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
262 P.sep [ forall, cs, headers' ]
263 where
264 prty = pretty Never
266 forall = if null rqs && null fqs then P.empty else
267 P.text "\x2200" <+> frees <+> rigids
269 frees = P.hsep $ map prty fqs
270 rigids = if null rqs then P.empty else P.braces . P.hsep $ map prty rqs
272 cs = case constraint of
273 CTrue -> P.empty
274 CAnd [] -> P.empty
275 _ -> P.brackets (pretty Never constraint)
277 headers' = if Map.size headers > 0 then dict else P.empty
278 dict = P.parens . commaSep . map prettyPair $ Map.toList headers
279 prettyPair (n,t) = P.text n <+> P.text ":" <+> pretty Never t
282extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
283extraPretty t = pretty Never <$> addNames t
285addNames :: (Crawl t) => t -> IO t
286addNames value = do
287 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
288 let vars = map head . List.group $ List.sort rawVars
289 suffix s = map (++s) (map (:[]) ['a'..'z'])
290 allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
291 okayVars = filter (`notElem` vars) allVars
292 runStateT (crawl rename value) (okayVars, 0, 0, 0)
293 return value
294 where
295 getNames desc state@(vars, a, b, c) =
296 let name' = name desc in
297 case name' of
298 Just (Var.Canonical _ var) -> (name', (var:vars, a, b, c))
299 _ -> (name', state)
301 rename desc state@(vars, a, b, c) =
302 case name desc of
303 Just var -> (Just var, state)
304 Nothing ->
305 case flex desc of
306 Is Number -> (local $ "number" ++ replicate a '\'', (vars, a+1, b, c))
307 Is Comparable -> (local $ "comparable" ++ replicate b '\'', (vars, a, b+1, c))
308 Is Appendable -> (local $ "appendable" ++ replicate c '\'', (vars, a, b, c+1))
309 _ -> (local $ head vars, (tail vars, a, b, c))
310 where
311 local v = Just (Var.local v)
313type CrawlState = ([String], Int, Int, Int)
315-- Code for traversing all the type data-structures and giving
316-- names to the variables embedded deep in there.
317class Crawl t where
318 crawl :: (Descriptor -> CrawlState -> (Maybe TypeName, CrawlState))
319 -> t
320 -> StateT CrawlState IO t
322instance Crawl e => Crawl (Annotated a e) where
323 crawl nextState (A ann e) = A ann <$> crawl nextState e
325instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
326 crawl nextState constraint =
327 let rnm = crawl nextState in
328 case constraint of
329 CTrue -> return CTrue
330 CSaveEnv -> return CSaveEnv
331 CEqual a b -> CEqual <$> rnm a <*> rnm b
332 CAnd cs -> CAnd <$> crawl nextState cs
333 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
334 CInstance name tipe -> CInstance name <$> rnm tipe
336instance Crawl a => Crawl [a] where
337 crawl nextState list = mapM (crawl nextState) list
339instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
340 crawl nextState (Scheme rqs fqs c headers) =
341 let rnm = crawl nextState in
342 Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
344instance Crawl t => Crawl (TermN t) where
345 crawl nextState tipe =
346 case tipe of
347 VarN a x -> VarN a <$> crawl nextState x
348 TermN a term -> TermN a <$> crawl nextState term
350instance Crawl t => Crawl (Term1 t) where
351 crawl nextState term =
352 let rnm = crawl nextState in
353 case term of
354 App1 a b -> App1 <$> rnm a <*> rnm b
355 Fun1 a b -> Fun1 <$> rnm a <*> rnm b
356 Var1 a -> Var1 <$> rnm a
357 EmptyRecord1 -> return EmptyRecord1
358 Record1 fields ext ->
359 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
361instance Crawl a => Crawl (UF.Point a) where
362 crawl nextState point = do
363 desc <- liftIO $ UF.descriptor point
364 desc' <- crawl nextState desc
365 liftIO $ UF.setDescriptor point desc'
366 return point
368instance Crawl Descriptor where
369 crawl nextState desc = do
370 state <- get
371 let (name', state') = nextState desc state
372 structure' <- traverse (crawl nextState) (structure desc)
373 put state'
374 return $ desc { name = name', structure = structure' }
377toSrcType :: Variable -> IO T.CanonicalType
378toSrcType var =
379 go =<< addNames var
380 where
381 go v = do
382 desc <- UF.descriptor v
383 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
384 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
386 backupSrcType desc =
387 case name desc of
388 Just v@(Var.Canonical _ x@(c:_))
389 | Char.isLower c -> return (T.Var x)
390 | otherwise -> return $ T.Type v
392 _ -> error $ concat
393 [ "Problem converting the following type "
394 , "from a type-checker type to a source-syntax type:"
395 , P.render (pretty Never var) ]
397 termToSrcType term =
398 case term of
399 App1 a b -> do
400 a' <- go a
401 b' <- go b
402 case a' of
403 T.App f args -> return $ T.App f (args ++ [b'])
404 _ -> return $ T.App a' [b']
406 Fun1 a b -> T.Lambda <$> go a <*> go b
408 Var1 a -> go a
410 EmptyRecord1 -> return $ T.Record [] Nothing
412 Record1 tfields extension -> do
413 fields' <- traverse (mapM go) tfields
414 let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
415 ext' <- dealias <$> go extension
416 return $ case ext' of
417 T.Record fs ext -> T.Record (fs ++ fields) ext
418 T.Var _ -> T.Record fields (Just ext')
419 _ -> error "Used toSrcType on a type that is not well-formed"
421 dealias :: T.CanonicalType -> T.CanonicalType
422 dealias t =
423 case t of
424 T.Aliased _ t' -> t'
425 _ -> t
428data AppStructure = List Variable | Tuple [Variable] | Other
430collectApps :: Variable -> IO AppStructure
431collectApps var = go [] var
432 where
433 go vars var = do
434 desc <- UF.descriptor var
435 case (structure desc, vars) of
436 (Nothing, [v]) -> case name desc of
437 Just n | Var.isList n -> return (List v)
438 _ -> return Other
439 (Nothing, vs) -> case name desc of
440 Just n | Var.isTuple n -> return (Tuple vs)
441 _ -> return Other
442 (Just term, _) -> case term of
443 App1 a b -> go (vars ++ [b]) a
444 _ -> return Other