git.iko.soy/elk
on ff98144 help sign in
elk/src/Type/Constrain/Expression.hs
574 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.If 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.Update expr fields ->
122 exists $ \t ->
123 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
124 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
125 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
127 newVars <- Monad.forM fields $ \_ -> variable Flexible
128 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
129 let cNew = CEqual Error.Record region tipe (record newFields t)
131 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
133 return $ cOld /\ ex newVars (CAnd (cNew : cs))
135 E.Record fields ->
136 do vars <- Monad.forM fields (\_ -> variable Flexible)
137 fieldCons <-
138 Monad.zipWithM
139 (constrain env)
140 (map snd fields)
141 (map varN vars)
142 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
143 let recordType = record fields' (termN EmptyRecord1)
144 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region tipe recordType])))
146 E.Let defs body ->
147 do bodyCon <- constrain env body tipe
149 (Info schemes rqs fqs headers c2 c1) <-
150 Monad.foldM
151 (constrainDef env)
152 (Info [] [] [] Map.empty CTrue CTrue)
153 (concatMap expandPattern defs)
155 let letScheme =
156 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
158 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
160 E.Port impl ->
161 case impl of
162 E.In _ _ ->
163 return CTrue
165 E.Out _ expr _ ->
166 constrain env expr tipe
168 E.Task _ expr _ ->
169 constrain env expr tipe
172-- CONSTRAIN APP
174constrainApp
175 :: Env.Environment
176 -> R.Region
177 -> Canonical.Expr
178 -> [Canonical.Expr]
179 -> Type
180 -> IO TypeConstraint
181constrainApp env region f args tipe =
182 do funcVar <- variable Flexible
183 funcCon <- constrain env f (varN funcVar)
185 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
186 argConstraints env maybeName region (length args) funcVar 1 args
188 let returnCon =
189 CEqual (Error.Function maybeName) region (varN returnVar) tipe
191 return $ ex (funcVar : vars) $
192 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
193 where
194 maybeName =
195 case f of
196 A.A _ (E.Var canonicalName) ->
197 Just canonicalName
199 _ ->
200 Nothing
203argConstraints
204 :: Env.Environment
205 -> Maybe V.Canonical
206 -> R.Region
207 -> Int
208 -> Variable
209 -> Int
210 -> [Canonical.Expr]
211 -> IO ([Variable], [TypeConstraint], [TypeConstraint], [TypeConstraint], Maybe R.Region, Variable)
212argConstraints env name region totalArgs overallVar index args =
213 case args of
214 [] ->
215 return ([], [], [], [], Nothing, overallVar)
217 expr@(A.A subregion _) : rest ->
218 do argVar <- variable Flexible
219 argCon <- constrain env expr (varN argVar)
220 argIndexVar <- variable Flexible
221 localReturnVar <- variable Flexible
223 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
224 argConstraints env name region totalArgs localReturnVar (index + 1) rest
226 let arityRegion =
227 maybe subregion (R.merge subregion) restRegion
229 let numberOfArgsCon =
230 CEqual
231 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
232 region
233 (varN argIndexVar ==> varN localReturnVar)
234 (varN overallVar)
236 let argMatchCon =
237 CEqual
238 (Error.UnexpectedArg name index subregion)
239 region
240 (varN argIndexVar)
241 (varN argVar)
243 return
244 ( argVar : argIndexVar : localReturnVar : vars
245 , argCon : argConRest
246 , numberOfArgsCon : numberOfArgsRest
247 , argMatchCon : argMatchRest
248 , Just arityRegion
249 , returnVar
250 )
255-- CONSTRAIN BINOP
257constrainBinop
258 :: Env.Environment
259 -> R.Region
260 -> V.Canonical
261 -> Canonical.Expr
262 -> Canonical.Expr
263 -> Type
264 -> IO TypeConstraint
265constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
266 do leftVar <- variable Flexible
267 rightVar <- variable Flexible
269 leftCon <- constrain env leftExpr (varN leftVar)
270 rightCon <- constrain env rightExpr (varN rightVar)
272 leftVar' <- variable Flexible
273 rightVar' <- variable Flexible
274 answerVar <- variable Flexible
276 let opType = varN leftVar' ==> varN rightVar' ==> varN answerVar
278 return $
279 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
280 [ leftCon
281 , rightCon
282 , CInstance region (V.toString op) opType
283 , CEqual (Error.BinopLeft op leftRegion) region (varN leftVar') (varN leftVar)
284 , CEqual (Error.BinopRight op rightRegion) region (varN rightVar') (varN rightVar)
285 , CEqual (Error.Binop op) region tipe (varN answerVar)
286 ]
289-- CONSTRAIN LISTS
291constrainList
292 :: Env.Environment
293 -> R.Region
294 -> [Canonical.Expr]
295 -> Type
296 -> IO TypeConstraint
297constrainList env region exprs tipe =
298 do (exprInfo, exprCons) <-
299 unzip <$> mapM elementConstraint exprs
301 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
303 return $ ex vars (CAnd (exprCons ++ cons))
304 where
305 elementConstraint expr@(A.A region' _) =
306 do var <- variable Flexible
307 con <- constrain env expr (varN var)
308 return ( (var, region'), con )
310 varToCon var =
311 CEqual Error.List region tipe (Env.get env Env.types "List" <| varN var)
314-- CONSTRAIN IF EXPRESSIONS
316constrainIf
317 :: Env.Environment
318 -> R.Region
319 -> [(Canonical.Expr, Canonical.Expr)]
320 -> Canonical.Expr
321 -> Type
322 -> IO TypeConstraint
323constrainIf env region branches finally tipe =
324 do let (conditions, branchExprs) =
325 second (++ [finally]) (unzip branches)
327 (condVars, condCons) <-
328 unzip <$> mapM constrainCondition conditions
330 (branchInfo, branchExprCons) <-
331 unzip <$> mapM constrainBranch branchExprs
333 (vars,cons) <- branchCons branchInfo
335 return $ ex (condVars ++ vars) (CAnd (condCons ++ branchExprCons ++ cons))
336 where
337 bool =
338 Env.get env Env.types "Bool"
340 constrainCondition condition@(A.A condRegion _) =
341 do condVar <- variable Flexible
342 condCon <- constrain env condition (varN condVar)
343 let boolCon = CEqual Error.IfCondition condRegion (varN condVar) bool
344 return (condVar, CAnd [ condCon, boolCon ])
346 constrainBranch expr@(A.A branchRegion _) =
347 do branchVar <- variable Flexible
348 exprCon <- constrain env expr (varN branchVar)
349 return
350 ( (branchVar, branchRegion)
351 , exprCon
352 )
354 branchCons branchInfo =
355 case branchInfo of
356 [(thenVar, _), (elseVar, _)] ->
357 return
358 ( [thenVar,elseVar]
359 , [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
360 , varToCon thenVar
361 ]
362 )
364 _ ->
365 pairCons region Error.MultiIfBranch varToCon branchInfo
367 varToCon var =
368 CEqual Error.If region (varN var) tipe
371-- CONSTRAIN CASE EXPRESSIONS
373constrainCase
374 :: Env.Environment
375 -> R.Region
376 -> Canonical.Expr
377 -> [(P.CanonicalPattern, Canonical.Expr)]
378 -> Type
379 -> IO TypeConstraint
380constrainCase env region expr branches tipe =
381 do exprVar <- variable Flexible
382 exprCon <- constrain env expr (varN exprVar)
384 (branchInfo, branchExprCons) <-
385 unzip <$> mapM (branch (varN exprVar)) branches
387 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
389 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
390 where
391 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
392 do branchVar <- variable Flexible
393 fragment <- Pattern.constrain env pattern patternType
394 branchCon <- constrain env branchExpr (varN branchVar)
395 return
396 ( (branchVar, branchRegion)
397 , CLet [Fragment.toScheme fragment] branchCon
398 )
400 varToCon var =
401 CEqual Error.Case region tipe (varN var)
404-- COLLECT PAIRS
406data Pair = Pair
407 { _index :: Int
408 , _var1 :: Variable
409 , _var2 :: Variable
410 , _region :: R.Region
411 }
414pairCons
415 :: R.Region
416 -> (Int -> R.Region -> Error.Hint)
417 -> (Variable -> TypeConstraint)
418 -> [(Variable, R.Region)]
419 -> IO ([Variable], [TypeConstraint])
420pairCons region pairHint varToCon items =
421 let
422 pairToCon (Pair index var1 var2 subregion) =
423 CEqual (pairHint index subregion) region (varN var1) (varN var2)
424 in
425 case collectPairs 2 items of
426 Nothing ->
427 do var <- variable Flexible
428 return ([var], [varToCon var])
430 Just (pairs, var) ->
431 return (map fst items, map pairToCon pairs ++ [varToCon var])
434collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
435collectPairs index items =
436 case items of
437 [] ->
438 Nothing
440 (var,_) : [] ->
441 Just ([], var)
443 (var,_) : rest@((var',region) : _) ->
444 do (pairs, summaryVar) <- collectPairs (index+1) rest
445 return (Pair index var var' region : pairs, summaryVar)
448-- EXPAND PATTERNS
450expandPattern :: Canonical.Def -> [Canonical.Def]
451expandPattern def@(Canonical.Definition facts lpattern expr maybeType) =
452 let (A.A patternRegion pattern) = lpattern
453 in
454 case pattern of
455 P.Var _ ->
456 [def]
458 _ ->
459 mainDef : map toDef vars
460 where
461 vars = P.boundVarList lpattern
463 combinedName = "$" ++ concat vars
465 pvar name =
466 A.A patternRegion (P.Var name)
468 localVar name =
469 A.A patternRegion (E.localVar name)
471 mainDef = Canonical.Definition facts (pvar combinedName) expr maybeType
473 toDef name =
474 let extract =
475 E.Case (localVar combinedName) [(lpattern, localVar name)]
476 in
477 Canonical.Definition facts (pvar name) (A.A patternRegion extract) Nothing
480-- CONSTRAIN DEFINITIONS
482data Info = Info
483 { iSchemes :: [TypeScheme]
484 , iRigid :: [Variable]
485 , iFlex :: [Variable]
486 , iHeaders :: Map.Map String (A.Located Type)
487 , iC2 :: TypeConstraint
488 , iC1 :: TypeConstraint
489 }
492constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
493constrainDef env info (Canonical.Definition _ (A.A patternRegion pattern) expr maybeTipe) =
494 let qs = [] -- should come from the def, but I'm not sure what would live there...
495 in
496 case (pattern, maybeTipe) of
497 (P.Var name, Just (A.A typeRegion tipe)) ->
498 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
500 (P.Var name, Nothing) ->
501 constrainUnannotatedDef env info qs patternRegion name expr
503 _ -> error ("problem in constrainDef with " ++ show pattern)
506constrainAnnotatedDef
507 :: Env.Environment
508 -> Info
509 -> [String]
510 -> R.Region
511 -> R.Region
512 -> String
513 -> Canonical.Expr
514 -> ST.Canonical
515 -> IO Info
516constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
517 do -- Some mistake may be happening here. Currently, qs is always [].
518 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
520 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
522 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
524 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
526 (vars, typ) <- Env.instantiateType env tipe Map.empty
528 let scheme =
529 Scheme
530 { rigidQuantifiers = []
531 , flexibleQuantifiers = flexiVars ++ vars
532 , constraint = CTrue
533 , header = Map.singleton name (A.A patternRegion typ)
534 }
536 var <- variable Flexible
537 defCon <- constrain env' expr (varN var)
538 let annCon =
539 CEqual (Error.BadTypeAnnotation name) typeRegion typ (varN var)
541 return $ info
542 { iSchemes = scheme : iSchemes info
543 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
544 }
547constrainUnannotatedDef
548 :: Env.Environment
549 -> Info
550 -> [String]
551 -> R.Region
552 -> String
553 -> Canonical.Expr
554 -> IO Info
555constrainUnannotatedDef env info qs patternRegion name expr =
556 do -- Some mistake may be happening here. Currently, qs is always [].
557 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
559 v <- variable Flexible
561 let tipe = varN v
563 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
565 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
567 con <- constrain env' expr tipe
569 return $ info
570 { iRigid = rigidVars ++ iRigid info
571 , iFlex = v : iFlex info
572 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
573 , iC2 = con /\ iC2 info
574 }