git.iko.soy/elk
on 501c607 help sign in
elk/src/Type/Constrain/Expression.hs
239 lines 9.2 kB history raw
1module Type.Constrain.Expression where
3import Control.Applicative ((<$>))
4import qualified Control.Monad as Monad
5import Control.Monad.Error
6import qualified Data.List as List
7import qualified Data.Map as Map
8import qualified Text.PrettyPrint as PP
10import AST.Literal as Lit
11import AST.Annotation as Ann
12import AST.Expression.General
13import qualified AST.Expression.Canonical as Canonical
14import qualified AST.Pattern as P
15import qualified AST.Type as ST
16import qualified AST.Variable as V
17import Type.Type hiding (Descriptor(..))
18import Type.Fragment
19import qualified Type.Environment as Env
20import qualified Type.Constrain.Literal as Literal
21import qualified Type.Constrain.Pattern as Pattern
24constrain
25 :: Env.Environment
26 -> Canonical.Expr
27 -> Type
28 -> ErrorT [PP.Doc] IO TypeConstraint
29constrain env (A region expr) tipe =
30 let list t = Env.get env Env.types "List" <| t
31 and = A region . CAnd
32 true = A region CTrue
33 t1 === t2 = A region (CEqual t1 t2)
34 x <? t = A region (CInstance x t)
35 clet schemes c = A region (CLet schemes c)
36 in
37 case expr of
38 Literal lit -> liftIO $ Literal.constrain env region lit tipe
40 GLShader _uid _src gltipe ->
41 exists $ \attr ->
42 exists $ \unif ->
43 let
44 shaderTipe a u v = Env.get env Env.types "WebGL.Shader" <| a <| u <| v
45 glTipe = Env.get env Env.types . Lit.glTipeName
46 makeRec accessor baseRec =
47 let decls = accessor gltipe
48 in if Map.size decls == 0
49 then baseRec
50 else record (Map.map (\t -> [glTipe t]) decls) baseRec
51 attribute = makeRec Lit.attribute attr
52 uniform = makeRec Lit.uniform unif
53 varying = makeRec Lit.varying (termN EmptyRecord1)
54 in return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
56 Var var
57 | name == saveEnvName -> return (A region CSaveEnv)
58 | otherwise -> return (name <? tipe)
59 where
60 name = V.toString var
62 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]
68 ExplicitList exprs ->
69 exists $ \x -> do
70 cs <- mapM (\e -> constrain env e x) exprs
71 return . and $ list x === tipe : cs
73 Binop op e1 e2 ->
74 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) ]
80 Lambda p e ->
81 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)
89 App e1 e2 ->
90 exists $ \t -> do
91 c1 <- constrain env e1 (t ==> tipe)
92 c2 <- constrain env e2 t
93 return $ c1 /\ c2
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
101 return (cb /\ ce)
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 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)
116 where
117 step (t,c) (e,x) = do
118 c' <- constrain env e x
119 return (x ==> t, c /\ c')
121 Access e label ->
122 exists $ \t ->
123 constrain env e (record (Map.singleton label [tipe]) t)
125 Remove e label ->
126 exists $ \t ->
127 constrain env e (record (Map.singleton label [t]) tipe)
129 Insert e label value ->
130 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])
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)
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
147 cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
149 return $ cOld /\ ex newVars (and (cNew : cs))
151 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
158 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 Input _ _ ->
169 return true
171 Output _ _ signal ->
172 constrain env signal tipe
174 Loopback _ _ maybeExpr ->
175 case maybeExpr of
176 Nothing ->
177 return true
178 Just expr ->
179 constrain env expr tipe
182constrainDef env info (Canonical.Definition pattern expr maybeTipe) =
183 let qs = [] -- should come from the def, but I'm not sure what would live there...
184 (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
185 in
186 do rigidVars <- forM qs (\_ -> liftIO $ variable Rigid) -- Some mistake may be happening here.
187 -- Currently, qs is always [].
188 case (pattern, maybeTipe) of
189 (P.Var name, Just tipe) -> do
190 flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)
191 let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars
192 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
193 (vars, typ) <- Env.instantiateType env tipe Map.empty
194 let scheme = Scheme { rigidQuantifiers = [],
195 flexibleQuantifiers = flexiVars ++ vars,
196 constraint = Ann.noneNoDocs CTrue,
197 header = Map.singleton name typ }
198 c <- constrain env' expr typ
199 return ( scheme : schemes
200 , rigidQuantifiers
201 , flexibleQuantifiers
202 , headers
203 , c2
204 , fl rigidVars c /\ c1 )
206 (P.Var name, Nothing) -> do
207 v <- liftIO $ variable Flexible
208 let tipe = varN v
209 inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars
210 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
211 c <- constrain env' expr tipe
212 return ( schemes
213 , rigidVars ++ rigidQuantifiers
214 , v : flexibleQuantifiers
215 , Map.insert name tipe headers
216 , c /\ c2
217 , c1 )
219 _ -> error ("problem in constrainDef with " ++ show pattern)
222expandPattern :: Canonical.Def -> [Canonical.Def]
223expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =
224 case pattern of
225 P.Var _ -> [def]
226 _ -> Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars
227 where
228 vars = P.boundVarList pattern
229 x = "$" ++ concat vars
230 mkVar = A r . localVar
231 toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
234try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
235try region computation =
236 do result <- liftIO $ runErrorT computation
237 case result of
238 Left err -> throwError [err region]
239 Right value -> return value