git.iko.soy/elk
on 445ea07 help sign in
elk/src/Type/Type.hs
470 lines 11 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Type where
5import Control.Monad (when)
6import Control.Monad.State.Strict (StateT, liftIO)
7import qualified Control.Monad.State.Strict as State
8import qualified Data.Char as Char
9import qualified Data.Map as Map
10import Data.Monoid ((<>))
11import qualified Data.Text as Text
12import Data.Text (Text)
14import qualified AST.Type as T
15import qualified AST.Variable as Var
16import qualified Reporting.Annotation as A
17import qualified Reporting.Error.Type as Error
18import qualified Reporting.Region as R
19import qualified Type.UnionFind as UF
23-- TYPE PRIMITIVES
26type Variable =
27 UF.Point Descriptor
30data FlatType
31 = App1 Var.Canonical [Variable]
32 | Fun1 Variable Variable
33 | EmptyRecord1
34 | Record1 (Map.Map Text Variable) Variable
37data Type
38 = PlaceHolder Text
39 | AliasN Var.Canonical [(Text, Type)] Type
40 | VarN Variable
41 | AppN Var.Canonical [Type]
42 | FunN Type Type
43 | EmptyRecordN
44 | RecordN (Map.Map Text Type) Type
48-- DESCRIPTORS
51data Descriptor =
52 Descriptor
53 { _content :: Content
54 , _rank :: Int
55 , _mark :: Int
56 , _copy :: Maybe Variable
57 }
60data Content
61 = Structure FlatType
62 | Var Flex (Maybe Super) (Maybe Text)
63 | Alias Var.Canonical [(Text,Variable)] Variable
64 | Error Text
67data Flex
68 = Rigid
69 | Flex
72data Super
73 = Number
74 | Comparable
75 | Appendable
76 | CompAppend
77 deriving (Eq)
80noRank :: Int
81noRank = -1
84outermostRank :: Int
85outermostRank = 0
88noMark :: Int
89noMark = 0
92initialMark :: Int
93initialMark = 1
96occursMark :: Int
97occursMark =
98 -1
101getVarNamesMark :: Int
102getVarNamesMark =
103 -2
107-- CONSTRAINTS
110data Constraint
111 = CTrue
112 | CSaveEnv
113 | CEqual Error.Hint R.Region Type Type
114 | CAnd [Constraint]
115 | CLet [Scheme] Constraint
116 | CInstance R.Region SchemeName Type
119type SchemeName = Text
122data Scheme =
123 Scheme
124 { _rigidQuantifiers :: [Variable]
125 , _flexibleQuantifiers :: [Variable]
126 , _constraint :: Constraint
127 , _header :: Map.Map Text (A.Located Type)
128 }
132-- TYPE HELPERS
135infixr 9 ==>
138{-# INLINE (==>) #-}
139(==>) :: Type -> Type -> Type
140(==>) =
141 FunN
145-- VARIABLE CREATION
148mkDescriptor :: Content -> Descriptor
149mkDescriptor content =
150 Descriptor
151 { _content = content
152 , _rank = noRank
153 , _mark = noMark
154 , _copy = Nothing
155 }
158mkVar :: Maybe Super -> IO Variable
159mkVar maybeSuper =
160 UF.fresh $ mkDescriptor (Var Flex maybeSuper Nothing)
163mkNamedVar :: Flex -> Text -> IO Variable
164mkNamedVar flex name =
165 UF.fresh $ mkDescriptor $ Var flex (toSuper name) (Just name)
168toSuper :: Text -> Maybe Super
169toSuper name =
170 if Text.isPrefixOf "number" name then
171 Just Number
173 else if Text.isPrefixOf "comparable" name then
174 Just Comparable
176 else if Text.isPrefixOf "appendable" name then
177 Just Appendable
179 else
180 Nothing
184-- CONSTRAINT HELPERS
187monoscheme :: Map.Map Text (A.Located Type) -> Scheme
188monoscheme headers =
189 Scheme [] [] CTrue headers
192infixl 8 /\
195(/\) :: Constraint -> Constraint -> Constraint
196(/\) c1 c2 =
197 case (c1, c2) of
198 (CTrue, _) -> c2
199 (_, CTrue) -> c1
200 _ -> CAnd [c1,c2]
203-- ex qs constraint == exists qs. constraint
204ex :: [Variable] -> Constraint -> Constraint
205ex fqs constraint =
206 CLet [Scheme [] fqs constraint Map.empty] CTrue
209forall :: [Variable] -> Constraint -> Constraint
210forall rqs constraint =
211 CLet [Scheme rqs [] constraint Map.empty] CTrue
214exists :: (Type -> IO Constraint) -> IO Constraint
215exists f =
216 do v <- mkVar Nothing
217 ex [v] <$> f (VarN v)
220existsNumber :: (Type -> IO Constraint) -> IO Constraint
221existsNumber f =
222 do v <- mkVar (Just Number)
223 ex [v] <$> f (VarN v)
227-- CONVERT TO SOURCE TYPES
230-- TODO: Attach resulting type to the descriptor so that you
231-- never have to do extra work, particularly nice for aliased types
232toSrcType :: Variable -> IO T.Canonical
233toSrcType variable =
234 do takenNames <- State.execStateT (getVarNames variable) Map.empty
235 State.evalStateT (variableToSrcType variable) (makeNameState takenNames)
238variableToSrcType :: Variable -> StateT NameState IO T.Canonical
239variableToSrcType variable =
240 do descriptor <- liftIO $ UF.descriptor variable
241 let mark = _mark descriptor
242 if mark == occursMark
243 then
244 return (T.Var "∞")
246 else
247 do liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = occursMark })
248 srcType <- contentToSrcType variable (_content descriptor)
249 liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = mark })
250 return srcType
253contentToSrcType :: Variable -> Content -> StateT NameState IO T.Canonical
254contentToSrcType variable content =
255 case content of
256 Structure term ->
257 termToSrcType term
259 Var _ _ (Just name) ->
260 return (T.Var name)
262 Var flex maybeSuper Nothing ->
263 do freshName <- getFreshName maybeSuper
264 liftIO $ UF.modifyDescriptor variable $ \desc ->
265 desc { _content = Var flex maybeSuper (Just freshName) }
266 return (T.Var freshName)
268 Alias name args realVariable ->
269 do srcArgs <- traverse (traverse variableToSrcType) args
270 srcType <- variableToSrcType realVariable
271 return (T.Aliased name srcArgs (T.Filled srcType))
273 Error name ->
274 return (T.Var name)
277termToSrcType :: FlatType -> StateT NameState IO T.Canonical
278termToSrcType term =
279 case term of
280 App1 name args ->
281 T.Type name <$> traverse variableToSrcType args
283 Fun1 a b ->
284 T.Lambda
285 <$> variableToSrcType a
286 <*> variableToSrcType b
288 EmptyRecord1 ->
289 return $ T.Record [] Nothing
291 Record1 fields extension ->
292 do srcFields <- Map.toList <$> traverse variableToSrcType fields
293 srcExt <- T.iteratedDealias <$> variableToSrcType extension
294 return $
295 case srcExt of
296 T.Record subFields subExt ->
297 T.Record (subFields ++ srcFields) subExt
299 T.Var _ ->
300 T.Record srcFields (Just srcExt)
302 _ ->
303 error "Used toSrcType on a type that is not well-formed"
307-- MANAGE FRESH VARIABLE NAMES
310data NameState =
311 NameState
312 { _taken :: TakenNames
313 , _normals :: Int
314 , _numbers :: Int
315 , _comparables :: Int
316 , _appendables :: Int
317 , _compAppends :: Int
318 }
321type TakenNames = Map.Map Text Variable
324makeNameState :: TakenNames -> NameState
325makeNameState taken =
326 NameState taken 0 0 0 0 0
329getFreshName :: (Monad m) => Maybe Super -> StateT NameState m Text
330getFreshName maybeSuper =
331 case maybeSuper of
332 Nothing ->
333 do index <- State.gets _normals
334 taken <- State.gets _taken
335 let (uniqueName, newIndex) = getFreshNormal index taken
336 State.modify (\state -> state { _normals = newIndex })
337 return uniqueName
339 Just Number ->
340 getFreshSuper "number" _numbers (\index state -> state { _numbers = index })
342 Just Comparable ->
343 getFreshSuper "comparable" _comparables (\index state -> state { _comparables = index })
345 Just Appendable ->
346 getFreshSuper "appendable" _appendables (\index state -> state { _appendables = index })
348 Just CompAppend ->
349 getFreshSuper "compappend" _compAppends (\index state -> state { _compAppends = index })
352getFreshNormal :: Int -> TakenNames -> (Text, Int)
353getFreshNormal index taken =
354 let
355 (postfix, letter) =
356 quotRem index 26
358 char =
359 Char.chr (97 + letter)
361 name =
362 Text.pack (if postfix <= 0 then [char] else char : show postfix)
363 in
364 if Map.member name taken then
365 getFreshNormal (index + 1) taken
367 else
368 (name, index + 1)
371getFreshSuper
372 :: (Monad m)
373 => Text
374 -> (NameState -> Int)
375 -> (Int -> NameState -> NameState)
376 -> StateT NameState m Text
377getFreshSuper name getter setter =
378 do index <- State.gets getter
379 taken <- State.gets _taken
380 let (uniqueName, newIndex) = getFreshSuperHelp name index taken
381 State.modify (setter newIndex)
382 return uniqueName
385getFreshSuperHelp :: Text -> Int -> TakenNames -> (Text, Int)
386getFreshSuperHelp name index taken =
387 let
388 newName =
389 if index <= 0 then name else name <> Text.pack (show index)
390 in
391 if Map.member newName taken then
392 getFreshSuperHelp name (index + 1) taken
394 else
395 (newName, index + 1)
399-- GET ALL VARIABLE NAMES
402getVarNames :: Variable -> StateT TakenNames IO ()
403getVarNames var =
404 do desc <- liftIO $ UF.descriptor var
405 case _mark desc == getVarNamesMark of
406 True ->
407 return ()
409 False ->
410 do liftIO $ UF.setDescriptor var (desc { _mark = getVarNamesMark })
411 case _content desc of
412 Error _ ->
413 return ()
415 Var _ _ Nothing ->
416 return ()
418 Var flex maybeSuper (Just name) ->
419 do oldTaken <- State.get
420 newTaken <- liftIO $ addVarName 0 name var flex maybeSuper oldTaken
421 State.put newTaken
423 Alias _ args realVar ->
424 do mapM_ (getVarNames . snd) args
425 getVarNames realVar
427 Structure (App1 _ args) ->
428 mapM_ getVarNames args
430 Structure (Fun1 arg body) ->
431 do getVarNames arg
432 getVarNames body
434 Structure EmptyRecord1 ->
435 return ()
437 Structure (Record1 fields extension) ->
438 do mapM_ getVarNames fields
439 getVarNames extension
442addVarName :: Int -> Text -> Variable -> Flex -> Maybe Super -> TakenNames -> IO TakenNames
443addVarName index givenName var flex maybeSuper taken =
444 let
445 name =
446 makeIndexedName givenName index
447 in
448 case Map.lookup name taken of
449 Nothing ->
450 do when (name /= givenName) $ UF.modifyDescriptor var $ \desc ->
451 desc { _content = Var flex maybeSuper (Just name) }
452 return $ Map.insert name var taken
454 Just otherVar ->
455 do same <- UF.equivalent var otherVar
456 if same
457 then return taken
458 else addVarName (index + 1) givenName var flex maybeSuper taken
461makeIndexedName :: Text -> Int -> Text
462makeIndexedName name index =
463 if index <= 0 then
464 name
466 else if Char.isDigit (Text.last name) then
467 name <> Text.pack ('_' : show index)
469 else
470 name <> Text.pack (show index)