on master help sign in
Continue getting the new type-checker in order.
ca8441fEvan Czaplicki
compiler/Type/Constrain/Expression.hs+12−11
@@ -128,16 +128,16 @@ constrain env (L _ _ expr) tipe =
128 recordType = record fieldTypes (TermN EmptyRecord1)
128 recordType = record fieldTypes (TermN EmptyRecord1)
129 return $ ex (map snd pairs) (CAnd (tipe === recordType : cs))
129 return $ ex (map snd pairs) (CAnd (tipe === recordType : cs))
130 where
130 where
131− field (name, args, body) = do
131+ field (name, body) = do
132− let value = List.foldl' (\e arg -> Loc.none (Lambda (PVar arg) e)) body args
133 v <- flexibleVar -- needs an ex
132 v <- flexibleVar -- needs an ex
134− c <- constrain env value (VarN v)
133+ c <- constrain env body (VarN v)
135 return ((name, v), c)
134 return ((name, v), c)
136
135
137
136
138 Markdown _ ->
137 Markdown _ ->
139 return $ tipe === Env.get env builtin "Element"
138 return $ tipe === Env.get env builtin "Element"
140
139
140+{--
141 Let defs body ->
141 Let defs body ->
142 do c <- constrain env body tipe
142 do c <- constrain env body tipe
143 (schemes, rqs, fqs, header, c2, c1) <-
143 (schemes, rqs, fqs, header, c2, c1) <-
@@ -149,12 +149,12 @@ constrain env (L _ _ expr) tipe =
149 (c1 /\ c))
149 (c1 /\ c))
150
150
151
151
152−constrainDef env info (name, args, expr, maybeTipe) =
152+constrainDef env info (name, qs, expr, maybeTipe) =
153 let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
153 let (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info in
154 case maybeTipe of
154 case maybeTipe of
155 Just tipe ->
155 Just tipe ->
156− do flexiVars <- mapM (\_ -> flexibleVar) args
156+ do flexiVars <- mapM (\_ -> flexibleVar) qs
157− let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) args flexiVars
157+ let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
158 env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
158 env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
159 typ = error "This should be the internal representation of the user defined type."
159 typ = error "This should be the internal representation of the user defined type."
160 scheme = Scheme { rigidQuantifiers = [],
160 scheme = Scheme { rigidQuantifiers = [],
@@ -171,9 +171,9 @@ constrainDef env info (name, args, expr, maybeTipe) =
171
171
172 Nothing ->
172 Nothing ->
173 do var <- flexibleVar
173 do var <- flexibleVar
174− rigidVars <- mapM (\_ -> rigidVar) args
174+ rigidVars <- mapM (\_ -> rigidVar) qs
175 let tipe = VarN var
175 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
177 env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
177 env' = env { value = List.foldl' (\x f -> f x) (value env) inserts }
178 c <- constrain env' expr tipe
178 c <- constrain env' expr tipe
179 return ( schemes
179 return ( schemes
@@ -185,7 +185,7 @@ constrainDef env info (name, args, expr, maybeTipe) =
185
185
186--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
186--collapseDefs :: [Def t v] -> [(String, [String], LExpr t v, Maybe Type)]
187collapseDefs definitions =
187collapseDefs definitions =
188− map (\(name, (args, expr, tipe)) -> (name, args, expr, tipe)) defPairs
188+ map (\(name, (expr, tipe)) -> (name, expr, tipe)) defPairs
189 where
189 where
190 defPairs = Map.toList (go Map.empty Map.empty definitions)
190 defPairs = Map.toList (go Map.empty Map.empty definitions)
191
191
@@ -193,7 +193,8 @@ collapseDefs definitions =
193 (Map.map ($ Nothing) (Map.difference defs typs))
193 (Map.map ($ Nothing) (Map.difference defs typs))
194 go defs typs (d:ds) =
194 go defs typs (d:ds) =
195 case d of
195 case d of
196− Def name args body ->
196+ Def name body ->
197− go (Map.insert name ((,,) args body) defs) typs ds
197+ go (Map.insert name ((,) body) defs) typs ds
198 TypeAnnotation name typ ->
198 TypeAnnotation name typ ->
199 go defs (Map.insert name typ typs) ds
199 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 {
43 structure :: Maybe (Term1 Variable),
43 structure :: Maybe (Term1 Variable),
44 rank :: Int,
44 rank :: Int,
45 flex :: Flex,
45 flex :: Flex,
46− name :: Maybe TypeName
46+ name :: Maybe TypeName,
47+ mark :: Int
47}
48}
48
49
49−noRank = 0
50+noRank = -1
51+outermostRank = 0 :: Int
52+
50data Flex = Rigid | Flexible | Constant
53data Flex = Rigid | Flexible | Constant
51− deriving Show
54+ deriving (Show, Eq)
52
55
53type Variable = UF.Point Descriptor
56type Variable = UF.Point Descriptor
54
57
@@ -75,21 +78,24 @@ namedVar name = UF.fresh $ Descriptor {
75 structure = Nothing,
78 structure = Nothing,
76 rank = noRank,
79 rank = noRank,
77 flex = Constant,
80 flex = Constant,
78− name = Just name
81+ name = Just name,
82+ mark = 0
79 }
83 }
80
84
81flexibleVar = UF.fresh $ Descriptor {
85flexibleVar = UF.fresh $ Descriptor {
82 structure = Nothing,
86 structure = Nothing,
83 rank = noRank,
87 rank = noRank,
84 flex = Flexible,
88 flex = Flexible,
85− name = Nothing
89+ name = Nothing,
90+ mark = 0
86 }
91 }
87
92
88rigidVar = UF.fresh $ Descriptor {
93rigidVar = UF.fresh $ Descriptor {
89 structure = Nothing,
94 structure = Nothing,
90 rank = noRank,
95 rank = noRank,
91 flex = Rigid,
96 flex = Rigid,
92− name = Nothing
97+ name = Nothing,
98+ mark = 0
93 }
99 }
94
100
95-- ex qs constraint == exists qs. constraint
101-- 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+