git.iko.soy/elk
on fe1e5d2 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.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 let mark = _mark descriptor
270 if mark == occursMark
271 then
272 return (T.Var "∞")
274 else
275 do liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = occursMark })
276 srcType <- contentToSrcType variable (_content descriptor)
277 liftIO $ UF.modifyDescriptor variable (\desc -> desc { _mark = mark })
278 return srcType
281contentToSrcType :: Variable -> Content -> StateT NameState IO T.Canonical
282contentToSrcType variable content =
283 case content of
284 Structure term ->
285 termToSrcType term
287 Atom name ->
288 return (T.Type name)
290 Var _ _ (Just name) ->
291 return (T.Var name)
293 Var flex maybeSuper Nothing ->
294 do freshName <- getFreshName maybeSuper
295 liftIO $ UF.modifyDescriptor variable $ \desc ->
296 desc { _content = Var flex maybeSuper (Just freshName) }
297 return (T.Var freshName)
299 Alias name args realVariable ->
300 do srcArgs <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType tvar) args
301 srcType <- variableToSrcType realVariable
302 return (T.Aliased name srcArgs (T.Filled srcType))
304 Error ->
305 return (T.Var "?")
308termToSrcType :: Term1 Variable -> StateT NameState IO T.Canonical
309termToSrcType term =
310 case term of
311 App1 func arg ->
312 do srcFunc <- variableToSrcType func
313 srcArg <- variableToSrcType arg
314 case srcFunc of
315 T.App f args ->
316 return (T.App f (args ++ [srcArg]))
318 _ ->
319 return (T.App srcFunc [srcArg])
321 Fun1 a b ->
322 T.Lambda
323 <$> variableToSrcType a
324 <*> variableToSrcType b
326 EmptyRecord1 ->
327 return $ T.Record [] Nothing
329 Record1 fields extension ->
330 do srcFields <- Map.toList <$> Traverse.traverse variableToSrcType fields
331 srcExt <- T.iteratedDealias <$> variableToSrcType extension
332 return $
333 case srcExt of
334 T.Record subFields subExt ->
335 T.Record (subFields ++ srcFields) subExt
337 T.Var _ ->
338 T.Record srcFields (Just srcExt)
340 _ ->
341 error "Used toSrcType on a type that is not well-formed"
345-- MANAGE FRESH VARIABLE NAMES
348data NameState = NameState
349 { _freeNames :: [String]
350 , _numberPrimes :: Int
351 , _comparablePrimes :: Int
352 , _appendablePrimes :: Int
353 , _compAppendPrimes :: Int
354 }
357makeNameState :: Set.Set String -> NameState
358makeNameState usedNames =
359 let
360 makeName suffix =
361 map (:suffix) ['a'..'z']
363 allNames =
364 concatMap makeName ("" : map show [ (1 :: Int) .. ])
366 freeNames =
367 filter (\name -> Set.notMember name usedNames) allNames
368 in
369 NameState freeNames 0 0 0 0
372getFreshName :: (Monad m) => Maybe Super -> StateT NameState m String
373getFreshName maybeSuper =
374 case maybeSuper of
375 Nothing ->
376 do names <- State.gets _freeNames
377 State.modify (\state -> state { _freeNames = tail names })
378 return (head names)
380 Just Number ->
381 do primes <- State.gets _numberPrimes
382 State.modify (\state -> state { _numberPrimes = primes + 1 })
383 return ("number" ++ replicate primes '\'')
385 Just Comparable ->
386 do primes <- State.gets _comparablePrimes
387 State.modify (\state -> state { _comparablePrimes = primes + 1 })
388 return ("comparable" ++ replicate primes '\'')
390 Just Appendable ->
391 do primes <- State.gets _appendablePrimes
392 State.modify (\state -> state { _appendablePrimes = primes + 1 })
393 return ("appendable" ++ replicate primes '\'')
395 Just CompAppend ->
396 do primes <- State.gets _compAppendPrimes
397 State.modify (\state -> state { _compAppendPrimes = primes + 1 })
398 return ("compappend" ++ replicate primes '\'')
402-- GET ALL VARIABLE NAMES
405getVarNames :: Variable -> IO (Set.Set String)
406getVarNames var =
407 do desc <- UF.descriptor var
408 if _mark desc == getVarNamesMark
409 then
410 return Set.empty
412 else
413 do UF.setDescriptor var (desc { _mark = getVarNamesMark })
414 getVarNamesHelp (_content desc)
417getVarNamesHelp :: Content -> IO (Set.Set String)
418getVarNamesHelp content =
419 case content of
420 Var _ _ (Just name) ->
421 return (Set.singleton name)
423 Var _ _ Nothing ->
424 return Set.empty
426 Structure term ->
427 getVarNamesTerm term
429 Alias _name args realVar ->
430 do let argSet = Set.fromList (map fst args)
431 realSet <- getVarNames realVar
432 sets <- mapM (getVarNames . snd) args
433 return (Set.unions (realSet : argSet : sets))
435 Atom _ ->
436 return Set.empty
438 Error ->
439 return Set.empty
442getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
443getVarNamesTerm term =
444 let go = getVarNames in
445 case term of
446 App1 a b ->
447 Set.union <$> go a <*> go b
449 Fun1 a b ->
450 Set.union <$> go a <*> go b
452 EmptyRecord1 ->
453 return Set.empty
455 Record1 fields extension ->
456 do fieldVars <- Set.unions <$> mapM go (Map.elems fields)
457 Set.union fieldVars <$> go extension