@@ -3,212 +3,362 @@ module Type.Constrain.Expression where
33
44import Control.Applicative ((<$>))
55import qualified Control.Monad as Monad
6−import Control.Monad.Error
76import qualified Data.List as List
87import qualified Data.Map as Map
9−import Prelude hiding (and)
10−import qualified Text.PrettyPrint as PP
118
12−import qualified AST.Literal as Lit
13−import AST.Annotation as Ann
14−import AST.Expression.General
9+import qualified AST.Expression.General as E
1510import qualified AST.Expression.Canonical as Canonical
11+import qualified AST.Literal as Lit
1612import qualified AST.Pattern as P
1713import qualified AST.Type as ST
1814import qualified AST.Variable as V
19−import Type.Type hiding (Descriptor(..))
20−import qualified Type.Fragment as Fragment
21−import qualified Type.Environment as Env
15+import qualified Reporting.Annotation as A
16+import qualified Reporting.Error.Type as Error
17+import qualified Reporting.Region as R
2218import qualified Type.Constrain.Literal as Literal
2319import qualified Type.Constrain.Pattern as Pattern
20+import qualified Type.Environment as Env
21+import qualified Type.Fragment as Fragment
22+import Type.Type hiding (Descriptor(..))
2423
2524
2625constrain
2726 :: Env.Environment
2827 -> Canonical.Expr
2928 -> Type
30− -> ErrorT [PP.Doc] IO TypeConstraint
31−constrain env (A region expression) tipe =
29+ -> IO TypeConstraint
30+constrain env (A.A region expression) tipe =
3231 let list t = Env.get env Env.types "List" <| t
33− and = A region . CAnd
34− true = A region CTrue
35− t1 === t2 = A region (CEqual t1 t2)
36− x <? t = A region (CInstance x t)
37− clet schemes c = A region (CLet schemes c)
32+ (===) = CEqual Error.None region
33+ (<?) = CInstance region
3834 in
3935 case expression of
40− Literal lit ->
41− liftIO $ Literal.constrain env region lit tipe
36+ E.Literal lit ->
37+ Literal.constrain env region lit tipe
4238
43− GLShader _uid _src gltipe ->
39+ E.GLShader _uid _src gltipe ->
4440 exists $ \attr ->
4541 exists $ \unif ->
4642 let
47− shaderTipe a u v = Env.get env Env.types "WebGL.Shader" <| a <| u <| v
48− glTipe = Env.get env Env.types . Lit.glTipeName
49− makeRec accessor baseRec =
50− let decls = accessor gltipe
51− in if Map.size decls == 0
52− then baseRec
53− else record (Map.map (\t -> [glTipe t]) decls) baseRec
54− attribute = makeRec Lit.attribute attr
55− uniform = makeRec Lit.uniform unif
56− varying = makeRec Lit.varying (termN EmptyRecord1)
43+ shaderTipe a u v =
44+ Env.get env Env.types "WebGL.Shader" <| a <| u <| v
45+
46+ glTipe =
47+ Env.get env Env.types . Lit.glTipeName
48+
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
55+
56+ attribute = makeRec Lit.attribute attr
57+ uniform = makeRec Lit.uniform unif
58+ varying = makeRec Lit.varying (termN EmptyRecord1)
5759 in
58− return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
60+ return (tipe === shaderTipe attribute uniform varying)
5961
60− Var var
61− | name == saveEnvName -> return (A region CSaveEnv)
62− | otherwise -> return (name <? tipe)
63− where
64− name = V.toString var
62+ E.Var var ->
63+ let name = V.toString var
64+ in
65+ return (if name == E.saveEnvName then CSaveEnv else name <? tipe)
6566
66− Range lo hi ->
67+ E.Range lowExpr highExpr ->
6768 existsNumber $ \n ->
68− do clo <- constrain env lo n
69− chi <- constrain env hi n
70− return $ and [clo, chi, list n === tipe]
71−
72− ExplicitList exprs ->
73− exists $ \x ->
74− do constraints <- mapM (\e -> constrain env e x) exprs
75− return . and $ list x === tipe : constraints
76−
77− Binop op e1 e2 ->
78− exists $ \t1 ->
79− exists $ \t2 ->
80− do c1 <- constrain env e1 t1
81− c2 <- constrain env e2 t2
82− return $ and [ c1, c2, V.toString op <? (t1 ==> t2 ==> tipe) ]
83−
84− Lambda p e ->
85− exists $ \t1 ->
86− exists $ \t2 ->
87− do fragment <- try region $ Pattern.constrain env p t1
88− c2 <- constrain env e t2
89− let c = ex (Fragment.vars fragment)
90− (clet [monoscheme (Fragment.typeEnv fragment)]
91− (Fragment.typeConstraint fragment /\ c2)
92− )
93− return $ c /\ tipe === (t1 ==> t2)
94−
95− App e1 e2 ->
96− exists $ \t ->
97− do c1 <- constrain env e1 (t ==> tipe)
98− c2 <- constrain env e2 t
99− return $ c1 /\ c2
100−
101− MultiIf branches ->
102− and <$> mapM constrain' branches
103− where
104− bool = Env.get env Env.types "Bool"
105−
106− constrain' (cond, expr) =
107− do cb <- constrain env cond bool
108− ce <- constrain env expr tipe
109− return (cb /\ ce)
110−
111− Case expr branches ->
112− exists $ \t ->
113− do ce <- constrain env expr t
114− and . (:) ce <$> mapM (branch t) branches
115− where
116− branch t (pattern, branchExpr) =
117− do fragment <- try region $ Pattern.constrain env pattern t
118− clet [Fragment.toScheme fragment] <$> constrain env branchExpr tipe
119−
120− Data name exprs ->
121− do vars <- forM exprs $ \_ -> liftIO (variable Flexible)
69+ do lowCon <- constrain env lowExpr n
70+ highCon <- constrain env highExpr n
71+ return $ CAnd [lowCon, highCon, list n === tipe]
72+
73+ E.ExplicitList exprs ->
74+ constrainList env region exprs tipe
75+
76+ E.Binop op leftExpr rightExpr ->
77+ exists $ \leftType ->
78+ exists $ \rightType ->
79+ do leftCon <- constrain env leftExpr leftType
80+ rightCon <- constrain env rightExpr rightType
81+ return $ CAnd
82+ [ leftCon
83+ , rightCon
84+ , V.toString op <? (leftType ==> rightType ==> tipe)
85+ ]
86+
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 /\ tipe === (argType ==> resType)
98+
99+ E.App func arg ->
100+ do argVar <- variable Flexible
101+ resultVar <- variable Flexible
102+ argCon <- constrain env arg (varN argVar)
103+ funcCon <- constrain env func (varN argVar ==> varN resultVar)
104+ let appCon = tipe === varN resultVar
105+ return $
106+ ex [argVar,resultVar] (CAnd [ argCon, funcCon, appCon ])
107+
108+ E.MultiIf branches ->
109+ constrainIf env region branches tipe
110+
111+ E.Case expr branches ->
112+ constrainCase env region expr branches tipe
113+
114+ E.Data name exprs ->
115+ do vars <- Monad.forM exprs $ \_ -> variable Flexible
122116 let pairs = zip exprs (map varN vars)
123− (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
117+ (ctipe, cs) <- Monad.foldM step (tipe, CTrue) (reverse pairs)
124118 return $ ex vars (cs /\ name <? ctipe)
125119 where
126120 step (t,c) (e,x) =
127121 do c' <- constrain env e x
128122 return (x ==> t, c /\ c')
129123
130− Access expr label ->
124+ E.Access expr label ->
131125 exists $ \t ->
132126 constrain env expr (record (Map.singleton label [tipe]) t)
133127
134− Remove expr label ->
128+ E.Remove expr label ->
135129 exists $ \t ->
136130 constrain env expr (record (Map.singleton label [t]) tipe)
137131
138− Insert expr label value ->
139− exists $ \tVal ->
140− exists $ \tRec ->
141− do cVal <- constrain env value tVal
142− cRec <- constrain env expr tRec
143− let c = tipe === record (Map.singleton label [tVal]) tRec
144− return (and [cVal, cRec, c])
132+ E.Insert expr label value ->
133+ exists $ \valueType ->
134+ exists $ \recordType ->
135+ do valueCon <- constrain env value valueType
136+ recordCon <- constrain env expr recordType
137+ let newRecordType =
138+ record (Map.singleton label [valueType]) recordType
139+ return (CAnd [valueCon, recordCon, tipe === newRecordType])
145140
146− Modify expr fields ->
141+ E.Modify expr fields ->
147142 exists $ \t ->
148− do oldVars <- forM fields $ \_ -> liftIO (variable Flexible)
143+ do oldVars <- Monad.forM fields $ \_ -> variable Flexible
149144 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
150145 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
151146
152− newVars <- forM fields $ \_ -> liftIO (variable Flexible)
147+ newVars <- Monad.forM fields $ \_ -> variable Flexible
153148 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
154149 let cNew = tipe === record newFields t
155150
156− cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
151+ cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
157152
158− return $ cOld /\ ex newVars (and (cNew : cs))
153+ return $ cOld /\ ex newVars (CAnd (cNew : cs))
159154
160− Record fields ->
161− do vars <- forM fields $ \_ -> liftIO (variable Flexible)
162− cs <- zipWithM (constrain env) (map snd fields) (map varN vars)
155+ E.Record fields ->
156+ do vars <- Monad.forM fields (\_ -> variable Flexible)
157+ fieldCons <-
158+ Monad.zipWithM
159+ (constrain env)
160+ (map snd fields)
161+ (map varN vars)
163162 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
164163 let recordType = record fields' (termN EmptyRecord1)
165− return . ex vars . and $ tipe === recordType : cs
164+ return (ex vars (CAnd (fieldCons ++ [tipe === recordType])))
166165
167− Let defs body ->
168− do c <- constrain env body tipe
166+ E.Let defs body ->
167+ do bodyCon <- constrain env body tipe
169168
170169 (Info schemes rqs fqs headers c2 c1) <-
171170 Monad.foldM
172171 (constrainDef env)
173− (Info [] [] [] Map.empty true true)
172+ (Info [] [] [] Map.empty CTrue CTrue)
174173 (concatMap expandPattern defs)
175174
176− let letScheme = [ Scheme rqs fqs (clet [monoscheme headers] c2) headers ]
175+ let letScheme = [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
177176
178− return $ clet schemes (clet letScheme (c1 /\ c))
177+ return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
179178
180− Port impl ->
179+ E.Port impl ->
181180 case impl of
182− In _ _ ->
183− return true
181+ E.In _ _ ->
182+ return CTrue
184183
185− Out _ expr _ ->
184+ E.Out _ expr _ ->
186185 constrain env expr tipe
187186
188− Task _ expr _ ->
187+ E.Task _ expr _ ->
189188 constrain env expr tipe
190189
191190
191+-- CONSTRAIN LISTS
192+
193+constrainList
194+ :: Env.Environment
195+ -> R.Region
196+ -> [Canonical.Expr]
197+ -> Type
198+ -> IO TypeConstraint
199+constrainList env region exprs tipe =
200+ do (exprInfo, exprCons) <-
201+ unzip <$> mapM elementConstraint exprs
202+
203+ let pairwiseCons = pairwiseConstraints 2 exprInfo
204+
205+ return $
206+ ex (map fst exprInfo)
207+ (CAnd (exprCons ++ pairwiseCons))
208+ where
209+ list t =
210+ Env.get env Env.types "List" <| t
211+
212+ elementConstraint expr@(A.A region' _) =
213+ do var <- variable Flexible
214+ con <- constrain env expr (varN var)
215+ return ( (var, region'), con )
216+
217+ pairwiseConstraints n exprInfo =
218+ case exprInfo of
219+ [] ->
220+ []
221+
222+ (var,_) : [] ->
223+ [ CEqual Error.List region tipe (list (varN var)) ]
224+
225+ (var,_) : (var',region') : rest ->
226+ let
227+ hint = Error.ListElement n region'
228+ con = CEqual hint region (varN var) (varN var')
229+ in
230+ con : pairwiseConstraints (n+1) ((var', region') : rest)
231+
232+
233+-- CONSTRAIN IF EXPRESSIONS
234+
235+constrainIf
236+ :: Env.Environment
237+ -> R.Region
238+ -> [(Canonical.Expr, Canonical.Expr)]
239+ -> Type
240+ -> IO TypeConstraint
241+constrainIf env region branches tipe =
242+ do (branchInfo, branchExprCons) <-
243+ unzip <$> mapM constrainBranch branches
244+
245+ return $
246+ ex (map fst branchInfo)
247+ (CAnd (branchExprCons ++ branchCons branchInfo))
248+ where
249+ bool = Env.get env Env.types "Bool"
250+
251+ constrainBranch (cond, expr@(A.A branchRegion _)) =
252+ do branchVar <- variable Flexible
253+ condCon <- constrain env cond bool
254+ exprCon <- constrain env expr (varN branchVar)
255+ return
256+ ( (branchVar, branchRegion)
257+ , condCon /\ exprCon
258+ )
259+
260+ branchCons branchInfo =
261+ case branchInfo of
262+ [(thenVar, _), (elseVar, _)] ->
263+ [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
264+ , CEqual Error.If region tipe (varN thenVar)
265+ ]
266+
267+ _ ->
268+ buildBranchCons 2 branchInfo
269+
270+ buildBranchCons n branchInfo =
271+ case branchInfo of
272+ [] ->
273+ []
274+
275+ (var,_) : [] ->
276+ [ CEqual Error.If region tipe (varN var) ]
277+
278+ (var,_) : (var',region') : rest ->
279+ let
280+ hint = Error.MultiIfBranch n region'
281+ con = CEqual hint region (varN var) (varN var')
282+ in
283+ con : buildBranchCons (n+1) ((var', region') : rest)
284+
285+
286+-- CONSTRAIN CASE EXPRESSIONS
287+
288+constrainCase
289+ :: Env.Environment
290+ -> R.Region
291+ -> Canonical.Expr
292+ -> [(P.CanonicalPattern, Canonical.Expr)]
293+ -> Type
294+ -> IO TypeConstraint
295+constrainCase env region expr branches tipe =
296+ do exprVar <- variable Flexible
297+
298+ exprCon <- constrain env expr (varN exprVar)
299+
300+ (branchInfo, branchExprCons) <-
301+ unzip <$> mapM (branch (varN exprVar)) branches
302+
303+ return $
304+ ex (exprVar : map fst branchInfo)
305+ (CAnd (exprCon : branchExprCons ++ branchCons 2 branchInfo))
306+ where
307+ branch patternType (pattern, branchExpr@(A.A branchRegion _)) =
308+ do branchVar <- variable Flexible
309+ fragment <- Pattern.constrain env pattern patternType
310+ branchCon <- constrain env branchExpr (varN branchVar)
311+ return
312+ ( (branchVar, branchRegion)
313+ , CLet [Fragment.toScheme fragment] branchCon
314+ )
315+
316+ branchCons n branchInfo =
317+ case branchInfo of
318+ [] ->
319+ []
320+
321+ (var,_) : [] ->
322+ [ CEqual Error.Case region tipe (varN var) ]
323+
324+ (var,_) : (var',region') : rest ->
325+ let
326+ hint = Error.CaseBranch n region'
327+ con = CEqual hint region (varN var) (varN var')
328+ in
329+ con : branchCons (n+1) ((var', region') : rest)
330+
331+
332+-- EXPAND PATTERNS
333+
192334expandPattern :: Canonical.Def -> [Canonical.Def]
193−expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =
194− case pattern of
195− P.Var _ ->
196− [def]
197− _ ->
198− Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars
199− where
200− vars = P.boundVarList pattern
201− x = "$" ++ concat vars
202− mkVar = A r . localVar
203− toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
204−
205−
206−try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
207−try region computation =
208− do result <- liftIO $ runErrorT computation
209− case result of
210− Left err -> throwError [err region]
211− Right value -> return value
335+expandPattern def@(Canonical.Definition lpattern expr maybeType) =
336+ let (A.A patternRegion pattern) = lpattern
337+ in
338+ case pattern of
339+ P.Var _ ->
340+ [def]
341+
342+ _ ->
343+ mainDef : map toDef vars
344+ where
345+ vars = P.boundVarList lpattern
346+
347+ combinedName = "$" ++ concat vars
348+
349+ pvar name =
350+ A.A patternRegion (P.Var name)
351+
352+ localVar name =
353+ A.A patternRegion (E.localVar name)
354+
355+ mainDef = Canonical.Definition (pvar combinedName) expr maybeType
356+
357+ toDef name =
358+ let extract =
359+ E.Case (localVar combinedName) [(lpattern, localVar name)]
360+ in
361+ Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
212362
213363
214364-- CONSTRAIN DEFINITIONS
@@ -223,8 +373,8 @@ data Info = Info
223373 }
224374
225375
226−constrainDef :: Env.Environment -> Info -> Canonical.Def -> ErrorT [PP.Doc] IO Info
227−constrainDef env info (Canonical.Definition pattern expr maybeTipe) =
376+constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
377+constrainDef env info (Canonical.Definition (A.A _ pattern) expr maybeTipe) =
228378 let qs = [] -- should come from the def, but I'm not sure what would live there...
229379 in
230380 case (pattern, maybeTipe) of
@@ -243,13 +393,13 @@ constrainAnnotatedDef
243393 -> [String]
244394 -> String
245395 -> Canonical.Expr
246− -> ST.CanonicalType
247− -> ErrorT [PP.Doc] IO Info
396+ -> ST.Canonical
397+ -> IO Info
248398constrainAnnotatedDef env info qs name expr tipe =
249399 do -- Some mistake may be happening here. Currently, qs is always [].
250− rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)
400+ rigidVars <- Monad.forM qs (\_ -> variable Rigid)
251401
252− flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)
402+ flexiVars <- Monad.forM qs (\_ -> variable Flexible)
253403
254404 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
255405
@@ -261,7 +411,7 @@ constrainAnnotatedDef env info qs name expr tipe =
261411 Scheme
262412 { rigidQuantifiers = []
263413 , flexibleQuantifiers = flexiVars ++ vars
264− , constraint = Ann.noneNoDocs CTrue
414+ , constraint = CTrue
265415 , header = Map.singleton name typ
266416 }
267417
@@ -279,12 +429,12 @@ constrainUnannotatedDef
279429 -> [String]
280430 -> String
281431 -> Canonical.Expr
282− -> ErrorT [PP.Doc] IO Info
432+ -> IO Info
283433constrainUnannotatedDef env info qs name expr =
284434 do -- Some mistake may be happening here. Currently, qs is always [].
285− rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)
435+ rigidVars <- Monad.forM qs (\_ -> variable Rigid)
286436
287− v <- liftIO $ variable Flexible
437+ v <- variable Flexible
288438
289439 let tipe = varN v
290440