@@ -3,212 +3,362 @@ module Type.Constrain.Expression where
4import Control.Applicative ((<$>))
4import Control.Applicative ((<$>))
5import qualified Control.Monad as Monad
5import qualified Control.Monad as Monad
6−import Control.Monad.Error
7import qualified Data.List as List
6import qualified Data.List as List
8import qualified Data.Map as Map
7import qualified Data.Map as Map
9−import Prelude hiding (and)
10−import qualified Text.PrettyPrint as PP
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
15import qualified AST.Expression.Canonical as Canonical
10import qualified AST.Expression.Canonical as Canonical
11+import qualified AST.Literal as Lit
16import qualified AST.Pattern as P
12import qualified AST.Pattern as P
17import qualified AST.Type as ST
13import qualified AST.Type as ST
18import qualified AST.Variable as V
14import qualified AST.Variable as V
19−import Type.Type hiding (Descriptor(..))
15+import qualified Reporting.Annotation as A
20−import qualified Type.Fragment as Fragment
16+import qualified Reporting.Error.Type as Error
21−import qualified Type.Environment as Env
17+import qualified Reporting.Region as R
22import qualified Type.Constrain.Literal as Literal
18import qualified Type.Constrain.Literal as Literal
23import qualified Type.Constrain.Pattern as Pattern
19import 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(..))
27 :: Env.Environment
26 :: Env.Environment
28 -> Canonical.Expr
27 -> Canonical.Expr
30− -> ErrorT [PP.Doc] IO TypeConstraint
29+ -> IO TypeConstraint
31−constrain env (A region expression) tipe =
30+constrain env (A.A region expression) tipe =
32 let list t = Env.get env Env.types "List" <| t
31 let list t = Env.get env Env.types "List" <| t
33− and = A region . CAnd
32+ (===) = CEqual Error.None region
34− true = A region CTrue
35− t1 === t2 = A region (CEqual t1 t2)
36− x <? t = A region (CInstance x t)
33+ (<?) = CInstance region
37− clet schemes c = A region (CLet schemes c)
39 case expression of
35 case expression of
40− Literal lit ->
36+ E.Literal lit ->
41− liftIO $ Literal.constrain env region lit tipe
37+ Literal.constrain env region lit tipe
43− GLShader _uid _src gltipe ->
39+ E.GLShader _uid _src gltipe ->
44 exists $ \attr ->
40 exists $ \attr ->
45 exists $ \unif ->
41 exists $ \unif ->
47− shaderTipe a u v = Env.get env Env.types "WebGL.Shader" <| a <| u <| v
44+ Env.get env Env.types "WebGL.Shader" <| a <| u <| v
48− glTipe = Env.get env Env.types . Lit.glTipeName
47+ Env.get env Env.types . Lit.glTipeName
49− makeRec accessor baseRec =
49+ makeRec accessor baseRec =
50− let decls = accessor gltipe
50+ let decls = accessor gltipe
51− in if Map.size decls == 0
52+ if Map.size decls == 0
52− then baseRec
53+ then baseRec
53− else record (Map.map (\t -> [glTipe t]) decls) baseRec
54+ else record (Map.map (\t -> [glTipe t]) decls) baseRec
54− attribute = makeRec Lit.attribute attr
56+ attribute = makeRec Lit.attribute attr
55− uniform = makeRec Lit.uniform unif
57+ uniform = makeRec Lit.uniform unif
56− varying = makeRec Lit.varying (termN EmptyRecord1)
58+ varying = makeRec Lit.varying (termN EmptyRecord1)
58− return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
60+ return (tipe === shaderTipe attribute uniform varying)
60− Var var
62+ E.Var var ->
63+ let name = V.toString var
61− | name == saveEnvName -> return (A region CSaveEnv)
65+ return (if name == E.saveEnvName then CSaveEnv else name <? tipe)
62− | otherwise -> return (name <? tipe)
64− name = V.toString var
66− Range lo hi ->
67+ E.Range lowExpr highExpr ->
67 existsNumber $ \n ->
68 existsNumber $ \n ->
68− do clo <- constrain env lo n
69+ do lowCon <- constrain env lowExpr n
69− chi <- constrain env hi n
70+ highCon <- constrain env highExpr n
70− return $ and [clo, chi, list n === tipe]
71+ return $ CAnd [lowCon, highCon, list n === tipe]
72− ExplicitList exprs ->
73+ E.ExplicitList exprs ->
73− exists $ \x ->
74+ constrainList env region exprs tipe
74− do constraints <- mapM (\e -> constrain env e x) exprs
75+
75− return . and $ list x === tipe : constraints
76+ E.Binop op leftExpr rightExpr ->
78− exists $ \t1 ->
77+ exists $ \leftType ->
79− exists $ \t2 ->
78+ exists $ \rightType ->
80− do c1 <- constrain env e1 t1
79+ do leftCon <- constrain env leftExpr leftType
81− c2 <- constrain env e2 t2
80+ rightCon <- constrain env rightExpr rightType
82− return $ and [ c1, c2, V.toString op <? (t1 ==> t2 ==> tipe) ]
84+ , V.toString op <? (leftType ==> rightType ==> tipe)
84− Lambda p e ->
87+ E.Lambda pattern body ->
85− exists $ \t1 ->
88+ exists $ \argType ->
86− exists $ \t2 ->
89+ exists $ \resType ->
87− do fragment <- try region $ Pattern.constrain env p t1
90+ do fragment <- Pattern.constrain env pattern argType
88− c2 <- constrain env e t2
91+ bodyCon <- constrain env body resType
89− let c = ex (Fragment.vars fragment)
93+ ex (Fragment.vars fragment)
90− (clet [monoscheme (Fragment.typeEnv fragment)]
94+ (CLet [monoscheme (Fragment.typeEnv fragment)]
91− (Fragment.typeConstraint fragment /\ c2)
95+ (Fragment.typeConstraint fragment /\ bodyCon)
93− return $ c /\ tipe === (t1 ==> t2)
97+ return $ con /\ tipe === (argType ==> resType)
95− App e1 e2 ->
99+ E.App func arg ->
96− exists $ \t ->
100+ do argVar <- variable Flexible
101+ resultVar <- variable Flexible
97− do c1 <- constrain env e1 (t ==> tipe)
102+ argCon <- constrain env arg (varN argVar)
98− c2 <- constrain env e2 t
103+ funcCon <- constrain env func (varN argVar ==> varN resultVar)
104+ let appCon = tipe === varN resultVar
99− return $ c1 /\ c2
105+ return $
100−
106+ ex [argVar,resultVar] (CAnd [ argCon, funcCon, appCon ])
101− MultiIf branches ->
108+ E.MultiIf branches ->
102− and <$> mapM constrain' branches
109+ constrainIf env region branches tipe
104− bool = Env.get env Env.types "Bool"
106− constrain' (cond, expr) =
107− do cb <- constrain env cond bool
108− ce <- constrain env expr tipe
111− Case expr branches ->
111+ E.Case expr branches ->
112− exists $ \t ->
112+ constrainCase env region expr branches tipe
113− do ce <- constrain env expr t
113+
114− and . (:) ce <$> mapM (branch t) branches
116− branch t (pattern, branchExpr) =
117− do fragment <- try region $ Pattern.constrain env pattern t
118− clet [Fragment.toScheme fragment] <$> constrain env branchExpr tipe
120− Data name exprs ->
114+ E.Data name exprs ->
121− do vars <- forM exprs $ \_ -> liftIO (variable Flexible)
115+ do vars <- Monad.forM exprs $ \_ -> variable Flexible
122 let pairs = zip exprs (map varN vars)
116 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)
124 return $ ex vars (cs /\ name <? ctipe)
118 return $ ex vars (cs /\ name <? ctipe)
126 step (t,c) (e,x) =
120 step (t,c) (e,x) =
127 do c' <- constrain env e x
121 do c' <- constrain env e x
128 return (x ==> t, c /\ c')
122 return (x ==> t, c /\ c')
130− Access expr label ->
124+ E.Access expr label ->
131 exists $ \t ->
125 exists $ \t ->
132 constrain env expr (record (Map.singleton label [tipe]) t)
126 constrain env expr (record (Map.singleton label [tipe]) t)
134− Remove expr label ->
128+ E.Remove expr label ->
135 exists $ \t ->
129 exists $ \t ->
136 constrain env expr (record (Map.singleton label [t]) tipe)
130 constrain env expr (record (Map.singleton label [t]) tipe)
138− Insert expr label value ->
132+ E.Insert expr label value ->
139− exists $ \tVal ->
133+ exists $ \valueType ->
140− exists $ \tRec ->
134+ exists $ \recordType ->
141− do cVal <- constrain env value tVal
135+ do valueCon <- constrain env value valueType
142− cRec <- constrain env expr tRec
136+ recordCon <- constrain env expr recordType
143− let c = tipe === record (Map.singleton label [tVal]) tRec
138+ record (Map.singleton label [valueType]) recordType
144− return (and [cVal, cRec, c])
139+ return (CAnd [valueCon, recordCon, tipe === newRecordType])
146− Modify expr fields ->
141+ E.Modify expr fields ->
147 exists $ \t ->
142 exists $ \t ->
148− do oldVars <- forM fields $ \_ -> liftIO (variable Flexible)
143+ do oldVars <- Monad.forM fields $ \_ -> variable Flexible
149 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
144 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
150 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
145 cOld <- ex oldVars <$> constrain env expr (record oldFields t)
152− newVars <- forM fields $ \_ -> liftIO (variable Flexible)
147+ newVars <- Monad.forM fields $ \_ -> variable Flexible
153 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
148 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
154 let cNew = tipe === record newFields t
149 let cNew = tipe === record newFields t
156− cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
151+ cs <- Monad.zipWithM (constrain env) (map snd fields) (map varN newVars)
158− return $ cOld /\ ex newVars (and (cNew : cs))
153+ return $ cOld /\ ex newVars (CAnd (cNew : cs))
160− Record fields ->
155+ E.Record fields ->
161− do vars <- forM fields $ \_ -> liftIO (variable Flexible)
156+ do vars <- Monad.forM fields (\_ -> variable Flexible)
162− cs <- zipWithM (constrain env) (map snd fields) (map varN vars)
159+ (constrain env)
163 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
162 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
164 let recordType = record fields' (termN EmptyRecord1)
163 let recordType = record fields' (termN EmptyRecord1)
165− return . ex vars . and $ tipe === recordType : cs
164+ return (ex vars (CAnd (fieldCons ++ [tipe === recordType])))
167− Let defs body ->
166+ E.Let defs body ->
168− do c <- constrain env body tipe
167+ do bodyCon <- constrain env body tipe
170 (Info schemes rqs fqs headers c2 c1) <-
169 (Info schemes rqs fqs headers c2 c1) <-
171 Monad.foldM
170 Monad.foldM
172 (constrainDef env)
171 (constrainDef env)
173− (Info [] [] [] Map.empty true true)
172+ (Info [] [] [] Map.empty CTrue CTrue)
174 (concatMap expandPattern defs)
173 (concatMap expandPattern defs)
176− let letScheme = [ Scheme rqs fqs (clet [monoscheme headers] c2) headers ]
175+ let letScheme = [ Scheme rqs fqs (CLet [monoscheme headers] c2) headers ]
178− return $ clet schemes (clet letScheme (c1 /\ c))
177+ return $ CLet schemes (CLet letScheme (c1 /\ bodyCon))
180− Port impl ->
179+ E.Port impl ->
181 case impl of
180 case impl of
182− In _ _ ->
181+ E.In _ _ ->
183− return true
182+ return CTrue
185− Out _ expr _ ->
184+ E.Out _ expr _ ->
186 constrain env expr tipe
185 constrain env expr tipe
188− Task _ expr _ ->
187+ E.Task _ expr _ ->
189 constrain env expr tipe
188 constrain env expr tipe
198+ -> IO TypeConstraint
199+constrainList env region exprs tipe =
200+ do (exprInfo, exprCons) <-
201+ unzip <$> mapM elementConstraint exprs
203+ let pairwiseCons = pairwiseConstraints 2 exprInfo
206+ ex (map fst exprInfo)
207+ (CAnd (exprCons ++ pairwiseCons))
210+ Env.get env Env.types "List" <| t
212+ elementConstraint expr@(A.A region' _) =
213+ do var <- variable Flexible
214+ con <- constrain env expr (varN var)
215+ return ( (var, region'), con )
217+ pairwiseConstraints n exprInfo =
223+ [ CEqual Error.List region tipe (list (varN var)) ]
225+ (var,_) : (var',region') : rest ->
227+ hint = Error.ListElement n region'
228+ con = CEqual hint region (varN var) (varN var')
230+ con : pairwiseConstraints (n+1) ((var', region') : rest)
233+-- CONSTRAIN IF EXPRESSIONS
238+ -> [(Canonical.Expr, Canonical.Expr)]
240+ -> IO TypeConstraint
241+constrainIf env region branches tipe =
242+ do (branchInfo, branchExprCons) <-
243+ unzip <$> mapM constrainBranch branches
246+ ex (map fst branchInfo)
247+ (CAnd (branchExprCons ++ branchCons branchInfo))
249+ bool = Env.get env Env.types "Bool"
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)
256+ ( (branchVar, branchRegion)
257+ , condCon /\ exprCon
260+ branchCons branchInfo =
262+ [(thenVar, _), (elseVar, _)] ->
263+ [ CEqual Error.IfBranches region (varN thenVar) (varN elseVar)
264+ , CEqual Error.If region tipe (varN thenVar)
268+ buildBranchCons 2 branchInfo
270+ buildBranchCons n branchInfo =
276+ [ CEqual Error.If region tipe (varN var) ]
278+ (var,_) : (var',region') : rest ->
280+ hint = Error.MultiIfBranch n region'
281+ con = CEqual hint region (varN var) (varN var')
283+ con : buildBranchCons (n+1) ((var', region') : rest)
286+-- CONSTRAIN CASE EXPRESSIONS
292+ -> [(P.CanonicalPattern, Canonical.Expr)]
294+ -> IO TypeConstraint
295+constrainCase env region expr branches tipe =
296+ do exprVar <- variable Flexible
298+ exprCon <- constrain env expr (varN exprVar)
300+ (branchInfo, branchExprCons) <-
301+ unzip <$> mapM (branch (varN exprVar)) branches
304+ ex (exprVar : map fst branchInfo)
305+ (CAnd (exprCon : branchExprCons ++ branchCons 2 branchInfo))
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)
312+ ( (branchVar, branchRegion)
313+ , CLet [Fragment.toScheme fragment] branchCon
316+ branchCons n branchInfo =
322+ [ CEqual Error.Case region tipe (varN var) ]
324+ (var,_) : (var',region') : rest ->
326+ hint = Error.CaseBranch n region'
327+ con = CEqual hint region (varN var) (varN var')
329+ con : branchCons (n+1) ((var', region') : rest)
192expandPattern :: Canonical.Def -> [Canonical.Def]
334expandPattern :: Canonical.Def -> [Canonical.Def]
193−expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =
335+expandPattern def@(Canonical.Definition lpattern expr maybeType) =
336+ let (A.A patternRegion pattern) = lpattern
194− case pattern of
338+ case pattern of
195− P.Var _ ->
339+ P.Var _ ->
198− Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars
343+ mainDef : map toDef vars
200− vars = P.boundVarList pattern
345+ vars = P.boundVarList lpattern
201− x = "$" ++ concat vars
347+ combinedName = "$" ++ concat vars
350+ A.A patternRegion (P.Var name)
202− mkVar = A r . localVar
352+ localVar name =
203− toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
353+ A.A patternRegion (E.localVar name)
205−
355+ mainDef = Canonical.Definition (pvar combinedName) expr maybeType
206−try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
356+
207−try region computation =
357+ toDef name =
208− do result <- liftIO $ runErrorT computation
358+ let extract =
209− case result of
359+ E.Case (localVar combinedName) [(lpattern, localVar name)]
210− Left err -> throwError [err region]
360+ in
211− Right value -> return value
361+ Canonical.Definition (pvar name) (A.A patternRegion extract) Nothing
214-- CONSTRAIN DEFINITIONS
364-- CONSTRAIN DEFINITIONS
@@ -223,8 +373,8 @@ data Info = Info
226−constrainDef :: Env.Environment -> Info -> Canonical.Def -> ErrorT [PP.Doc] IO Info
376+constrainDef :: Env.Environment -> Info -> Canonical.Def -> IO Info
227−constrainDef env info (Canonical.Definition pattern expr maybeTipe) =
377+constrainDef env info (Canonical.Definition (A.A _ pattern) expr maybeTipe) =
228 let qs = [] -- should come from the def, but I'm not sure what would live there...
378 let qs = [] -- should come from the def, but I'm not sure what would live there...
230 case (pattern, maybeTipe) of
380 case (pattern, maybeTipe) of
@@ -243,13 +393,13 @@ constrainAnnotatedDef
243 -> [String]
393 -> [String]
244 -> String
394 -> String
245 -> Canonical.Expr
395 -> Canonical.Expr
246− -> ST.CanonicalType
396+ -> ST.Canonical
247− -> ErrorT [PP.Doc] IO Info
397+ -> IO Info
248constrainAnnotatedDef env info qs name expr tipe =
398constrainAnnotatedDef env info qs name expr tipe =
249 do -- Some mistake may be happening here. Currently, qs is always [].
399 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)
252− flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)
402+ flexiVars <- Monad.forM qs (\_ -> variable Flexible)
254 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
404 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
@@ -261,7 +411,7 @@ constrainAnnotatedDef env info qs name expr tipe =
262 { rigidQuantifiers = []
412 { rigidQuantifiers = []
263 , flexibleQuantifiers = flexiVars ++ vars
413 , flexibleQuantifiers = flexiVars ++ vars
264− , constraint = Ann.noneNoDocs CTrue
414+ , constraint = CTrue
265 , header = Map.singleton name typ
415 , header = Map.singleton name typ
@@ -279,12 +429,12 @@ constrainUnannotatedDef
279 -> [String]
429 -> [String]
280 -> String
430 -> String
281 -> Canonical.Expr
431 -> Canonical.Expr
282− -> ErrorT [PP.Doc] IO Info
432+ -> IO Info
283constrainUnannotatedDef env info qs name expr =
433constrainUnannotatedDef env info qs name expr =
284 do -- Some mistake may be happening here. Currently, qs is always [].
434 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)
287− v <- liftIO $ variable Flexible
437+ v <- variable Flexible
289 let tipe = varN v
439 let tipe = varN v