git.iko.soy/elk
on ea343fc help sign in
elk/src/Type/Constrain/Expression.hs
501 lines 16 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Constrain.Expression where
4import Control.Applicative ((<$>))
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 (A.A region expression) tipe =
31 let list t = Env.get env Env.types "List" <| t
32 (===) = CEqual Error.None region
33 (<?) = CInstance region
34 in
35 case expression of
36 E.Literal lit ->
37 Literal.constrain env region lit tipe
39 E.GLShader _uid _src gltipe ->
40 exists $ \attr ->
41 exists $ \unif ->
42 let
43 shaderTipe a u v =
44 Env.get env Env.types "WebGL.Shader" <| a <| u <| v
46 glTipe =
47 Env.get env Env.types . Lit.glTipeName
49 makeRec accessor baseRec =
50 let decls = accessor gltipe
51 in
52 if Map.size decls == 0
53 then baseRec
54 else record (Map.map (\t -> [glTipe t]) decls) baseRec
56 attribute = makeRec Lit.attribute attr
57 uniform = makeRec Lit.uniform unif
58 varying = makeRec Lit.varying (termN EmptyRecord1)
59 in
60 return (tipe === shaderTipe attribute uniform varying)
62 E.Var var ->
63 let name = V.toString var
64 in
65 return (if name == E.saveEnvName then CSaveEnv else name <? tipe)
67 E.Range lowExpr highExpr ->
68 existsNumber $ \n ->
69 do lowCon <- constrain env lowExpr n
70 highCon <- constrain env highExpr n
71 return $ CAnd [lowCon, highCon, list n === tipe]
73 E.ExplicitList exprs ->
74 constrainList env region exprs tipe
76 E.Binop op leftExpr rightExpr ->
77 constrainBinop env region op leftExpr rightExpr tipe
79 E.Lambda pattern body ->
80 exists $ \argType ->
81 exists $ \resType ->
82 do fragment <- Pattern.constrain env pattern argType
83 bodyCon <- constrain env body resType
84 let con =
85 ex (Fragment.vars fragment)
86 (CLet [monoscheme (Fragment.typeEnv fragment)]
87 (Fragment.typeConstraint fragment /\ bodyCon)
88 )
89 return $ con /\ tipe === (argType ==> resType)
91 E.App func@(A.A funcRegion _) arg@(A.A argRegion _) ->
92 do argVar <- variable Flexible
93 argCon <- constrain env arg (varN argVar)
95 funcVar <- variable Flexible
96 funcCon <- constrain env func (varN funcVar)
98 argVar' <- variable Flexible
99 resultVar <- variable Flexible
101 return $ ex [argVar,argVar',resultVar] $ CAnd $
102 [ argCon
103 , funcCon
104 , CEqual (Error.ExtraArgument funcRegion) region
105 (varN funcVar)
106 (varN argVar' ==> varN resultVar)
107 , CEqual (Error.BadArgument argRegion) region (varN argVar') (varN argVar)
108 , tipe === varN resultVar
109 ]
111 E.MultiIf branches ->
112 constrainIf env region branches tipe
114 E.Case expr branches ->
115 constrainCase env region expr branches tipe
117 E.Data name exprs ->
118 do vars <- Monad.forM exprs $ \_ -> variable Flexible
119 let pairs = zip exprs (map varN vars)
120 (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
121 return $ ex vars (cs /\ name <? ctipe)
122 where
123 step (t,c) (e,x) =
124 do c' <- constrain env e x
125 return (x ==> t, c /\ c')
127 E.Access expr label ->
128 exists $ \t ->
129 constrain env expr (record (Map.singleton label [tipe]) t)
131 E.Remove expr label ->
132 exists $ \t ->
133 constrain env expr (record (Map.singleton label [t]) tipe)
135 E.Insert expr label value ->
136 exists $ \valueType ->
137 exists $ \recordType ->
138 do valueCon <- constrain env value valueType
139 recordCon <- constrain env expr recordType
140 let newRecordType =
141 record (Map.singleton label [valueType]) recordType
142 return (CAnd [valueCon, recordCon, tipe === newRecordType])
144 E.Modify expr fields ->
145 exists $ \t ->
146 do oldVars <- Monad.forM fields $ \_ -> variable Flexible
147 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
148 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
150 newVars <- Monad.forM fields $ \_ -> variable Flexible
151 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
152 let cNew = tipe === record newFields t
154 cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
156 return $ cOld /\ ex newVars (CAnd (cNew : cs))
158 E.Record fields ->
159 do vars <- Monad.forM fields (\_ -> variable Flexible)
160 fieldCons <-
161 Monad.zipWithM
162 (constrain env)
163 (map snd fields)
164 (map varN vars)
165 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
166 let recordType = record fields' (termN EmptyRecord1)
167 return (ex vars (CAnd (fieldCons ++ [tipe === recordType])))
169 E.Let defs body ->
170 do bodyCon <- constrain env body tipe
172 (Info schemes rqs fqs headers c2 c1) <-
173 Monad.foldM
174 (constrainDef env)
175 (Info [] [] [] Map.empty CTrue CTrue)
176 (concatMap expandPattern defs)
178 let letScheme =
179 [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
181 return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
183 E.Port impl ->
184 case impl of
185 E.In _ _ ->
186 return CTrue
188 E.Out _ expr _ ->
189 constrain env expr tipe
191 E.Task _ expr _ ->
192 constrain env expr tipe
195-- CONSTRAIN BINOP
197constrainBinop
198 :: Env.Environment
199 -> R.Region
200 -> V.Canonical
201 -> Canonical.Expr
202 -> Canonical.Expr
203 -> Type
204 -> IO TypeConstraint
205constrainBinop env region op leftExpr@(A.A leftRegion _) rightExpr@(A.A rightRegion _) tipe =
206 do leftVar <- variable Flexible
207 rightVar <- variable Flexible
209 leftCon <- constrain env leftExpr (varN leftVar)
210 rightCon <- constrain env rightExpr (varN rightVar)
212 leftVar' <- variable Flexible
213 rightVar' <- variable Flexible
214 answerVar <- variable Flexible
216 let opType = varN leftVar' ==> varN rightVar' ==> varN answerVar
218 return $
219 ex [leftVar,rightVar,leftVar',rightVar',answerVar] $ CAnd $
220 [ leftCon
221 , rightCon
222 , CInstance region (V.toString op) opType
223 , CEqual (Error.BinopLeft op leftRegion) region (varN leftVar') (varN leftVar)
224 , CEqual (Error.BinopRight op rightRegion) region (varN rightVar') (varN rightVar)
225 , CEqual (Error.Binop op) region tipe (varN answerVar)
226 ]
229-- CONSTRAIN LISTS
231constrainList
232 :: Env.Environment
233 -> R.Region
234 -> [Canonical.Expr]
235 -> Type
236 -> IO TypeConstraint
237constrainList env region exprs tipe =
238 do (exprInfo, exprCons) <-
239 unzip <$> mapM elementConstraint exprs
241 (vars, cons) <- pairCons region Error.ListElement varToCon exprInfo
243 return $ ex vars (CAnd (exprCons ++ cons))
244 where
245 elementConstraint expr@(A.A region' _) =
246 do var <- variable Flexible
247 con <- constrain env expr (varN var)
248 return ( (var, region'), con )
250 varToCon var =
251 CEqual Error.List region tipe (Env.get env Env.types "List" <| varN var)
254-- CONSTRAIN IF EXPRESSIONS
256constrainIf
257 :: Env.Environment
258 -> R.Region
259 -> [(Canonical.Expr, Canonical.Expr)]
260 -> Type
261 -> IO TypeConstraint
262constrainIf env region branches tipe =
263 do (branchInfo, branchExprCons) <-
264 unzip <$> mapM constrainBranch branches
266 (vars,cons) <- branchCons branchInfo
268 return $ ex vars (CAnd (branchExprCons ++ cons))
269 where
270 bool = Env.get env Env.types "Bool"
272 constrainBranch (cond, expr@(A.A branchRegion _)) =
273 do branchVar <- variable Flexible
274 condCon <- constrain env cond bool
275 exprCon <- constrain env expr (varN branchVar)
276 return
277 ( (branchVar, branchRegion)
278 , condCon /\ exprCon
279 )
281 branchCons branchInfo =
282 case branchInfo of
283 [(thenVar, _), (elseVar, _)] ->
284 return
285 ( [thenVar,elseVar]
286 , [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
287 , varToCon thenVar
288 ]
289 )
291 _ ->
292 pairCons region Error.MultiIfBranch varToCon branchInfo
294 varToCon var =
295 CEqual Error.If region tipe (varN var)
298-- CONSTRAIN CASE EXPRESSIONS
300constrainCase
301 :: Env.Environment
302 -> R.Region
303 -> Canonical.Expr
304 -> [(P.CanonicalPattern, Canonical.Expr)]
305 -> Type
306 -> IO TypeConstraint
307constrainCase env region expr branches tipe =
308 do exprVar <- variable Flexible
309 exprCon <- constrain env expr (varN exprVar)
311 (branchInfo, branchExprCons) <-
312 unzip <$> mapM (branch (varN exprVar)) branches
314 (vars, cons) <- pairCons region Error.CaseBranch varToCon branchInfo
316 return $ ex (exprVar : vars) (CAnd (exprCon : branchExprCons ++ cons))
317 where
318 branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
319 do branchVar <- variable Flexible
320 fragment <- Pattern.constrain env pattern patternType
321 branchCon <- constrain env branchExpr (varN branchVar)
322 return
323 ( (branchVar, branchRegion)
324 , CLet [Fragment.toScheme fragment] branchCon
325 )
327 varToCon var =
328 CEqual Error.Case region tipe (varN var)
331-- COLLECT PAIRS
333data Pair = Pair
334 { _index :: Int
335 , _var1 :: Variable
336 , _var2 :: Variable
337 , _region :: R.Region
338 }
341pairCons
342 :: R.Region
343 -> (Int -> R.Region -> Error.Hint)
344 -> (Variable -> TypeConstraint)
345 -> [(Variable, R.Region)]
346 -> IO ([Variable], [TypeConstraint])
347pairCons region pairHint varToCon items =
348 let
349 pairToCon (Pair index var1 var2 subregion) =
350 CEqual (pairHint index subregion) region (varN var1) (varN var2)
351 in
352 case collectPairs 2 items of
353 Nothing ->
354 do var <- variable Flexible
355 return ([var], [varToCon var])
357 Just (pairs, var) ->
358 return (map fst items, map pairToCon pairs ++ [varToCon var])
361collectPairs :: Int -> [(Variable, R.Region)] -> Maybe ([Pair], Variable)
362collectPairs index items =
363 case items of
364 [] ->
365 Nothing
367 (var,_) : [] ->
368 Just ([], var)
370 (var,_) : rest@((var',region) : _) ->
371 do (pairs, summaryVar) <- collectPairs (index+1) rest
372 return (Pair index var var' region : pairs, summaryVar)
375-- EXPAND PATTERNS
377expandPattern :: Canonical.Def -> [Canonical.Def]
378expandPattern def@(Canonical.Definition lpattern expr maybeType) =
379 let (A.A patternRegion pattern) = lpattern
380 in
381 case pattern of
382 P.Var _ ->
383 [def]
385 _ ->
386 mainDef : map toDef vars
387 where
388 vars = P.boundVarList lpattern
390 combinedName = "$" ++ concat vars
392 pvar name =
393 A.A patternRegion (P.Var name)
395 localVar name =
396 A.A patternRegion (E.localVar name)
398 mainDef = Canonical.Definition (pvar combinedName) expr maybeType
400 toDef name =
401 let extract =
402 E.Case (localVar combinedName) [(lpattern, localVar name)]
403 in
404 Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
407-- CONSTRAIN DEFINITIONS
409data Info = Info
410 { iSchemes :: [TypeScheme]
411 , iRigid :: [Variable]
412 , iFlex :: [Variable]
413 , iHeaders :: Map.Map String (A.Located Type)
414 , iC2 :: TypeConstraint
415 , iC1 :: TypeConstraint
416 }
419constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
420constrainDef env info (Canonical.Definition (A.A patternRegion pattern) expr maybeTipe) =
421 let qs = [] -- should come from the def, but I'm not sure what would live there...
422 in
423 case (pattern, maybeTipe) of
424 (P.Var name, Just (A.A typeRegion tipe)) ->
425 constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe
427 (P.Var name, Nothing) ->
428 constrainUnannotatedDef env info qs patternRegion name expr
430 _ -> error ("problem in constrainDef with " ++ show pattern)
433constrainAnnotatedDef
434 :: Env.Environment
435 -> Info
436 -> [String]
437 -> R.Region
438 -> R.Region
439 -> String
440 -> Canonical.Expr
441 -> ST.Canonical
442 -> IO Info
443constrainAnnotatedDef env info qs patternRegion typeRegion name expr tipe =
444 do -- Some mistake may be happening here. Currently, qs is always [].
445 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
447 flexiVars <- Monad.forM qs (\_ -> variable Flexible)
449 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
451 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
453 (vars, typ) <- Env.instantiateType env tipe Map.empty
455 let scheme =
456 Scheme
457 { rigidQuantifiers = []
458 , flexibleQuantifiers = flexiVars ++ vars
459 , constraint = CTrue
460 , header = Map.singleton name (A.A patternRegion typ)
461 }
463 var <- variable Flexible
464 defCon <- constrain env' expr (varN var)
465 let annCon =
466 CEqual (Error.BadTypeAnnotation name) typeRegion typ (varN var)
468 return $ info
469 { iSchemes = scheme : iSchemes info
470 , iC1 = iC1 info /\ ex [var] (defCon /\ fl rigidVars annCon)
471 }
474constrainUnannotatedDef
475 :: Env.Environment
476 -> Info
477 -> [String]
478 -> R.Region
479 -> String
480 -> Canonical.Expr
481 -> IO Info
482constrainUnannotatedDef env info qs patternRegion name expr =
483 do -- Some mistake may be happening here. Currently, qs is always [].
484 rigidVars <- Monad.forM qs (\_ -> variable Rigid)
486 v <- variable Flexible
488 let tipe = varN v
490 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
492 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
494 con <- constrain env' expr tipe
496 return $ info
497 { iRigid = rigidVars ++ iRigid info
498 , iFlex = v : iFlex info
499 , iHeaders = Map.insert name (A.A patternRegion tipe) (iHeaders info)
500 , iC2 = con /\ iC2 info
501 }