on 267f708 help sign in
elk/src/Type/Constrain/Expression.hs
584 lines 17 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.Map as Map
8import qualified AST.Expression.General as E
9import qualified AST.Expression.Canonical as Canonical
10import qualified AST.Literal as Lit
11import qualified AST.Pattern as P
12import qualified AST.Type as ST
13import qualified AST.Variable as V
14import qualified Reporting.Annotation as A
15import qualified Reporting.Error.Type as Error
16import qualified Reporting.Region as R
17import qualified Type.Constrain.Effects as Effects
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(..))
26constrain
27 :: Env.Environment
28 -> Canonical.Expr
29 -> Type
30 -> IO TypeConstraint
31constrain env annotatedExpr@(A.A region expression) tipe =
32 case expression of
33 E.Literal lit ->
34 Literal.constrain env region lit tipe
36 E.Cmd _ ->
37 return CTrue
39 E.Sub _ ->
40 return CTrue
42 E.OutgoingPort _ _ ->
43 return CTrue
45 E.IncomingPort _ _ ->
46 return CTrue
48 E.Program _ _ ->
49 error "DANGER - Program AST nodes should not be in type inference."
51 E.SaveEnv moduleName effects ->
52 Effects.constrain env moduleName effects
54 E.GLShader _uid _src gltipe ->
55 exists $ \attr ->
56 exists $ \unif ->
57 let
58 shaderTipe a u v =
59 Env.getType env "WebGL.Shader" <| a <| u <| v
61 glToType glTipe =
62 Env.getType env (Lit.glTipeName glTipe)
64 makeRec accessor baseRec =
65 let decls = accessor gltipe
66 in
67 if Map.size decls == 0 then
68 baseRec
69 else
70 record (Map.map glToType decls) baseRec
72 attribute = makeRec Lit.attribute attr
73 uniform = makeRec Lit.uniform unif
74 varying = makeRec Lit.varying (TermN EmptyRecord1)
75 in
76 return (CEqual Error.Shader region (shaderTipe attribute uniform varying) tipe)
78 E.Var var ->
79 return (CInstance region (V.toString var) tipe)
81 E.ExplicitList exprs ->
82 constrainList env region exprs tipe
84 E.Binop op leftExpr rightExpr ->
85 constrainBinop env region op leftExpr rightExpr tipe
87 E.Lambda pattern body ->
88 exists $ \argType ->
89 exists $ \resType ->
90 do fragment <- Pattern.constrain env pattern argType
91 bodyCon <- constrain env body resType
92 let con =
93 ex (Fragment.vars fragment)
94 (CLet [monoscheme (Fragment.typeEnv fragment)]
95 (Fragment.typeConstraint fragment /\ bodyCon)
96 )
97 return $ con /\ CEqual Error.Lambda region (argType ==> resType) tipe
99 E.App _ _ ->
100 let
101 (f:args) = E.collectApps annotatedExpr
102 in
103 constrainApp env region f args tipe
105 E.If branches finally ->
106 constrainIf env region branches finally tipe
108 E.Case expr branches ->
109 constrainCase env region expr branches tipe
111 E.Data name exprs ->
112 do vars <- Monad.forM exprs $ \_ -> mkVar Nothing
113 let pairs = zip exprs (map VarN vars)
114 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
115 return $ ex vars (cs /\ CInstance region name ctipe)
116 where
117 step (t,c) (e,x) =
118 do c' <- constrain env e x
119 return (x ==> t, c /\ c')
121 E.Access expr label ->
122 exists $ \t ->
123 constrain env expr (record (Map.singleton label tipe) t)
125 E.Update expr fields ->
126 exists $ \t ->
127 do oldVars <- mapM (\_ -> mkVar Nothing) fields
128 let oldFields = Map.fromList (zip (map fst fields) (map VarN oldVars))
129 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
131 newVars <- mapM (\_ -> mkVar Nothing) fields
132 let newFields = Map.fromList (zip (map fst fields) (map VarN newVars))
133 let cNew = CEqual Error.Record region (record newFields t) tipe
135 cs <- Monad.zipWithM (constrain env) (map snd fields) (map VarN newVars)
137 return $ cOld /\ ex newVars (CAnd (cNew : cs))
139 E.Record fields ->
140 do vars <- Monad.forM fields (\_ -> mkVar Nothing)
141 fieldCons <-
142 Monad.zipWithM
143 (constrain env)
144 (map snd fields)
145 (map VarN vars)
146 let fields' = Map.fromList (zip (map fst fields) (map VarN vars))
147 let recordType = record fields' (TermN EmptyRecord1)
148 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region recordType tipe])))
150 E.Let defs body ->
151 do bodyCon <- constrain env body tipe
153 (Info schemes rqs fqs headers c2 c1) <-
154 Monad.foldM
155 (constrainDef env)
156 (Info [] [] [] Map.empty CTrue CTrue)
157 (concatMap expandPattern defs)
159 let letScheme =
160 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
162 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
166-- CONSTRAIN APP
169constrainApp
170 :: Env.Environment
171 -> R.Region
172 -> Canonical.Expr
173 -> [Canonical.Expr]
174 -> Type
175 -> IO TypeConstraint
176constrainApp env region f args tipe =
177 do funcVar <- mkVar Nothing
178 funcCon <- constrain env f (VarN funcVar)
180 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
181 argConstraints env maybeName region (length args) funcVar 1 args
183 let returnCon =
184 CEqual (Error.Function maybeName) region (VarN returnVar) tipe
186 return $ ex (funcVar : vars) $
187 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
188 where
189 maybeName =
190 case f of
191 A.A _ (E.Var canonicalName) ->
192 Just canonicalName
194 _ ->
195 Nothing
198argConstraints
199 :: Env.Environment
200 -> Maybe V.Canonical
201 -> R.Region
202 -> Int
203 -> Variable
204 -> Int
205 -> [Canonical.Expr]
206 -> IO ([Variable], [TypeConstraint], [TypeConstraint], [TypeConstraint], Maybe R.Region, Variable)
207argConstraints env name region totalArgs overallVar index args =
208 case args of
209 [] ->
210 return ([], [], [], [], Nothing, overallVar)
212 expr@(A.A subregion _) : rest ->
213 do argVar <- mkVar Nothing
214 argCon <- constrain env expr (VarN argVar)
215 argIndexVar <- mkVar Nothing
216 localReturnVar <- mkVar Nothing
218 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
219 argConstraints env name region totalArgs localReturnVar (index + 1) rest
221 let arityRegion =
222 maybe subregion (R.merge subregion) restRegion
224 let numberOfArgsCon =
225 CEqual
226 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
227 region
228 (VarN argIndexVar ==> VarN localReturnVar)
229 (VarN overallVar)
231 let argMatchCon =
232 CEqual
233 (Error.UnexpectedArg name index totalArgs subregion)
234 region
235 (VarN argIndexVar)
236 (VarN argVar)
238 return
239 ( argVar : argIndexVar : localReturnVar : vars
240 , argCon : argConRest
241 , numberOfArgsCon : numberOfArgsRest
242 , argMatchCon : argMatchRest
243 , Just arityRegion
244 , returnVar
245 )
249-- CONSTRAIN BINOP
252constrainBinop
253 :: Env.Environment
254 -> R.Region
255 -> V.Canonical
256 -> Canonical.Expr
257 -> Canonical.Expr
258 -> Type
259 -> IO TypeConstraint
260constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
261 do leftVar <- mkVar Nothing
262 rightVar <- mkVar Nothing
264 leftCon <- constrain env leftExpr (VarN leftVar)
265 rightCon <- constrain env rightExpr (VarN rightVar)
267 leftVar' <- mkVar Nothing
268 rightVar' <- mkVar Nothing
269 answerVar <- mkVar Nothing
271 let opType = VarN leftVar' ==> VarN rightVar' ==> VarN answerVar
273 return $
274 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
275 [ leftCon
276 , rightCon
277 , CInstance region (V.toString op) opType
278 , CEqual (Error.BinopLeft op leftRegion) region (VarN leftVar') (VarN leftVar)
279 , CEqual (Error.BinopRight op rightRegion) region (VarN rightVar') (VarN rightVar)
280 , CEqual (Error.Binop op) region (VarN answerVar) tipe
281 ]
285-- CONSTRAIN LISTS
288constrainList
289 :: Env.Environment
290 -> R.Region
291 -> [Canonical.Expr]
292 -> Type
293 -> IO TypeConstraint
294constrainList env region exprs tipe =
295 do (exprInfo, exprCons) <-
296 unzip <$> mapM elementConstraint exprs
298 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
300 return $ ex vars (CAnd (exprCons ++ cons))
301 where
302 elementConstraint expr@(A.A region' _) =
303 do var <- mkVar Nothing
304 con <- constrain env expr (VarN var)
305 return ( (var, region'), con )
307 varToCon var =
308 CEqual Error.List region (Env.getType env "List" <| VarN var) tipe
312-- 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.getType env "Bool"
339 constrainCondition condition@(A.A condRegion _) =
340 do condVar <- mkVar Nothing
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 <- mkVar Nothing
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
371-- CONSTRAIN CASE EXPRESSIONS
374constrainCase
375 :: Env.Environment
376 -> R.Region
377 -> Canonical.Expr
378 -> [(P.Canonical, Canonical.Expr)]
379 -> Type
380 -> IO TypeConstraint
381constrainCase env region expr branches tipe =
382 do exprVar <- mkVar Nothing
383 exprCon <- constrain env expr (VarN exprVar)
385 (branchInfo, branchExprCons) <-
386 unzip <$> mapM (branch (VarN exprVar)) branches
388 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
390 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
391 where
392 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
393 do branchVar <- mkVar Nothing
394 fragment <- Pattern.constrain env pattern patternType
395 branchCon <- constrain env branchExpr (VarN branchVar)
396 return
397 ( (branchVar, branchRegion)
398 , CLet [Fragment.toScheme fragment] branchCon
399 )
401 varToCon var =
402 CEqual Error.Case region tipe (VarN var)
406-- 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 <- mkVar Nothing
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)
452-- EXPAND PATTERNS
455expandPattern :: Canonical.Def -> [Canonical.Def]
456expandPattern def@(Canonical.Def facts lpattern expr maybeType) =
457 let
458 (A.A patternRegion pattern) =
459 lpattern
460 in
461 case pattern of
462 P.Var _ ->
463 [def]
465 _ ->
466 mainDef : map toDef vars
467 where
468 vars =
469 P.boundVarList lpattern
471 combinedName =
472 "$" ++ concat vars
474 pvar name =
475 A.A patternRegion (P.Var name)
477 localVar name =
478 A.A patternRegion (E.localVar name)
480 mainDef =
481 Canonical.Def facts (pvar combinedName) expr maybeType
483 toDef name =
484 let
485 extract =
486 E.Case (localVar combinedName) [(lpattern, localVar name)]
487 in
488 Canonical.Def facts (pvar name) (A.A patternRegion extract) Nothing
492-- CONSTRAIN DEFINITIONS
495data Info = Info
496 { iSchemes :: [TypeScheme]
497 , iRigid :: [Variable]
498 , iFlex :: [Variable]
499 , iHeaders :: Map.Map String (A.Located Type)
500 , iC2 :: TypeConstraint
501 , iC1 :: TypeConstraint
502 }
505constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
506constrainDef env info (Canonical.Def _ (A.A patternRegion pattern) expr maybeTipe) =
507 let qs = [] -- should come from the def, but I'm not sure what would live there...
508 in
509 case (pattern, maybeTipe) of
510 (P.Var name, Just (A.A typeRegion tipe)) ->
511 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
513 (P.Var name, Nothing) ->
514 constrainUnannotatedDef env info qs patternRegion name expr
516 _ ->
517 error "canonical definitions must not have complex patterns as names in the contstraint generation phase"
520constrainAnnotatedDef
521 :: Env.Environment
522 -> Info
523 -> [String]
524 -> R.Region
525 -> R.Region
526 -> String
527 -> Canonical.Expr
528 -> ST.Canonical
529 -> IO Info
530constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
531 do -- Some mistake may be happening here. Currently, qs is always [].
532 rigidVars <- mapM mkRigid qs
534 flexiVars <- mapM mkNamedVar qs
536 let env' = Env.addValues env (zip qs flexiVars)
538 (vars, typ) <- Env.instantiateType env tipe Map.empty
540 let scheme =
541 Scheme
542 { _rigidQuantifiers = []
543 , _flexibleQuantifiers = flexiVars ++ vars
544 , _constraint = CTrue
545 , _header = Map.singleton name (A.A patternRegion typ)
546 }
548 var <- mkVar Nothing
549 defCon <- constrain env' expr (VarN var)
550 let annCon =
551 CEqual (Error.BadTypeAnnotation name) typeRegion typ (VarN var)
553 return $ info
554 { iSchemes = scheme : iSchemes info
555 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
556 }
559constrainUnannotatedDef
560 :: Env.Environment
561 -> Info
562 -> [String]
563 -> R.Region
564 -> String
565 -> Canonical.Expr
566 -> IO Info
567constrainUnannotatedDef env info qs patternRegion name expr =
568 do -- Some mistake may be happening here. Currently, qs is always [].
569 rigidVars <- mapM mkRigid qs
571 v <- mkVar Nothing
573 let tipe = VarN v
575 let env' = Env.addValues env (zip qs rigidVars)
577 con <- constrain env' expr tipe
579 return $ info
580 { iRigid = rigidVars ++ iRigid info
581 , iFlex = v : iFlex info
582 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
583 , iC2 = con /\ iC2 info
584 }