on 4a5d921 help sign in
elk/src/Type/Constrain/Expression.hs
452 lines 14 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Constrain.Expression where
4import Control.Applicative ((<$>))
5import qualified Control.Monad as Monad
6import qualified Data.List as List
7import qualified Data.Map as Map
9import qualified AST.Expression.General as E
10import qualified AST.Expression.Canonical as Canonical
11import qualified AST.Literal as Lit
12import qualified AST.Pattern as P
13import qualified AST.Type as ST
14import qualified AST.Variable as V
15import qualified Reporting.Annotation as A
16import qualified Reporting.Error.Type as Error
17import qualified Reporting.Region as R
18import qualified Type.Constrain.Literal as Literal
19import qualified Type.Constrain.Pattern as Pattern
20import qualified Type.Environment as Env
21import qualified Type.Fragment as Fragment
22import Type.Type hiding (Descriptor(..))
25constrain
26 :: Env.Environment
27 -> Canonical.Expr
28 -> Type
29 -> IO TypeConstraint
30constrain env (A.A region expression) tipe =
31 let list t = Env.get env Env.types "List" <| t
32 (===) = CEqual Error.None region
33 (<?) = CInstance region
34 in
35 case expression of
36 E.Literal lit ->
37 Literal.constrain env region lit tipe
39 E.GLShader _uid _src gltipe ->
40 exists $ \attr ->
41 exists $ \unif ->
42 let
43 shaderTipe a u v =
44 Env.get env Env.types "WebGL.Shader" <| a <| u <| v
46 glTipe =
47 Env.get env Env.types . Lit.glTipeName
49 makeRec accessor baseRec =
50 let decls = accessor gltipe
51 in
52 if Map.size decls == 0
53 then baseRec
54 else record (Map.map (\t -> [glTipe t]) decls) baseRec
56 attribute = makeRec Lit.attribute attr
57 uniform = makeRec Lit.uniform unif
58 varying = makeRec Lit.varying (termN EmptyRecord1)
59 in
60 return (tipe === shaderTipe attribute uniform varying)
62 E.Var var ->
63 let name = V.toString var
64 in
65 return (if name == E.saveEnvName then CSaveEnv else name <? tipe)
67 E.Range lowExpr highExpr ->
68 existsNumber $ \n ->
69 do lowCon <- constrain env lowExpr n
70 highCon <- constrain env highExpr n
71 return $ CAnd [lowCon, highCon, list n === tipe]
73 E.ExplicitList exprs ->
74 constrainList env region exprs tipe
76 E.Binop op leftExpr rightExpr ->
77 exists $ \leftType ->
78 exists $ \rightType ->
79 do leftCon <- constrain env leftExpr leftType
80 rightCon <- constrain env rightExpr rightType
81 return $ CAnd
82 [ leftCon
83 , rightCon
84 , V.toString op <? (leftType ==> rightType ==> tipe)
85 ]
87 E.Lambda pattern body ->
88 exists $ \argType ->
89 exists $ \resType ->
90 do fragment <- Pattern.constrain env pattern argType
91 bodyCon <- constrain env body resType
92 let con =
93 ex (Fragment.vars fragment)
94 (CLet [monoscheme (Fragment.typeEnv fragment)]
95 (Fragment.typeConstraint fragment /\ bodyCon)
96 )
97 return $ con /\ tipe === (argType ==> resType)
99 E.App func arg ->
100 do argVar <- variable Flexible
101 resultVar <- variable Flexible
102 argCon <- constrain env arg (varN argVar)
103 funcCon <- constrain env func (varN argVar ==> varN resultVar)
104 let appCon = tipe === varN resultVar
105 return $
106 ex [argVar,resultVar] (CAnd [ argCon, funcCon, appCon ])
108 E.MultiIf branches ->
109 constrainIf env region branches tipe
111 E.Case expr branches ->
112 constrainCase env region expr branches tipe
114 E.Data name exprs ->
115 do vars <- Monad.forM exprs $ \_ -> variable Flexible
116 let pairs = zip exprs (map varN vars)
117 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
118 return $ ex vars (cs /\ name <? ctipe)
119 where
120 step (t,c) (e,x) =
121 do c' <- constrain env e x
122 return (x ==> t, c /\ c')
124 E.Access expr label ->
125 exists $ \t ->
126 constrain env expr (record (Map.singleton label [tipe]) t)
128 E.Remove expr label ->
129 exists $ \t ->
130 constrain env expr (record (Map.singleton label [t]) tipe)
132 E.Insert expr label value ->
133 exists $ \valueType ->
134 exists $ \recordType ->
135 do valueCon <- constrain env value valueType
136 recordCon <- constrain env expr recordType
137 let newRecordType =
138 record (Map.singleton label [valueType]) recordType
139 return (CAnd [valueCon, recordCon, tipe === newRecordType])
141 E.Modify expr fields ->
142 exists $ \t ->
143 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
144 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
145 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
147 newVars <- Monad.forM fields $ \_ -> variable Flexible
148 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
149 let cNew = tipe === record newFields t
151 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
153 return $ cOld /\ ex newVars (CAnd (cNew : cs))
155 E.Record fields ->
156 do vars <- Monad.forM fields (\_ -> variable Flexible)
157 fieldCons <-
158 Monad.zipWithM
159 (constrain env)
160 (map snd fields)
161 (map varN vars)
162 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
163 let recordType = record fields' (termN EmptyRecord1)
164 return (ex vars (CAnd (fieldCons ++ [tipe === recordType])))
166 E.Let defs body ->
167 do bodyCon <- constrain env body tipe
169 (Info schemes rqs fqs headers c2 c1) <-
170 Monad.foldM
171 (constrainDef env)
172 (Info [] [] [] Map.empty CTrue CTrue)
173 (concatMap expandPattern defs)
175 let letScheme = [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
177 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
179 E.Port impl ->
180 case impl of
181 E.In _ _ ->
182 return CTrue
184 E.Out _ expr _ ->
185 constrain env expr tipe
187 E.Task _ expr _ ->
188 constrain env expr tipe
191-- CONSTRAIN LISTS
193constrainList
194 :: Env.Environment
195 -> R.Region
196 -> [Canonical.Expr]
197 -> Type
198 -> IO TypeConstraint
199constrainList env region exprs tipe =
200 do (exprInfo, exprCons) <-
201 unzip <$> mapM elementConstraint exprs
203 let pairwiseCons = pairwiseConstraints 2 exprInfo
205 return $
206 ex (map fst exprInfo)
207 (CAnd (exprCons ++ pairwiseCons))
208 where
209 list t =
210 Env.get env Env.types "List" <| t
212 elementConstraint expr@(A.A region' _) =
213 do var <- variable Flexible
214 con <- constrain env expr (varN var)
215 return ( (var, region'), con )
217 pairwiseConstraints n exprInfo =
218 case exprInfo of
219 [] ->
220 []
222 (var,_) : [] ->
223 [ CEqual Error.List region tipe (list (varN var)) ]
225 (var,_) : (var',region') : rest ->
226 let
227 hint = Error.ListElement n region'
228 con = CEqual hint region (varN var) (varN var')
229 in
230 con : pairwiseConstraints (n+1) ((var', region') : rest)
233-- CONSTRAIN IF EXPRESSIONS
235constrainIf
236 :: Env.Environment
237 -> R.Region
238 -> [(Canonical.Expr, Canonical.Expr)]
239 -> Type
240 -> IO TypeConstraint
241constrainIf env region branches tipe =
242 do (branchInfo, branchExprCons) <-
243 unzip <$> mapM constrainBranch branches
245 return $
246 ex (map fst branchInfo)
247 (CAnd (branchExprCons ++ branchCons branchInfo))
248 where
249 bool = Env.get env Env.types "Bool"
251 constrainBranch (cond, expr@(A.A branchRegion _)) =
252 do branchVar <- variable Flexible
253 condCon <- constrain env cond bool
254 exprCon <- constrain env expr (varN branchVar)
255 return
256 ( (branchVar, branchRegion)
257 , condCon /\ exprCon
258 )
260 branchCons branchInfo =
261 case branchInfo of
262 [(thenVar, _), (elseVar, _)] ->
263 [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
264 , CEqual Error.If region tipe (varN thenVar)
265 ]
267 _ ->
268 buildBranchCons 2 branchInfo
270 buildBranchCons n branchInfo =
271 case branchInfo of
272 [] ->
273 []
275 (var,_) : [] ->
276 [ CEqual Error.If region tipe (varN var) ]
278 (var,_) : (var',region') : rest ->
279 let
280 hint = Error.MultiIfBranch n region'
281 con = CEqual hint region (varN var) (varN var')
282 in
283 con : buildBranchCons (n+1) ((var', region') : rest)
286-- CONSTRAIN CASE EXPRESSIONS
288constrainCase
289 :: Env.Environment
290 -> R.Region
291 -> Canonical.Expr
292 -> [(P.CanonicalPattern, Canonical.Expr)]
293 -> Type
294 -> IO TypeConstraint
295constrainCase env region expr branches tipe =
296 do exprVar <- variable Flexible
298 exprCon <- constrain env expr (varN exprVar)
300 (branchInfo, branchExprCons) <-
301 unzip <$> mapM (branch (varN exprVar)) branches
303 return $
304 ex (exprVar : map fst branchInfo)
305 (CAnd (exprCon : branchExprCons ++ branchCons 2 branchInfo))
306 where
307 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
308 do branchVar <- variable Flexible
309 fragment <- Pattern.constrain env pattern patternType
310 branchCon <- constrain env branchExpr (varN branchVar)
311 return
312 ( (branchVar, branchRegion)
313 , CLet [Fragment.toScheme fragment] branchCon
314 )
316 branchCons n branchInfo =
317 case branchInfo of
318 [] ->
319 []
321 (var,_) : [] ->
322 [ CEqual Error.Case region tipe (varN var) ]
324 (var,_) : (var',region') : rest ->
325 let
326 hint = Error.CaseBranch n region'
327 con = CEqual hint region (varN var) (varN var')
328 in
329 con : branchCons (n+1) ((var', region') : rest)
332-- EXPAND PATTERNS
334expandPattern :: Canonical.Def -> [Canonical.Def]
335expandPattern def@(Canonical.Definition lpattern expr maybeType) =
336 let (A.A patternRegion pattern) = lpattern
337 in
338 case pattern of
339 P.Var _ ->
340 [def]
342 _ ->
343 mainDef : map toDef vars
344 where
345 vars = P.boundVarList lpattern
347 combinedName = "$" ++ concat vars
349 pvar name =
350 A.A patternRegion (P.Var name)
352 localVar name =
353 A.A patternRegion (E.localVar name)
355 mainDef = Canonical.Definition (pvar combinedName) expr maybeType
357 toDef name =
358 let extract =
359 E.Case (localVar combinedName) [(lpattern, localVar name)]
360 in
361 Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
364-- CONSTRAIN DEFINITIONS
366data Info = Info
367 { iSchemes :: [TypeScheme]
368 , iRigid :: [Variable]
369 , iFlex :: [Variable]
370 , iHeaders :: Map.Map String Type
371 , iC2 :: TypeConstraint
372 , iC1 :: TypeConstraint
373 }
376constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
377constrainDef env info (Canonical.Definition (A.A _ pattern) expr maybeTipe) =
378 let qs = [] -- should come from the def, but I'm not sure what would live there...
379 in
380 case (pattern, maybeTipe) of
381 (P.Var name, Just tipe) ->
382 constrainAnnotatedDef env info qs name expr tipe
384 (P.Var name, Nothing) ->
385 constrainUnannotatedDef env info qs name expr
387 _ -> error ("problem in constrainDef with " ++ show pattern)
390constrainAnnotatedDef
391 :: Env.Environment
392 -> Info
393 -> [String]
394 -> String
395 -> Canonical.Expr
396 -> ST.Canonical
397 -> IO Info
398constrainAnnotatedDef env info qs name expr tipe =
399 do -- Some mistake may be happening here. Currently, qs is always [].
400 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
402 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
404 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
406 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
408 (vars, typ) <- Env.instantiateType env tipe Map.empty
410 let scheme =
411 Scheme
412 { rigidQuantifiers = []
413 , flexibleQuantifiers = flexiVars ++ vars
414 , constraint = CTrue
415 , header = Map.singleton name typ
416 }
418 c <- constrain env' expr typ
420 return $ info
421 { iSchemes = scheme : iSchemes info
422 , iC1 = fl rigidVars c /\ iC1 info
423 }
426constrainUnannotatedDef
427 :: Env.Environment
428 -> Info
429 -> [String]
430 -> String
431 -> Canonical.Expr
432 -> IO Info
433constrainUnannotatedDef env info qs name expr =
434 do -- Some mistake may be happening here. Currently, qs is always [].
435 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
437 v <- variable Flexible
439 let tipe = varN v
441 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
443 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
445 c <- constrain env' expr tipe
447 return $ info
448 { iRigid = rigidVars ++ iRigid info
449 , iFlex = v : iFlex info
450 , iHeaders = Map.insert name tipe (iHeaders info)
451 , iC2 = c /\ iC2 info
452 }