git.iko.soy/elk
on 54dfb21 help sign in
elk/src/Type/Constrain/Expression.hs
573 lines 18 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Constrain.Expression where
4import Control.Arrow (second)
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.If branches finally ->
101 constrainIf env region branches finally 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.Update expr fields ->
121 exists $ \t ->
122 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
123 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
124 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
126 newVars <- Monad.forM fields $ \_ -> variable Flexible
127 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
128 let cNew = CEqual Error.Record region tipe (record newFields t)
130 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
132 return $ cOld /\ ex newVars (CAnd (cNew : cs))
134 E.Record fields ->
135 do vars <- Monad.forM fields (\_ -> variable Flexible)
136 fieldCons <-
137 Monad.zipWithM
138 (constrain env)
139 (map snd fields)
140 (map varN vars)
141 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
142 let recordType = record fields' (termN EmptyRecord1)
143 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region tipe recordType])))
145 E.Let defs body ->
146 do bodyCon <- constrain env body tipe
148 (Info schemes rqs fqs headers c2 c1) <-
149 Monad.foldM
150 (constrainDef env)
151 (Info [] [] [] Map.empty CTrue CTrue)
152 (concatMap expandPattern defs)
154 let letScheme =
155 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
157 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
159 E.Port impl ->
160 case impl of
161 E.In _ _ ->
162 return CTrue
164 E.Out _ expr _ ->
165 constrain env expr tipe
167 E.Task _ expr _ ->
168 constrain env expr tipe
171-- CONSTRAIN APP
173constrainApp
174 :: Env.Environment
175 -> R.Region
176 -> Canonical.Expr
177 -> [Canonical.Expr]
178 -> Type
179 -> IO TypeConstraint
180constrainApp env region f args tipe =
181 do funcVar <- variable Flexible
182 funcCon <- constrain env f (varN funcVar)
184 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
185 argConstraints env maybeName region (length args) funcVar 1 args
187 let returnCon =
188 CEqual (Error.Function maybeName) region (varN returnVar) tipe
190 return $ ex (funcVar : vars) $
191 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
192 where
193 maybeName =
194 case f of
195 A.A _ (E.Var canonicalName) ->
196 Just canonicalName
198 _ ->
199 Nothing
202argConstraints
203 :: Env.Environment
204 -> Maybe V.Canonical
205 -> R.Region
206 -> Int
207 -> Variable
208 -> Int
209 -> [Canonical.Expr]
210 -> IO ([Variable], [TypeConstraint], [TypeConstraint], [TypeConstraint], Maybe R.Region, Variable)
211argConstraints env name region totalArgs overallVar index args =
212 case args of
213 [] ->
214 return ([], [], [], [], Nothing, overallVar)
216 expr@(A.A subregion _) : rest ->
217 do argVar <- variable Flexible
218 argCon <- constrain env expr (varN argVar)
219 argIndexVar <- variable Flexible
220 localReturnVar <- variable Flexible
222 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
223 argConstraints env name region totalArgs localReturnVar (index + 1) rest
225 let arityRegion =
226 maybe subregion (R.merge subregion) restRegion
228 let numberOfArgsCon =
229 CEqual
230 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
231 region
232 (varN argIndexVar ==> varN localReturnVar)
233 (varN overallVar)
235 let argMatchCon =
236 CEqual
237 (Error.UnexpectedArg name index subregion)
238 region
239 (varN argIndexVar)
240 (varN argVar)
242 return
243 ( argVar : argIndexVar : localReturnVar : vars
244 , argCon : argConRest
245 , numberOfArgsCon : numberOfArgsRest
246 , argMatchCon : argMatchRest
247 , Just arityRegion
248 , returnVar
249 )
254-- CONSTRAIN BINOP
256constrainBinop
257 :: Env.Environment
258 -> R.Region
259 -> V.Canonical
260 -> Canonical.Expr
261 -> Canonical.Expr
262 -> Type
263 -> IO TypeConstraint
264constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
265 do leftVar <- variable Flexible
266 rightVar <- variable Flexible
268 leftCon <- constrain env leftExpr (varN leftVar)
269 rightCon <- constrain env rightExpr (varN rightVar)
271 leftVar' <- variable Flexible
272 rightVar' <- variable Flexible
273 answerVar <- variable Flexible
275 let opType = varN leftVar' ==> varN rightVar' ==> varN answerVar
277 return $
278 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
279 [ leftCon
280 , rightCon
281 , CInstance region (V.toString op) opType
282 , CEqual (Error.BinopLeft op leftRegion) region (varN leftVar') (varN leftVar)
283 , CEqual (Error.BinopRight op rightRegion) region (varN rightVar') (varN rightVar)
284 , CEqual (Error.Binop op) region tipe (varN answerVar)
285 ]
288-- CONSTRAIN LISTS
290constrainList
291 :: Env.Environment
292 -> R.Region
293 -> [Canonical.Expr]
294 -> Type
295 -> IO TypeConstraint
296constrainList env region exprs tipe =
297 do (exprInfo, exprCons) <-
298 unzip <$> mapM elementConstraint exprs
300 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
302 return $ ex vars (CAnd (exprCons ++ cons))
303 where
304 elementConstraint expr@(A.A region' _) =
305 do var <- variable Flexible
306 con <- constrain env expr (varN var)
307 return ( (var, region'), con )
309 varToCon var =
310 CEqual Error.List region tipe (Env.get env Env.types "List" <| varN var)
313-- CONSTRAIN IF EXPRESSIONS
315constrainIf
316 :: Env.Environment
317 -> R.Region
318 -> [(Canonical.Expr, Canonical.Expr)]
319 -> Canonical.Expr
320 -> Type
321 -> IO TypeConstraint
322constrainIf env region branches finally tipe =
323 do let (conditions, branchExprs) =
324 second (++ [finally]) (unzip branches)
326 (condVars, condCons) <-
327 unzip <$> mapM constrainCondition conditions
329 (branchInfo, branchExprCons) <-
330 unzip <$> mapM constrainBranch branchExprs
332 (vars,cons) <- branchCons branchInfo
334 return $ ex (condVars ++ vars) (CAnd (condCons ++ branchExprCons ++ cons))
335 where
336 bool =
337 Env.get env Env.types "Bool"
339 constrainCondition condition@(A.A condRegion _) =
340 do condVar <- variable Flexible
341 condCon <- constrain env condition (varN condVar)
342 let boolCon = CEqual Error.IfCondition condRegion (varN condVar) bool
343 return (condVar, CAnd [ condCon, boolCon ])
345 constrainBranch expr@(A.A branchRegion _) =
346 do branchVar <- variable Flexible
347 exprCon <- constrain env expr (varN branchVar)
348 return
349 ( (branchVar, branchRegion)
350 , exprCon
351 )
353 branchCons branchInfo =
354 case branchInfo of
355 [(thenVar, _), (elseVar, _)] ->
356 return
357 ( [thenVar,elseVar]
358 , [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
359 , varToCon thenVar
360 ]
361 )
363 _ ->
364 pairCons region Error.MultiIfBranch varToCon branchInfo
366 varToCon var =
367 CEqual Error.If region (varN var) tipe
370-- CONSTRAIN CASE EXPRESSIONS
372constrainCase
373 :: Env.Environment
374 -> R.Region
375 -> Canonical.Expr
376 -> [(P.CanonicalPattern, Canonical.Expr)]
377 -> Type
378 -> IO TypeConstraint
379constrainCase env region expr branches tipe =
380 do exprVar <- variable Flexible
381 exprCon <- constrain env expr (varN exprVar)
383 (branchInfo, branchExprCons) <-
384 unzip <$> mapM (branch (varN exprVar)) branches
386 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
388 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
389 where
390 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
391 do branchVar <- variable Flexible
392 fragment <- Pattern.constrain env pattern patternType
393 branchCon <- constrain env branchExpr (varN branchVar)
394 return
395 ( (branchVar, branchRegion)
396 , CLet [Fragment.toScheme fragment] branchCon
397 )
399 varToCon var =
400 CEqual Error.Case region tipe (varN var)
403-- COLLECT PAIRS
405data Pair = Pair
406 { _index :: Int
407 , _var1 :: Variable
408 , _var2 :: Variable
409 , _region :: R.Region
410 }
413pairCons
414 :: R.Region
415 -> (Int -> R.Region -> Error.Hint)
416 -> (Variable -> TypeConstraint)
417 -> [(Variable, R.Region)]
418 -> IO ([Variable], [TypeConstraint])
419pairCons region pairHint varToCon items =
420 let
421 pairToCon (Pair index var1 var2 subregion) =
422 CEqual (pairHint index subregion) region (varN var1) (varN var2)
423 in
424 case collectPairs 2 items of
425 Nothing ->
426 do var <- variable Flexible
427 return ([var], [varToCon var])
429 Just (pairs, var) ->
430 return (map fst items, map pairToCon pairs ++ [varToCon var])
433collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
434collectPairs index items =
435 case items of
436 [] ->
437 Nothing
439 (var,_) : [] ->
440 Just ([], var)
442 (var,_) : rest@((var',region) : _) ->
443 do (pairs, summaryVar) <- collectPairs (index+1) rest
444 return (Pair index var var' region : pairs, summaryVar)
447-- EXPAND PATTERNS
449expandPattern :: Canonical.Def -> [Canonical.Def]
450expandPattern def@(Canonical.Definition facts lpattern expr maybeType) =
451 let (A.A patternRegion pattern) = lpattern
452 in
453 case pattern of
454 P.Var _ ->
455 [def]
457 _ ->
458 mainDef : map toDef vars
459 where
460 vars = P.boundVarList lpattern
462 combinedName = "$" ++ concat vars
464 pvar name =
465 A.A patternRegion (P.Var name)
467 localVar name =
468 A.A patternRegion (E.localVar name)
470 mainDef = Canonical.Definition facts (pvar combinedName) expr maybeType
472 toDef name =
473 let extract =
474 E.Case (localVar combinedName) [(lpattern, localVar name)]
475 in
476 Canonical.Definition facts (pvar name) (A.A patternRegion extract) Nothing
479-- CONSTRAIN DEFINITIONS
481data Info = Info
482 { iSchemes :: [TypeScheme]
483 , iRigid :: [Variable]
484 , iFlex :: [Variable]
485 , iHeaders :: Map.Map String (A.Located Type)
486 , iC2 :: TypeConstraint
487 , iC1 :: TypeConstraint
488 }
491constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
492constrainDef env info (Canonical.Definition _ (A.A patternRegion pattern) expr maybeTipe) =
493 let qs = [] -- should come from the def, but I'm not sure what would live there...
494 in
495 case (pattern, maybeTipe) of
496 (P.Var name, Just (A.A typeRegion tipe)) ->
497 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
499 (P.Var name, Nothing) ->
500 constrainUnannotatedDef env info qs patternRegion name expr
502 _ -> error ("problem in constrainDef with " ++ show pattern)
505constrainAnnotatedDef
506 :: Env.Environment
507 -> Info
508 -> [String]
509 -> R.Region
510 -> R.Region
511 -> String
512 -> Canonical.Expr
513 -> ST.Canonical
514 -> IO Info
515constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
516 do -- Some mistake may be happening here. Currently, qs is always [].
517 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
519 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
521 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
523 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
525 (vars, typ) <- Env.instantiateType env tipe Map.empty
527 let scheme =
528 Scheme
529 { rigidQuantifiers = []
530 , flexibleQuantifiers = flexiVars ++ vars
531 , constraint = CTrue
532 , header = Map.singleton name (A.A patternRegion typ)
533 }
535 var <- variable Flexible
536 defCon <- constrain env' expr (varN var)
537 let annCon =
538 CEqual (Error.BadTypeAnnotation name) typeRegion typ (varN var)
540 return $ info
541 { iSchemes = scheme : iSchemes info
542 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
543 }
546constrainUnannotatedDef
547 :: Env.Environment
548 -> Info
549 -> [String]
550 -> R.Region
551 -> String
552 -> Canonical.Expr
553 -> IO Info
554constrainUnannotatedDef env info qs patternRegion name expr =
555 do -- Some mistake may be happening here. Currently, qs is always [].
556 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
558 v <- variable Flexible
560 let tipe = varN v
562 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
564 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
566 con <- constrain env' expr tipe
568 return $ info
569 { iRigid = rigidVars ++ iRigid info
570 , iFlex = v : iFlex info
571 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
572 , iC2 = con /\ iC2 info
573 }