git.iko.soy/elk
on cb3a2fa help sign in
elk/src/Type/Constrain/Expression.hs
594 lines 18 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Constrain.Expression where
4import Control.Applicative ((<$>))
5import Control.Arrow (second)
6import qualified Control.Monad as Monad
7import qualified Data.List as List
8import qualified Data.Map as Map
10import qualified AST.Expression.General as E
11import qualified AST.Expression.Canonical as Canonical
12import qualified AST.Literal as Lit
13import qualified AST.Pattern as P
14import qualified AST.Type as ST
15import qualified AST.Variable as V
16import qualified Reporting.Annotation as A
17import qualified Reporting.Error.Type as Error
18import qualified Reporting.Region as R
19import qualified Type.Constrain.Literal as Literal
20import qualified Type.Constrain.Pattern as Pattern
21import qualified Type.Environment as Env
22import qualified Type.Fragment as Fragment
23import Type.Type hiding (Descriptor(..))
26constrain
27 :: Env.Environment
28 -> Canonical.Expr
29 -> Type
30 -> IO TypeConstraint
31constrain env annotatedExpr@(A.A region expression) tipe =
32 let list t = Env.get env Env.types "List" <| t
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 (CEqual Error.Shader region 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
72 [ lowCon
73 , highCon
74 , CEqual Error.Range region (list n) tipe
75 ]
77 E.ExplicitList exprs ->
78 constrainList env region exprs tipe
80 E.Binop op leftExpr rightExpr ->
81 constrainBinop env region op leftExpr rightExpr tipe
83 E.Lambda pattern body ->
84 exists $ \argType ->
85 exists $ \resType ->
86 do fragment <- Pattern.constrain env pattern argType
87 bodyCon <- constrain env body resType
88 let con =
89 ex (Fragment.vars fragment)
90 (CLet [monoscheme (Fragment.typeEnv fragment)]
91 (Fragment.typeConstraint fragment /\ bodyCon)
92 )
93 return $ con /\ CEqual Error.Lambda region tipe (argType ==> resType)
95 E.App _ _ ->
96 let
97 (f:args) = E.collectApps annotatedExpr
98 in
99 constrainApp env region f args tipe
101 E.MultiIf branches finally ->
102 constrainIf env region branches finally tipe
104 E.Case expr branches ->
105 constrainCase env region expr branches tipe
107 E.Data name exprs ->
108 do vars <- Monad.forM exprs $ \_ -> variable Flexible
109 let pairs = zip exprs (map varN vars)
110 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
111 return $ ex vars (cs /\ name <? ctipe)
112 where
113 step (t,c) (e,x) =
114 do c' <- constrain env e x
115 return (x ==> t, c /\ c')
117 E.Access expr label ->
118 exists $ \t ->
119 constrain env expr (record (Map.singleton label [tipe]) t)
121 E.Remove expr label ->
122 exists $ \t ->
123 constrain env expr (record (Map.singleton label [t]) tipe)
125 E.Insert expr label value ->
126 exists $ \valueType ->
127 exists $ \recordType ->
128 do valueCon <- constrain env value valueType
129 recordCon <- constrain env expr recordType
130 let newRecordType =
131 record (Map.singleton label [valueType]) recordType
132 return $ CAnd
133 [ valueCon
134 , recordCon
135 , CEqual Error.Record region tipe newRecordType
136 ]
138 E.Modify expr fields ->
139 exists $ \t ->
140 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
141 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
142 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
144 newVars <- Monad.forM fields $ \_ -> variable Flexible
145 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
146 let cNew = CEqual Error.Record region tipe (record newFields t)
148 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
150 return $ cOld /\ ex newVars (CAnd (cNew : cs))
152 E.Record fields ->
153 do vars <- Monad.forM fields (\_ -> variable Flexible)
154 fieldCons <-
155 Monad.zipWithM
156 (constrain env)
157 (map snd fields)
158 (map varN vars)
159 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
160 let recordType = record fields' (termN EmptyRecord1)
161 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region tipe recordType])))
163 E.Let defs body ->
164 do bodyCon <- constrain env body tipe
166 (Info schemes rqs fqs headers c2 c1) <-
167 Monad.foldM
168 (constrainDef env)
169 (Info [] [] [] Map.empty CTrue CTrue)
170 (concatMap expandPattern defs)
172 let letScheme =
173 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
175 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
177 E.Port impl ->
178 case impl of
179 E.In _ _ ->
180 return CTrue
182 E.Out _ expr _ ->
183 constrain env expr tipe
185 E.Task _ expr _ ->
186 constrain env expr tipe
188 E.Crash _ ->
189 return CTrue
192-- CONSTRAIN APP
194constrainApp
195 :: Env.Environment
196 -> R.Region
197 -> Canonical.Expr
198 -> [Canonical.Expr]
199 -> Type
200 -> IO TypeConstraint
201constrainApp env region f args tipe =
202 do funcVar <- variable Flexible
203 funcCon <- constrain env f (varN funcVar)
205 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
206 argConstraints env maybeName region (length args) funcVar 1 args
208 let returnCon =
209 CEqual (Error.Function maybeName) region (varN returnVar) tipe
211 return $ ex (funcVar : vars) $
212 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
213 where
214 maybeName =
215 case f of
216 A.A _ (E.Var canonicalName) ->
217 Just canonicalName
219 _ ->
220 Nothing
223argConstraints
224 :: Env.Environment
225 -> Maybe V.Canonical
226 -> R.Region
227 -> Int
228 -> Variable
229 -> Int
230 -> [Canonical.Expr]
231 -> IO ([Variable], [TypeConstraint], [TypeConstraint], [TypeConstraint], Maybe R.Region, Variable)
232argConstraints env name region totalArgs overallVar index args =
233 case args of
234 [] ->
235 return ([], [], [], [], Nothing, overallVar)
237 expr@(A.A subregion _) : rest ->
238 do argVar <- variable Flexible
239 argCon <- constrain env expr (varN argVar)
240 argIndexVar <- variable Flexible
241 localReturnVar <- variable Flexible
243 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
244 argConstraints env name region totalArgs localReturnVar (index + 1) rest
246 let arityRegion =
247 maybe subregion (R.merge subregion) restRegion
249 let numberOfArgsCon =
250 CEqual
251 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
252 region
253 (varN argIndexVar ==> varN localReturnVar)
254 (varN overallVar)
256 let argMatchCon =
257 CEqual
258 (Error.UnexpectedArg name index subregion)
259 region
260 (varN argIndexVar)
261 (varN argVar)
263 return
264 ( argVar : argIndexVar : localReturnVar : vars
265 , argCon : argConRest
266 , numberOfArgsCon : numberOfArgsRest
267 , argMatchCon : argMatchRest
268 , Just arityRegion
269 , returnVar
270 )
275-- CONSTRAIN BINOP
277constrainBinop
278 :: Env.Environment
279 -> R.Region
280 -> V.Canonical
281 -> Canonical.Expr
282 -> Canonical.Expr
283 -> Type
284 -> IO TypeConstraint
285constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
286 do leftVar <- variable Flexible
287 rightVar <- variable Flexible
289 leftCon <- constrain env leftExpr (varN leftVar)
290 rightCon <- constrain env rightExpr (varN rightVar)
292 leftVar' <- variable Flexible
293 rightVar' <- variable Flexible
294 answerVar <- variable Flexible
296 let opType = varN leftVar' ==> varN rightVar' ==> varN answerVar
298 return $
299 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
300 [ leftCon
301 , rightCon
302 , CInstance region (V.toString op) opType
303 , CEqual (Error.BinopLeft op leftRegion) region (varN leftVar') (varN leftVar)
304 , CEqual (Error.BinopRight op rightRegion) region (varN rightVar') (varN rightVar)
305 , CEqual (Error.Binop op) region tipe (varN answerVar)
306 ]
309-- CONSTRAIN LISTS
311constrainList
312 :: Env.Environment
313 -> R.Region
314 -> [Canonical.Expr]
315 -> Type
316 -> IO TypeConstraint
317constrainList env region exprs tipe =
318 do (exprInfo, exprCons) <-
319 unzip <$> mapM elementConstraint exprs
321 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
323 return $ ex vars (CAnd (exprCons ++ cons))
324 where
325 elementConstraint expr@(A.A region' _) =
326 do var <- variable Flexible
327 con <- constrain env expr (varN var)
328 return ( (var, region'), con )
330 varToCon var =
331 CEqual Error.List region tipe (Env.get env Env.types "List" <| varN var)
334-- CONSTRAIN IF EXPRESSIONS
336constrainIf
337 :: Env.Environment
338 -> R.Region
339 -> [(Canonical.Expr, Canonical.Expr)]
340 -> Canonical.Expr
341 -> Type
342 -> IO TypeConstraint
343constrainIf env region branches finally tipe =
344 do let (conditions, branchExprs) =
345 second (++ [finally]) (unzip branches)
347 (condVars, condCons) <-
348 unzip <$> mapM constrainCondition conditions
350 (branchInfo, branchExprCons) <-
351 unzip <$> mapM constrainBranch branchExprs
353 (vars,cons) <- branchCons branchInfo
355 return $ ex (condVars ++ vars) (CAnd (condCons ++ branchExprCons ++ cons))
356 where
357 bool =
358 Env.get env Env.types "Bool"
360 constrainCondition condition@(A.A condRegion _) =
361 do condVar <- variable Flexible
362 condCon <- constrain env condition (varN condVar)
363 let boolCon = CEqual Error.IfCondition condRegion (varN condVar) bool
364 return (condVar, CAnd [ condCon, boolCon ])
366 constrainBranch expr@(A.A branchRegion _) =
367 do branchVar <- variable Flexible
368 exprCon <- constrain env expr (varN branchVar)
369 return
370 ( (branchVar, branchRegion)
371 , exprCon
372 )
374 branchCons branchInfo =
375 case branchInfo of
376 [(thenVar, _), (elseVar, _)] ->
377 return
378 ( [thenVar,elseVar]
379 , [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
380 , varToCon thenVar
381 ]
382 )
384 _ ->
385 pairCons region Error.MultiIfBranch varToCon branchInfo
387 varToCon var =
388 CEqual Error.If region (varN var) tipe
391-- CONSTRAIN CASE EXPRESSIONS
393constrainCase
394 :: Env.Environment
395 -> R.Region
396 -> Canonical.Expr
397 -> [(P.CanonicalPattern, Canonical.Expr)]
398 -> Type
399 -> IO TypeConstraint
400constrainCase env region expr branches tipe =
401 do exprVar <- variable Flexible
402 exprCon <- constrain env expr (varN exprVar)
404 (branchInfo, branchExprCons) <-
405 unzip <$> mapM (branch (varN exprVar)) branches
407 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
409 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
410 where
411 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
412 do branchVar <- variable Flexible
413 fragment <- Pattern.constrain env pattern patternType
414 branchCon <- constrain env branchExpr (varN branchVar)
415 return
416 ( (branchVar, branchRegion)
417 , CLet [Fragment.toScheme fragment] branchCon
418 )
420 varToCon var =
421 CEqual Error.Case region tipe (varN var)
424-- COLLECT PAIRS
426data Pair = Pair
427 { _index :: Int
428 , _var1 :: Variable
429 , _var2 :: Variable
430 , _region :: R.Region
431 }
434pairCons
435 :: R.Region
436 -> (Int -> R.Region -> Error.Hint)
437 -> (Variable -> TypeConstraint)
438 -> [(Variable, R.Region)]
439 -> IO ([Variable], [TypeConstraint])
440pairCons region pairHint varToCon items =
441 let
442 pairToCon (Pair index var1 var2 subregion) =
443 CEqual (pairHint index subregion) region (varN var1) (varN var2)
444 in
445 case collectPairs 2 items of
446 Nothing ->
447 do var <- variable Flexible
448 return ([var], [varToCon var])
450 Just (pairs, var) ->
451 return (map fst items, map pairToCon pairs ++ [varToCon var])
454collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
455collectPairs index items =
456 case items of
457 [] ->
458 Nothing
460 (var,_) : [] ->
461 Just ([], var)
463 (var,_) : rest@((var',region) : _) ->
464 do (pairs, summaryVar) <- collectPairs (index+1) rest
465 return (Pair index var var' region : pairs, summaryVar)
468-- EXPAND PATTERNS
470expandPattern :: Canonical.Def -> [Canonical.Def]
471expandPattern def@(Canonical.Definition lpattern expr maybeType) =
472 let (A.A patternRegion pattern) = lpattern
473 in
474 case pattern of
475 P.Var _ ->
476 [def]
478 _ ->
479 mainDef : map toDef vars
480 where
481 vars = P.boundVarList lpattern
483 combinedName = "$" ++ concat vars
485 pvar name =
486 A.A patternRegion (P.Var name)
488 localVar name =
489 A.A patternRegion (E.localVar name)
491 mainDef = Canonical.Definition (pvar combinedName) expr maybeType
493 toDef name =
494 let extract =
495 E.Case (localVar combinedName) [(lpattern, localVar name)]
496 in
497 Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
500-- CONSTRAIN DEFINITIONS
502data Info = Info
503 { iSchemes :: [TypeScheme]
504 , iRigid :: [Variable]
505 , iFlex :: [Variable]
506 , iHeaders :: Map.Map String (A.Located Type)
507 , iC2 :: TypeConstraint
508 , iC1 :: TypeConstraint
509 }
512constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
513constrainDef env info (Canonical.Definition (A.A patternRegion pattern) expr maybeTipe) =
514 let qs = [] -- should come from the def, but I'm not sure what would live there...
515 in
516 case (pattern, maybeTipe) of
517 (P.Var name, Just (A.A typeRegion tipe)) ->
518 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
520 (P.Var name, Nothing) ->
521 constrainUnannotatedDef env info qs patternRegion name expr
523 _ -> error ("problem in constrainDef with " ++ show pattern)
526constrainAnnotatedDef
527 :: Env.Environment
528 -> Info
529 -> [String]
530 -> R.Region
531 -> R.Region
532 -> String
533 -> Canonical.Expr
534 -> ST.Canonical
535 -> IO Info
536constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
537 do -- Some mistake may be happening here. Currently, qs is always [].
538 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
540 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
542 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
544 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
546 (vars, typ) <- Env.instantiateType env tipe Map.empty
548 let scheme =
549 Scheme
550 { rigidQuantifiers = []
551 , flexibleQuantifiers = flexiVars ++ vars
552 , constraint = CTrue
553 , header = Map.singleton name (A.A patternRegion typ)
554 }
556 var <- variable Flexible
557 defCon <- constrain env' expr (varN var)
558 let annCon =
559 CEqual (Error.BadTypeAnnotation name) typeRegion typ (varN var)
561 return $ info
562 { iSchemes = scheme : iSchemes info
563 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
564 }
567constrainUnannotatedDef
568 :: Env.Environment
569 -> Info
570 -> [String]
571 -> R.Region
572 -> String
573 -> Canonical.Expr
574 -> IO Info
575constrainUnannotatedDef env info qs patternRegion name expr =
576 do -- Some mistake may be happening here. Currently, qs is always [].
577 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
579 v <- variable Flexible
581 let tipe = varN v
583 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
585 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
587 con <- constrain env' expr tipe
589 return $ info
590 { iRigid = rigidVars ++ iRigid info
591 , iFlex = v : iFlex info
592 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
593 , iC2 = con /\ iC2 info
594 }