on 8a87749 help sign in
elk/src/Type/Constrain/Expression.hs
294 lines 10 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2module Type.Constrain.Expression where
4import Control.Applicative ((<$>))
5import qualified Control.Monad as Monad
6import Control.Monad.Error
7import qualified Data.List as List
8import qualified Data.Map as Map
9import Prelude hiding (and)
10import qualified Text.PrettyPrint as PP
12import qualified AST.Literal as Lit
13import AST.Annotation as Ann
14import AST.Expression.General
15import qualified AST.Expression.Canonical as Canonical
16import qualified AST.Pattern as P
17import qualified AST.Type as ST
18import qualified AST.Variable as V
19import Type.Type hiding (Descriptor(..))
20import qualified Type.Fragment as Fragment
21import qualified Type.Environment as Env
22import qualified Type.Constrain.Literal as Literal
23import qualified Type.Constrain.Pattern as Pattern
26constrain
27 :: Env.Environment
28 -> Canonical.Expr
29 -> Type
30 -> ErrorT [PP.Doc] IO TypeConstraint
31constrain env (A region expression) tipe =
32 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)
38 in
39 case expression of
40 Literal lit ->
41 liftIO $ Literal.constrain env region lit tipe
43 GLShader _uid _src gltipe ->
44 exists $ \attr ->
45 exists $ \unif ->
46 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)
57 in
58 return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
60 Var var
61 | name == saveEnvName -> return (A region CSaveEnv)
62 | otherwise -> return (name <? tipe)
63 where
64 name = V.toString var
66 Range lo hi ->
67 existsNumber $ \n ->
68 do clo <- constrain env lo n
69 chi <- constrain env hi n
70 return $ and [clo, chi, list n === tipe]
72 ExplicitList exprs ->
73 exists $ \x ->
74 do constraints <- mapM (\e -> constrain env e x) exprs
75 return . and $ list x === tipe : constraints
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) ]
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)
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
101 MultiIf branches ->
102 and <$> mapM constrain' branches
103 where
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
109 return (cb /\ ce)
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
120 Data name exprs ->
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)
125 where
126 step (t,c) (e,x) =
127 do c' <- constrain env e x
128 return (x ==> t, c /\ c')
130 Access expr label ->
131 exists $ \t ->
132 constrain env expr (record (Map.singleton label [tipe]) t)
134 Remove expr label ->
135 exists $ \t ->
136 constrain env expr (record (Map.singleton label [t]) tipe)
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])
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)
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
156 cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
158 return $ cOld /\ ex newVars (and (cNew : cs))
160 Record fields ->
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
167 Let defs body ->
168 do c <- constrain env body tipe
170 (Info schemes rqs fqs headers c2 c1) <-
171 Monad.foldM
172 (constrainDef env)
173 (Info [] [] [] Map.empty true true)
174 (concatMap expandPattern defs)
176 let letScheme = [ Scheme rqs fqs (clet [monoscheme headers] c2) headers ]
178 return $ clet schemes (clet letScheme (c1 /\ c))
180 Port _ _ ->
181 return true
184expandPattern :: Canonical.Def -> [Canonical.Def]
185expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =
186 case pattern of
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
198try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
199try region computation =
200 do result <- liftIO $ runErrorT computation
201 case result of
202 Left err -> throwError [err region]
203 Right value -> return value
206-- CONSTRAIN DEFINITIONS
208data Info = Info
209 { iSchemes :: [TypeScheme]
210 , iRigid :: [Variable]
211 , iFlex :: [Variable]
212 , iHeaders :: Map.Map String Type
213 , iC2 :: TypeConstraint
214 , iC1 :: TypeConstraint
215 }
218constrainDef :: Env.Environment -> Info -> Canonical.Def -> ErrorT [PP.Doc] IO Info
219constrainDef 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
226 (P.Var name, Nothing) ->
227 constrainUnannotatedDef env info qs name expr
229 _ -> error ("problem in constrainDef with " ++ show pattern)
232constrainAnnotatedDef
233 :: Env.Environment
234 -> Info
235 -> [String]
236 -> String
237 -> Canonical.Expr
238 -> ST.CanonicalType
239 -> ErrorT [PP.Doc] IO Info
240constrainAnnotatedDef 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)
244 flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)
246 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
248 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
250 (vars, typ) <- Env.instantiateType env tipe Map.empty
252 let scheme =
253 Scheme
254 { rigidQuantifiers = []
255 , flexibleQuantifiers = flexiVars ++ vars
256 , constraint = Ann.noneNoDocs CTrue
257 , header = Map.singleton name typ
258 }
260 c <- constrain env' expr typ
262 return $ info
263 { iSchemes = scheme : iSchemes info
264 , iC1 = fl rigidVars c /\ iC1 info
265 }
268constrainUnannotatedDef
269 :: Env.Environment
270 -> Info
271 -> [String]
272 -> String
273 -> Canonical.Expr
274 -> ErrorT [PP.Doc] IO Info
275constrainUnannotatedDef env info qs name expr =
276 do -- Some mistake may be happening here. Currently, qs is always [].
277 rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)
279 v <- liftIO $ variable Flexible
281 let tipe = varN v
283 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
285 let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
287 c <- constrain env' expr tipe
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 }