git.iko.soy/elk
on e00a3f3 help sign in
elk/src/Type/Constrain/Expression.hs
606 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 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 qualified Type.Constrain.Effects as Effects
20import qualified Type.Constrain.Literal as Literal
21import qualified Type.Constrain.Pattern as Pattern
22import qualified Type.Environment as Env
23import Type.Type hiding (Descriptor(..))
27constrain :: Env.Env -> C.Expr -> Type -> IO Constraint
28constrain env annotatedExpr@(A.A region expression) tipe =
29 case expression of
30 C.Literal lit ->
31 Literal.constrain env region lit tipe
33 C.Cmd _ _ ->
34 return CTrue
36 C.Sub _ _ ->
37 return CTrue
39 C.OutgoingPort _ _ ->
40 return CTrue
42 C.IncomingPort _ _ ->
43 return CTrue
45 C.Program _ _ ->
46 error "DANGER - Program AST nodes should not be in type inference."
48 C.SaveEnv moduleName effects ->
49 Effects.constrain env moduleName effects
51 C.GLShader _uid _src glType ->
52 exists $ \attr ->
53 exists $ \unif ->
54 let
55 shaderTipe a u v =
56 Env.getType env "WebGL.Shader" <| a <| u <| v
58 glToType gl =
59 Env.getType env (Lit.glTypeToText gl)
61 makeRec accessor baseRec =
62 let decls = accessor glType
63 in
64 if Map.null decls then
65 baseRec
66 else
67 RecordN (Map.map glToType decls) baseRec
69 attribute = makeRec Lit.attribute attr
70 uniform = makeRec Lit.uniform unif
71 varying = makeRec Lit.varying EmptyRecordN
72 in
73 return (CEqual Error.Shader region (shaderTipe attribute uniform varying) tipe)
75 C.Var var ->
76 return (CInstance region (V.toText var) tipe)
78 C.List exprs ->
79 constrainList env region exprs tipe
81 C.Binop op leftExpr rightExpr ->
82 constrainBinop env region op leftExpr rightExpr tipe
84 C.Lambda pattern body ->
85 exists $ \argType ->
86 exists $ \resType ->
87 do (Pattern.Info headers vars cons) <- Pattern.constrain env pattern argType
88 bodyCon <- constrain env body resType
89 return $
90 ex vars (CLet [monoscheme headers] (cons /\ bodyCon))
91 /\ CEqual Error.Lambda region (argType ==> resType) tipe
93 C.App _ _ ->
94 let
95 (f:args) = C.collectApps annotatedExpr
96 in
97 constrainApp env region f args tipe
99 C.If branches finally ->
100 constrainIf env region branches finally tipe
102 C.Case expr branches ->
103 constrainCase env region expr branches tipe
105 C.Ctor name exprs ->
106 do vars <- Monad.forM exprs $ \_ -> mkVar Nothing
107 let pairs = zip exprs (map VarN vars)
108 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
109 return $ ex vars (cs /\ CInstance region (V.toText name) ctipe)
110 where
111 step (t,c) (e,x) =
112 do c' <- constrain env e x
113 return (x ==> t, c /\ c')
115 C.Access expr field ->
116 exists $ \recordType ->
117 exists $ \ext ->
118 do recordCon <- constrain env expr recordType
119 let maybeBody = C.collectFields expr
120 let desiredType = RecordN (Map.singleton field tipe) ext
121 let fieldCon = CEqual (Error.Access maybeBody field) region recordType desiredType
122 return $ recordCon /\ fieldCon
124 C.Update expr fields ->
125 exists $ \t ->
126 do oldVars <- mapM (\_ -> mkVar Nothing) fields
127 let oldFields = Map.fromList (zip (map fst fields) (map VarN oldVars))
128 cOld <- ex oldVars <$> constrain env expr (RecordN oldFields t)
130 newVars <- mapM (\_ -> mkVar Nothing) fields
131 let newFields = Map.fromList (zip (map fst fields) (map VarN newVars))
132 let cNew = CEqual Error.Record region (RecordN newFields t) tipe
134 cs <- Monad.zipWithM (constrain env) (map snd fields) (map VarN newVars)
136 return $ cOld /\ ex newVars (CAnd (cNew : cs))
138 C.Record fields ->
139 do vars <- Monad.forM fields (\_ -> mkVar Nothing)
140 fieldCons <-
141 Monad.zipWithM
142 (constrain env)
143 (map snd fields)
144 (map VarN vars)
145 let fields' = Map.fromList (zip (map fst fields) (map VarN vars))
146 let recordType = RecordN fields' EmptyRecordN
147 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region recordType tipe])))
149 C.Let defs body ->
150 do bodyCon <- constrain env body tipe
152 (Info schemes rqs fqs headers c2 c1) <-
153 Monad.foldM
154 (constrainDef env)
155 (Info [] [] [] Map.empty CTrue CTrue)
156 (concatMap expandPattern defs)
158 let letScheme =
159 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
161 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
165-- CONSTRAIN APP
168constrainApp
169 :: Env.Env
170 -> R.Region
171 -> C.Expr
172 -> [C.Expr]
173 -> Type
174 -> IO Constraint
175constrainApp env region f args tipe =
176 do funcVar <- mkVar Nothing
177 funcCon <- constrain env f (VarN funcVar)
179 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
180 argConstraints env maybeName region (length args) funcVar 1 args
182 let returnCon =
183 CEqual (Error.Function maybeName) region (VarN returnVar) tipe
185 return $ ex (funcVar : vars) $
186 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
187 where
188 maybeName =
189 case f of
190 A.A _ (C.Var canonicalName) ->
191 Just canonicalName
193 _ ->
194 Nothing
197argConstraints
198 :: Env.Env
199 -> Maybe V.Canonical
200 -> R.Region
201 -> Int
202 -> Variable
203 -> Int
204 -> [C.Expr]
205 -> IO ([Variable], [Constraint], [Constraint], [Constraint], Maybe R.Region, Variable)
206argConstraints env name region totalArgs overallVar index args =
207 case args of
208 [] ->
209 return ([], [], [], [], Nothing, overallVar)
211 expr@(A.A subregion _) : rest ->
212 do argVar <- mkVar Nothing
213 argCon <- constrain env expr (VarN argVar)
214 argIndexVar <- mkVar Nothing
215 localReturnVar <- mkVar Nothing
217 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
218 argConstraints env name region totalArgs localReturnVar (index + 1) rest
220 let arityRegion =
221 maybe subregion (R.merge subregion) restRegion
223 let numberOfArgsCon =
224 CEqual
225 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
226 region
227 (VarN argIndexVar ==> VarN localReturnVar)
228 (VarN overallVar)
230 let argMatchCon =
231 CEqual
232 (Error.UnexpectedArg name index totalArgs subregion)
233 region
234 (VarN argIndexVar)
235 (VarN argVar)
237 return
238 ( argVar : argIndexVar : localReturnVar : vars
239 , argCon : argConRest
240 , numberOfArgsCon : numberOfArgsRest
241 , argMatchCon : argMatchRest
242 , Just arityRegion
243 , returnVar
244 )
248-- CONSTRAIN BINOP
251constrainBinop
252 :: Env.Env
253 -> R.Region
254 -> V.Canonical
255 -> C.Expr
256 -> C.Expr
257 -> Type
258 -> IO Constraint
259constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
260 do leftVar <- mkVar Nothing
261 rightVar <- mkVar Nothing
263 leftCon <- constrain env leftExpr (VarN leftVar)
264 rightCon <- constrain env rightExpr (VarN rightVar)
266 leftVar' <- mkVar Nothing
267 rightVar' <- mkVar Nothing
268 answerVar <- mkVar Nothing
270 let opType = VarN leftVar' ==> VarN rightVar' ==> VarN answerVar
272 return $
273 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
274 [ leftCon
275 , rightCon
276 , CInstance region (V.toText op) opType
277 , CEqual (Error.BinopLeft op leftRegion) region (VarN leftVar') (VarN leftVar)
278 , CEqual (Error.BinopRight op rightRegion) region (VarN rightVar') (VarN rightVar)
279 , CEqual (Error.Binop op) region (VarN answerVar) tipe
280 ]
284-- CONSTRAIN LISTS
287constrainList :: Env.Env -> R.Region -> [C.Expr] -> Type -> IO Constraint
288constrainList env region exprs tipe =
289 do (exprInfo, exprCons) <-
290 unzip <$> mapM elementConstraint exprs
292 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
294 return $ ex vars (CAnd (exprCons ++ cons))
295 where
296 elementConstraint expr@(A.A region' _) =
297 do var <- mkVar Nothing
298 con <- constrain env expr (VarN var)
299 return ( (var, region'), con )
301 varToCon var =
302 CEqual Error.List region (Env.getType env "List" <| VarN var) tipe
306-- CONSTRAIN IF EXPRESSIONS
309constrainIf
310 :: Env.Env
311 -> R.Region
312 -> [(C.Expr, C.Expr)]
313 -> C.Expr
314 -> Type
315 -> IO Constraint
316constrainIf env region branches finally tipe =
317 do let (conditions, branchExprs) =
318 second (++ [finally]) (unzip branches)
320 (condVars, condCons) <-
321 unzip <$> mapM constrainCondition conditions
323 (branchInfo, branchExprCons) <-
324 unzip <$> mapM constrainBranch branchExprs
326 (vars,cons) <- branchCons branchInfo
328 return $ ex (condVars ++ vars) (CAnd (condCons ++ branchExprCons ++ cons))
329 where
330 bool =
331 Env.getType env "Bool"
333 constrainCondition condition@(A.A condRegion _) =
334 do condVar <- mkVar Nothing
335 condCon <- constrain env condition (VarN condVar)
336 let boolCon = CEqual Error.IfCondition condRegion (VarN condVar) bool
337 return (condVar, CAnd [ condCon, boolCon ])
339 constrainBranch expr@(A.A branchRegion _) =
340 do branchVar <- mkVar Nothing
341 exprCon <- constrain env expr (VarN branchVar)
342 return
343 ( (branchVar, branchRegion)
344 , exprCon
345 )
347 branchCons branchInfo =
348 case branchInfo of
349 [(thenVar, _), (elseVar, _)] ->
350 return
351 ( [thenVar,elseVar]
352 , [ CEqual Error.IfBranches region (VarN thenVar) (VarN elseVar)
353 , varToCon thenVar
354 ]
355 )
357 _ ->
358 pairCons region Error.MultiIfBranch varToCon branchInfo
360 varToCon var =
361 CEqual Error.If region (VarN var) tipe
365-- CONSTRAIN CASE EXPRESSIONS
368constrainCase
369 :: Env.Env
370 -> R.Region
371 -> C.Expr
372 -> [(P.Canonical, C.Expr)]
373 -> Type
374 -> IO Constraint
375constrainCase env region expr branches tipe =
376 do exprVar <- mkVar Nothing
377 exprCon <- constrain env expr (VarN exprVar)
379 (branchInfo, branchExprCons) <-
380 unzip <$> mapM (branch (VarN exprVar)) branches
382 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
384 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
385 where
386 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
387 do branchVar <- mkVar Nothing
388 scheme <- Pattern.infoToScheme <$> Pattern.constrain env pattern patternType
389 branchCon <- constrain env branchExpr (VarN branchVar)
390 return
391 ( (branchVar, branchRegion)
392 , CLet [scheme] branchCon
393 )
395 varToCon var =
396 CEqual Error.Case region tipe (VarN var)
400-- COLLECT PAIRS
403data Pair = Pair
404 { _index :: Int
405 , _var1 :: Variable
406 , _var2 :: Variable
407 , _region :: R.Region
408 }
411pairCons
412 :: R.Region
413 -> (Int -> R.Region -> Error.Hint)
414 -> (Variable -> Constraint)
415 -> [(Variable, R.Region)]
416 -> IO ([Variable], [Constraint])
417pairCons region pairHint varToCon items =
418 let
419 pairToCon (Pair index var1 var2 subregion) =
420 CEqual (pairHint index subregion) region (VarN var1) (VarN var2)
421 in
422 case collectPairs 2 items of
423 Nothing ->
424 do var <- mkVar Nothing
425 return ([var], [varToCon var])
427 Just (pairs, var) ->
428 return (map fst items, map pairToCon pairs ++ [varToCon var])
431collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
432collectPairs index items =
433 case items of
434 [] ->
435 Nothing
437 (var,_) : [] ->
438 Just ([], var)
440 (var,_) : rest@((var',region) : _) ->
441 do (pairs, summaryVar) <- collectPairs (index+1) rest
442 return (Pair index var var' region : pairs, summaryVar)
446-- EXPAND PATTERNS
449expandPattern :: C.Def -> [C.Def]
450expandPattern def@(C.Def facts lpattern expr maybeType) =
451 let
452 (A.A patternRegion pattern) =
453 lpattern
454 in
455 case pattern of
456 P.Var _ ->
457 [def]
459 _ ->
460 mainDef : map toDef vars
461 where
462 vars =
463 P.boundVarList lpattern
465 combinedName =
466 Text.intercalate "$" ("" : vars)
468 pvar name =
469 A.A patternRegion (P.Var name)
471 localVar name =
472 A.A patternRegion (C.localVar name)
474 mainDef =
475 C.Def facts (pvar combinedName) expr maybeType
477 toDef name =
478 let
479 extract =
480 C.Case (localVar combinedName) [(lpattern, localVar name)]
481 in
482 C.Def facts (pvar name) (A.A patternRegion extract) Nothing
486-- CONSTRAIN DEFINITIONS
489data Info =
490 Info
491 { iSchemes :: [Scheme]
492 , iRigid :: [Variable]
493 , iFlex :: [Variable]
494 , iHeaders :: Map.Map Text (A.Located Type)
495 , iC2 :: Constraint
496 , iC1 :: Constraint
497 }
500constrainDef :: Env.Env -> Info -> C.Def -> IO Info
501constrainDef env info (C.Def defRegion (A.A patternRegion pattern) expr maybeTipe) =
502 case (pattern, maybeTipe) of
503 (P.Var name, Nothing) ->
504 constrainUnannotatedDef env patternRegion name expr info
506 (P.Var name, Just (A.A _ tipe)) ->
507 constrainAnnotatedDef env defRegion patternRegion name expr tipe info
509 _ ->
510 error "canonical definitions must not have complex patterns as names in the contstraint generation phase"
513constrainUnannotatedDef
514 :: Env.Env
515 -> R.Region
516 -> Text
517 -> C.Expr
518 -> Info
519 -> IO Info
520constrainUnannotatedDef env patternRegion name expr info =
521 do v <- mkVar Nothing
522 let tipe = VarN v
523 defCon <- constrain env expr tipe
524 return $ info
525 { iFlex = v : iFlex info
526 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
527 , iC2 = defCon /\ iC2 info
528 }
531constrainAnnotatedDef
532 :: Env.Env
533 -> R.Region
534 -> R.Region
535 -> Text
536 -> C.Expr
537 -> ST.Canonical
538 -> Info
539 -> IO Info
540constrainAnnotatedDef env defRegion region name expr tipe info =
541 do (flexType, flexVars) <- Env.instantiateType Flex env tipe
543 let scheme =
544 Scheme
545 { _rigidQuantifiers = []
546 , _flexibleQuantifiers = Map.elems flexVars
547 , _constraint = CTrue
548 , _header = Map.singleton name (A.A region flexType)
549 }
551 defCon <- constrainAnnDefHelp expr tipe (ArgInfo name defRegion env [] [])
553 return $ info
554 { iSchemes = scheme : iSchemes info
555 , iC1 = iC1 info /\ defCon
556 }
559data ArgInfo =
560 ArgInfo
561 { _name :: Text
562 , _def :: R.Region
563 , _env :: Env.Env
564 , _args :: [(P.Canonical, Type)]
565 , _vars :: [Variable]
566 }
569constrainAnnDefHelp :: C.Expr -> ST.Canonical -> ArgInfo -> IO Constraint
570constrainAnnDefHelp expr tipe (ArgInfo name defRegion env args vars) =
571 case (expr, tipe) of
572 (A.A _ (C.Lambda arg result), ST.Lambda argType resultType) ->
573 do (rigidArgType, newVars) <- Env.instantiateType Rigid env argType
575 constrainAnnDefHelp result resultType $
576 ArgInfo
577 { _name = name
578 , _def = defRegion
579 , _env = Env.addValues newVars env
580 , _args = (arg, rigidArgType) : args
581 , _vars = Map.elems newVars ++ vars
582 }
584 (A.A region _, _) ->
585 do (rigidType, newVars) <- Env.instantiateType Rigid env tipe
587 let finalEnv = Env.addValues newVars env
588 let finalArgs = reverse args
589 let rigidVars = Map.elems newVars ++ vars
591 (Pattern.Info headers argVars argCons) <-
592 Pattern.joinInfos <$> mapM (uncurry (Pattern.constrain finalEnv)) finalArgs
594 resultVar <- mkVar Nothing
595 let resultType = VarN resultVar
596 defCon <- constrain finalEnv expr resultType
598 let sharedArity = length args
599 let typeArity = sharedArity + length (ST.collectLambdas tipe) - 1
600 let argsArity = sharedArity + length (fst (C.collectLambdas expr))
601 let hint = Error.ReturnType name typeArity argsArity region
602 let resultCon =
603 CEqual hint defRegion rigidType resultType
605 return $ forall rigidVars $ ex (resultVar : argVars) $ CLet [monoscheme headers] $
606 CAnd [ argCons, defCon, resultCon ]