git.iko.soy/elk
on ba5bfd2 help sign in
elk/src/Type/Type.hs
466 lines 10 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Type where
4import Control.Monad.State (StateT, liftIO)
5import qualified Control.Monad.State as State
6import qualified Data.List as List
7import qualified Data.Map as Map
8import qualified Data.Set as Set
9import qualified Data.Traversable as Traverse (traverse)
10import qualified Data.UnionFind.IO as UF
12import qualified AST.Module.Name as ModuleName
13import qualified AST.Type as T
14import qualified AST.Variable as Var
15import qualified Reporting.Annotation as A
16import qualified Reporting.Error.Type as Error
17import qualified Reporting.Region as R
21-- CONCRETE TYPES
24type Type =
25 TermN Variable
28type Variable =
29 UF.Point Descriptor
32type TypeConstraint =
33 Constraint Type Variable
36type TypeScheme =
37 Scheme Type Variable
41-- TYPE PRIMITIVES
44data Term1 a
45 = App1 a a
46 | Fun1 a a
47 | EmptyRecord1
48 | Record1 (Map.Map String a) a
49 | Effects1 (Set.Set ModuleName.Canonical)
52data TermN a
53 = PlaceHolder String
54 | AliasN Var.Canonical [(String, TermN a)] (TermN a)
55 | VarN a
56 | TermN (Term1 (TermN a))
59record :: Map.Map String (TermN a) -> TermN a -> TermN a
60record fs rec =
61 TermN (Record1 fs rec)
65-- DESCRIPTORS
68data Descriptor = Descriptor
69 { _content :: Content
70 , _rank :: Int
71 , _mark :: Int
72 , _copy :: Maybe Variable
73 }
76data Content
77 = Structure (Term1 Variable)
78 | Atom Var.Canonical
79 | Var Flex (Maybe Super) (Maybe String)
80 | Alias Var.Canonical [(String,Variable)] Variable
81 | Error
84data Flex
85 = Rigid
86 | Flex
89data Super
90 = Number
91 | Comparable
92 | Appendable
93 | CompAppend
94 deriving (Eq)
97noRank :: Int
98noRank = -1
101outermostRank :: Int
102outermostRank = 0
105noMark :: Int
106noMark = 0
109initialMark :: Int
110initialMark = 1
113occursMark :: Int
114occursMark =
115 -1
118getVarNamesMark :: Int
119getVarNamesMark =
120 -2
124-- CONSTRAINTS
127data Constraint a b
128 = CTrue
129 | CSaveEnv
130 | CEqual Error.Hint R.Region a a
131 | CAnd [Constraint a b]
132 | CLet [Scheme a b] (Constraint a b)
133 | CInstance R.Region SchemeName a
136type SchemeName = String
139data Scheme a b = Scheme
140 { _rigidQuantifiers :: [b]
141 , _flexibleQuantifiers :: [b]
142 , _constraint :: Constraint a b
143 , _header :: Map.Map String (A.Located a)
144 }
148-- TYPE HELPERS
151infixr 9 ==>
154(==>) :: Type -> Type -> Type
155(==>) a b =
156 TermN (Fun1 a b)
159(<|) :: TermN a -> TermN a -> TermN a
160(<|) f a =
161 TermN (App1 f a)
165-- VARIABLE CREATION
168mkDescriptor :: Content -> Descriptor
169mkDescriptor content =
170 Descriptor
171 { _content = content
172 , _rank = noRank
173 , _mark = noMark
174 , _copy = Nothing
175 }
178mkAtom :: Var.Canonical -> IO Variable
179mkAtom name =
180 UF.fresh $ mkDescriptor (Atom name)
183mkVar :: Maybe Super -> IO Variable
184mkVar maybeSuper =
185 UF.fresh $ mkDescriptor (Var Flex maybeSuper Nothing)
188mkNamedVar :: String -> IO Variable
189mkNamedVar name =
190 UF.fresh $ mkDescriptor (Var Flex (toSuper name) Nothing)
193mkRigid :: String -> IO Variable
194mkRigid name =
195 UF.fresh $ mkDescriptor (Var Rigid (toSuper name) (Just name))
198toSuper :: String -> Maybe Super
199toSuper name =
200 if List.isPrefixOf "number" name then
201 Just Number
203 else if List.isPrefixOf "comparable" name then
204 Just Comparable
206 else if List.isPrefixOf "appendable" name then
207 Just Appendable
209 else
210 Nothing
214-- CONSTRAINT HELPERS
217monoscheme :: Map.Map String (A.Located a) -> Scheme a b
218monoscheme headers =
219 Scheme [] [] CTrue headers
222infixl 8 /\
224(/\) :: Constraint a b -> Constraint a b -> Constraint a b
225(/\) c1 c2 =
226 case (c1, c2) of
227 (CTrue, _) -> c2
228 (_, CTrue) -> c1
229 _ -> CAnd [c1,c2]
232-- ex qs constraint == exists qs. constraint
233ex :: [Variable] -> TypeConstraint -> TypeConstraint
234ex fqs constraint =
235 CLet [Scheme [] fqs constraint Map.empty] CTrue
238-- fl qs constraint == forall qs. constraint
239fl :: [Variable] -> TypeConstraint -> TypeConstraint
240fl rqs constraint =
241 CLet [Scheme rqs [] constraint Map.empty] CTrue
244exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
245exists f =
246 do v <- mkVar Nothing
247 ex [v] <$> f (VarN v)
250existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
251existsNumber f =
252 do v <- mkVar (Just Number)
253 ex [v] <$> f (VarN v)
257-- CONVERT TO SOURCE TYPES
260-- TODO: Attach resulting type to the descriptor so that you
261-- never have to do extra work, particularly nice for aliased types
262toSrcType :: Variable -> IO T.Canonical
263toSrcType variable =
264 do usedNames <- getVarNames variable
265 State.evalStateT (variableToSrcType variable) (makeNameState usedNames)
268variableToSrcType :: Variable -> StateT NameState IO T.Canonical
269variableToSrcType variable =
270 do descriptor <- liftIO $ UF.descriptor variable
271 let mark = _mark descriptor
272 if mark == occursMark
273 then
274 return (T.Var "∞")
276 else
277 do liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = occursMark })
278 srcType <- contentToSrcType variable (_content descriptor)
279 liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = mark })
280 return srcType
283contentToSrcType :: Variable -> Content -> StateT NameState IO T.Canonical
284contentToSrcType variable content =
285 case content of
286 Structure term ->
287 termToSrcType term
289 Atom name ->
290 return (T.Type name)
292 Var _ _ (Just name) ->
293 return (T.Var name)
295 Var flex maybeSuper Nothing ->
296 do freshName <- getFreshName maybeSuper
297 liftIO $ UF.modifyDescriptor variable $ \desc ->
298 desc { _content = Var flex maybeSuper (Just freshName) }
299 return (T.Var freshName)
301 Alias name args realVariable ->
302 do srcArgs <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType tvar) args
303 srcType <- variableToSrcType realVariable
304 return (T.Aliased name srcArgs (T.Filled srcType))
306 Error ->
307 return (T.Var "?")
310termToSrcType :: Term1 Variable -> StateT NameState IO T.Canonical
311termToSrcType term =
312 case term of
313 App1 func arg ->
314 do srcFunc <- variableToSrcType func
315 srcArg <- variableToSrcType arg
316 case srcFunc of
317 T.App f args ->
318 return (T.App f (args ++ [srcArg]))
320 _ ->
321 return (T.App srcFunc [srcArg])
323 Fun1 a b ->
324 T.Lambda
325 <$> variableToSrcType a
326 <*> variableToSrcType b
328 EmptyRecord1 ->
329 return $ T.Record [] Nothing
331 Record1 fields extension ->
332 do srcFields <- Map.toList <$> Traverse.traverse variableToSrcType fields
333 srcExt <- T.iteratedDealias <$> variableToSrcType extension
334 return $
335 case srcExt of
336 T.Record subFields subExt ->
337 T.Record (subFields ++ srcFields) subExt
339 T.Var _ ->
340 T.Record srcFields (Just srcExt)
342 _ ->
343 error "Used toSrcType on a type that is not well-formed"
345 Effects1 names ->
346 return $ T.Effects names
350-- MANAGE FRESH VARIABLE NAMES
353data NameState = NameState
354 { _freeNames :: [String]
355 , _numberPrimes :: Int
356 , _comparablePrimes :: Int
357 , _appendablePrimes :: Int
358 , _compAppendPrimes :: Int
359 }
362makeNameState :: Set.Set String -> NameState
363makeNameState usedNames =
364 let
365 makeName suffix =
366 map (:suffix) ['a'..'z']
368 allNames =
369 concatMap makeName ("" : map show [ (1 :: Int) .. ])
371 freeNames =
372 filter (\name -> Set.notMember name usedNames) allNames
373 in
374 NameState freeNames 0 0 0 0
377getFreshName :: (Monad m) => Maybe Super -> StateT NameState m String
378getFreshName maybeSuper =
379 case maybeSuper of
380 Nothing ->
381 do names <- State.gets _freeNames
382 State.modify (\state -> state { _freeNames = tail names })
383 return (head names)
385 Just Number ->
386 do primes <- State.gets _numberPrimes
387 State.modify (\state -> state { _numberPrimes = primes + 1 })
388 return ("number" ++ replicate primes '\'')
390 Just Comparable ->
391 do primes <- State.gets _comparablePrimes
392 State.modify (\state -> state { _comparablePrimes = primes + 1 })
393 return ("comparable" ++ replicate primes '\'')
395 Just Appendable ->
396 do primes <- State.gets _appendablePrimes
397 State.modify (\state -> state { _appendablePrimes = primes + 1 })
398 return ("appendable" ++ replicate primes '\'')
400 Just CompAppend ->
401 do primes <- State.gets _compAppendPrimes
402 State.modify (\state -> state { _compAppendPrimes = primes + 1 })
403 return ("compappend" ++ replicate primes '\'')
407-- GET ALL VARIABLE NAMES
410getVarNames :: Variable -> IO (Set.Set String)
411getVarNames var =
412 do desc <- UF.descriptor var
413 if _mark desc == getVarNamesMark
414 then
415 return Set.empty
417 else
418 do UF.setDescriptor var (desc { _mark = getVarNamesMark })
419 getVarNamesHelp (_content desc)
422getVarNamesHelp :: Content -> IO (Set.Set String)
423getVarNamesHelp content =
424 case content of
425 Var _ _ (Just name) ->
426 return (Set.singleton name)
428 Var _ _ Nothing ->
429 return Set.empty
431 Structure term ->
432 getVarNamesTerm term
434 Alias _name args realVar ->
435 do let argSet = Set.fromList (map fst args)
436 realSet <- getVarNames realVar
437 sets <- mapM (getVarNames . snd) args
438 return (Set.unions (realSet : argSet : sets))
440 Atom _ ->
441 return Set.empty
443 Error ->
444 return Set.empty
447getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
448getVarNamesTerm term =
449 let go = getVarNames in
450 case term of
451 App1 a b ->
452 Set.union <$> go a <*> go b
454 Fun1 a b ->
455 Set.union <$> go a <*> go b
457 EmptyRecord1 ->
458 return Set.empty
460 Record1 fields extension ->
461 do fieldVars <- Set.unions <$> mapM go (Map.elems fields)
462 Set.union fieldVars <$> go extension
464 Effects1 _ ->
465 return Set.empty