git.iko.soy/elk
on 2b8044e help sign in
elk/src/Type/Type.hs
458 lines 10.0 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
51data TermN a
52 = PlaceHolder String
53 | AliasN Var.Canonical [(String, TermN a)] (TermN a)
54 | VarN a
55 | TermN (Term1 (TermN a))
58record :: Map.Map String (TermN a) -> TermN a -> TermN a
59record fs rec =
60 TermN (Record1 fs rec)
64-- DESCRIPTORS
67data Descriptor = Descriptor
68 { _content :: Content
69 , _rank :: Int
70 , _mark :: Int
71 , _copy :: Maybe Variable
72 }
75data Content
76 = Structure (Term1 Variable)
77 | Atom Var.Canonical
78 | Var Flex (Maybe Super) (Maybe String)
79 | Alias Var.Canonical [(String,Variable)] Variable
80 | Error
83data Flex
84 = Rigid
85 | Flex
88data Super
89 = Number
90 | Comparable
91 | Appendable
92 | CompAppend
93 deriving (Eq)
96noRank :: Int
97noRank = -1
100outermostRank :: Int
101outermostRank = 0
104noMark :: Int
105noMark = 0
108initialMark :: Int
109initialMark = 1
112occursMark :: Int
113occursMark =
114 -1
117getVarNamesMark :: Int
118getVarNamesMark =
119 -2
123-- CONSTRAINTS
126data Constraint a b
127 = CTrue
128 | CSaveEnv
129 | CEqual Error.Hint R.Region a a
130 | CAnd [Constraint a b]
131 | CLet [Scheme a b] (Constraint a b)
132 | CInstance R.Region SchemeName a
135type SchemeName = String
138data Scheme a b = Scheme
139 { _rigidQuantifiers :: [b]
140 , _flexibleQuantifiers :: [b]
141 , _constraint :: Constraint a b
142 , _header :: Map.Map String (A.Located a)
143 }
147-- TYPE HELPERS
150infixr 9 ==>
153(==>) :: Type -> Type -> Type
154(==>) a b =
155 TermN (Fun1 a b)
158(<|) :: TermN a -> TermN a -> TermN a
159(<|) f a =
160 TermN (App1 f a)
164-- VARIABLE CREATION
167mkDescriptor :: Content -> Descriptor
168mkDescriptor content =
169 Descriptor
170 { _content = content
171 , _rank = noRank
172 , _mark = noMark
173 , _copy = Nothing
174 }
177mkAtom :: Var.Canonical -> IO Variable
178mkAtom name =
179 UF.fresh $ mkDescriptor (Atom name)
182mkVar :: Maybe Super -> IO Variable
183mkVar maybeSuper =
184 UF.fresh $ mkDescriptor (Var Flex maybeSuper Nothing)
187mkNamedVar :: String -> IO Variable
188mkNamedVar name =
189 UF.fresh $ mkDescriptor (Var Flex (toSuper name) Nothing)
192mkRigid :: String -> IO Variable
193mkRigid name =
194 UF.fresh $ mkDescriptor (Var Rigid (toSuper name) (Just name))
197toSuper :: String -> Maybe Super
198toSuper name =
199 if List.isPrefixOf "number" name then
200 Just Number
202 else if List.isPrefixOf "comparable" name then
203 Just Comparable
205 else if List.isPrefixOf "appendable" name then
206 Just Appendable
208 else
209 Nothing
213-- CONSTRAINT HELPERS
216monoscheme :: Map.Map String (A.Located a) -> Scheme a b
217monoscheme headers =
218 Scheme [] [] CTrue headers
221infixl 8 /\
223(/\) :: Constraint a b -> Constraint a b -> Constraint a b
224(/\) c1 c2 =
225 case (c1, c2) of
226 (CTrue, _) -> c2
227 (_, CTrue) -> c1
228 _ -> CAnd [c1,c2]
231-- ex qs constraint == exists qs. constraint
232ex :: [Variable] -> TypeConstraint -> TypeConstraint
233ex fqs constraint =
234 CLet [Scheme [] fqs constraint Map.empty] CTrue
237-- fl qs constraint == forall qs. constraint
238fl :: [Variable] -> TypeConstraint -> TypeConstraint
239fl rqs constraint =
240 CLet [Scheme rqs [] constraint Map.empty] CTrue
243exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
244exists f =
245 do v <- mkVar Nothing
246 ex [v] <$> f (VarN v)
249existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
250existsNumber f =
251 do v <- mkVar (Just Number)
252 ex [v] <$> f (VarN v)
256-- CONVERT TO SOURCE TYPES
259-- TODO: Attach resulting type to the descriptor so that you
260-- never have to do extra work, particularly nice for aliased types
261toSrcType :: Variable -> IO T.Canonical
262toSrcType variable =
263 do usedNames <- getVarNames variable
264 State.evalStateT (variableToSrcType variable) (makeNameState usedNames)
267variableToSrcType :: Variable -> StateT NameState IO T.Canonical
268variableToSrcType variable =
269 do descriptor <- liftIO $ UF.descriptor variable
270 let mark = _mark descriptor
271 if mark == occursMark
272 then
273 return (T.Var "∞")
275 else
276 do liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = occursMark })
277 srcType <- contentToSrcType variable (_content descriptor)
278 liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = mark })
279 return srcType
282contentToSrcType :: Variable -> Content -> StateT NameState IO T.Canonical
283contentToSrcType variable content =
284 case content of
285 Structure term ->
286 termToSrcType term
288 Atom name ->
289 return (T.Type name)
291 Var _ _ (Just name) ->
292 return (T.Var name)
294 Var flex maybeSuper Nothing ->
295 do freshName <- getFreshName maybeSuper
296 liftIO $ UF.modifyDescriptor variable $ \desc ->
297 desc { _content = Var flex maybeSuper (Just freshName) }
298 return (T.Var freshName)
300 Alias name args realVariable ->
301 do srcArgs <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType tvar) args
302 srcType <- variableToSrcType realVariable
303 return (T.Aliased name srcArgs (T.Filled srcType))
305 Error ->
306 return (T.Var "?")
309termToSrcType :: Term1 Variable -> StateT NameState IO T.Canonical
310termToSrcType term =
311 case term of
312 App1 func arg ->
313 do srcFunc <- variableToSrcType func
314 srcArg <- variableToSrcType arg
315 case srcFunc of
316 T.App f args ->
317 return (T.App f (args ++ [srcArg]))
319 _ ->
320 return (T.App srcFunc [srcArg])
322 Fun1 a b ->
323 T.Lambda
324 <$> variableToSrcType a
325 <*> variableToSrcType b
327 EmptyRecord1 ->
328 return $ T.Record [] Nothing
330 Record1 fields extension ->
331 do srcFields <- Map.toList <$> Traverse.traverse variableToSrcType fields
332 srcExt <- T.iteratedDealias <$> variableToSrcType extension
333 return $
334 case srcExt of
335 T.Record subFields subExt ->
336 T.Record (subFields ++ srcFields) subExt
338 T.Var _ ->
339 T.Record srcFields (Just srcExt)
341 _ ->
342 error "Used toSrcType on a type that is not well-formed"
346-- MANAGE FRESH VARIABLE NAMES
349data NameState = NameState
350 { _freeNames :: [String]
351 , _numberPrimes :: Int
352 , _comparablePrimes :: Int
353 , _appendablePrimes :: Int
354 , _compAppendPrimes :: Int
355 }
358makeNameState :: Set.Set String -> NameState
359makeNameState usedNames =
360 let
361 makeName suffix =
362 map (:suffix) ['a'..'z']
364 allNames =
365 concatMap makeName ("" : map show [ (1 :: Int) .. ])
367 freeNames =
368 filter (\name -> Set.notMember name usedNames) allNames
369 in
370 NameState freeNames 0 0 0 0
373getFreshName :: (Monad m) => Maybe Super -> StateT NameState m String
374getFreshName maybeSuper =
375 case maybeSuper of
376 Nothing ->
377 do names <- State.gets _freeNames
378 State.modify (\state -> state { _freeNames = tail names })
379 return (head names)
381 Just Number ->
382 do primes <- State.gets _numberPrimes
383 State.modify (\state -> state { _numberPrimes = primes + 1 })
384 return ("number" ++ replicate primes '\'')
386 Just Comparable ->
387 do primes <- State.gets _comparablePrimes
388 State.modify (\state -> state { _comparablePrimes = primes + 1 })
389 return ("comparable" ++ replicate primes '\'')
391 Just Appendable ->
392 do primes <- State.gets _appendablePrimes
393 State.modify (\state -> state { _appendablePrimes = primes + 1 })
394 return ("appendable" ++ replicate primes '\'')
396 Just CompAppend ->
397 do primes <- State.gets _compAppendPrimes
398 State.modify (\state -> state { _compAppendPrimes = primes + 1 })
399 return ("compappend" ++ replicate primes '\'')
403-- GET ALL VARIABLE NAMES
406getVarNames :: Variable -> IO (Set.Set String)
407getVarNames var =
408 do desc <- UF.descriptor var
409 if _mark desc == getVarNamesMark
410 then
411 return Set.empty
413 else
414 do UF.setDescriptor var (desc { _mark = getVarNamesMark })
415 getVarNamesHelp (_content desc)
418getVarNamesHelp :: Content -> IO (Set.Set String)
419getVarNamesHelp content =
420 case content of
421 Var _ _ (Just name) ->
422 return (Set.singleton name)
424 Var _ _ Nothing ->
425 return Set.empty
427 Structure term ->
428 getVarNamesTerm term
430 Alias _name args realVar ->
431 do let argSet = Set.fromList (map fst args)
432 realSet <- getVarNames realVar
433 sets <- mapM (getVarNames . snd) args
434 return (Set.unions (realSet : argSet : sets))
436 Atom _ ->
437 return Set.empty
439 Error ->
440 return Set.empty
443getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
444getVarNamesTerm term =
445 let go = getVarNames in
446 case term of
447 App1 a b ->
448 Set.union <$> go a <*> go b
450 Fun1 a b ->
451 Set.union <$> go a <*> go b
453 EmptyRecord1 ->
454 return Set.empty
456 Record1 fields extension ->
457 do fieldVars <- Set.unions <$> mapM go (Map.elems fields)
458 Set.union fieldVars <$> go extension