git.iko.soy/elk
on a67b4dc help sign in
elk/src/Type/Constrain/Expression.hs
577 lines 18 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 annotatedExpr@(A.A region expression) tipe =
31 let list t = Env.get env Env.types "List" <| t
32 (<?) = CInstance region
33 in
34 case expression of
35 E.Literal lit ->
36 Literal.constrain env region lit tipe
38 E.GLShader _uid _src gltipe ->
39 exists $ \attr ->
40 exists $ \unif ->
41 let
42 shaderTipe a u v =
43 Env.get env Env.types "WebGL.Shader" <| a <| u <| v
45 glTipe =
46 Env.get env Env.types . Lit.glTipeName
48 makeRec accessor baseRec =
49 let decls = accessor gltipe
50 in
51 if Map.size decls == 0
52 then baseRec
53 else record (Map.map (\t -> [glTipe t]) decls) baseRec
55 attribute = makeRec Lit.attribute attr
56 uniform = makeRec Lit.uniform unif
57 varying = makeRec Lit.varying (termN EmptyRecord1)
58 in
59 return (CEqual Error.Shader region tipe (shaderTipe attribute uniform varying))
61 E.Var var ->
62 let name = V.toString var
63 in
64 return (if name == E.saveEnvName then CSaveEnv else name <? tipe)
66 E.Range lowExpr highExpr ->
67 existsNumber $ \n ->
68 do lowCon <- constrain env lowExpr n
69 highCon <- constrain env highExpr n
70 return $ CAnd
71 [ lowCon
72 , highCon
73 , CEqual Error.Range region (list n) tipe
74 ]
76 E.ExplicitList exprs ->
77 constrainList env region exprs tipe
79 E.Binop op leftExpr rightExpr ->
80 constrainBinop env region op leftExpr rightExpr tipe
82 E.Lambda pattern body ->
83 exists $ \argType ->
84 exists $ \resType ->
85 do fragment <- Pattern.constrain env pattern argType
86 bodyCon <- constrain env body resType
87 let con =
88 ex (Fragment.vars fragment)
89 (CLet [monoscheme (Fragment.typeEnv fragment)]
90 (Fragment.typeConstraint fragment /\ bodyCon)
91 )
92 return $ con /\ CEqual Error.Lambda region tipe (argType ==> resType)
94 E.App _ _ ->
95 let
96 (f:args) = E.collectApps annotatedExpr
97 in
98 constrainApp env region f args tipe
100 E.MultiIf branches ->
101 constrainIf env region branches tipe
103 E.Case expr branches ->
104 constrainCase env region expr branches tipe
106 E.Data name exprs ->
107 do vars <- Monad.forM exprs $ \_ -> variable Flexible
108 let pairs = zip exprs (map varN vars)
109 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
110 return $ ex vars (cs /\ name <? ctipe)
111 where
112 step (t,c) (e,x) =
113 do c' <- constrain env e x
114 return (x ==> t, c /\ c')
116 E.Access expr label ->
117 exists $ \t ->
118 constrain env expr (record (Map.singleton label [tipe]) t)
120 E.Remove expr label ->
121 exists $ \t ->
122 constrain env expr (record (Map.singleton label [t]) tipe)
124 E.Insert expr label value ->
125 exists $ \valueType ->
126 exists $ \recordType ->
127 do valueCon <- constrain env value valueType
128 recordCon <- constrain env expr recordType
129 let newRecordType =
130 record (Map.singleton label [valueType]) recordType
131 return $ CAnd
132 [ valueCon
133 , recordCon
134 , CEqual Error.Record region tipe newRecordType
135 ]
137 E.Modify expr fields ->
138 exists $ \t ->
139 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
140 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
141 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
143 newVars <- Monad.forM fields $ \_ -> variable Flexible
144 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
145 let cNew = CEqual Error.Record region tipe (record newFields t)
147 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
149 return $ cOld /\ ex newVars (CAnd (cNew : cs))
151 E.Record fields ->
152 do vars <- Monad.forM fields (\_ -> variable Flexible)
153 fieldCons <-
154 Monad.zipWithM
155 (constrain env)
156 (map snd fields)
157 (map varN vars)
158 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
159 let recordType = record fields' (termN EmptyRecord1)
160 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region tipe recordType])))
162 E.Let defs body ->
163 do bodyCon <- constrain env body tipe
165 (Info schemes rqs fqs headers c2 c1) <-
166 Monad.foldM
167 (constrainDef env)
168 (Info [] [] [] Map.empty CTrue CTrue)
169 (concatMap expandPattern defs)
171 let letScheme =
172 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
174 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
176 E.Port impl ->
177 case impl of
178 E.In _ _ ->
179 return CTrue
181 E.Out _ expr _ ->
182 constrain env expr tipe
184 E.Task _ expr _ ->
185 constrain env expr tipe
188-- CONSTRAIN APP
190constrainApp
191 :: Env.Environment
192 -> R.Region
193 -> Canonical.Expr
194 -> [Canonical.Expr]
195 -> Type
196 -> IO TypeConstraint
197constrainApp env region f args tipe =
198 do funcVar <- variable Flexible
199 funcCon <- constrain env f (varN funcVar)
201 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
202 argConstraints env maybeName region (length args) funcVar 1 args
204 let returnCon =
205 CEqual (Error.Function maybeName) region (varN returnVar) tipe
207 return $ ex (funcVar : vars) $
208 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
209 where
210 maybeName =
211 case f of
212 A.A _ (E.Var canonicalName) ->
213 Just canonicalName
215 _ ->
216 Nothing
219argConstraints
220 :: Env.Environment
221 -> Maybe V.Canonical
222 -> R.Region
223 -> Int
224 -> Variable
225 -> Int
226 -> [Canonical.Expr]
227 -> IO ([Variable], [TypeConstraint], [TypeConstraint], [TypeConstraint], Maybe R.Region, Variable)
228argConstraints env name region totalArgs overallVar index args =
229 case args of
230 [] ->
231 return ([], [], [], [], Nothing, overallVar)
233 expr@(A.A subregion _) : rest ->
234 do argVar <- variable Flexible
235 argCon <- constrain env expr (varN argVar)
236 argIndexVar <- variable Flexible
237 localReturnVar <- variable Flexible
239 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
240 argConstraints env name region totalArgs localReturnVar (index + 1) rest
242 let arityRegion =
243 maybe subregion (R.merge subregion) restRegion
245 let numberOfArgsCon =
246 CEqual
247 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
248 region
249 (varN argIndexVar ==> varN localReturnVar)
250 (varN overallVar)
252 let argMatchCon =
253 CEqual
254 (Error.UnexpectedArg name index subregion)
255 region
256 (varN argIndexVar)
257 (varN argVar)
259 return
260 ( argVar : argIndexVar : localReturnVar : vars
261 , argCon : argConRest
262 , numberOfArgsCon : numberOfArgsRest
263 , argMatchCon : argMatchRest
264 , Just arityRegion
265 , returnVar
266 )
271-- CONSTRAIN BINOP
273constrainBinop
274 :: Env.Environment
275 -> R.Region
276 -> V.Canonical
277 -> Canonical.Expr
278 -> Canonical.Expr
279 -> Type
280 -> IO TypeConstraint
281constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
282 do leftVar <- variable Flexible
283 rightVar <- variable Flexible
285 leftCon <- constrain env leftExpr (varN leftVar)
286 rightCon <- constrain env rightExpr (varN rightVar)
288 leftVar' <- variable Flexible
289 rightVar' <- variable Flexible
290 answerVar <- variable Flexible
292 let opType = varN leftVar' ==> varN rightVar' ==> varN answerVar
294 return $
295 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
296 [ leftCon
297 , rightCon
298 , CInstance region (V.toString op) opType
299 , CEqual (Error.BinopLeft op leftRegion) region (varN leftVar') (varN leftVar)
300 , CEqual (Error.BinopRight op rightRegion) region (varN rightVar') (varN rightVar)
301 , CEqual (Error.Binop op) region tipe (varN answerVar)
302 ]
305-- CONSTRAIN LISTS
307constrainList
308 :: Env.Environment
309 -> R.Region
310 -> [Canonical.Expr]
311 -> Type
312 -> IO TypeConstraint
313constrainList env region exprs tipe =
314 do (exprInfo, exprCons) <-
315 unzip <$> mapM elementConstraint exprs
317 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
319 return $ ex vars (CAnd (exprCons ++ cons))
320 where
321 elementConstraint expr@(A.A region' _) =
322 do var <- variable Flexible
323 con <- constrain env expr (varN var)
324 return ( (var, region'), con )
326 varToCon var =
327 CEqual Error.List region tipe (Env.get env Env.types "List" <| varN var)
330-- CONSTRAIN IF EXPRESSIONS
332constrainIf
333 :: Env.Environment
334 -> R.Region
335 -> [(Canonical.Expr, Canonical.Expr)]
336 -> Type
337 -> IO TypeConstraint
338constrainIf env region branches tipe =
339 do (branchInfo, branchExprCons) <-
340 unzip <$> mapM constrainBranch branches
342 (vars,cons) <- branchCons branchInfo
344 return $ ex vars (CAnd (branchExprCons ++ cons))
345 where
346 bool = Env.get env Env.types "Bool"
348 constrainBranch (cond, expr@(A.A branchRegion _)) =
349 do branchVar <- variable Flexible
350 condCon <- constrain env cond bool
351 exprCon <- constrain env expr (varN branchVar)
352 return
353 ( (branchVar, branchRegion)
354 , condCon /\ exprCon
355 )
357 branchCons branchInfo =
358 case branchInfo of
359 [(thenVar, _), (elseVar, _)] ->
360 return
361 ( [thenVar,elseVar]
362 , [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
363 , varToCon thenVar
364 ]
365 )
367 _ ->
368 pairCons region Error.MultiIfBranch varToCon branchInfo
370 varToCon var =
371 CEqual Error.If region tipe (varN var)
374-- CONSTRAIN CASE EXPRESSIONS
376constrainCase
377 :: Env.Environment
378 -> R.Region
379 -> Canonical.Expr
380 -> [(P.CanonicalPattern, Canonical.Expr)]
381 -> Type
382 -> IO TypeConstraint
383constrainCase env region expr branches tipe =
384 do exprVar <- variable Flexible
385 exprCon <- constrain env expr (varN exprVar)
387 (branchInfo, branchExprCons) <-
388 unzip <$> mapM (branch (varN exprVar)) branches
390 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
392 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
393 where
394 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
395 do branchVar <- variable Flexible
396 fragment <- Pattern.constrain env pattern patternType
397 branchCon <- constrain env branchExpr (varN branchVar)
398 return
399 ( (branchVar, branchRegion)
400 , CLet [Fragment.toScheme fragment] branchCon
401 )
403 varToCon var =
404 CEqual Error.Case region tipe (varN var)
407-- COLLECT PAIRS
409data Pair = Pair
410 { _index :: Int
411 , _var1 :: Variable
412 , _var2 :: Variable
413 , _region :: R.Region
414 }
417pairCons
418 :: R.Region
419 -> (Int -> R.Region -> Error.Hint)
420 -> (Variable -> TypeConstraint)
421 -> [(Variable, R.Region)]
422 -> IO ([Variable], [TypeConstraint])
423pairCons region pairHint varToCon items =
424 let
425 pairToCon (Pair index var1 var2 subregion) =
426 CEqual (pairHint index subregion) region (varN var1) (varN var2)
427 in
428 case collectPairs 2 items of
429 Nothing ->
430 do var <- variable Flexible
431 return ([var], [varToCon var])
433 Just (pairs, var) ->
434 return (map fst items, map pairToCon pairs ++ [varToCon var])
437collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
438collectPairs index items =
439 case items of
440 [] ->
441 Nothing
443 (var,_) : [] ->
444 Just ([], var)
446 (var,_) : rest@((var',region) : _) ->
447 do (pairs, summaryVar) <- collectPairs (index+1) rest
448 return (Pair index var var' region : pairs, summaryVar)
451-- EXPAND PATTERNS
453expandPattern :: Canonical.Def -> [Canonical.Def]
454expandPattern def@(Canonical.Definition lpattern expr maybeType) =
455 let (A.A patternRegion pattern) = lpattern
456 in
457 case pattern of
458 P.Var _ ->
459 [def]
461 _ ->
462 mainDef : map toDef vars
463 where
464 vars = P.boundVarList lpattern
466 combinedName = "$" ++ concat vars
468 pvar name =
469 A.A patternRegion (P.Var name)
471 localVar name =
472 A.A patternRegion (E.localVar name)
474 mainDef = Canonical.Definition (pvar combinedName) expr maybeType
476 toDef name =
477 let extract =
478 E.Case (localVar combinedName) [(lpattern, localVar name)]
479 in
480 Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
483-- CONSTRAIN DEFINITIONS
485data Info = Info
486 { iSchemes :: [TypeScheme]
487 , iRigid :: [Variable]
488 , iFlex :: [Variable]
489 , iHeaders :: Map.Map String (A.Located Type)
490 , iC2 :: TypeConstraint
491 , iC1 :: TypeConstraint
492 }
495constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
496constrainDef env info (Canonical.Definition (A.A patternRegion pattern) expr maybeTipe) =
497 let qs = [] -- should come from the def, but I'm not sure what would live there...
498 in
499 case (pattern, maybeTipe) of
500 (P.Var name, Just (A.A typeRegion tipe)) ->
501 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
503 (P.Var name, Nothing) ->
504 constrainUnannotatedDef env info qs patternRegion name expr
506 _ -> error ("problem in constrainDef with " ++ show pattern)
509constrainAnnotatedDef
510 :: Env.Environment
511 -> Info
512 -> [String]
513 -> R.Region
514 -> R.Region
515 -> String
516 -> Canonical.Expr
517 -> ST.Canonical
518 -> IO Info
519constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
520 do -- Some mistake may be happening here. Currently, qs is always [].
521 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
523 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
525 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
527 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
529 (vars, typ) <- Env.instantiateType env tipe Map.empty
531 let scheme =
532 Scheme
533 { rigidQuantifiers = []
534 , flexibleQuantifiers = flexiVars ++ vars
535 , constraint = CTrue
536 , header = Map.singleton name (A.A patternRegion typ)
537 }
539 var <- variable Flexible
540 defCon <- constrain env' expr (varN var)
541 let annCon =
542 CEqual (Error.BadTypeAnnotation name) typeRegion typ (varN var)
544 return $ info
545 { iSchemes = scheme : iSchemes info
546 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
547 }
550constrainUnannotatedDef
551 :: Env.Environment
552 -> Info
553 -> [String]
554 -> R.Region
555 -> String
556 -> Canonical.Expr
557 -> IO Info
558constrainUnannotatedDef env info qs patternRegion name expr =
559 do -- Some mistake may be happening here. Currently, qs is always [].
560 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
562 v <- variable Flexible
564 let tipe = varN v
566 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
568 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
570 con <- constrain env' expr tipe
572 return $ info
573 { iRigid = rigidVars ++ iRigid info
574 , iFlex = v : iFlex info
575 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
576 , iC2 = con /\ iC2 info
577 }