git.iko.soy/elk
on 727d708 help sign in
elk/compiler/Type/Constrain/Expression.hs
243 lines 9.5 kB history raw
1module Type.Constrain.Expression where
3import qualified Data.List as List
4import qualified Data.Map as Map
5import qualified Data.Set as Set
6import Control.Arrow (second)
7import Control.Applicative ((<$>),(<*>))
8import qualified Control.Monad as Monad
9import Control.Monad.State
10import Data.Traversable (traverse)
12import SourceSyntax.Location as Loc
13import SourceSyntax.Pattern (Pattern(PVar))
14import SourceSyntax.Expression
15import qualified SourceSyntax.Type as SrcT
16import Type.Type hiding (Descriptor(..))
17import Type.Fragment
18import qualified Type.Environment as Env
19import qualified Type.Constrain.Literal as Literal
20import qualified Type.Constrain.Pattern as Pattern
22{-- Testing section --}
23import SourceSyntax.PrettyPrint
24import Text.PrettyPrint as P
25import Parse.Expression
26import Parse.Helpers (iParse)
27import Type.Solve (solve)
28import qualified Type.State as TS
29import qualified Transform.SortDefinitions as SD
31test str =
32 case iParse expr "" str of
33 Left err -> error $ "Parse error at " ++ show err
34 Right expression -> do
35 env <- Env.initialEnvironment []
36 v <- var Flexible
37 let expr = SD.sortDefs expression
38 print (pretty expr)
39 constraint <- constrain env expr (VarN v)
40 print =<< extraPretty constraint
41 state <- execStateT (solve constraint) TS.initialState
42 let errors = TS.sErrors state
43 forM (Map.toList (TS.sSavedEnv state)) $ \(n,t) -> do
44 pt <- extraPretty t
45 print $ P.text n <+> P.text ":" <+> pt
46 if null errors then return () else do
47 putStrLn "\n"
48 mapM_ print =<< sequence errors
49{-- todo: remove testing code --}
51constrain :: Env.Environment -> LExpr a b -> Type -> IO TypeConstraint
52constrain env (L _ _ expr) tipe =
53 let list t = TermN (App1 (Env.get env Env.types "_List") t) in
54 case expr of
55 Literal lit -> Literal.constrain env lit tipe
57 Var name -> return (name <? tipe)
59 Range lo hi ->
60 exists $ \x -> do
61 clo <- constrain env lo x
62 chi <- constrain env hi x
63 return $ CAnd [clo, chi, list x === tipe]
65 ExplicitList exprs ->
66 exists $ \x -> do
67 cs <- mapM (\e -> constrain env e x) exprs
68 return $ CAnd (list x === tipe : cs)
70 Binop op e1 e2 ->
71 exists $ \t1 ->
72 exists $ \t2 -> do
73 c1 <- constrain env e1 t1
74 c2 <- constrain env e2 t2
75 return $ CAnd [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
77 Lambda p e ->
78 exists $ \t1 ->
79 exists $ \t2 -> do
80 fragment <- Pattern.constrain env p t1
81 c2 <- constrain env e t2
82 let c = ex (vars fragment) (CLet [monoscheme (typeEnv fragment)]
83 (typeConstraint fragment /\ c2 ))
84 return $ c /\ tipe === (t1 ==> t2)
86 App e1 e2 ->
87 exists $ \t -> do
88 c1 <- constrain env e1 (t ==> tipe)
89 c2 <- constrain env e2 t
90 return $ c1 /\ c2
92 MultiIf branches -> CAnd <$> mapM constrain' branches
93 where
94 bool = Env.get env Env.types "Bool"
95 constrain' (b,e) = do
96 cb <- constrain env b bool
97 ce <- constrain env e tipe
98 return (cb /\ ce)
100 Case exp branches ->
101 exists $ \t -> do
102 ce <- constrain env exp t
103 let branch (p,e) = do
104 fragment <- Pattern.constrain env p t
105 CLet [toScheme fragment] <$> constrain env e tipe
106 CAnd . (:) ce <$> mapM branch branches
108 Data name exprs ->
109 do pairs <- mapM pair exprs
110 (ctipe, cs) <- Monad.foldM step (tipe,CTrue) (reverse pairs)
111 return (cs /\ name <? ctipe)
112 where
113 pair e = do v <- var Flexible -- needs an ex
114 return (e, VarN v)
116 step (t,c) (e,x) = do
117 c' <- constrain env e x
118 return (x ==> t, c /\ c')
120 Access e label ->
121 exists $ \t ->
122 constrain env e (record (Map.singleton label [tipe]) t)
124 Remove e label ->
125 exists $ \t ->
126 constrain env e (record (Map.singleton label [t]) tipe)
128 Insert e label value ->
129 exists $ \tVal ->
130 exists $ \tRec -> do
131 cVal <- constrain env value tVal
132 cRec <- constrain env e tRec
133 let c = tipe === record (Map.singleton label [tVal]) tRec
134 return (CAnd [cVal, cRec, c])
136 Modify e fields ->
137 exists $ \t -> do
138 dummyFields <- Map.fromList <$> mapM dummyField fields
139 cOld <- constrain env e (record dummyFields t)
140 (fieldTypes, constraints) <- unzip <$> mapM field fields
141 let cNew = tipe === record (Map.fromList fieldTypes) t
142 return (CAnd (cOld : cNew : constraints))
143 where
144 dummyField (label, _) = do
145 v <- var Flexible -- needs an ex
146 return (label, [VarN v])
148 field (label, value) = do
149 v <- var Flexible -- needs an ex
150 c <- ex [v] <$> constrain env value (VarN v)
151 return ((label, [VarN v]), c)
153 Record fields ->
154 do (pairs, cs) <- unzip <$> mapM field fields
155 let fieldTypes = Map.fromList (map (second (\t -> [VarN t])) pairs)
156 recordType = record fieldTypes (TermN EmptyRecord1)
157 return $ ex (map snd pairs) (CAnd (tipe === recordType : cs))
158 where
159 field (name, body) = do
160 v <- var Flexible -- needs an ex
161 c <- constrain env body (VarN v)
162 return ((name, v), c)
164 Markdown _ ->
165 return $ tipe === Env.get env Env.types "Element"
167 Let defs body ->
168 do c <- case body of
169 L _ _ (Var name) | name == saveEnvName -> return CSaveEnv
170 _ -> constrain env body tipe
171 (schemes, rqs, fqs, header, c2, c1) <-
172 Monad.foldM (constrainDef env)
173 ([], [], [], Map.empty, CTrue, CTrue)
174 (collapseDefs defs)
175 return $ CLet schemes
176 (CLet [Scheme rqs fqs (CLet [monoscheme header] c2) header ]
177 (c1 /\ c))
179constrainDef env info (pattern, expr, maybeTipe) =
180 let qs = [] -- should come from the def, but I'm not sure what would live there...
181 (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
182 in
183 case (pattern, maybeTipe) of
184 (PVar name, Just tipe) ->
185 do flexiVars <- mapM (\_ -> var Flexible) qs
186 let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
187 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
188 (vars, typ) <- Env.instantiateTypeWithContext env tipe Map.empty
189 let scheme = Scheme { rigidQuantifiers = [],
190 flexibleQuantifiers = flexiVars ++ vars,
191 constraint = CTrue,
192 header = Map.singleton name typ }
193 c <- constrain env' expr typ
194 return ( scheme : schemes
195 , rigidQuantifiers
196 , flexibleQuantifiers
197 , headers
198 , c2
199 , fl rigidQuantifiers c /\ c1 )
201 (PVar name, Nothing) ->
202 do v <- var Flexible
203 rigidVars <- mapM (\_ -> var Rigid) qs -- Some mistake may be happening here.
204 -- Currently, qs is always the empty list.
205 let tipe = VarN v
206 inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
207 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
208 c <- constrain env' expr tipe
209 return ( schemes
210 , rigidVars ++ rigidQuantifiers
211 , v : flexibleQuantifiers
212 , Map.insert name tipe headers
213 , c /\ c2
214 , c1 )
217expandPattern :: (Pattern, LExpr t v, Maybe SrcT.Type)
218 -> [(Pattern, LExpr t v, Maybe SrcT.Type)]
219expandPattern triple@(pattern, lexpr, maybeType) =
220 case pattern of
221 PVar _ -> [triple]
222 _ -> (PVar x, lexpr, maybeType) : map toDef vars
223 where
224 vars = Set.toList $ SD.boundVars pattern
225 x = concat vars
226 var = Loc.none . Var
227 toDef y = (PVar y, Loc.none $ Case (var x) [(pattern, var y)], Nothing)
229collapseDefs :: [Def t v] -> [(Pattern, LExpr t v, Maybe SrcT.Type)]
230collapseDefs = concatMap expandPattern . go [] Map.empty Map.empty
231 where
232 go output defs typs [] =
233 output ++ concatMap Map.elems [
234 Map.intersectionWithKey (\k v t -> (PVar k, v, Just t)) defs typs,
235 Map.mapWithKey (\k v -> (PVar k, v, Nothing)) (Map.difference defs typs) ]
236 go output defs typs (d:ds) =
237 case d of
238 Def (PVar name) body ->
239 go output (Map.insert name body defs) typs ds
240 Def pattern body ->
241 go ((pattern, body, Nothing) : output) defs typs ds
242 TypeAnnotation name typ ->
243 go output defs (Map.insert name typ typs) ds