git.iko.soy/elk
on master help sign in
Continue getting the new type-checker in order.
commitca8441ff2f15339b663932d85e932a2b66a4f23e authorEvan Czaplicki <evan@Evans-MacBook-Air.local> dateSun 7 Jul 2013, 12:52 (13 years ago) parent947b82e
6 files changed+195−17
compare with master
unifiedsplit
compiler/Type/Constrain/Expression.hs+12−11 compiler/Type/Constrain/Environment.hs → compiler/Type/Environment.hs compiler/Type/Constrain/Fragment.hs → compiler/Type/Fragment.hs compiler/Type/Solve.hs+111 compiler/Type/Type.hs+12−6 compiler/Type/Unify.hs+60
compiler/Type/Constrain/Expression.hs+12−11
@@ -128,16 +128,16 @@ constrain env (L _ _ expr) tipe =
128128 recordType = record fieldTypes (TermN EmptyRecord1)
129129 return $ ex (map snd pairs) (CAnd (tipe === recordType : cs))
130130 where
131− field (name, args, body) = do
132− let value = List.foldl' (\e arg -> Loc.none (Lambda (PVar arg) e)) body args
131+ field (name, body) = do
133132 v <- flexibleVar -- needs an ex
134− c <- constrain env value (VarN v)
133+ c <- constrain env body (VarN v)
135134 return ((name, v), c)
136135
137136
138137 Markdown _ ->
139138 return $ tipe === Env.get env builtin "Element"
140139
140+{--
141141 Let defs body ->
142142 do c <- constrain env body tipe
143143 (schemes, rqs, fqs, header, c2, c1) <-
@@ -149,12 +149,12 @@ constrain env (L _ _ expr) tipe =
149149 (c1 /\ c))
150150
151151
152−constrainDef env info (name, args, expr, maybeTipe) =
152+constrainDef env info (name, qs, expr, maybeTipe) =
153153 let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
154154 case maybeTipe of
155155 Just tipe ->
156− do flexiVars <- mapM (\_ -> flexibleVar) args
157− let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args flexiVars
156+ do flexiVars <- mapM (\_ -> flexibleVar) qs
157+ let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
158158 env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
159159 typ = error "This should be the internal representation of the user defined type."
160160 scheme = Scheme { rigidQuantifiers = [],
@@ -171,9 +171,9 @@ constrainDef env info (name, args, expr, maybeTipe) =
171171
172172 Nothing ->
173173 do var <- flexibleVar
174− rigidVars <- mapM (\_ -> rigidVar) args
174+ rigidVars <- mapM (\_ -> rigidVar) qs
175175 let tipe = VarN var
176− inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args rigidVars
176+ inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
177177 env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
178178 c <- constrain env' expr tipe
179179 return ( schemes
@@ -185,7 +185,7 @@ constrainDef env info (name, args, expr, maybeTipe) =
185185
186186--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
187187collapseDefs definitions =
188− map (\(name, (args, expr, tipe)) -> (name, args, expr, tipe)) defPairs
188+ map (\(name, (expr, tipe)) -> (name, expr, tipe)) defPairs
189189 where
190190 defPairs = Map.toList (go Map.empty Map.empty definitions)
191191
@@ -193,7 +193,8 @@ collapseDefs definitions =
193193 (Map.map ($ Nothing) (Map.difference defs typs))
194194 go defs typs (d:ds) =
195195 case d of
196− Def name args body ->
197− go (Map.insert name ((,,) args body) defs) typs ds
196+ Def name body ->
197+ go (Map.insert name ((,) body) defs) typs ds
198198 TypeAnnotation name typ ->
199199 go defs (Map.insert name typ typs) ds
200+--}
compiler/Type/Constrain/Environment.hs → compiler/Type/Environment.hsrenamed

The content is the same.

compiler/Type/Constrain/Fragment.hs → compiler/Type/Fragment.hsrenamed

The content is the same.

compiler/Type/Solve.hsnew file+111
@@ -0,0 +1,111 @@
1+
2+module Type.Solve where
3+
4+import Control.Monad
5+import qualified Data.UnionFind.IO as UF
6+import qualified Data.Array.IO as Array
7+import qualified Data.Map as Map
8+import qualified Data.Maybe as Maybe
9+import Type.Type
10+import Type.Unify
11+import Type.Environment
12+
13+-- Pool
14+-- Holds a bunch of variables
15+-- The rank of each variable is less than or equal to the pool's "number"
16+-- The young pool exists to make it possible to identify these vars in constant time.
17+
18+-- inhabitants :: Pool -> [Variable]
19+
20+data Pool = Pool {
21+ maxRank :: Int,
22+ inhabitants :: [Variable]
23+}
24+
25+register = undefined
26+
27+generalize :: Pool -> Pool -> IO [Variable]
28+generalize oldPool youngPool = do
29+ let young = 0
30+ visited = 1
31+ youngRank = maxRank youngPool
32+
33+ array' <- Array.newArray (0, youngRank) []
34+ let array = array' :: Array.IOArray Int [Variable]
35+
36+ -- Insert all of the youngPool variables into the array.
37+ -- They are placed into a list at the index corresponding
38+ -- to their rank.
39+ forM (inhabitants youngPool) $ \var -> do
40+ desc <- UF.descriptor var
41+ vars <- Array.readArray array (rank desc)
42+ Array.writeArray array (rank desc) (var : vars)
43+
44+ -- get the ranks right for each entry
45+ forM [0 .. youngRank] $ \i -> do
46+ vars <- Array.readArray array i
47+ mapM (traverse young visited i) vars
48+
49+ -- do not need to work with variables that have become redundant
50+ vars <- Array.readArray array youngRank
51+ forM vars $ \var -> do
52+ isRedundant <- UF.redundant var
53+ if isRedundant then do
54+ desc <- UF.descriptor var
55+ if rank desc < youngRank
56+ then register oldPool var
57+ else let flex' = if flex desc == Flexible then Rigid else flex desc
58+ in UF.setDescriptor var (desc { rank = noRank, flex = flex' })
59+ else return ()
60+
61+ return vars
62+
63+traverse :: Int -> Int -> Int -> Variable -> IO Int
64+traverse young visited k variable =
65+ let f = traverse young visited k in
66+ do desc <- UF.descriptor variable
67+ case mark desc == young of
68+ True -> do
69+ rank' <- case structure desc of
70+ Nothing -> return k
71+ Just term -> case term of
72+ App1 a b -> max `liftM` f a `ap` f b
73+ Fun1 a b -> max `liftM` f a `ap` f b
74+ Var1 x -> f x
75+ EmptyRecord1 -> return outermostRank
76+ Record1 fields extension -> do
77+ ranks <- mapM f (concat (Map.elems fields))
78+ max (maximum ranks) `liftM` f extension
79+ UF.setDescriptor variable (desc { mark = visited, rank = rank' })
80+ return rank'
81+
82+ False -> do
83+ if mark desc /= visited then do
84+ let rank' = min k (rank desc)
85+ UF.setDescriptor variable (desc { mark = visited, rank = rank' })
86+ return rank'
87+ else return (rank desc)
88+
89+success = return []
90+
91+solve env pool constraint =
92+ case constraint of
93+ CTrue -> success
94+
95+ CEqual term1 term2 ->
96+ unify (register pool) term1 term2
97+
98+ CAnd cs -> do
99+ results <- mapM (solve env pool) cs
100+ return (concat results)
101+
102+ CLet schemes constraint' -> do
103+ env' <- foldM (\env' scheme -> (++) env' `liftM` solveScheme env pool scheme) env schemes
104+ solve env' pool constraint'
105+
106+ CInstance name term -> do
107+ let inst = instance' pool (Env.get env value name)
108+ t = chop pool term
109+ unify pool inst t
110+
111+solveScheme = undefined
compiler/Type/Type.hs+12−6
@@ -43,12 +43,15 @@ data Descriptor = Descriptor {
4343 structure :: Maybe (Term1 Variable),
4444 rank :: Int,
4545 flex :: Flex,
46− name :: Maybe TypeName
46+ name :: Maybe TypeName,
47+ mark :: Int
4748}
4849
49−noRank = 0
50+noRank = -1
51+outermostRank = 0 :: Int
52+
5053data Flex = Rigid | Flexible | Constant
51− deriving Show
54+ deriving (Show, Eq)
5255
5356type Variable = UF.Point Descriptor
5457
@@ -75,21 +78,24 @@ namedVar name = UF.fresh $ Descriptor {
7578 structure = Nothing,
7679 rank = noRank,
7780 flex = Constant,
78− name = Just name
81+ name = Just name,
82+ mark = 0
7983 }
8084
8185flexibleVar = UF.fresh $ Descriptor {
8286 structure = Nothing,
8387 rank = noRank,
8488 flex = Flexible,
85− name = Nothing
89+ name = Nothing,
90+ mark = 0
8691 }
8792
8893rigidVar = UF.fresh $ Descriptor {
8994 structure = Nothing,
9095 rank = noRank,
9196 flex = Rigid,
92− name = Nothing
97+ name = Nothing,
98+ mark = 0
9399 }
94100
95101-- ex qs constraint == exists qs. constraint
compiler/Type/Unify.hsnew file+60
@@ -0,0 +1,60 @@
1+module Type.Unify (unify) where
2+
3+import Type.Type
4+import qualified Data.UnionFind.IO as UF
5+
6+success = return []
7+
8+unify register variable1 variable2 =
9+ do equivalent <- UF.equivalent variable1 variable2
10+ if equivalent then success else do
11+ desc1 <- UF.descriptor variable1
12+ desc2 <- UF.descriptor variable2
13+ let name' = case (name desc1, name desc2) of
14+ (Just name1, Just name2)
15+ | name1 == name2 -> Just name1
16+ | flex desc1 /= Flexible -> Just name1
17+ | flex desc2 /= Flexible -> Just name2
18+ | otherwise -> Nothing
19+ (Just name1, _) -> Just name1
20+ (_, Just name2) -> Just name2
21+ _ -> Nothing
22+
23+ flex' = if flex desc1 /= Flexible then flex desc1 else
24+ if flex desc2 /= Flexible then flex desc2 else Flexible
25+
26+ rank' = min (rank desc1) (rank desc2)
27+
28+ merge1 = do
29+ UF.union variable2 variable1
30+ UF.setDescriptor variable1 (desc1 { flex = flex', name = name', rank = rank', mark = undefined })
31+
32+ merge2 = do
33+ UF.union variable1 variable2
34+ UF.setDescriptor variable2 (desc2 { flex = flex', name = name', rank = rank', mark = undefined })
35+
36+ fresh structure = -- gotta register this
37+ UF.fresh $ Descriptor {
38+ structure = structure, rank = rank', flex = flex', name = name', mark = undefined
39+ }
40+
41+ case (structure desc1, structure desc2) of
42+ (Nothing, _) | flex desc1 == Flexible -> merge2 >> success
43+ (_, Nothing) | flex desc2 == Flexible -> merge1 >> success
44+ (Just (Var1 v), _) -> unify register v variable2
45+ (_, Just (Var1 v)) -> unify register v variable1
46+ (Nothing, _) -> return ["Cannot unify rigid type variable."]
47+ (_, Nothing) -> return ["Cannot unify rigid type variable."]
48+ (Just type1, Just type2) ->
49+ case (type1,type2) of
50+ (App1 term1 term2, App1 term1' term2') ->
51+ do merge1
52+ ok1 <- unify register term1 term1'
53+ ok2 <- unify register term2 term2'
54+ return (ok1 ++ ok2)
55+ (Fun1 term1 term2, Fun1 term1' term2') ->
56+ do merge1
57+ ok1 <- unify register term1 term1'
58+ ok2 <- unify register term2 term2'
59+ return (ok1 ++ ok2)
60+