on 73cb511 help sign in
elk/src/Type/Constrain/Expression.hs
227 lines 9.1 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
23constrain :: Env.Environment -> Canonical.Expr -> Type
24 -> ErrorT [PP.Doc] IO TypeConstraint
25constrain env (A region expr) tipe =
26 let list t = Env.get env Env.types "List" <| t
27 and = A region . CAnd
28 true = A region CTrue
29 t1 === t2 = A region (CEqual t1 t2)
30 x <? t = A region (CInstance x t)
31 clet schemes c = A region (CLet schemes c)
32 in
33 case expr of
34 Literal lit -> liftIO $ Literal.constrain env region lit tipe
36 GLShader _uid _src gltipe ->
37 exists $ \attr ->
38 exists $ \unif ->
39 let
40 shaderTipe a u v = Env.get env Env.types "Graphics.WebGL.Shader" <| a <| u <| v
41 glTipe = Env.get env Env.types . Lit.glTipeName
42 makeRec accessor baseRec =
43 let decls = accessor gltipe
44 in if Map.size decls == 0
45 then baseRec
46 else record (Map.map (\t -> [glTipe t]) decls) baseRec
47 attribute = makeRec Lit.attribute attr
48 uniform = makeRec Lit.uniform unif
49 varying = makeRec Lit.varying (termN EmptyRecord1)
50 in return . A region $ CEqual tipe (shaderTipe attribute uniform varying)
52 Var var
53 | name == saveEnvName -> return (A region CSaveEnv)
54 | otherwise -> return (name <? tipe)
55 where
56 name = V.toString var
58 Range lo hi ->
59 existsNumber $ \n -> do
60 clo <- constrain env lo n
61 chi <- constrain env hi n
62 return $ and [clo, chi, list n === tipe]
64 ExplicitList exprs ->
65 exists $ \x -> do
66 cs <- mapM (\e -> constrain env e x) exprs
67 return . and $ list x === tipe : cs
69 Binop op e1 e2 ->
70 exists $ \t1 ->
71 exists $ \t2 -> do
72 c1 <- constrain env e1 t1
73 c2 <- constrain env e2 t2
74 return $ and [ c1, c2, V.toString op <? (t1 ==> t2 ==> tipe) ]
76 Lambda p e ->
77 exists $ \t1 ->
78 exists $ \t2 -> do
79 fragment <- try region $ Pattern.constrain env p t1
80 c2 <- constrain env e t2
81 let c = ex (vars fragment) (clet [monoscheme (typeEnv fragment)]
82 (typeConstraint fragment /\ c2 ))
83 return $ c /\ tipe === (t1 ==> t2)
85 App e1 e2 ->
86 exists $ \t -> do
87 c1 <- constrain env e1 (t ==> tipe)
88 c2 <- constrain env e2 t
89 return $ c1 /\ c2
91 MultiIf branches -> and <$> mapM constrain' branches
92 where
93 bool = Env.get env Env.types "Bool"
94 constrain' (b,e) = do
95 cb <- constrain env b bool
96 ce <- constrain env e tipe
97 return (cb /\ ce)
99 Case exp branches ->
100 exists $ \t -> do
101 ce <- constrain env exp t
102 let branch (p,e) = do
103 fragment <- try region $ Pattern.constrain env p t
104 clet [toScheme fragment] <$> constrain env e tipe
105 and . (:) ce <$> mapM branch branches
107 Data name exprs ->
108 do vars <- forM exprs $ \_ -> liftIO (variable Flexible)
109 let pairs = zip exprs (map varN vars)
110 (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
111 return $ ex vars (cs /\ name <? ctipe)
112 where
113 step (t,c) (e,x) = do
114 c' <- constrain env e x
115 return (x ==> t, c /\ c')
117 Access e label ->
118 exists $ \t ->
119 constrain env e (record (Map.singleton label [tipe]) t)
121 Remove e label ->
122 exists $ \t ->
123 constrain env e (record (Map.singleton label [t]) tipe)
125 Insert e label value ->
126 exists $ \tVal ->
127 exists $ \tRec -> do
128 cVal <- constrain env value tVal
129 cRec <- constrain env e tRec
130 let c = tipe === record (Map.singleton label [tVal]) tRec
131 return (and [cVal, cRec, c])
133 Modify e fields ->
134 exists $ \t -> do
135 oldVars <- forM fields $ \_ -> liftIO (variable Flexible)
136 let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))
137 cOld <- ex oldVars <$> constrain env e (record oldFields t)
139 newVars <- forM fields $ \_ -> liftIO (variable Flexible)
140 let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))
141 let cNew = tipe === record newFields t
143 cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)
145 return $ cOld /\ ex newVars (and (cNew : cs))
147 Record fields ->
148 do vars <- forM fields $ \_ -> liftIO (variable Flexible)
149 cs <- zipWithM (constrain env) (map snd fields) (map varN vars)
150 let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))
151 recordType = record fields' (termN EmptyRecord1)
152 return . ex vars . and $ tipe === recordType : cs
154 Markdown _ _ ->
155 return ("Text.markdown" <? tipe)
157 Let defs body ->
158 do c <- constrain env body tipe
159 (schemes, rqs, fqs, header, c2, c1) <-
160 Monad.foldM (constrainDef env)
161 ([], [], [], Map.empty, true, true)
162 (concatMap expandPattern defs)
163 return $ clet schemes
164 (clet [Scheme rqs fqs (clet [monoscheme header] c2) header ]
165 (c1 /\ c))
167 PortIn _ _ -> return true
169 PortOut _ _ signal ->
170 constrain env signal tipe
172constrainDef 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 )
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 )
209 _ -> error ("problem in constrainDef with " ++ show pattern)
211expandPattern :: Canonical.Def -> [Canonical.Def]
212expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =
213 case pattern of
214 P.Var _ -> [def]
215 _ -> Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars
216 where
217 vars = P.boundVarList pattern
218 x = "$" ++ concat vars
219 mkVar = A r . localVar
220 toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
222try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
223try region computation = do
224 result <- liftIO $ runErrorT computation
225 case result of
226 Left err -> throwError [err region]
227 Right value -> return value