git.iko.soy/elk
on 74db13f help sign in
elk/src/Type/Type.hs
424 lines 9.2 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Type where
4import Control.Monad.State (StateT)
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
112-- CONSTRAINTS
115data Constraint a b
116 = CTrue
117 | CSaveEnv
118 | CEqual Error.Hint R.Region a a
119 | CAnd [Constraint a b]
120 | CLet [Scheme a b] (Constraint a b)
121 | CInstance R.Region SchemeName a
124type SchemeName = String
127data Scheme a b = Scheme
128 { _rigidQuantifiers :: [b]
129 , _flexibleQuantifiers :: [b]
130 , _constraint :: Constraint a b
131 , _header :: Map.Map String (A.Located a)
132 }
136-- TYPE HELPERS
139infixr 9 ==>
142(==>) :: Type -> Type -> Type
143(==>) a b =
144 TermN (Fun1 a b)
147(<|) :: TermN a -> TermN a -> TermN a
148(<|) f a =
149 TermN (App1 f a)
153-- VARIABLE CREATION
156mkDescriptor :: Content -> Descriptor
157mkDescriptor content =
158 Descriptor
159 { _content = content
160 , _rank = noRank
161 , _mark = noMark
162 , _copy = Nothing
163 }
166mkAtom :: Var.Canonical -> IO Variable
167mkAtom name =
168 UF.fresh $ mkDescriptor (Atom name)
171mkVar :: Maybe Super -> IO Variable
172mkVar maybeSuper =
173 UF.fresh $ mkDescriptor (Var Flex maybeSuper Nothing)
176mkNamedVar :: String -> IO Variable
177mkNamedVar name =
178 UF.fresh $ mkDescriptor (Var Flex (toSuper name) Nothing)
181mkRigid :: String -> IO Variable
182mkRigid name =
183 UF.fresh $ mkDescriptor (Var Rigid (toSuper name) (Just name))
186toSuper :: String -> Maybe Super
187toSuper name =
188 if List.isPrefixOf "number" name then
189 Just Number
191 else if List.isPrefixOf "comparable" name then
192 Just Comparable
194 else if List.isPrefixOf "appendable" name then
195 Just Appendable
197 else
198 Nothing
202-- CONSTRAINT HELPERS
205monoscheme :: Map.Map String (A.Located a) -> Scheme a b
206monoscheme headers =
207 Scheme [] [] CTrue headers
210infixl 8 /\
212(/\) :: Constraint a b -> Constraint a b -> Constraint a b
213(/\) c1 c2 =
214 case (c1, c2) of
215 (CTrue, _) -> c2
216 (_, CTrue) -> c1
217 _ -> CAnd [c1,c2]
220-- ex qs constraint == exists qs. constraint
221ex :: [Variable] -> TypeConstraint -> TypeConstraint
222ex fqs constraint =
223 CLet [Scheme [] fqs constraint Map.empty] CTrue
226-- fl qs constraint == forall qs. constraint
227fl :: [Variable] -> TypeConstraint -> TypeConstraint
228fl rqs constraint =
229 CLet [Scheme rqs [] constraint Map.empty] CTrue
232exists :: (Type -> IO TypeConstraint) -> IO TypeConstraint
233exists f =
234 do v <- mkVar Nothing
235 ex [v] <$> f (VarN v)
238existsNumber :: (Type -> IO TypeConstraint) -> IO TypeConstraint
239existsNumber f =
240 do v <- mkVar (Just Number)
241 ex [v] <$> f (VarN v)
245-- CONVERT TO SOURCE TYPES
248-- TODO: Attach resulting type to the descriptor so that you
249-- never have to do extra work, particularly nice for aliased types
250toSrcType :: Variable -> IO T.Canonical
251toSrcType variable =
252 do usedNames <- getVarNames variable
253 State.evalStateT (variableToSrcType variable) (makeNameState usedNames)
256variableToSrcType :: Variable -> StateT NameState IO T.Canonical
257variableToSrcType variable =
258 do descriptor <- State.liftIO (UF.descriptor variable)
259 case _content descriptor of
260 Structure term ->
261 termToSrcType term
263 Atom name ->
264 return (T.Type name)
266 Var _ _ (Just name) ->
267 return (T.Var name)
269 Var flex maybeSuper Nothing ->
270 do freshName <- getFreshName maybeSuper
271 State.liftIO $ UF.modifyDescriptor variable $ \desc ->
272 desc { _content = Var flex maybeSuper (Just freshName) }
273 return (T.Var freshName)
275 Alias name args realVariable ->
276 do srcArgs <- mapM (\(arg,tvar) -> (,) arg <$> variableToSrcType tvar) args
277 srcType <- variableToSrcType realVariable
278 return (T.Aliased name srcArgs (T.Filled srcType))
280 Error ->
281 return (T.Var "?")
284termToSrcType :: Term1 Variable -> StateT NameState IO T.Canonical
285termToSrcType term =
286 case term of
287 App1 func arg ->
288 do srcFunc <- variableToSrcType func
289 srcArg <- variableToSrcType arg
290 case srcFunc of
291 T.App f args ->
292 return (T.App f (args ++ [srcArg]))
294 _ ->
295 return (T.App srcFunc [srcArg])
297 Fun1 a b ->
298 T.Lambda
299 <$> variableToSrcType a
300 <*> variableToSrcType b
302 EmptyRecord1 ->
303 return $ T.Record [] Nothing
305 Record1 fields extension ->
306 do srcFields <- Map.toList <$> Traverse.traverse variableToSrcType fields
307 srcExt <- T.iteratedDealias <$> variableToSrcType extension
308 return $
309 case srcExt of
310 T.Record subFields subExt ->
311 T.Record (subFields ++ srcFields) subExt
313 T.Var _ ->
314 T.Record srcFields (Just srcExt)
316 _ ->
317 error "Used toSrcType on a type that is not well-formed"
321-- MANAGE FRESH VARIABLE NAMES
324data NameState = NameState
325 { _freeNames :: [String]
326 , _numberPrimes :: Int
327 , _comparablePrimes :: Int
328 , _appendablePrimes :: Int
329 , _compAppendPrimes :: Int
330 }
333makeNameState :: Set.Set String -> NameState
334makeNameState usedNames =
335 let
336 makeName suffix =
337 map (:suffix) ['a'..'z']
339 allNames =
340 concatMap makeName ("" : map show [ (1 :: Int) .. ])
342 freeNames =
343 filter (\name -> Set.notMember name usedNames) allNames
344 in
345 NameState freeNames 0 0 0 0
348getFreshName :: (Monad m) => Maybe Super -> StateT NameState m String
349getFreshName maybeSuper =
350 case maybeSuper of
351 Nothing ->
352 do names <- State.gets _freeNames
353 State.modify (\state -> state { _freeNames = tail names })
354 return (head names)
356 Just Number ->
357 do primes <- State.gets _numberPrimes
358 State.modify (\state -> state { _numberPrimes = primes + 1 })
359 return ("number" ++ replicate primes '\'')
361 Just Comparable ->
362 do primes <- State.gets _comparablePrimes
363 State.modify (\state -> state { _comparablePrimes = primes + 1 })
364 return ("comparable" ++ replicate primes '\'')
366 Just Appendable ->
367 do primes <- State.gets _appendablePrimes
368 State.modify (\state -> state { _appendablePrimes = primes + 1 })
369 return ("appendable" ++ replicate primes '\'')
371 Just CompAppend ->
372 do primes <- State.gets _compAppendPrimes
373 State.modify (\state -> state { _compAppendPrimes = primes + 1 })
374 return ("compappend" ++ replicate primes '\'')
378-- GET ALL VARIABLE NAMES
381getVarNames :: Variable -> IO (Set.Set String)
382getVarNames var =
383 do desc <- UF.descriptor var
385 case _content desc of
386 Var _ _ (Just name) ->
387 return (Set.singleton name)
389 Var _ _ Nothing ->
390 return Set.empty
392 Structure term ->
393 getVarNamesTerm term
395 Alias _name args realVar ->
396 do let argSet = Set.fromList (map fst args)
397 realSet <- getVarNames realVar
398 sets <- mapM (getVarNames . snd) args
399 return (Set.unions (realSet : argSet : sets))
401 Atom _ ->
402 return Set.empty
404 Error ->
405 return Set.empty
408getVarNamesTerm :: Term1 Variable -> IO (Set.Set String)
409getVarNamesTerm term =
410 let go = getVarNames in
411 case term of
412 App1 a b ->
413 Set.union <$> go a <*> go b
415 Fun1 a b ->
416 Set.union <$> go a <*> go b
418 EmptyRecord1 ->
419 return Set.empty
421 Record1 fields extension ->
422 do fieldVars <- Set.unions <$> mapM go (Map.elems fields)
423 Set.union fieldVars <$> go extension