git.iko.soy/elk
on dca97ae help sign in
elk/src/Type/Constrain/Expression.hs
489 lines 15 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 constrainBinop env region op leftExpr rightExpr tipe
79 E.Lambda pattern body ->
80 exists $ \argType ->
81 exists $ \resType ->
82 do fragment <- Pattern.constrain env pattern argType
83 bodyCon <- constrain env body resType
84 let con =
85 ex (Fragment.vars fragment)
86 (CLet [monoscheme (Fragment.typeEnv fragment)]
87 (Fragment.typeConstraint fragment /\ bodyCon)
88 )
89 return $ con /\ tipe === (argType ==> resType)
91 E.App func@(A.A funcRegion _) arg@(A.A argRegion _) ->
92 do argVar <- variable Flexible
93 argCon <- constrain env arg (varN argVar)
95 funcVar <- variable Flexible
96 funcCon <- constrain env func (varN funcVar)
98 argVar' <- variable Flexible
99 resultVar <- variable Flexible
101 return $ ex [argVar,argVar',resultVar] $ CAnd $
102 [ argCon
103 , funcCon
104 , CEqual (Error.ExtraArgument funcRegion) region
105 (varN funcVar)
106 (varN argVar' ==> varN resultVar)
107 , CEqual (Error.BadArgument argRegion) region (varN argVar') (varN argVar)
108 , tipe === varN resultVar
109 ]
111 E.MultiIf branches ->
112 constrainIf env region branches tipe
114 E.Case expr branches ->
115 constrainCase env region expr branches tipe
117 E.Data name exprs ->
118 do vars <- Monad.forM exprs $ \_ -> variable Flexible
119 let pairs = zip exprs (map varN vars)
120 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
121 return $ ex vars (cs /\ name <? ctipe)
122 where
123 step (t,c) (e,x) =
124 do c' <- constrain env e x
125 return (x ==> t, c /\ c')
127 E.Access expr label ->
128 exists $ \t ->
129 constrain env expr (record (Map.singleton label [tipe]) t)
131 E.Remove expr label ->
132 exists $ \t ->
133 constrain env expr (record (Map.singleton label [t]) tipe)
135 E.Insert expr label value ->
136 exists $ \valueType ->
137 exists $ \recordType ->
138 do valueCon <- constrain env value valueType
139 recordCon <- constrain env expr recordType
140 let newRecordType =
141 record (Map.singleton label [valueType]) recordType
142 return (CAnd [valueCon, recordCon, tipe === newRecordType])
144 E.Modify expr fields ->
145 exists $ \t ->
146 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
147 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
148 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
150 newVars <- Monad.forM fields $ \_ -> variable Flexible
151 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
152 let cNew = tipe === record newFields t
154 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
156 return $ cOld /\ ex newVars (CAnd (cNew : cs))
158 E.Record fields ->
159 do vars <- Monad.forM fields (\_ -> variable Flexible)
160 fieldCons <-
161 Monad.zipWithM
162 (constrain env)
163 (map snd fields)
164 (map varN vars)
165 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
166 let recordType = record fields' (termN EmptyRecord1)
167 return (ex vars (CAnd (fieldCons ++ [tipe === recordType])))
169 E.Let defs body ->
170 do bodyCon <- constrain env body tipe
172 (Info schemes rqs fqs headers c2 c1) <-
173 Monad.foldM
174 (constrainDef env)
175 (Info [] [] [] Map.empty CTrue CTrue)
176 (concatMap expandPattern defs)
178 let letScheme = [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
180 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
182 E.Port impl ->
183 case impl of
184 E.In _ _ ->
185 return CTrue
187 E.Out _ expr _ ->
188 constrain env expr tipe
190 E.Task _ expr _ ->
191 constrain env expr tipe
194-- CONSTRAIN BINOP
196constrainBinop
197 :: Env.Environment
198 -> R.Region
199 -> V.Canonical
200 -> Canonical.Expr
201 -> Canonical.Expr
202 -> Type
203 -> IO TypeConstraint
204constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
205 do leftVar <- variable Flexible
206 rightVar <- variable Flexible
208 leftCon <- constrain env leftExpr (varN leftVar)
209 rightCon <- constrain env rightExpr (varN rightVar)
211 leftVar' <- variable Flexible
212 rightVar' <- variable Flexible
213 answerVar <- variable Flexible
215 let opType = varN leftVar' ==> varN rightVar' ==> varN answerVar
217 return $
218 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
219 [ leftCon
220 , rightCon
221 , CInstance region (V.toString op) opType
222 , CEqual (Error.BinopLeft op leftRegion) region (varN leftVar') (varN leftVar)
223 , CEqual (Error.BinopRight op rightRegion) region (varN rightVar') (varN rightVar)
224 , CEqual (Error.Binop op) region tipe (varN answerVar)
225 ]
228-- CONSTRAIN LISTS
230constrainList
231 :: Env.Environment
232 -> R.Region
233 -> [Canonical.Expr]
234 -> Type
235 -> IO TypeConstraint
236constrainList env region exprs tipe =
237 do (exprInfo, exprCons) <-
238 unzip <$> mapM elementConstraint exprs
240 let pairwiseCons = pairwiseConstraints 2 exprInfo
242 return $
243 ex (map fst exprInfo)
244 (CAnd (exprCons ++ pairwiseCons))
245 where
246 list t =
247 Env.get env Env.types "List" <| t
249 elementConstraint expr@(A.A region' _) =
250 do var <- variable Flexible
251 con <- constrain env expr (varN var)
252 return ( (var, region'), con )
254 pairwiseConstraints n exprInfo =
255 case exprInfo of
256 [] ->
257 []
259 (var,_) : [] ->
260 [ CEqual Error.List region tipe (list (varN var)) ]
262 (var,_) : (var',region') : rest ->
263 let
264 hint = Error.ListElement n region'
265 con = CEqual hint region (varN var) (varN var')
266 in
267 con : pairwiseConstraints (n+1) ((var', region') : rest)
270-- CONSTRAIN IF EXPRESSIONS
272constrainIf
273 :: Env.Environment
274 -> R.Region
275 -> [(Canonical.Expr, Canonical.Expr)]
276 -> Type
277 -> IO TypeConstraint
278constrainIf env region branches tipe =
279 do (branchInfo, branchExprCons) <-
280 unzip <$> mapM constrainBranch branches
282 return $
283 ex (map fst branchInfo)
284 (CAnd (branchExprCons ++ branchCons branchInfo))
285 where
286 bool = Env.get env Env.types "Bool"
288 constrainBranch (cond, expr@(A.A branchRegion _)) =
289 do branchVar <- variable Flexible
290 condCon <- constrain env cond bool
291 exprCon <- constrain env expr (varN branchVar)
292 return
293 ( (branchVar, branchRegion)
294 , condCon /\ exprCon
295 )
297 branchCons branchInfo =
298 case branchInfo of
299 [(thenVar, _), (elseVar, _)] ->
300 [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
301 , CEqual Error.If region tipe (varN thenVar)
302 ]
304 _ ->
305 buildBranchCons 2 branchInfo
307 buildBranchCons n branchInfo =
308 case branchInfo of
309 [] ->
310 []
312 (var,_) : [] ->
313 [ CEqual Error.If region tipe (varN var) ]
315 (var,_) : (var',region') : rest ->
316 let
317 hint = Error.MultiIfBranch n region'
318 con = CEqual hint region (varN var) (varN var')
319 in
320 con : buildBranchCons (n+1) ((var', region') : rest)
323-- CONSTRAIN CASE EXPRESSIONS
325constrainCase
326 :: Env.Environment
327 -> R.Region
328 -> Canonical.Expr
329 -> [(P.CanonicalPattern, Canonical.Expr)]
330 -> Type
331 -> IO TypeConstraint
332constrainCase env region expr branches tipe =
333 do exprVar <- variable Flexible
335 exprCon <- constrain env expr (varN exprVar)
337 (branchInfo, branchExprCons) <-
338 unzip <$> mapM (branch (varN exprVar)) branches
340 return $
341 ex (exprVar : map fst branchInfo)
342 (CAnd (exprCon : branchExprCons ++ branchCons 2 branchInfo))
343 where
344 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
345 do branchVar <- variable Flexible
346 fragment <- Pattern.constrain env pattern patternType
347 branchCon <- constrain env branchExpr (varN branchVar)
348 return
349 ( (branchVar, branchRegion)
350 , CLet [Fragment.toScheme fragment] branchCon
351 )
353 branchCons n branchInfo =
354 case branchInfo of
355 [] ->
356 []
358 (var,_) : [] ->
359 [ CEqual Error.Case region tipe (varN var) ]
361 (var,_) : (var',region') : rest ->
362 let
363 hint = Error.CaseBranch n region'
364 con = CEqual hint region (varN var) (varN var')
365 in
366 con : branchCons (n+1) ((var', region') : rest)
369-- EXPAND PATTERNS
371expandPattern :: Canonical.Def -> [Canonical.Def]
372expandPattern def@(Canonical.Definition lpattern expr maybeType) =
373 let (A.A patternRegion pattern) = lpattern
374 in
375 case pattern of
376 P.Var _ ->
377 [def]
379 _ ->
380 mainDef : map toDef vars
381 where
382 vars = P.boundVarList lpattern
384 combinedName = "$" ++ concat vars
386 pvar name =
387 A.A patternRegion (P.Var name)
389 localVar name =
390 A.A patternRegion (E.localVar name)
392 mainDef = Canonical.Definition (pvar combinedName) expr maybeType
394 toDef name =
395 let extract =
396 E.Case (localVar combinedName) [(lpattern, localVar name)]
397 in
398 Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
401-- CONSTRAIN DEFINITIONS
403data Info = Info
404 { iSchemes :: [TypeScheme]
405 , iRigid :: [Variable]
406 , iFlex :: [Variable]
407 , iHeaders :: Map.Map String Type
408 , iC2 :: TypeConstraint
409 , iC1 :: TypeConstraint
410 }
413constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
414constrainDef env info (Canonical.Definition (A.A _ pattern) expr maybeTipe) =
415 let qs = [] -- should come from the def, but I'm not sure what would live there...
416 in
417 case (pattern, maybeTipe) of
418 (P.Var name, Just tipe) ->
419 constrainAnnotatedDef env info qs name expr tipe
421 (P.Var name, Nothing) ->
422 constrainUnannotatedDef env info qs name expr
424 _ -> error ("problem in constrainDef with " ++ show pattern)
427constrainAnnotatedDef
428 :: Env.Environment
429 -> Info
430 -> [String]
431 -> String
432 -> Canonical.Expr
433 -> ST.Canonical
434 -> IO Info
435constrainAnnotatedDef env info qs name expr tipe =
436 do -- Some mistake may be happening here. Currently, qs is always [].
437 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
439 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
441 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
443 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
445 (vars, typ) <- Env.instantiateType env tipe Map.empty
447 let scheme =
448 Scheme
449 { rigidQuantifiers = []
450 , flexibleQuantifiers = flexiVars ++ vars
451 , constraint = CTrue
452 , header = Map.singleton name typ
453 }
455 c <- constrain env' expr typ
457 return $ info
458 { iSchemes = scheme : iSchemes info
459 , iC1 = fl rigidVars c /\ iC1 info
460 }
463constrainUnannotatedDef
464 :: Env.Environment
465 -> Info
466 -> [String]
467 -> String
468 -> Canonical.Expr
469 -> IO Info
470constrainUnannotatedDef env info qs name expr =
471 do -- Some mistake may be happening here. Currently, qs is always [].
472 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
474 v <- variable Flexible
476 let tipe = varN v
478 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
480 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
482 c <- constrain env' expr tipe
484 return $ info
485 { iRigid = rigidVars ++ iRigid info
486 , iFlex = v : iFlex info
487 , iHeaders = Map.insert name tipe (iHeaders info)
488 , iC2 = c /\ iC2 info
489 }