git.iko.soy/elk
on 17618de help sign in
elk/src/Type/Constrain/Expression.hs
598 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 let
33 list t =
34 Env.getType env "List" <| t
35 in
36 case expression of
37 E.Literal lit ->
38 Literal.constrain env region lit tipe
40 E.Cmd _ ->
41 return CTrue
43 E.Sub _ ->
44 return CTrue
46 E.OutgoingPort _ _ ->
47 return CTrue
49 E.IncomingPort _ _ ->
50 return CTrue
52 E.Program _ _ ->
53 error "DANGER - Program AST nodes should not be in type inference."
55 E.SaveEnv moduleName effects ->
56 Effects.constrain env moduleName effects
58 E.GLShader _uid _src gltipe ->
59 exists $ \attr ->
60 exists $ \unif ->
61 let
62 shaderTipe a u v =
63 Env.getType env "WebGL.Shader" <| a <| u <| v
65 glToType glTipe =
66 Env.getType env (Lit.glTipeName glTipe)
68 makeRec accessor baseRec =
69 let decls = accessor gltipe
70 in
71 if Map.size decls == 0 then
72 baseRec
73 else
74 record (Map.map glToType decls) baseRec
76 attribute = makeRec Lit.attribute attr
77 uniform = makeRec Lit.uniform unif
78 varying = makeRec Lit.varying (TermN EmptyRecord1)
79 in
80 return (CEqual Error.Shader region (shaderTipe attribute uniform varying) tipe)
82 E.Var var ->
83 return (CInstance region (V.toString var) tipe)
85 E.Range lowExpr highExpr ->
86 existsNumber $ \n ->
87 do lowCon <- constrain env lowExpr n
88 highCon <- constrain env highExpr n
89 return $ CAnd
90 [ lowCon
91 , highCon
92 , CEqual Error.Range region (list n) tipe
93 ]
95 E.ExplicitList exprs ->
96 constrainList env region exprs tipe
98 E.Binop op leftExpr rightExpr ->
99 constrainBinop env region op leftExpr rightExpr tipe
101 E.Lambda pattern body ->
102 exists $ \argType ->
103 exists $ \resType ->
104 do fragment <- Pattern.constrain env pattern argType
105 bodyCon <- constrain env body resType
106 let con =
107 ex (Fragment.vars fragment)
108 (CLet [monoscheme (Fragment.typeEnv fragment)]
109 (Fragment.typeConstraint fragment /\ bodyCon)
110 )
111 return $ con /\ CEqual Error.Lambda region (argType ==> resType) tipe
113 E.App _ _ ->
114 let
115 (f:args) = E.collectApps annotatedExpr
116 in
117 constrainApp env region f args tipe
119 E.If branches finally ->
120 constrainIf env region branches finally tipe
122 E.Case expr branches ->
123 constrainCase env region expr branches tipe
125 E.Data name exprs ->
126 do vars <- Monad.forM exprs $ \_ -> mkVar Nothing
127 let pairs = zip exprs (map VarN vars)
128 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
129 return $ ex vars (cs /\ CInstance region name ctipe)
130 where
131 step (t,c) (e,x) =
132 do c' <- constrain env e x
133 return (x ==> t, c /\ c')
135 E.Access expr label ->
136 exists $ \t ->
137 constrain env expr (record (Map.singleton label tipe) t)
139 E.Update expr fields ->
140 exists $ \t ->
141 do oldVars <- mapM (\_ -> mkVar Nothing) fields
142 let oldFields = Map.fromList (zip (map fst fields) (map VarN oldVars))
143 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
145 newVars <- mapM (\_ -> mkVar Nothing) fields
146 let newFields = Map.fromList (zip (map fst fields) (map VarN newVars))
147 let cNew = CEqual Error.Record region (record newFields t) tipe
149 cs <- Monad.zipWithM (constrain env) (map snd fields) (map VarN newVars)
151 return $ cOld /\ ex newVars (CAnd (cNew : cs))
153 E.Record fields ->
154 do vars <- Monad.forM fields (\_ -> mkVar Nothing)
155 fieldCons <-
156 Monad.zipWithM
157 (constrain env)
158 (map snd fields)
159 (map VarN vars)
160 let fields' = Map.fromList (zip (map fst fields) (map VarN vars))
161 let recordType = record fields' (TermN EmptyRecord1)
162 return (ex vars (CAnd (fieldCons ++ [CEqual Error.Record region recordType tipe])))
164 E.Let defs body ->
165 do bodyCon <- constrain env body tipe
167 (Info schemes rqs fqs headers c2 c1) <-
168 Monad.foldM
169 (constrainDef env)
170 (Info [] [] [] Map.empty CTrue CTrue)
171 (concatMap expandPattern defs)
173 let letScheme =
174 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
176 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
180-- CONSTRAIN APP
183constrainApp
184 :: Env.Environment
185 -> R.Region
186 -> Canonical.Expr
187 -> [Canonical.Expr]
188 -> Type
189 -> IO TypeConstraint
190constrainApp env region f args tipe =
191 do funcVar <- mkVar Nothing
192 funcCon <- constrain env f (VarN funcVar)
194 (vars, argCons, numberOfArgsCons, argMatchCons, _, returnVar) <-
195 argConstraints env maybeName region (length args) funcVar 1 args
197 let returnCon =
198 CEqual (Error.Function maybeName) region (VarN returnVar) tipe
200 return $ ex (funcVar : vars) $
201 CAnd (funcCon : argCons ++ numberOfArgsCons ++ argMatchCons ++ [returnCon])
202 where
203 maybeName =
204 case f of
205 A.A _ (E.Var canonicalName) ->
206 Just canonicalName
208 _ ->
209 Nothing
212argConstraints
213 :: Env.Environment
214 -> Maybe V.Canonical
215 -> R.Region
216 -> Int
217 -> Variable
218 -> Int
219 -> [Canonical.Expr]
220 -> IO ([Variable], [TypeConstraint], [TypeConstraint], [TypeConstraint], Maybe R.Region, Variable)
221argConstraints env name region totalArgs overallVar index args =
222 case args of
223 [] ->
224 return ([], [], [], [], Nothing, overallVar)
226 expr@(A.A subregion _) : rest ->
227 do argVar <- mkVar Nothing
228 argCon <- constrain env expr (VarN argVar)
229 argIndexVar <- mkVar Nothing
230 localReturnVar <- mkVar Nothing
232 (vars, argConRest, numberOfArgsRest, argMatchRest, restRegion, returnVar) <-
233 argConstraints env name region totalArgs localReturnVar (index + 1) rest
235 let arityRegion =
236 maybe subregion (R.merge subregion) restRegion
238 let numberOfArgsCon =
239 CEqual
240 (Error.FunctionArity name (index - 1) totalArgs arityRegion)
241 region
242 (VarN argIndexVar ==> VarN localReturnVar)
243 (VarN overallVar)
245 let argMatchCon =
246 CEqual
247 (Error.UnexpectedArg name index totalArgs subregion)
248 region
249 (VarN argIndexVar)
250 (VarN argVar)
252 return
253 ( argVar : argIndexVar : localReturnVar : vars
254 , argCon : argConRest
255 , numberOfArgsCon : numberOfArgsRest
256 , argMatchCon : argMatchRest
257 , Just arityRegion
258 , returnVar
259 )
263-- CONSTRAIN BINOP
266constrainBinop
267 :: Env.Environment
268 -> R.Region
269 -> V.Canonical
270 -> Canonical.Expr
271 -> Canonical.Expr
272 -> Type
273 -> IO TypeConstraint
274constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
275 do leftVar <- mkVar Nothing
276 rightVar <- mkVar Nothing
278 leftCon <- constrain env leftExpr (VarN leftVar)
279 rightCon <- constrain env rightExpr (VarN rightVar)
281 leftVar' <- mkVar Nothing
282 rightVar' <- mkVar Nothing
283 answerVar <- mkVar Nothing
285 let opType = VarN leftVar' ==> VarN rightVar' ==> VarN answerVar
287 return $
288 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
289 [ leftCon
290 , rightCon
291 , CInstance region (V.toString op) opType
292 , CEqual (Error.BinopLeft op leftRegion) region (VarN leftVar') (VarN leftVar)
293 , CEqual (Error.BinopRight op rightRegion) region (VarN rightVar') (VarN rightVar)
294 , CEqual (Error.Binop op) region (VarN answerVar) tipe
295 ]
299-- CONSTRAIN LISTS
302constrainList
303 :: Env.Environment
304 -> R.Region
305 -> [Canonical.Expr]
306 -> Type
307 -> IO TypeConstraint
308constrainList env region exprs tipe =
309 do (exprInfo, exprCons) <-
310 unzip <$> mapM elementConstraint exprs
312 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
314 return $ ex vars (CAnd (exprCons ++ cons))
315 where
316 elementConstraint expr@(A.A region' _) =
317 do var <- mkVar Nothing
318 con <- constrain env expr (VarN var)
319 return ( (var, region'), con )
321 varToCon var =
322 CEqual Error.List region (Env.getType env "List" <| VarN var) tipe
326-- CONSTRAIN IF EXPRESSIONS
329constrainIf
330 :: Env.Environment
331 -> R.Region
332 -> [(Canonical.Expr, Canonical.Expr)]
333 -> Canonical.Expr
334 -> Type
335 -> IO TypeConstraint
336constrainIf env region branches finally tipe =
337 do let (conditions, branchExprs) =
338 second (++ [finally]) (unzip branches)
340 (condVars, condCons) <-
341 unzip <$> mapM constrainCondition conditions
343 (branchInfo, branchExprCons) <-
344 unzip <$> mapM constrainBranch branchExprs
346 (vars,cons) <- branchCons branchInfo
348 return $ ex (condVars ++ vars) (CAnd (condCons ++ branchExprCons ++ cons))
349 where
350 bool =
351 Env.getType env "Bool"
353 constrainCondition condition@(A.A condRegion _) =
354 do condVar <- mkVar Nothing
355 condCon <- constrain env condition (VarN condVar)
356 let boolCon = CEqual Error.IfCondition condRegion (VarN condVar) bool
357 return (condVar, CAnd [ condCon, boolCon ])
359 constrainBranch expr@(A.A branchRegion _) =
360 do branchVar <- mkVar Nothing
361 exprCon <- constrain env expr (VarN branchVar)
362 return
363 ( (branchVar, branchRegion)
364 , exprCon
365 )
367 branchCons branchInfo =
368 case branchInfo of
369 [(thenVar, _), (elseVar, _)] ->
370 return
371 ( [thenVar,elseVar]
372 , [ CEqual Error.IfBranches region (VarN thenVar) (VarN elseVar)
373 , varToCon thenVar
374 ]
375 )
377 _ ->
378 pairCons region Error.MultiIfBranch varToCon branchInfo
380 varToCon var =
381 CEqual Error.If region (VarN var) tipe
385-- CONSTRAIN CASE EXPRESSIONS
388constrainCase
389 :: Env.Environment
390 -> R.Region
391 -> Canonical.Expr
392 -> [(P.Canonical, Canonical.Expr)]
393 -> Type
394 -> IO TypeConstraint
395constrainCase env region expr branches tipe =
396 do exprVar <- mkVar Nothing
397 exprCon <- constrain env expr (VarN exprVar)
399 (branchInfo, branchExprCons) <-
400 unzip <$> mapM (branch (VarN exprVar)) branches
402 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
404 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
405 where
406 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
407 do branchVar <- mkVar Nothing
408 fragment <- Pattern.constrain env pattern patternType
409 branchCon <- constrain env branchExpr (VarN branchVar)
410 return
411 ( (branchVar, branchRegion)
412 , CLet [Fragment.toScheme fragment] branchCon
413 )
415 varToCon var =
416 CEqual Error.Case region tipe (VarN var)
420-- COLLECT PAIRS
423data Pair = Pair
424 { _index :: Int
425 , _var1 :: Variable
426 , _var2 :: Variable
427 , _region :: R.Region
428 }
431pairCons
432 :: R.Region
433 -> (Int -> R.Region -> Error.Hint)
434 -> (Variable -> TypeConstraint)
435 -> [(Variable, R.Region)]
436 -> IO ([Variable], [TypeConstraint])
437pairCons region pairHint varToCon items =
438 let
439 pairToCon (Pair index var1 var2 subregion) =
440 CEqual (pairHint index subregion) region (VarN var1) (VarN var2)
441 in
442 case collectPairs 2 items of
443 Nothing ->
444 do var <- mkVar Nothing
445 return ([var], [varToCon var])
447 Just (pairs, var) ->
448 return (map fst items, map pairToCon pairs ++ [varToCon var])
451collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
452collectPairs index items =
453 case items of
454 [] ->
455 Nothing
457 (var,_) : [] ->
458 Just ([], var)
460 (var,_) : rest@((var',region) : _) ->
461 do (pairs, summaryVar) <- collectPairs (index+1) rest
462 return (Pair index var var' region : pairs, summaryVar)
466-- EXPAND PATTERNS
469expandPattern :: Canonical.Def -> [Canonical.Def]
470expandPattern def@(Canonical.Def facts lpattern expr maybeType) =
471 let
472 (A.A patternRegion pattern) =
473 lpattern
474 in
475 case pattern of
476 P.Var _ ->
477 [def]
479 _ ->
480 mainDef : map toDef vars
481 where
482 vars =
483 P.boundVarList lpattern
485 combinedName =
486 "$" ++ concat vars
488 pvar name =
489 A.A patternRegion (P.Var name)
491 localVar name =
492 A.A patternRegion (E.localVar name)
494 mainDef =
495 Canonical.Def facts (pvar combinedName) expr maybeType
497 toDef name =
498 let
499 extract =
500 E.Case (localVar combinedName) [(lpattern, localVar name)]
501 in
502 Canonical.Def facts (pvar name) (A.A patternRegion extract) Nothing
506-- CONSTRAIN DEFINITIONS
509data Info = Info
510 { iSchemes :: [TypeScheme]
511 , iRigid :: [Variable]
512 , iFlex :: [Variable]
513 , iHeaders :: Map.Map String (A.Located Type)
514 , iC2 :: TypeConstraint
515 , iC1 :: TypeConstraint
516 }
519constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
520constrainDef env info (Canonical.Def _ (A.A patternRegion pattern) expr maybeTipe) =
521 let qs = [] -- should come from the def, but I'm not sure what would live there...
522 in
523 case (pattern, maybeTipe) of
524 (P.Var name, Just (A.A typeRegion tipe)) ->
525 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
527 (P.Var name, Nothing) ->
528 constrainUnannotatedDef env info qs patternRegion name expr
530 _ ->
531 error "canonical definitions must not have complex patterns as names in the contstraint generation phase"
534constrainAnnotatedDef
535 :: Env.Environment
536 -> Info
537 -> [String]
538 -> R.Region
539 -> R.Region
540 -> String
541 -> Canonical.Expr
542 -> ST.Canonical
543 -> IO Info
544constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
545 do -- Some mistake may be happening here. Currently, qs is always [].
546 rigidVars <- mapM mkRigid qs
548 flexiVars <- mapM mkNamedVar qs
550 let env' = Env.addValues env (zip qs flexiVars)
552 (vars, typ) <- Env.instantiateType env tipe Map.empty
554 let scheme =
555 Scheme
556 { _rigidQuantifiers = []
557 , _flexibleQuantifiers = flexiVars ++ vars
558 , _constraint = CTrue
559 , _header = Map.singleton name (A.A patternRegion typ)
560 }
562 var <- mkVar Nothing
563 defCon <- constrain env' expr (VarN var)
564 let annCon =
565 CEqual (Error.BadTypeAnnotation name) typeRegion typ (VarN var)
567 return $ info
568 { iSchemes = scheme : iSchemes info
569 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
570 }
573constrainUnannotatedDef
574 :: Env.Environment
575 -> Info
576 -> [String]
577 -> R.Region
578 -> String
579 -> Canonical.Expr
580 -> IO Info
581constrainUnannotatedDef env info qs patternRegion name expr =
582 do -- Some mistake may be happening here. Currently, qs is always [].
583 rigidVars <- mapM mkRigid qs
585 v <- mkVar Nothing
587 let tipe = VarN v
589 let env' = Env.addValues env (zip qs rigidVars)
591 con <- constrain env' expr tipe
593 return $ info
594 { iRigid = rigidVars ++ iRigid info
595 , iFlex = v : iFlex info
596 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
597 , iC2 = con /\ iC2 info
598 }