@@ -1,3 +1,4 @@
1+{-# OPTIONS_GHC -Wall #-}
12module Type.Constrain.Expression where
23
34import Control.Applicative ((<$>))
@@ -5,9 +6,10 @@ import qualified Control.Monad as Monad
56import Control.Monad.Error
67import qualified Data.List as List
78import qualified Data.Map as Map
9+import Prelude hiding (and)
810import qualified Text.PrettyPrint as PP
911
10−import AST.Literal as Lit
12+import qualified AST.Literal as Lit
1113import AST.Annotation as Ann
1214import AST.Expression.General
1315import qualified AST.Expression.Canonical as Canonical
@@ -15,7 +17,7 @@ import qualified AST.Pattern as P
1517import qualified AST.Type as ST
1618import qualified AST.Variable as V
1719import Type.Type hiding (Descriptor(..))
18−import Type.Fragment
20+import qualified Type.Fragment as Fragment
1921import qualified Type.Environment as Env
2022import qualified Type.Constrain.Literal as Literal
2123import qualified Type.Constrain.Pattern as Pattern
@@ -26,7 +28,7 @@ constrain
2628 -> Canonical.Expr
2729 -> Type
2830 -> ErrorT [PP.Doc] IO TypeConstraint
29−constrain env (A region expr) tipe =
31+constrain env (A region expression) tipe =
3032 let list t = Env.get env Env.types "List" <| t
3133 and = A region . CAnd
3234 true = A region CTrue
@@ -34,8 +36,9 @@ constrain env (A region expr) tipe =
3436 x <? t = A region (CInstance x t)
3537 clet schemes c = A region (CLet schemes c)
3638 in
37− case expr of
38− Literal lit -> liftIO $ Literal.constrain env region lit tipe
39+ case expression of
40+ Literal lit ->
41+ liftIO $ Literal.constrain env region lit tipe
3942
4043 GLShader _uid _src gltipe ->
4144 exists $ \attr ->
@@ -51,7 +54,8 @@ constrain env (A region expr) tipe =
5154 attribute = makeRec Lit.attribute attr
5255 uniform = makeRec Lit.uniform unif
5356 varying = makeRec Lit.varying (termN EmptyRecord1)
54− in return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
57+ in
58+ return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
5559
5660 Var var
5761 | name == saveEnvName -> return (A region CSaveEnv)
@@ -60,165 +64,135 @@ constrain env (A region expr) tipe =
6064 name = V.toString var
6165
6266 Range lo hi ->
63− existsNumber $ \n -> do
64− clo <- constrain env lo n
65− chi <- constrain env hi n
66− return $ and [clo, chi, list n === tipe]
67+ existsNumber $ \n ->
68+ do clo <- constrain env lo n
69+ chi <- constrain env hi n
70+ return $ and [clo, chi, list n === tipe]
6771
6872 ExplicitList exprs ->
69− exists $ \x -> do
70− cs <- mapM (\e -> constrain env e x) exprs
71− return . and $ list x === tipe : cs
73+ exists $ \x ->
74+ do constraints <- mapM (\e -> constrain env e x) exprs
75+ return . and $ list x === tipe : constraints
7276
7377 Binop op e1 e2 ->
7478 exists $ \t1 ->
75− exists $ \t2 -> do
76− c1 <- constrain env e1 t1
77− c2 <- constrain env e2 t2
78− return $ and [ c1, c2, V.toString op <? (t1 ==> t2 ==> tipe) ]
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) ]
7983
8084 Lambda p e ->
8185 exists $ \t1 ->
82− exists $ \t2 -> do
83− fragment <- try region $ Pattern.constrain env p t1
84− c2 <- constrain env e t2
85− let c = ex (vars fragment) (clet [monoscheme (typeEnv fragment)]
86− (typeConstraint fragment /\ c2 ))
87− return $ c /\ tipe === (t1 ==> t2)
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)
8894
8995 App e1 e2 ->
90− exists $ \t -> do
91− c1 <- constrain env e1 (t ==> tipe)
92− c2 <- constrain env e2 t
93− return $ c1 /\ c2
94−
95− MultiIf branches -> and <$> mapM constrain' branches
96− where
97− bool = Env.get env Env.types "Bool"
98− constrain' (b,e) = do
99− cb <- constrain env b bool
100− ce <- constrain env e tipe
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
101109 return (cb /\ ce)
102110
103− Case exp branches ->
104− exists $ \t -> do
105− ce <- constrain env exp t
106− let branch (p,e) = do
107− fragment <- try region $ Pattern.constrain env p t
108− clet [toScheme fragment] <$> constrain env e tipe
109− and . (:) ce <$> mapM branch branches
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
110119
111120 Data name exprs ->
112− do vars <- forM exprs $ \_ -> liftIO (variable Flexible)
113− let pairs = zip exprs (map varN vars)
114− (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
115− return $ ex vars (cs /\ name <? ctipe)
121+ do vars <- forM exprs $ \_ -> liftIO (variable Flexible)
122+ let pairs = zip exprs (map varN vars)
123+ (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
124+ return $ ex vars (cs /\ name <? ctipe)
116125 where
117− step (t,c) (e,x) = do
118− c' <- constrain env e x
119− return (x ==> t, c /\ c')
126+ step (t,c) (e,x) =
127+ do c' <- constrain env e x
128+ return (x ==> t, c /\ c')
120129
121− Access e label ->
130+ Access expr label ->
122131 exists $ \t ->
123− constrain env e (record (Map.singleton label [tipe]) t)
132+ constrain env expr (record (Map.singleton label [tipe]) t)
124133
125− Remove e label ->
134+ Remove expr label ->
126135 exists $ \t ->
127− constrain env e (record (Map.singleton label [t]) tipe)
136+ constrain env expr (record (Map.singleton label [t]) tipe)
128137
129− Insert e label value ->
138+ Insert expr label value ->
130139 exists $ \tVal ->
131− exists $ \tRec -> do
132− cVal <- constrain env value tVal
133− cRec <- constrain env e tRec
134− let c = tipe === record (Map.singleton label [tVal]) tRec
135− return (and [cVal, cRec, c])
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])
136145
137− Modify e fields ->
138− exists $ \t -> do
139− oldVars <- forM fields $ \_ -> liftIO (variable Flexible)
140− let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
141− cOld <- ex oldVars <$> constrain env e (record oldFields t)
146+ Modify expr fields ->
147+ exists $ \t ->
148+ do oldVars <- forM fields $ \_ -> liftIO (variable Flexible)
149+ let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
150+ cOld <- ex oldVars <$> constrain env expr (record oldFields t)
142151
143− newVars <- forM fields $ \_ -> liftIO (variable Flexible)
144− let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
145− let cNew = tipe === record newFields t
152+ newVars <- forM fields $ \_ -> liftIO (variable Flexible)
153+ let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
154+ let cNew = tipe === record newFields t
146155
147− cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
156+ cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
148157
149− return $ cOld /\ ex newVars (and (cNew : cs))
158+ return $ cOld /\ ex newVars (and (cNew : cs))
150159
151160 Record fields ->
152− do vars <- forM fields $ \_ -> liftIO (variable Flexible)
153− cs <- zipWithM (constrain env) (map snd fields) (map varN vars)
154− let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
155− recordType = record fields' (termN EmptyRecord1)
156− return . ex vars . and $ tipe === recordType : cs
161+ do vars <- forM fields $ \_ -> liftIO (variable Flexible)
162+ cs <- zipWithM (constrain env) (map snd fields) (map varN vars)
163+ let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
164+ let recordType = record fields' (termN EmptyRecord1)
165+ return . ex vars . and $ tipe === recordType : cs
157166
158167 Let defs body ->
159− do c <- constrain env body tipe
160− (schemes, rqs, fqs, header, c2, c1) <-
161− Monad.foldM (constrainDef env)
162− ([], [], [], Map.empty, true, true)
163− (concatMap expandPattern defs)
164− return $ clet schemes
165− (clet [Scheme rqs fqs (clet [monoscheme header] c2) header ]
166− (c1 /\ c))
168+ do c <- constrain env body tipe
167169
168− Port _ _ ->
169− return true
170+ (Info schemes rqs fqs headers c2 c1) <-
171+ Monad.foldM
172+ (constrainDef env)
173+ (Info [] [] [] Map.empty true true)
174+ (concatMap expandPattern defs)
170175
176+ let letScheme = [ Scheme rqs fqs (clet [monoscheme headers] c2) headers ]
171177
172−constrainDef env info (Canonical.Definition pattern expr maybeTipe) =
173− let qs = [] -- should come from the def, but I'm not sure what would live there...
174− (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
175− in
176− do rigidVars <- forM qs (\_ -> liftIO $ variable Rigid) -- Some mistake may be happening here.
177− -- Currently, qs is always [].
178− case (pattern, maybeTipe) of
179− (P.Var name, Just tipe) -> do
180− flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)
181− let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
182− env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
183− (vars, typ) <- Env.instantiateType env tipe Map.empty
184− let scheme = Scheme { rigidQuantifiers = [],
185− flexibleQuantifiers = flexiVars ++ vars,
186− constraint = Ann.noneNoDocs CTrue,
187− header = Map.singleton name typ }
188− c <- constrain env' expr typ
189− return ( scheme : schemes
190− , rigidQuantifiers
191− , flexibleQuantifiers
192− , headers
193− , c2
194− , fl rigidVars c /\ c1 )
195−
196− (P.Var name, Nothing) -> do
197− v <- liftIO $ variable Flexible
198− let tipe = varN v
199− inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
200− env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
201− c <- constrain env' expr tipe
202− return ( schemes
203− , rigidVars ++ rigidQuantifiers
204− , v : flexibleQuantifiers
205− , Map.insert name tipe headers
206− , c /\ c2
207− , c1 )
208−
209− _ -> error ("problem in constrainDef with " ++ show pattern)
178+ return $ clet schemes (clet letScheme (c1 /\ c))
179+
180+ Port _ _ ->
181+ return true
210182
211183
212184expandPattern :: Canonical.Def -> [Canonical.Def]
213185expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =
214186 case pattern of
215− P.Var _ -> [def]
216− _ -> Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars
217− where
218− vars = P.boundVarList pattern
219− x = "$" ++ concat vars
220− mkVar = A r . localVar
221− toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
187+ P.Var _ ->
188+ [def]
189+ _ ->
190+ Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars
191+ where
192+ vars = P.boundVarList pattern
193+ x = "$" ++ concat vars
194+ mkVar = A r . localVar
195+ toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
222196
223197
224198try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
@@ -227,3 +201,94 @@ try region computation =
227201 case result of
228202 Left err -> throwError [err region]
229203 Right value -> return value
204+
205+
206+-- CONSTRAIN DEFINITIONS
207+
208+data Info = Info
209+ { iSchemes :: [TypeScheme]
210+ , iRigid :: [Variable]
211+ , iFlex :: [Variable]
212+ , iHeaders :: Map.Map String Type
213+ , iC2 :: TypeConstraint
214+ , iC1 :: TypeConstraint
215+ }
216+
217+
218+constrainDef :: Env.Environment -> Info -> Canonical.Def -> ErrorT [PP.Doc] IO Info
219+constrainDef env info (Canonical.Definition pattern expr maybeTipe) =
220+ let qs = [] -- should come from the def, but I'm not sure what would live there...
221+ in
222+ case (pattern, maybeTipe) of
223+ (P.Var name, Just tipe) ->
224+ constrainAnnotatedDef env info qs name expr tipe
225+
226+ (P.Var name, Nothing) ->
227+ constrainUnannotatedDef env info qs name expr
228+
229+ _ -> error ("problem in constrainDef with " ++ show pattern)
230+
231+
232+constrainAnnotatedDef
233+ :: Env.Environment
234+ -> Info
235+ -> [String]
236+ -> String
237+ -> Canonical.Expr
238+ -> ST.CanonicalType
239+ -> ErrorT [PP.Doc] IO Info
240+constrainAnnotatedDef env info qs name expr tipe =
241+ do -- Some mistake may be happening here. Currently, qs is always [].
242+ rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)
243+
244+ flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)
245+
246+ let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
247+
248+ let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
249+
250+ (vars, typ) <- Env.instantiateType env tipe Map.empty
251+
252+ let scheme =
253+ Scheme
254+ { rigidQuantifiers = []
255+ , flexibleQuantifiers = flexiVars ++ vars
256+ , constraint = Ann.noneNoDocs CTrue
257+ , header = Map.singleton name typ
258+ }
259+
260+ c <- constrain env' expr typ
261+
262+ return $ info
263+ { iSchemes = scheme : iSchemes info
264+ , iC1 = fl rigidVars c /\ iC1 info
265+ }
266+
267+
268+constrainUnannotatedDef
269+ :: Env.Environment
270+ -> Info
271+ -> [String]
272+ -> String
273+ -> Canonical.Expr
274+ -> ErrorT [PP.Doc] IO Info
275+constrainUnannotatedDef env info qs name expr =
276+ do -- Some mistake may be happening here. Currently, qs is always [].
277+ rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)
278+
279+ v <- liftIO $ variable Flexible
280+
281+ let tipe = varN v
282+
283+ let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
284+
285+ let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
286+
287+ c <- constrain env' expr tipe
288+
289+ return $ info
290+ { iRigid = rigidVars ++ iRigid info
291+ , iFlex = v : iFlex info
292+ , iHeaders = Map.insert name tipe (iHeaders info)
293+ , iC2 = c /\ iC2 info
294+ }