git.iko.soy/elk
on 8bbb580 help sign in
elk/src/Type/Type.hs
457 lines 9.9 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.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 :: String -> IO Variable
187mkNamedVar name =
188 UF.fresh $ mkDescriptor (Var Flex (toSuper name) Nothing)
191mkRigid :: String -> IO Variable
192mkRigid name =
193 UF.fresh $ mkDescriptor (Var Rigid (toSuper name) (Just name))
196toSuper :: String -> Maybe Super
197toSuper name =
198 if List.isPrefixOf "number" name then
199 Just Number
201 else if List.isPrefixOf "comparable" name then
202 Just Comparable
204 else if List.isPrefixOf "appendable" name then
205 Just Appendable
207 else
208 Nothing
212-- CONSTRAINT HELPERS
215monoscheme :: Map.Map String (A.Located a) -> Scheme a b
216monoscheme headers =
217 Scheme [] [] CTrue headers
220infixl 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
236-- fl qs constraint == forall qs. constraint
237fl :: [Variable] -> TypeConstraint -> TypeConstraint
238fl rqs constraint =
239 CLet [Scheme rqs [] constraint Map.empty] CTrue
242exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
243exists f =
244 do v <- mkVar Nothing
245 ex [v] <$> f (VarN v)
248existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
249existsNumber f =
250 do v <- mkVar (Just Number)
251 ex [v] <$> f (VarN v)
255-- CONVERT TO SOURCE TYPES
258-- TODO: Attach resulting type to the descriptor so that you
259-- never have to do extra work, particularly nice for aliased types
260toSrcType :: Variable -> IO T.Canonical
261toSrcType variable =
262 do usedNames <- getVarNames variable
263 State.evalStateT (variableToSrcType variable) (makeNameState usedNames)
266variableToSrcType :: Variable -> StateT NameState IO T.Canonical
267variableToSrcType variable =
268 do descriptor <- liftIO $ UF.descriptor variable
269 if _mark descriptor == occursMark
270 then
271 return (T.Var "∞")
273 else
274 do liftIO $ UF.setDescriptor variable (descriptor { _mark = occursMark })
275 srcType <- contentToSrcType variable (_content descriptor)
276 liftIO $ UF.setDescriptor variable descriptor
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 <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType tvar) 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.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 { _freeNames :: [String]
349 , _numberPrimes :: Int
350 , _comparablePrimes :: Int
351 , _appendablePrimes :: Int
352 , _compAppendPrimes :: Int
353 }
356makeNameState :: Set.Set String -> NameState
357makeNameState usedNames =
358 let
359 makeName suffix =
360 map (:suffix) ['a'..'z']
362 allNames =
363 concatMap makeName ("" : map show [ (1 :: Int) .. ])
365 freeNames =
366 filter (\name -> Set.notMember name usedNames) allNames
367 in
368 NameState freeNames 0 0 0 0
371getFreshName :: (Monad m) => Maybe Super -> StateT NameState m String
372getFreshName maybeSuper =
373 case maybeSuper of
374 Nothing ->
375 do names <- State.gets _freeNames
376 State.modify (\state -> state { _freeNames = tail names })
377 return (head names)
379 Just Number ->
380 do primes <- State.gets _numberPrimes
381 State.modify (\state -> state { _numberPrimes = primes + 1 })
382 return ("number" ++ replicate primes '\'')
384 Just Comparable ->
385 do primes <- State.gets _comparablePrimes
386 State.modify (\state -> state { _comparablePrimes = primes + 1 })
387 return ("comparable" ++ replicate primes '\'')
389 Just Appendable ->
390 do primes <- State.gets _appendablePrimes
391 State.modify (\state -> state { _appendablePrimes = primes + 1 })
392 return ("appendable" ++ replicate primes '\'')
394 Just CompAppend ->
395 do primes <- State.gets _compAppendPrimes
396 State.modify (\state -> state { _compAppendPrimes = primes + 1 })
397 return ("compappend" ++ replicate primes '\'')
401-- GET ALL VARIABLE NAMES
404getVarNames :: Variable -> IO (Set.Set String)
405getVarNames var =
406 do desc <- UF.descriptor var
407 if _mark desc == getVarNamesMark
408 then
409 return Set.empty
411 else
412 do UF.setDescriptor var (desc { _mark = getVarNamesMark })
413 getVarNamesHelp (_content desc)
416getVarNamesHelp :: Content -> IO (Set.Set String)
417getVarNamesHelp content =
418 case content of
419 Var _ _ (Just name) ->
420 return (Set.singleton name)
422 Var _ _ Nothing ->
423 return Set.empty
425 Structure term ->
426 getVarNamesTerm term
428 Alias _name args realVar ->
429 do let argSet = Set.fromList (map fst args)
430 realSet <- getVarNames realVar
431 sets <- mapM (getVarNames . snd) args
432 return (Set.unions (realSet : argSet : sets))
434 Atom _ ->
435 return Set.empty
437 Error ->
438 return Set.empty
441getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
442getVarNamesTerm term =
443 let go = getVarNames in
444 case term of
445 App1 a b ->
446 Set.union <$> go a <*> go b
448 Fun1 a b ->
449 Set.union <$> go a <*> go b
451 EmptyRecord1 ->
452 return Set.empty
454 Record1 fields extension ->
455 do fieldVars <- Set.unions <$> mapM go (Map.elems fields)
456 Set.union fieldVars <$> go extension