on b97576d help sign in
elk/src/Type/Type.hs
502 lines 11 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Type where
4import Control.Monad (when)
5import Control.Monad.State (StateT, liftIO)
6import qualified Control.Monad.State as State
7import qualified Data.Char as Char
8import qualified Data.List as List
9import qualified Data.Map as Map
10import qualified Data.UnionFind.IO as UF
12import qualified AST.Type as T
13import qualified AST.Variable as Var
14import qualified Reporting.Annotation as A
15import qualified Reporting.Error.Type as Error
16import qualified Reporting.Region as R
20-- CONCRETE TYPES
23type Type =
24 TermN Variable
27type Variable =
28 UF.Point Descriptor
31type TypeConstraint =
32 Constraint Type Variable
35type TypeScheme =
36 Scheme Type Variable
40-- TYPE PRIMITIVES
43data Term1 a
44 = App1 a a
45 | Fun1 a a
46 | EmptyRecord1
47 | Record1 (Map.Map String a) a
50data TermN a
51 = PlaceHolder String
52 | AliasN Var.Canonical [(String, TermN a)] (TermN a)
53 | VarN a
54 | TermN (Term1 (TermN a))
57record :: Map.Map String (TermN a) -> TermN a -> TermN a
58record fs rec =
59 TermN (Record1 fs rec)
63-- DESCRIPTORS
66data Descriptor = Descriptor
67 { _content :: Content
68 , _rank :: Int
69 , _mark :: Int
70 , _copy :: Maybe Variable
71 }
74data Content
75 = Structure (Term1 Variable)
76 | Atom Var.Canonical
77 | Var Flex (Maybe Super) (Maybe String)
78 | Alias Var.Canonical [(String,Variable)] Variable
79 | Error
82data Flex
83 = Rigid
84 | Flex
87data Super
88 = Number
89 | Comparable
90 | Appendable
91 | CompAppend
92 deriving (Eq)
95noRank :: Int
96noRank = -1
99outermostRank :: Int
100outermostRank = 0
103noMark :: Int
104noMark = 0
107initialMark :: Int
108initialMark = 1
111occursMark :: Int
112occursMark =
113 -1
116getVarNamesMark :: Int
117getVarNamesMark =
118 -2
122-- CONSTRAINTS
125data Constraint a b
126 = CTrue
127 | CSaveEnv
128 | CEqual Error.Hint R.Region a a
129 | CAnd [Constraint a b]
130 | CLet [Scheme a b] (Constraint a b)
131 | CInstance R.Region SchemeName a
134type SchemeName = String
137data Scheme a b = Scheme
138 { _rigidQuantifiers :: [b]
139 , _flexibleQuantifiers :: [b]
140 , _constraint :: Constraint a b
141 , _header :: Map.Map String (A.Located a)
142 }
146-- TYPE HELPERS
149infixr 9 ==>
152(==>) :: Type -> Type -> Type
153(==>) a b =
154 TermN (Fun1 a b)
157(<|) :: TermN a -> TermN a -> TermN a
158(<|) f a =
159 TermN (App1 f a)
163-- VARIABLE CREATION
166mkDescriptor :: Content -> Descriptor
167mkDescriptor content =
168 Descriptor
169 { _content = content
170 , _rank = noRank
171 , _mark = noMark
172 , _copy = Nothing
173 }
176mkAtom :: Var.Canonical -> IO Variable
177mkAtom name =
178 UF.fresh $ mkDescriptor (Atom name)
181mkVar :: Maybe Super -> IO Variable
182mkVar maybeSuper =
183 UF.fresh $ mkDescriptor (Var Flex maybeSuper Nothing)
186mkNamedVar :: Flex -> String -> IO Variable
187mkNamedVar flex name =
188 UF.fresh $ mkDescriptor $ Var flex (toSuper name) (Just name)
191toSuper :: String -> Maybe Super
192toSuper name =
193 if List.isPrefixOf "number" name then
194 Just Number
196 else if List.isPrefixOf "comparable" name then
197 Just Comparable
199 else if List.isPrefixOf "appendable" name then
200 Just Appendable
202 else
203 Nothing
207-- CONSTRAINT HELPERS
210monoscheme :: Map.Map String (A.Located a) -> Scheme a b
211monoscheme headers =
212 Scheme [] [] CTrue headers
215infixl 8 /\
217(/\) :: Constraint a b -> Constraint a b -> Constraint a b
218(/\) c1 c2 =
219 case (c1, c2) of
220 (CTrue, _) -> c2
221 (_, CTrue) -> c1
222 _ -> CAnd [c1,c2]
225-- ex qs constraint == exists qs. constraint
226ex :: [Variable] -> TypeConstraint -> TypeConstraint
227ex fqs constraint =
228 CLet [Scheme [] fqs constraint Map.empty] CTrue
231forall :: [Variable] -> TypeConstraint -> TypeConstraint
232forall rqs constraint =
233 CLet [Scheme rqs [] constraint Map.empty] CTrue
236exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
237exists f =
238 do v <- mkVar Nothing
239 ex [v] <$> f (VarN v)
242existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
243existsNumber f =
244 do v <- mkVar (Just Number)
245 ex [v] <$> f (VarN v)
249-- CONVERT TO SOURCE TYPES
252-- TODO: Attach resulting type to the descriptor so that you
253-- never have to do extra work, particularly nice for aliased types
254toSrcType :: Variable -> IO T.Canonical
255toSrcType variable =
256 do takenNames <- State.execStateT (getVarNames variable) Map.empty
257 State.evalStateT (variableToSrcType variable) (makeNameState takenNames)
260variableToSrcType :: Variable -> StateT NameState IO T.Canonical
261variableToSrcType variable =
262 do descriptor <- liftIO $ UF.descriptor variable
263 let mark = _mark descriptor
264 if mark == occursMark
265 then
266 return (T.Var "∞")
268 else
269 do liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = occursMark })
270 srcType <- contentToSrcType variable (_content descriptor)
271 liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = mark })
272 return srcType
275contentToSrcType :: Variable -> Content -> StateT NameState IO T.Canonical
276contentToSrcType variable content =
277 case content of
278 Structure term ->
279 termToSrcType term
281 Atom name ->
282 return (T.Type name)
284 Var _ _ (Just name) ->
285 return (T.Var name)
287 Var flex maybeSuper Nothing ->
288 do freshName <- getFreshName maybeSuper
289 liftIO $ UF.modifyDescriptor variable $ \desc ->
290 desc { _content = Var flex maybeSuper (Just freshName) }
291 return (T.Var freshName)
293 Alias name args realVariable ->
294 do srcArgs <- traverse (traverse variableToSrcType) args
295 srcType <- variableToSrcType realVariable
296 return (T.Aliased name srcArgs (T.Filled srcType))
298 Error ->
299 return (T.Var "?")
302termToSrcType :: Term1 Variable -> StateT NameState IO T.Canonical
303termToSrcType term =
304 case term of
305 App1 func arg ->
306 do srcFunc <- variableToSrcType func
307 srcArg <- variableToSrcType arg
308 case srcFunc of
309 T.App f args ->
310 return (T.App f (args ++ [srcArg]))
312 _ ->
313 return (T.App srcFunc [srcArg])
315 Fun1 a b ->
316 T.Lambda
317 <$> variableToSrcType a
318 <*> variableToSrcType b
320 EmptyRecord1 ->
321 return $ T.Record [] Nothing
323 Record1 fields extension ->
324 do srcFields <- Map.toList <$> traverse variableToSrcType fields
325 srcExt <- T.iteratedDealias <$> variableToSrcType extension
326 return $
327 case srcExt of
328 T.Record subFields subExt ->
329 T.Record (subFields ++ srcFields) subExt
331 T.Var _ ->
332 T.Record srcFields (Just srcExt)
334 _ ->
335 error "Used toSrcType on a type that is not well-formed"
339-- MANAGE FRESH VARIABLE NAMES
342data NameState = NameState
343 { _taken :: TakenNames
344 , _normals :: Int
345 , _numbers :: Int
346 , _comparables :: Int
347 , _appendables :: Int
348 , _compAppends :: Int
349 }
352type TakenNames = Map.Map String Variable
355makeNameState :: TakenNames -> NameState
356makeNameState taken =
357 NameState taken 0 0 0 0 0
360getFreshName :: (Monad m) => Maybe Super -> StateT NameState m String
361getFreshName maybeSuper =
362 case maybeSuper of
363 Nothing ->
364 do index <- State.gets _normals
365 taken <- State.gets _taken
366 let (uniqueName, newIndex) = getFreshNormal index taken
367 State.modify (\state -> state { _normals = newIndex })
368 return uniqueName
370 Just Number ->
371 getFreshSuper "number" _numbers (\index state -> state { _numbers = index })
373 Just Comparable ->
374 getFreshSuper "comparable" _comparables (\index state -> state { _comparables = index })
376 Just Appendable ->
377 getFreshSuper "appendable" _appendables (\index state -> state { _appendables = index })
379 Just CompAppend ->
380 getFreshSuper "compappend" _compAppends (\index state -> state { _compAppends = index })
383getFreshNormal :: Int -> TakenNames -> (String, Int)
384getFreshNormal index taken =
385 let
386 (postfix, letter) =
387 quotRem index 26
389 name =
390 Char.chr (97 + letter) : if postfix <= 0 then "" else show postfix
391 in
392 if Map.member name taken then
393 getFreshNormal (index + 1) taken
395 else
396 (name, index + 1)
399getFreshSuper
400 :: (Monad m)
401 => String
402 -> (NameState -> Int)
403 -> (Int -> NameState -> NameState)
404 -> StateT NameState m String
405getFreshSuper name getter setter =
406 do index <- State.gets getter
407 taken <- State.gets _taken
408 let (uniqueName, newIndex) = getFreshSuperHelp name index taken
409 State.modify (setter newIndex)
410 return uniqueName
413getFreshSuperHelp :: String -> Int -> TakenNames -> (String, Int)
414getFreshSuperHelp name index taken =
415 let
416 newName =
417 if index <= 0 then name else name ++ show index
418 in
419 if Map.member newName taken then
420 getFreshSuperHelp name (index + 1) taken
422 else
423 (newName, index + 1)
427-- GET ALL VARIABLE NAMES
430getVarNames :: Variable -> StateT TakenNames IO ()
431getVarNames var =
432 do desc <- liftIO $ UF.descriptor var
433 case _mark desc == getVarNamesMark of
434 True ->
435 return ()
437 False ->
438 do liftIO $ UF.setDescriptor var (desc { _mark = getVarNamesMark })
439 case _content desc of
440 Atom _ ->
441 return ()
443 Error ->
444 return ()
446 Var _ _ Nothing ->
447 return ()
449 Var flex maybeSuper (Just name) ->
450 do oldTaken <- State.get
451 newTaken <- liftIO $ addVarName 0 name var flex maybeSuper oldTaken
452 State.put newTaken
454 Alias _ args realVar ->
455 do mapM_ (getVarNames . snd) args
456 getVarNames realVar
458 Structure (App1 func arg) ->
459 do getVarNames func
460 getVarNames arg
462 Structure (Fun1 arg body) ->
463 do getVarNames arg
464 getVarNames body
466 Structure EmptyRecord1 ->
467 return ()
469 Structure (Record1 fields extension) ->
470 do mapM_ getVarNames fields
471 getVarNames extension
474addVarName :: Int -> String -> Variable -> Flex -> Maybe Super -> TakenNames -> IO TakenNames
475addVarName index givenName var flex maybeSuper taken =
476 let
477 name =
478 makeIndexedName givenName index
479 in
480 case Map.lookup name taken of
481 Nothing ->
482 do when (name /= givenName) $ UF.modifyDescriptor var $ \desc ->
483 desc { _content = Var flex maybeSuper (Just name) }
484 return $ Map.insert name var taken
486 Just otherVar ->
487 do same <- UF.equivalent var otherVar
488 if same
489 then return taken
490 else addVarName (index + 1) givenName var flex maybeSuper taken
493makeIndexedName :: String -> Int -> String
494makeIndexedName name index =
495 if index <= 0 then
496 name
498 else if Char.isDigit (last name) then
499 name ++ '_' : show index
501 else
502 name ++ show index