git.iko.soy/elk
on master help sign in
Get the solver working on basic programs. It outputs pretty types for the
497d478Evan Czaplicki
compiler/Type/Constrain/Expression.hs+6−3
compare with master
unifiedsplit
@@ -21,8 +21,11 @@ import qualified Type.Constrain.Pattern as Pattern
21
21
22{-- Testing section --}
22{-- Testing section --}
23import SourceSyntax.PrettyPrint
23import SourceSyntax.PrettyPrint
24+import Text.PrettyPrint as P
24import Parse.Expression
25import Parse.Expression
25import Parse.Helpers (iParse)
26import Parse.Helpers (iParse)
27+import Type.Solve (solve)
28+import qualified Type.State as TS
26
29
27test str =
30test str =
28 case iParse expr "" str of
31 case iParse expr "" str of
@@ -33,8 +36,9 @@ test str =
33 constraint <- constrain env expression (VarN var)
36 constraint <- constrain env expression (VarN var)
34 prettyNames constraint
37 prettyNames constraint
35 print (pretty constraint)
38 print (pretty constraint)
36− print (pretty var)
39+ print (P.text "Solving for:" <+> pretty var)
37− return ()
40+ (env,_,_,_) <- execStateT (solve constraint) TS.initialState
41+ mapM_ (\(n,t) -> print $ P.text n <+> P.text ":" <+> pretty t) $ Map.toList env
38{-- todo: remove testing code --}
42{-- todo: remove testing code --}
39
43
40constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
44constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
@@ -152,7 +156,6 @@ constrain env (L _ _ expr) tipe =
152 v <- flexibleVar -- needs an ex
156 v <- flexibleVar -- needs an ex
153 c <- constrain env body (VarN v)
157 c <- constrain env body (VarN v)
154 return ((name, v), c)
158 return ((name, v), c)
155−
156
159
157 Markdown _ ->
160 Markdown _ ->
158 return $ tipe === Env.get env Env.builtin "Element"
161 return $ tipe === Env.get env Env.builtin "Element"
compiler/Type/Solve.hs+106−76
@@ -4,7 +4,6 @@ module Type.Solve where
4import Control.Monad
4import Control.Monad
5import Control.Monad.State
5import Control.Monad.State
6import qualified Data.UnionFind.IO as UF
6import qualified Data.UnionFind.IO as UF
7−import qualified Data.Array.IO as Array
8import qualified Data.Map as Map
7import qualified Data.Map as Map
9import qualified Data.Traversable as Traversable
8import qualified Data.Traversable as Traversable
10import qualified Data.Maybe as Maybe
9import qualified Data.Maybe as Maybe
@@ -13,73 +12,78 @@ import Type.Unify
13import qualified Type.Environment as Env
12import qualified Type.Environment as Env
14import qualified Type.State as TS
13import qualified Type.State as TS
15
14
16−register = undefined
15+
17−
16+-- | Every variable has rank less than or equal to the maxRank of the pool.
17+-- This sorts variables into the young and old pools accordingly.
18−generalize :: TS.Pool -> TS.Pool -> IO [Variable]
18+generalize :: TS.Pool -> StateT TS.SolverState IO ()
19−generalize oldPool youngPool = do
19+generalize youngPool = do
20− let young = 0
21− visited = 1
22− youngRank = TS.maxRank youngPool
20+ let youngRank = TS.maxRank youngPool
23−
21+ insert dict var = do
24− array' <- Array.newArray (0, youngRank) []
22+ desc <- liftIO $ UF.descriptor var
25− let array = array' :: Array.IOArray Int [Variable]
23+ return $ Map.insertWith (++) (rank desc) [var] dict
26−
24+
27− -- Insert all of the youngPool variables into the array.
25+ -- Sort the youngPool variables by rank.
28− -- They are placed into a list at the index corresponding
29− -- to their rank.
30− forM (TS.inhabitants youngPool) $ \var -> do
26+ rankDict <- foldM insert Map.empty (TS.inhabitants youngPool)
31− desc <- UF.descriptor var
27+
32− vars <- Array.readArray array (rank desc)
33− Array.writeArray array (rank desc) (var : vars)
34−
35− -- get the ranks right for each entry
28+ -- get the ranks right for each entry.
36− forM [0 .. youngRank] $ \i -> do
29+ -- start at low ranks so that we only have to pass
37− vars <- Array.readArray array i
30+ -- over the information once.
38− mapM (traverse young visited i) vars
31+ youngMark <- TS.uniqueMark
39−
32+ visitedMark <- TS.uniqueMark
40− -- do not need to work with variables that have become redundant
33+ Traversable.traverse (mapM (adjustRank youngMark visitedMark youngRank)) rankDict
41− vars <- Array.readArray array youngRank
34+
42− forM vars $ \var -> do
35+ -- Move variables out of the young pool if they do not have a young rank.
36+ -- We should not generalize things we cannot use.
37+ let youngVars = (Map.!) rankDict youngRank
38+
39+ registerIfNotRedundant var = do
40+ isRedundant <- liftIO $ UF.redundant var
41+ if isRedundant then return var else TS.register var
42+
43+ registerIfHigherRank var = do
43− isRedundant <- UF.redundant var
44+ isRedundant <- liftIO $ UF.redundant var
44− if isRedundant then do
45+ if isRedundant then return () else do
45− desc <- UF.descriptor var
46+ desc <- liftIO $ UF.descriptor var
46− if rank desc < youngRank
47+ if rank desc < youngRank
47− then register oldPool var
48+ then TS.register var >> return ()
48− else let flex' = if flex desc == Flexible then Rigid else flex desc
49+ else let flex' = if flex desc == Flexible then Rigid else flex desc
49− in UF.setDescriptor var (desc { rank = noRank, flex = flex' })
50+ in liftIO $ UF.setDescriptor var (desc { rank = noRank, flex = flex' })
50− else return ()
51+
51−
52+ Traversable.traverse (mapM registerIfNotRedundant) rankDict
53+ Traversable.traverse (mapM registerIfHigherRank) rankDict
54+
52− return vars
55+ return ()
53−
56+
57+
58+-- adjust the ranks of variables such that ranks never increase as you
59+-- move deeper into a variable. This mean the rank actually represents the
60+-- deepest variable in the whole type, and we can ignore things at a lower
61+-- rank than the current constraints.
54−traverse :: Int -> Int -> Int -> Variable -> IO Int
62+adjustRank :: Int -> Int -> Int -> Variable -> StateT TS.SolverState IO Int
55−traverse young visited k variable =
63+adjustRank youngMark visitedMark groupRank variable =
56− let f = traverse young visited k in
64+ let adjust = adjustRank youngMark visitedMark groupRank in
57− do desc <- UF.descriptor variable
65+ do desc <- liftIO $ UF.descriptor variable
58− case mark desc == young of
66+ case mark desc == youngMark of
59 True -> do
67 True -> do
60 rank' <- case structure desc of
68 rank' <- case structure desc of
61− Nothing -> return k
69+ Nothing -> return groupRank
62 Just term -> case term of
70 Just term -> case term of
63− App1 a b -> max `liftM` f a `ap` f b
71+ App1 a b -> max `liftM` adjust a `ap` adjust b
64− Fun1 a b -> max `liftM` f a `ap` f b
72+ Fun1 a b -> max `liftM` adjust a `ap` adjust b
65− Var1 x -> f x
73+ Var1 x -> adjust x
66 EmptyRecord1 -> return outermostRank
74 EmptyRecord1 -> return outermostRank
67 Record1 fields extension -> do
75 Record1 fields extension -> do
68− ranks <- mapM f (concat (Map.elems fields))
76+ ranks <- mapM adjust (concat (Map.elems fields))
69− max (maximum ranks) `liftM` f extension
77+ max (maximum ranks) `liftM` adjust extension
70− UF.setDescriptor variable (desc { mark = visited, rank = rank' })
78+ liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
71 return rank'
79 return rank'
72
80
73 False -> do
81 False -> do
74− if mark desc /= visited then do
82+ if mark desc == visitedMark then return (rank desc) else do
75− let rank' = min k (rank desc)
83+ let rank' = min groupRank (rank desc)
76− UF.setDescriptor variable (desc { mark = visited, rank = rank' })
84+ liftIO $ UF.setDescriptor variable (desc { mark = visitedMark, rank = rank' })
77 return rank'
85 return rank'
78− else return (rank desc)
79
86
80−addTo = undefined
81−newPool = undefined
82−introduce = undefined
83
87
84solve :: TypeConstraint -> StateT TS.SolverState IO ()
88solve :: TypeConstraint -> StateT TS.SolverState IO ()
85solve constraint =
89solve constraint =
@@ -94,41 +98,67 @@ solve constraint =
94 CAnd cs -> mapM_ solve cs
98 CAnd cs -> mapM_ solve cs
95
99
96 CLet [Scheme [] fqs constraint' _] CTrue -> do
100 CLet [Scheme [] fqs constraint' _] CTrue -> do
97− mapM_ introduce fqs
101+ mapM_ TS.introduce fqs
98 solve constraint'
102 solve constraint'
99
103
100 CLet schemes constraint' -> do
104 CLet schemes constraint' -> do
101− mapM solveScheme schemes
105+ headers <- mapM solveScheme schemes
106+ TS.modifyEnv $ \env -> Map.unions (headers ++ [env])
102 solve constraint'
107 solve constraint'
103
108
104 CInstance name term -> do
109 CInstance name term -> do
105− let instance' = undefined
110+ env <- TS.getEnv
106− inst = undefined --instance' pool (Env.get env value name)
111+ freshCopy <- TS.makeInstance ((Map.!) env name)
107 t <- TS.flatten term
112 t <- TS.flatten term
108− unify inst t
113+ unify freshCopy t
109
114
110−solveScheme :: TypeScheme -> StateT TS.SolverState IO ()
115+solveScheme :: TypeScheme -> StateT TS.SolverState IO (Map.Map String Variable)
111solveScheme scheme =
116solveScheme scheme =
112 case scheme of
117 case scheme of
113 Scheme [] [] constraint header -> do
118 Scheme [] [] constraint header -> do
114 solve constraint
119 solve constraint
115 Traversable.traverse TS.flatten header
120 Traversable.traverse TS.flatten header
116− return ()
117
121
118 Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
122 Scheme rigidQuantifiers flexibleQuantifiers constraint header -> do
119 let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
123 let quantifiers = rigidQuantifiers ++ flexibleQuantifiers
120− globalPool <- TS.getPool
124+ currentPool <- TS.getPool
121− localPool <- TS.newPool
125+
122− TS.modifyPool (\_ -> localPool)
126+ -- fill in a new pool when working on this scheme's constraints
127+ emptyPool <- TS.nextRankPool
128+ TS.switchToPool emptyPool
123 mapM TS.introduce quantifiers
129 mapM TS.introduce quantifiers
124 header' <- Traversable.traverse TS.flatten header
130 header' <- Traversable.traverse TS.flatten header
125 solve constraint
131 solve constraint
126− -- distinct variables
127− -- generalize
128− -- generic variables
129− TS.modifyPool (\_ -> globalPool)
130−
131−isGeneric var =
132− do desc <- UF.descriptor var
133− undefined
134
132
133+ allDistinct rigidQuantifiers
134+ localPool <- TS.getPool
135+ TS.switchToPool currentPool
136+ generalize localPool
137+ mapM isGeneric rigidQuantifiers
138+ return header'
139+
140+
141+-- Checks that all of the given variables belong to distinct equivalence classes.
142+-- Also checks that their structure is Nothing, so they represent a variable, not
143+-- a more complex term.
144+allDistinct :: [Variable] -> StateT TS.SolverState IO ()
145+allDistinct vars = do
146+ seen <- TS.uniqueMark
147+ let check var = do
148+ desc <- liftIO $ UF.descriptor var
149+ case structure desc of
150+ Just _ -> TS.addError "Cannot generalize something that is not a type variable."
151+ Nothing -> do
152+ if mark desc == seen
153+ then TS.addError "Duplicate variable during generalization"
154+ else return ()
155+ liftIO $ UF.setDescriptor var (desc { mark = seen })
156+ mapM_ check vars
157+
158+-- Check that a variable has rank == noRank, meaning that it can be generalized.
159+isGeneric :: Variable -> StateT TS.SolverState IO ()
160+isGeneric var = do
161+ desc <- liftIO $ UF.descriptor var
162+ if rank desc == noRank
163+ then return ()
164+ else TS.addError "Cannot generalize. Variable must have not have a rank."
compiler/Type/State.hs+110−14
@@ -1,9 +1,16 @@
1+{-# OPTIONS_GHC -XMultiWayIf #-}
1module Type.State where
2module Type.State where
2
3
3import Type.Type
4import Type.Type
5+import qualified Data.Map as Map
4import qualified Type.Environment as Env
6import qualified Type.Environment as Env
5import qualified Data.UnionFind.IO as UF
7import qualified Data.UnionFind.IO as UF
6import Control.Monad.State
8import Control.Monad.State
9+import Control.Applicative ((<$>),(<*>), Applicative)
10+import qualified Data.Traversable as Traversable
11+
12+-- todo: remove later
13+import SourceSyntax.PrettyPrint
7
14
8-- Pool
15-- Pool
9-- Holds a bunch of variables
16-- Holds a bunch of variables
@@ -13,23 +20,41 @@ import Control.Monad.State
13data Pool = Pool {
20data Pool = Pool {
14 maxRank :: Int,
21 maxRank :: Int,
15 inhabitants :: [Variable]
22 inhabitants :: [Variable]
16−}
23+} deriving Show
24+
25+emptyPool = Pool { maxRank = 0, inhabitants = [] }
17
26
18-- Keeps track of the environment, type variable pool, and a list of errors
27-- Keeps track of the environment, type variable pool, and a list of errors
19−type SolverState = (Env.Environment, Pool, [String])
28+type SolverState = (Map.Map String Variable, Pool, Int, [String])
29+
30+-- The mark must never be equal to noMark!
31+initialState = (Map.empty, emptyPool, noMark + 1, [])
20
32
21−modifyEnv f = modify $ \(env, pool, errors) -> (f env, pool, errors)
33+modifyEnv f = modify $ \(env, pool, mark, errors) -> (f env, pool, mark, errors)
22−modifyPool f = modify $ \(env, pool, errors) -> (env, f pool, errors)
34+modifyPool f = modify $ \(env, pool, mark, errors) -> (env, f pool, mark, errors)
23−addError err = modify $ \(env, pool, errors) -> (env, pool, err:errors)
35+addError err = modify $ \(env, pool, mark, errors) -> (env, pool, mark, err:errors)
36+
37+switchToPool pool = modifyPool (\_ -> pool)
24
38
25getPool :: StateT SolverState IO Pool
39getPool :: StateT SolverState IO Pool
26getPool = do
40getPool = do
27− (_, pool, _) <- get
41+ (_, pool, _, _) <- get
28 return pool
42 return pool
29
43
44+getEnv :: StateT SolverState IO (Map.Map String Variable)
45+getEnv = do
46+ (env, _, _, _) <- get
47+ return env
48+
49+uniqueMark :: StateT SolverState IO Int
50+uniqueMark = do
51+ (env, pool, mark, errs) <- get
52+ put (env, pool, mark+1, errs)
53+ return mark
54+
30−newPool :: StateT SolverState IO Pool
55+nextRankPool :: StateT SolverState IO Pool
31−newPool = do
56+nextRankPool = do
32− (_, pool, _) <- get
57+ pool <- getPool
33 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
58 return $ Pool { maxRank = maxRank pool + 1, inhabitants = [] }
34
59
35register :: Variable -> StateT SolverState IO Variable
60register :: Variable -> StateT SolverState IO Variable
@@ -39,7 +64,7 @@ register variable = do
39
64
40introduce :: Variable -> StateT SolverState IO Variable
65introduce :: Variable -> StateT SolverState IO Variable
41introduce variable = do
66introduce variable = do
42− (_, pool, _) <- get
67+ pool <- getPool
43 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
68 liftIO $ UF.modifyDescriptor variable (\desc -> desc { rank = maxRank pool })
44 register variable
69 register variable
45
70
@@ -48,13 +73,84 @@ flatten term =
48 case term of
73 case term of
49 VarN v -> return v
74 VarN v -> return v
50 TermN t -> do
75 TermN t -> do
51− flatStructure <- undefined -- chop t
76+ flatStructure <- traverseTerm flatten t
52− (_, pool, _) <- get
77+ pool <- getPool
53 var <- liftIO . UF.fresh $ Descriptor {
78 var <- liftIO . UF.fresh $ Descriptor {
54 structure = Just flatStructure,
79 structure = Just flatStructure,
55 rank = maxRank pool,
80 rank = maxRank pool,
56 flex = Flexible,
81 flex = Flexible,
57 name = Nothing,
82 name = Nothing,
83+ copy = Nothing,
58− mark = 0
84+ mark = noMark
59 }
85 }
60− register var
86+ register var
87+
88+makeInstance :: Variable -> StateT SolverState IO Variable
89+makeInstance var = do
90+ alreadyCopied <- uniqueMark
91+ freshVar <- makeCopy alreadyCopied var
92+ restore alreadyCopied var
93+ return freshVar
94+
95+makeCopy :: Int -> Variable -> StateT SolverState IO Variable
96+makeCopy alreadyCopied variable = do
97+ desc <- liftIO $ UF.descriptor variable
98+ if | mark desc == alreadyCopied ->
99+ case copy desc of
100+ Just v -> return v
101+ Nothing -> error "This should be impossible."
102+
103+ | mark desc /= noRank || flex desc == Constant ->
104+ return variable
105+
106+ | otherwise -> do
107+ pool <- getPool
108+ newVar <- liftIO $ UF.fresh $ Descriptor {
109+ structure = Nothing,
110+ rank = maxRank pool,
111+ mark = noMark,
112+ flex = Flexible,
113+ copy = Nothing,
114+ name = case flex desc of
115+ Rigid -> Nothing
116+ _ -> name desc
117+ }
118+
119+ register newVar
120+
121+ -- Link the original variable to the new variable
122+ -- Need to do this before recursively copying to
123+ -- avoid looping on cyclic terms.
124+ liftIO $ UF.modifyDescriptor variable $ \desc ->
125+ desc { mark = alreadyCopied, copy = Just newVar }
126+
127+ case structure desc of
128+ Nothing -> return newVar
129+ Just term -> do
130+ newTerm <- traverseTerm (makeCopy alreadyCopied) term
131+ liftIO $ UF.modifyDescriptor newVar $ \desc ->
132+ desc { structure = Just newTerm }
133+ return newVar
134+
135+restore :: Int -> Variable -> StateT SolverState IO Variable
136+restore alreadyCopied variable = do
137+ desc <- liftIO $ UF.descriptor variable
138+ if mark desc /= alreadyCopied then return variable else do
139+ restoredStructure <-
140+ case structure desc of
141+ Nothing -> return Nothing
142+ Just term -> Just <$> traverseTerm (restore alreadyCopied) term
143+ liftIO $ UF.modifyDescriptor variable $ \desc ->
144+ desc { mark = noMark, rank = noRank, structure = restoredStructure }
145+ return variable
146+
147+traverseTerm :: (Monad f, Applicative f) => (a -> f b) -> Term1 a -> f (Term1 b)
148+traverseTerm f term =
149+ case term of
150+ App1 a b -> App1 <$> f a <*> f b
151+ Fun1 a b -> Fun1 <$> f a <*> f b
152+ Var1 x -> Var1 <$> f x
153+ EmptyRecord1 -> return EmptyRecord1
154+ Record1 fields ext ->
155+ Record1 <$> Traversable.traverse (mapM f) fields <*> f ext
156+
compiler/Type/Type.hs+10−3
@@ -50,12 +50,16 @@ data Descriptor = Descriptor {
50 rank :: Int,
50 rank :: Int,
51 flex :: Flex,
51 flex :: Flex,
52 name :: Maybe TypeName,
52 name :: Maybe TypeName,
53+ copy :: Maybe Variable,
53 mark :: Int
54 mark :: Int
54} deriving Show
55} deriving Show
55
56
56noRank = -1
57noRank = -1
57outermostRank = 0 :: Int
58outermostRank = 0 :: Int
58
59
60+noMark = 0
61+initialMark = 1
62+
59data Flex = Rigid | Flexible | Constant
63data Flex = Rigid | Flexible | Constant
60 deriving (Show, Eq)
64 deriving (Show, Eq)
61
65
@@ -85,7 +89,8 @@ namedVar name = UF.fresh $ Descriptor {
85 rank = noRank,
89 rank = noRank,
86 flex = Constant,
90 flex = Constant,
87 name = Just name,
91 name = Just name,
92+ copy = Nothing,
88− mark = 0
93+ mark = noMark
89 }
94 }
90
95
91flexibleVar = UF.fresh $ Descriptor {
96flexibleVar = UF.fresh $ Descriptor {
@@ -93,7 +98,8 @@ flexibleVar = UF.fresh $ Descriptor {
93 rank = noRank,
98 rank = noRank,
94 flex = Flexible,
99 flex = Flexible,
95 name = Nothing,
100 name = Nothing,
101+ copy = Nothing,
96− mark = 0
102+ mark = noMark
97 }
103 }
98
104
99rigidVar = UF.fresh $ Descriptor {
105rigidVar = UF.fresh $ Descriptor {
@@ -101,7 +107,8 @@ rigidVar = UF.fresh $ Descriptor {
101 rank = noRank,
107 rank = noRank,
102 flex = Rigid,
108 flex = Rigid,
103 name = Nothing,
109 name = Nothing,
110+ copy = Nothing,
104− mark = 0
111+ mark = noMark
105 }
112 }
106
113
107-- ex qs constraint == exists qs. constraint
114-- ex qs constraint == exists qs. constraint
compiler/Type/Unify.hs+5−3
@@ -37,17 +37,19 @@ actuallyUnify variable1 variable2 = do
37 merge1 :: StateT TS.SolverState IO ()
37 merge1 :: StateT TS.SolverState IO ()
38 merge1 = liftIO $ do
38 merge1 = liftIO $ do
39 UF.union variable2 variable1
39 UF.union variable2 variable1
40− UF.setDescriptor variable1 (desc1 { flex = flex', name = name', rank = rank', mark = undefined })
40+ UF.setDescriptor variable1 (desc1 {
41+ flex = flex', name = name', rank = rank', copy = Nothing, mark = noMark })
41
42
42 merge2 :: StateT TS.SolverState IO ()
43 merge2 :: StateT TS.SolverState IO ()
43 merge2 = liftIO $ do
44 merge2 = liftIO $ do
44 UF.union variable1 variable2
45 UF.union variable1 variable2
45− UF.setDescriptor variable2 (desc2 { flex = flex', name = name', rank = rank', mark = undefined })
46+ UF.setDescriptor variable2 (desc2 {
47+ flex = flex', name = name', rank = rank', copy = Nothing, mark = noMark })
46
48
47 fresh :: Maybe (Term1 Variable) -> StateT TS.SolverState IO Variable
49 fresh :: Maybe (Term1 Variable) -> StateT TS.SolverState IO Variable
48 fresh structure = do
50 fresh structure = do
49 var <- liftIO . UF.fresh $ Descriptor {
51 var <- liftIO . UF.fresh $ Descriptor {
50− structure = structure, rank = rank', flex = flex', name = name', mark = undefined
52+ structure = structure, rank = rank', flex = flex', name = name', copy = Nothing, mark = noMark
51 }
53 }
52 TS.register var
54 TS.register var
53
55