on aee2191 help sign in
elk/src/Type/Type.hs
510 lines 11 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Type where
5import Control.Monad (when)
6import Control.Monad.State (StateT, liftIO)
7import qualified Control.Monad.State as State
8import qualified Data.Char as Char
9import qualified Data.Map as Map
10import Data.Monoid ((<>))
11import qualified Data.Text as Text
12import qualified Data.UnionFind.IO as UF
13import Data.Text (Text)
15import qualified AST.Type as T
16import qualified AST.Variable as Var
17import qualified Reporting.Annotation as A
18import qualified Reporting.Error.Type as Error
19import qualified Reporting.Region as R
23-- CONCRETE TYPES
26type Type =
27 TermN Variable
30type Variable =
31 UF.Point Descriptor
34type TypeConstraint =
35 Constraint Type Variable
38type TypeScheme =
39 Scheme Type Variable
43-- TYPE PRIMITIVES
46data Term1 a
47 = App1 a a
48 | Fun1 a a
49 | EmptyRecord1
50 | Record1 (Map.Map Text a) a
53data TermN a
54 = PlaceHolder Text
55 | AliasN Var.Canonical [(Text, TermN a)] (TermN a)
56 | VarN a
57 | TermN (Term1 (TermN a))
60record :: Map.Map Text (TermN a) -> TermN a -> TermN a
61record fs rec =
62 TermN (Record1 fs rec)
66-- DESCRIPTORS
69data Descriptor =
70 Descriptor
71 { _content :: Content
72 , _rank :: Int
73 , _mark :: Int
74 , _copy :: Maybe Variable
75 }
78data Content
79 = Structure (Term1 Variable)
80 | Atom Var.Canonical
81 | Var Flex (Maybe Super) (Maybe Text)
82 | Alias Var.Canonical [(Text,Variable)] Variable
83 | Error
86data Flex
87 = Rigid
88 | Flex
91data Super
92 = Number
93 | Comparable
94 | Appendable
95 | CompAppend
96 deriving (Eq)
99noRank :: Int
100noRank = -1
103outermostRank :: Int
104outermostRank = 0
107noMark :: Int
108noMark = 0
111initialMark :: Int
112initialMark = 1
115occursMark :: Int
116occursMark =
117 -1
120getVarNamesMark :: Int
121getVarNamesMark =
122 -2
126-- CONSTRAINTS
129data Constraint a b
130 = CTrue
131 | CSaveEnv
132 | CEqual Error.Hint R.Region a a
133 | CAnd [Constraint a b]
134 | CLet [Scheme a b] (Constraint a b)
135 | CInstance R.Region SchemeName a
138type SchemeName = Text
141data Scheme a b = Scheme
142 { _rigidQuantifiers :: [b]
143 , _flexibleQuantifiers :: [b]
144 , _constraint :: Constraint a b
145 , _header :: Map.Map Text (A.Located a)
146 }
150-- TYPE HELPERS
153infixr 9 ==>
156(==>) :: Type -> Type -> Type
157(==>) a b =
158 TermN (Fun1 a b)
161(<|) :: TermN a -> TermN a -> TermN a
162(<|) f a =
163 TermN (App1 f a)
167-- VARIABLE CREATION
170mkDescriptor :: Content -> Descriptor
171mkDescriptor content =
172 Descriptor
173 { _content = content
174 , _rank = noRank
175 , _mark = noMark
176 , _copy = Nothing
177 }
180mkAtom :: Var.Canonical -> IO Variable
181mkAtom name =
182 UF.fresh $ mkDescriptor (Atom name)
185mkVar :: Maybe Super -> IO Variable
186mkVar maybeSuper =
187 UF.fresh $ mkDescriptor (Var Flex maybeSuper Nothing)
190mkNamedVar :: Flex -> Text -> IO Variable
191mkNamedVar flex name =
192 UF.fresh $ mkDescriptor $ Var flex (toSuper name) (Just name)
195toSuper :: Text -> Maybe Super
196toSuper name =
197 if Text.isPrefixOf "number" name then
198 Just Number
200 else if Text.isPrefixOf "comparable" name then
201 Just Comparable
203 else if Text.isPrefixOf "appendable" name then
204 Just Appendable
206 else
207 Nothing
211-- CONSTRAINT HELPERS
214monoscheme :: Map.Map Text (A.Located a) -> Scheme a b
215monoscheme headers =
216 Scheme [] [] CTrue headers
219infixl 8 /\
222(/\) :: Constraint a b -> Constraint a b -> Constraint a b
223(/\) c1 c2 =
224 case (c1, c2) of
225 (CTrue, _) -> c2
226 (_, CTrue) -> c1
227 _ -> CAnd [c1,c2]
230-- ex qs constraint == exists qs. constraint
231ex :: [Variable] -> TypeConstraint -> TypeConstraint
232ex fqs constraint =
233 CLet [Scheme [] fqs constraint Map.empty] CTrue
236forall :: [Variable] -> TypeConstraint -> TypeConstraint
237forall rqs constraint =
238 CLet [Scheme rqs [] constraint Map.empty] CTrue
241exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
242exists f =
243 do v <- mkVar Nothing
244 ex [v] <$> f (VarN v)
247existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
248existsNumber f =
249 do v <- mkVar (Just Number)
250 ex [v] <$> f (VarN v)
254-- CONVERT TO SOURCE TYPES
257-- TODO: Attach resulting type to the descriptor so that you
258-- never have to do extra work, particularly nice for aliased types
259toSrcType :: Variable -> IO T.Canonical
260toSrcType variable =
261 do takenNames <- State.execStateT (getVarNames variable) Map.empty
262 State.evalStateT (variableToSrcType variable) (makeNameState takenNames)
265variableToSrcType :: Variable -> StateT NameState IO T.Canonical
266variableToSrcType variable =
267 do descriptor <- liftIO $ UF.descriptor variable
268 let mark = _mark descriptor
269 if mark == occursMark
270 then
271 return (T.Var "∞")
273 else
274 do liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = occursMark })
275 srcType <- contentToSrcType variable (_content descriptor)
276 liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = mark })
277 return srcType
280contentToSrcType :: Variable -> Content -> StateT NameState IO T.Canonical
281contentToSrcType variable content =
282 case content of
283 Structure term ->
284 termToSrcType term
286 Atom name ->
287 return (T.Type name)
289 Var _ _ (Just name) ->
290 return (T.Var name)
292 Var flex maybeSuper Nothing ->
293 do freshName <- getFreshName maybeSuper
294 liftIO $ UF.modifyDescriptor variable $ \desc ->
295 desc { _content = Var flex maybeSuper (Just freshName) }
296 return (T.Var freshName)
298 Alias name args realVariable ->
299 do srcArgs <- traverse (traverse variableToSrcType) args
300 srcType <- variableToSrcType realVariable
301 return (T.Aliased name srcArgs (T.Filled srcType))
303 Error ->
304 return (T.Var "?")
307termToSrcType :: Term1 Variable -> StateT NameState IO T.Canonical
308termToSrcType term =
309 case term of
310 App1 func arg ->
311 do srcFunc <- variableToSrcType func
312 srcArg <- variableToSrcType arg
313 case srcFunc of
314 T.App f args ->
315 return (T.App f (args ++ [srcArg]))
317 _ ->
318 return (T.App srcFunc [srcArg])
320 Fun1 a b ->
321 T.Lambda
322 <$> variableToSrcType a
323 <*> variableToSrcType b
325 EmptyRecord1 ->
326 return $ T.Record [] Nothing
328 Record1 fields extension ->
329 do srcFields <- Map.toList <$> traverse variableToSrcType fields
330 srcExt <- T.iteratedDealias <$> variableToSrcType extension
331 return $
332 case srcExt of
333 T.Record subFields subExt ->
334 T.Record (subFields ++ srcFields) subExt
336 T.Var _ ->
337 T.Record srcFields (Just srcExt)
339 _ ->
340 error "Used toSrcType on a type that is not well-formed"
344-- MANAGE FRESH VARIABLE NAMES
347data NameState = NameState
348 { _taken :: TakenNames
349 , _normals :: Int
350 , _numbers :: Int
351 , _comparables :: Int
352 , _appendables :: Int
353 , _compAppends :: Int
354 }
357type TakenNames = Map.Map Text Variable
360makeNameState :: TakenNames -> NameState
361makeNameState taken =
362 NameState taken 0 0 0 0 0
365getFreshName :: (Monad m) => Maybe Super -> StateT NameState m Text
366getFreshName maybeSuper =
367 case maybeSuper of
368 Nothing ->
369 do index <- State.gets _normals
370 taken <- State.gets _taken
371 let (uniqueName, newIndex) = getFreshNormal index taken
372 State.modify (\state -> state { _normals = newIndex })
373 return uniqueName
375 Just Number ->
376 getFreshSuper "number" _numbers (\index state -> state { _numbers = index })
378 Just Comparable ->
379 getFreshSuper "comparable" _comparables (\index state -> state { _comparables = index })
381 Just Appendable ->
382 getFreshSuper "appendable" _appendables (\index state -> state { _appendables = index })
384 Just CompAppend ->
385 getFreshSuper "compappend" _compAppends (\index state -> state { _compAppends = index })
388getFreshNormal :: Int -> TakenNames -> (Text, Int)
389getFreshNormal index taken =
390 let
391 (postfix, letter) =
392 quotRem index 26
394 char =
395 Char.chr (97 + letter)
397 name =
398 Text.pack (if postfix <= 0 then [char] else char : show postfix)
399 in
400 if Map.member name taken then
401 getFreshNormal (index + 1) taken
403 else
404 (name, index + 1)
407getFreshSuper
408 :: (Monad m)
409 => Text
410 -> (NameState -> Int)
411 -> (Int -> NameState -> NameState)
412 -> StateT NameState m Text
413getFreshSuper name getter setter =
414 do index <- State.gets getter
415 taken <- State.gets _taken
416 let (uniqueName, newIndex) = getFreshSuperHelp name index taken
417 State.modify (setter newIndex)
418 return uniqueName
421getFreshSuperHelp :: Text -> Int -> TakenNames -> (Text, Int)
422getFreshSuperHelp name index taken =
423 let
424 newName =
425 if index <= 0 then name else name <> Text.pack (show index)
426 in
427 if Map.member newName taken then
428 getFreshSuperHelp name (index + 1) taken
430 else
431 (newName, index + 1)
435-- GET ALL VARIABLE NAMES
438getVarNames :: Variable -> StateT TakenNames IO ()
439getVarNames var =
440 do desc <- liftIO $ UF.descriptor var
441 case _mark desc == getVarNamesMark of
442 True ->
443 return ()
445 False ->
446 do liftIO $ UF.setDescriptor var (desc { _mark = getVarNamesMark })
447 case _content desc of
448 Atom _ ->
449 return ()
451 Error ->
452 return ()
454 Var _ _ Nothing ->
455 return ()
457 Var flex maybeSuper (Just name) ->
458 do oldTaken <- State.get
459 newTaken <- liftIO $ addVarName 0 name var flex maybeSuper oldTaken
460 State.put newTaken
462 Alias _ args realVar ->
463 do mapM_ (getVarNames . snd) args
464 getVarNames realVar
466 Structure (App1 func arg) ->
467 do getVarNames func
468 getVarNames arg
470 Structure (Fun1 arg body) ->
471 do getVarNames arg
472 getVarNames body
474 Structure EmptyRecord1 ->
475 return ()
477 Structure (Record1 fields extension) ->
478 do mapM_ getVarNames fields
479 getVarNames extension
482addVarName :: Int -> Text -> Variable -> Flex -> Maybe Super -> TakenNames -> IO TakenNames
483addVarName index givenName var flex maybeSuper taken =
484 let
485 name =
486 makeIndexedName givenName index
487 in
488 case Map.lookup name taken of
489 Nothing ->
490 do when (name /= givenName) $ UF.modifyDescriptor var $ \desc ->
491 desc { _content = Var flex maybeSuper (Just name) }
492 return $ Map.insert name var taken
494 Just otherVar ->
495 do same <- UF.equivalent var otherVar
496 if same
497 then return taken
498 else addVarName (index + 1) givenName var flex maybeSuper taken
501makeIndexedName :: Text -> Int -> Text
502makeIndexedName name index =
503 if index <= 0 then
504 name
506 else if Char.isDigit (Text.last name) then
507 name <> Text.pack ('_' : show index)
509 else
510 name <> Text.pack (show index)