on c19392f help sign in
elk/src/Type/Constrain/Expression.hs
604 lines 17 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Type.Constrain.Expression where
5import Control.Arrow (second)
6import qualified Control.Monad as Monad
7import qualified Data.Map.Strict as Map
8import qualified Data.Text as Text
9import Data.Text (Text)
11import qualified AST.Expression.Canonical as C
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 Type.Constraint
20import qualified Type.Constrain.Effects as Effects
21import qualified Type.Constrain.Literal as Literal
22import qualified Type.Constrain.Pattern as Pattern
23import qualified Type.Environment as Env
24import Type.Type as Type hiding (Descriptor(..))
28constrain :: Env.Env -> C.Expr -> Type -> IO Constraint
29constrain env annotatedExpr@(A.A region expression) tipe =
30 case expression of
31 C.Literal lit ->
32 Literal.constrain region lit tipe
34 C.Cmd _ _ ->
35 return CTrue
37 C.Sub _ _ ->
38 return CTrue
40 C.OutgoingPort _ _ ->
41 return CTrue
43 C.IncomingPort _ _ ->
44 return CTrue
46 C.Program _ _ ->
47 error "DANGER - Program AST nodes should not be in type inference."
49 C.SaveEnv moduleName effects ->
50 Effects.constrain moduleName effects
52 C.GLShader _uid _src glType ->
53 exists $ \attr ->
54 exists $ \unif ->
55 let
56 shaderTipe a u v =
57 AppN V.shader [a, u, v]
59 glToType gl =
60 AppN (Lit.glTypeToVar gl) []
62 makeRec accessor baseRec =
63 let decls = accessor glType
64 in
65 if Map.null decls then
66 baseRec
67 else
68 RecordN (Map.map glToType decls) baseRec
70 attribute = makeRec Lit.attribute attr
71 uniform = makeRec Lit.uniform unif
72 varying = makeRec Lit.varying EmptyRecordN
73 in
74 return (CEqual Error.Shader region (shaderTipe attribute uniform varying) tipe)
76 C.Var var ->
77 return (CInstance region (V.toText var) tipe)
79 C.List exprs ->
80 constrainList env region exprs tipe
82 C.Binop op leftExpr rightExpr ->
83 constrainBinop env region op leftExpr rightExpr tipe
85 C.Lambda pattern body ->
86 exists $ \argType ->
87 exists $ \resType ->
88 do (Pattern.Info headers vars cons) <- Pattern.constrain env pattern argType
89 bodyCon <- constrain env body resType
90 return $
91 ex vars (CLet [monoscheme headers] (cons /\ bodyCon))
92 /\ CEqual Error.Lambda region (argType ==> resType) tipe
94 C.App _ _ ->
95 let
96 (f:args) = C.collectApps annotatedExpr
97 in
98 constrainApp env region f args tipe
100 C.If branches finally ->
101 constrainIf env region branches finally tipe
103 C.Case expr branches ->
104 constrainCase env region expr branches tipe
106 C.Ctor name exprs ->
107 do vars <- mapM (\_ -> mkFlexVar) exprs
108 let pairs = zip exprs (map VarN vars)
109 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
110 return $ ex vars (cs /\ CInstance region (V.toText name) ctipe)
111 where
112 step (t,c) (e,x) =
113 do c' <- constrain env e x
114 return (x ==> t, c /\ c')
116 C.Access expr field ->
117 exists $ \recordType ->
118 exists $ \ext ->
119 do recordCon <- constrain env expr recordType
120 let maybeBody = C.collectFields expr
121 let desiredType = RecordN (Map.singleton field tipe) ext
122 let fieldCon = CEqual (Error.Access maybeBody field) region recordType desiredType
123 return $ recordCon /\ fieldCon
125 C.Update expr fields ->
126 exists $ \t ->
127 do oldVars <- mapM (\_ -> mkFlexVar) fields
128 let oldFields = Map.fromList (zip (map fst fields) (map VarN oldVars))
129 cOld <- ex oldVars <$> constrain env expr (RecordN oldFields t)
131 newVars <- mapM (\_ -> mkFlexVar) fields
132 let newFields = Map.fromList (zip (map fst fields) (map VarN newVars))
133 let cNew = CEqual Error.Record region (RecordN newFields t) tipe
135 cs <- Monad.zipWithM (constrain env) (map snd fields) (map VarN newVars)
137 return $ cOld /\ ex newVars (CAnd (cNew : cs))
139 C.Record fields ->
140 do vars <- mapM (\_ -> mkFlexVar) fields
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 = RecordN fields' EmptyRecordN
148 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region recordType tipe])))
150 C.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.Env
171 -> R.Region
172 -> C.Expr
173 -> [C.Expr]
174 -> Type
175 -> IO Constraint
176constrainApp env region f args tipe =
177 do funcVar <- mkFlexVar
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 _ (C.Var canonicalName) ->
192 Just canonicalName
194 _ ->
195 Nothing
198argConstraints
199 :: Env.Env
200 -> Maybe V.Canonical
201 -> R.Region
202 -> Int
203 -> Variable
204 -> Int
205 -> [C.Expr]
206 -> IO ([Variable], [Constraint], [Constraint], [Constraint], 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 <- mkFlexVar
214 argCon <- constrain env expr (VarN argVar)
215 argIndexVar <- mkFlexVar
216 localReturnVar <- mkFlexVar
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.Env
254 -> R.Region
255 -> V.Canonical
256 -> C.Expr
257 -> C.Expr
258 -> Type
259 -> IO Constraint
260constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
261 do leftVar <- mkFlexVar
262 rightVar <- mkFlexVar
264 leftCon <- constrain env leftExpr (VarN leftVar)
265 rightCon <- constrain env rightExpr (VarN rightVar)
267 leftVar' <- mkFlexVar
268 rightVar' <- mkFlexVar
269 answerVar <- mkFlexVar
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.toText 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 :: Env.Env -> R.Region -> [C.Expr] -> Type -> IO Constraint
289constrainList env region exprs tipe =
290 do (exprInfo, exprCons) <-
291 unzip <$> mapM elementConstraint exprs
293 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
295 return $ ex vars (CAnd (exprCons ++ cons))
296 where
297 elementConstraint expr@(A.A region' _) =
298 do var <- mkFlexVar
299 con <- constrain env expr (VarN var)
300 return ( (var, region'), con )
302 varToCon var =
303 CEqual Error.List region (AppN V.list [VarN var]) tipe
307-- CONSTRAIN IF EXPRESSIONS
310constrainIf
311 :: Env.Env
312 -> R.Region
313 -> [(C.Expr, C.Expr)]
314 -> C.Expr
315 -> Type
316 -> IO Constraint
317constrainIf env region branches finally tipe =
318 do let (conditions, branchExprs) =
319 second (++ [finally]) (unzip branches)
321 (condVars, condCons) <-
322 unzip <$> mapM constrainCondition conditions
324 (branchInfo, branchExprCons) <-
325 unzip <$> mapM constrainBranch branchExprs
327 (vars,cons) <- branchCons branchInfo
329 return $ ex (condVars ++ vars) (CAnd (condCons ++ branchExprCons ++ cons))
330 where
331 constrainCondition condition@(A.A condRegion _) =
332 do condVar <- mkFlexVar
333 condCon <- constrain env condition (VarN condVar)
334 let boolCon = CEqual Error.IfCondition condRegion (VarN condVar) Type.bool
335 return (condVar, CAnd [ condCon, boolCon ])
337 constrainBranch expr@(A.A branchRegion _) =
338 do branchVar <- mkFlexVar
339 exprCon <- constrain env expr (VarN branchVar)
340 return
341 ( (branchVar, branchRegion)
342 , exprCon
343 )
345 branchCons branchInfo =
346 case branchInfo of
347 [(thenVar, _), (elseVar, _)] ->
348 return
349 ( [thenVar,elseVar]
350 , [ CEqual Error.IfBranches region (VarN thenVar) (VarN elseVar)
351 , varToCon thenVar
352 ]
353 )
355 _ ->
356 pairCons region Error.MultiIfBranch varToCon branchInfo
358 varToCon var =
359 CEqual Error.If region (VarN var) tipe
363-- CONSTRAIN CASE EXPRESSIONS
366constrainCase
367 :: Env.Env
368 -> R.Region
369 -> C.Expr
370 -> [(P.Canonical, C.Expr)]
371 -> Type
372 -> IO Constraint
373constrainCase env region expr branches tipe =
374 do exprVar <- mkFlexVar
375 exprCon <- constrain env expr (VarN exprVar)
377 (branchInfo, branchExprCons) <-
378 unzip <$> mapM (branch (VarN exprVar)) branches
380 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
382 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
383 where
384 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
385 do branchVar <- mkFlexVar
386 scheme <- Pattern.infoToScheme <$> Pattern.constrain env pattern patternType
387 branchCon <- constrain env branchExpr (VarN branchVar)
388 return
389 ( (branchVar, branchRegion)
390 , CLet [scheme] branchCon
391 )
393 varToCon var =
394 CEqual Error.Case region tipe (VarN var)
398-- COLLECT PAIRS
401data Pair = Pair
402 { _index :: Int
403 , _var1 :: Variable
404 , _var2 :: Variable
405 , _region :: R.Region
406 }
409pairCons
410 :: R.Region
411 -> (Int -> R.Region -> Error.Hint)
412 -> (Variable -> Constraint)
413 -> [(Variable, R.Region)]
414 -> IO ([Variable], [Constraint])
415pairCons region pairHint varToCon items =
416 let
417 pairToCon (Pair index var1 var2 subregion) =
418 CEqual (pairHint index subregion) region (VarN var1) (VarN var2)
419 in
420 case collectPairs 2 items of
421 Nothing ->
422 do var <- mkFlexVar
423 return ([var], [varToCon var])
425 Just (pairs, var) ->
426 return (map fst items, map pairToCon pairs ++ [varToCon var])
429collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
430collectPairs index items =
431 case items of
432 [] ->
433 Nothing
435 (var,_) : [] ->
436 Just ([], var)
438 (var,_) : rest@((var',region) : _) ->
439 do (pairs, summaryVar) <- collectPairs (index+1) rest
440 return (Pair index var var' region : pairs, summaryVar)
444-- EXPAND PATTERNS
447expandPattern :: C.Def -> [C.Def]
448expandPattern def@(C.Def facts lpattern expr maybeType) =
449 let
450 (A.A patternRegion pattern) =
451 lpattern
452 in
453 case pattern of
454 P.Var _ ->
455 [def]
457 _ ->
458 mainDef : map toDef vars
459 where
460 vars =
461 P.boundVarList lpattern
463 combinedName =
464 Text.intercalate "$" ("" : vars)
466 pvar name =
467 A.A patternRegion (P.Var name)
469 localVar name =
470 A.A patternRegion (C.localVar name)
472 mainDef =
473 C.Def facts (pvar combinedName) expr maybeType
475 toDef name =
476 let
477 extract =
478 C.Case (localVar combinedName) [(lpattern, localVar name)]
479 in
480 C.Def facts (pvar name) (A.A patternRegion extract) Nothing
484-- CONSTRAIN DEFINITIONS
487data Info =
488 Info
489 { iSchemes :: [Scheme]
490 , iRigid :: [Variable]
491 , iFlex :: [Variable]
492 , iHeaders :: Map.Map Text (A.Located Type)
493 , iC2 :: Constraint
494 , iC1 :: Constraint
495 }
498constrainDef :: Env.Env -> Info -> C.Def -> IO Info
499constrainDef env info (C.Def defRegion (A.A patternRegion pattern) expr maybeTipe) =
500 case (pattern, maybeTipe) of
501 (P.Var name, Nothing) ->
502 constrainUnannotatedDef env patternRegion name expr info
504 (P.Var name, Just (A.A _ tipe)) ->
505 constrainAnnotatedDef env defRegion patternRegion name expr tipe info
507 _ ->
508 error "canonical definitions must not have complex patterns as names in the contstraint generation phase"
511constrainUnannotatedDef
512 :: Env.Env
513 -> R.Region
514 -> Text
515 -> C.Expr
516 -> Info
517 -> IO Info
518constrainUnannotatedDef env patternRegion name expr info =
519 do v <- mkFlexVar
520 let tipe = VarN v
521 defCon <- constrain env expr tipe
522 return $ info
523 { iFlex = v : iFlex info
524 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
525 , iC2 = defCon /\ iC2 info
526 }
529constrainAnnotatedDef
530 :: Env.Env
531 -> R.Region
532 -> R.Region
533 -> Text
534 -> C.Expr
535 -> ST.Canonical
536 -> Info
537 -> IO Info
538constrainAnnotatedDef env defRegion region name expr tipe info =
539 do (flexType, flexVars) <- Env.instantiateFlex env tipe
541 let scheme =
542 Scheme
543 { _rigidQuantifiers = []
544 , _flexibleQuantifiers = Map.elems flexVars
545 , _constraint = CTrue
546 , _header = Map.singleton name (A.A region flexType)
547 }
549 defCon <- constrainAnnDefHelp expr tipe (ArgInfo name defRegion env [] [])
551 return $ info
552 { iSchemes = scheme : iSchemes info
553 , iC1 = iC1 info /\ defCon
554 }
557data ArgInfo =
558 ArgInfo
559 { _name :: Text
560 , _def :: R.Region
561 , _env :: Env.Env
562 , _args :: [(P.Canonical, Type)]
563 , _vars :: [Variable]
564 }
567constrainAnnDefHelp :: C.Expr -> ST.Canonical -> ArgInfo -> IO Constraint
568constrainAnnDefHelp expr tipe (ArgInfo name defRegion env args vars) =
569 case (expr, tipe) of
570 (A.A _ (C.Lambda arg result), ST.Lambda argType resultType) ->
571 do (rigidArgType, newVars) <- Env.instantiateRigid env argType
573 constrainAnnDefHelp result resultType $
574 ArgInfo
575 { _name = name
576 , _def = defRegion
577 , _env = Env.addValues newVars env
578 , _args = (arg, rigidArgType) : args
579 , _vars = Map.elems newVars ++ vars
580 }
582 (A.A region _, _) ->
583 do (rigidType, newVars) <- Env.instantiateRigid env tipe
585 let finalEnv = Env.addValues newVars env
586 let finalArgs = reverse args
587 let rigidVars = Map.elems newVars ++ vars
589 (Pattern.Info headers argVars argCons) <-
590 Pattern.joinInfos <$> mapM (uncurry (Pattern.constrain finalEnv)) finalArgs
592 resultVar <- mkFlexVar
593 let resultType = VarN resultVar
594 defCon <- constrain finalEnv expr resultType
596 let sharedArity = length args
597 let typeArity = sharedArity + length (ST.collectLambdas tipe) - 1
598 let argsArity = sharedArity + length (fst (C.collectLambdas expr))
599 let hint = Error.ReturnType name typeArity argsArity region
600 let resultCon =
601 CEqual hint defRegion rigidType resultType
603 return $ forall rigidVars $ ex (resultVar : argVars) $ CLet [monoscheme headers] $
604 CAnd [ argCons, defCon, resultCon ]