git.iko.soy/elk
on 4bec310 help sign in
elk/compiler/Type/Constrain/Expression.hs
210 lines 8.3 kB history raw
1{-# OPTIONS_GHC -W #-}
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 qualified Text.PrettyPrint as PP
11import SourceSyntax.Annotation as Ann
12import SourceSyntax.Expression
13import qualified SourceSyntax.Pattern as P
14import qualified SourceSyntax.Type as ST
15import qualified SourceSyntax.Variable as V
16import Type.Type hiding (Descriptor(..))
17import Type.Fragment
18import qualified Type.Environment as Env
19import qualified Type.Constrain.Literal as Literal
20import qualified Type.Constrain.Pattern as Pattern
22constrain :: Env.Environment -> Expr -> Type -> ErrorT [PP.Doc] IO TypeConstraint
23constrain env (A region expr) tipe =
24 let list t = Env.get env Env.types "_List" <| t
25 and = A region . CAnd
26 true = A region CTrue
27 t1 === t2 = A region (CEqual t1 t2)
28 x <? t = A region (CInstance x t)
29 clet schemes c = A region (CLet schemes c)
30 in
31 case expr of
32 Literal lit -> liftIO $ Literal.constrain env region lit tipe
34 Var (V.Raw name)
35 | name == saveEnvName -> return (A region CSaveEnv)
36 | otherwise -> return (name <? tipe)
38 Range lo hi ->
39 existsNumber $ \n -> do
40 clo <- constrain env lo n
41 chi <- constrain env hi n
42 return $ and [clo, chi, list n === tipe]
44 ExplicitList exprs ->
45 exists $ \x -> do
46 cs <- mapM (\e -> constrain env e x) exprs
47 return . and $ list x === tipe : cs
49 Binop op e1 e2 ->
50 exists $ \t1 ->
51 exists $ \t2 -> do
52 c1 <- constrain env e1 t1
53 c2 <- constrain env e2 t2
54 return $ and [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
56 Lambda p e ->
57 exists $ \t1 ->
58 exists $ \t2 -> do
59 fragment <- try region $ Pattern.constrain env p t1
60 c2 <- constrain env e t2
61 let c = ex (vars fragment) (clet [monoscheme (typeEnv fragment)]
62 (typeConstraint fragment /\ c2 ))
63 return $ c /\ tipe === (t1 ==> t2)
65 App e1 e2 ->
66 exists $ \t -> do
67 c1 <- constrain env e1 (t ==> tipe)
68 c2 <- constrain env e2 t
69 return $ c1 /\ c2
71 MultiIf branches -> and <$> mapM constrain' branches
72 where
73 bool = Env.get env Env.types "Bool"
74 constrain' (b,e) = do
75 cb <- constrain env b bool
76 ce <- constrain env e tipe
77 return (cb /\ ce)
79 Case exp branches ->
80 exists $ \t -> do
81 ce <- constrain env exp t
82 let branch (p,e) = do
83 fragment <- try region $ Pattern.constrain env p t
84 clet [toScheme fragment] <$> constrain env e tipe
85 and . (:) ce <$> mapM branch branches
87 Data name exprs ->
88 do vars <- forM exprs $ \_ -> liftIO (var Flexible)
89 let pairs = zip exprs (map VarN vars)
90 (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
91 return $ ex vars (cs /\ name <? ctipe)
92 where
93 step (t,c) (e,x) = do
94 c' <- constrain env e x
95 return (x ==> t, c /\ c')
97 Access e label ->
98 exists $ \t ->
99 constrain env e (record (Map.singleton label [tipe]) t)
101 Remove e label ->
102 exists $ \t ->
103 constrain env e (record (Map.singleton label [t]) tipe)
105 Insert e label value ->
106 exists $ \tVal ->
107 exists $ \tRec -> do
108 cVal <- constrain env value tVal
109 cRec <- constrain env e tRec
110 let c = tipe === record (Map.singleton label [tVal]) tRec
111 return (and [cVal, cRec, c])
113 Modify e fields ->
114 exists $ \t -> do
115 oldVars <- forM fields $ \_ -> liftIO (var Flexible)
116 let oldFields = ST.fieldMap (zip (map fst fields) (map VarN oldVars))
117 cOld <- ex oldVars <$> constrain env e (record oldFields t)
119 newVars <- forM fields $ \_ -> liftIO (var Flexible)
120 let newFields = ST.fieldMap (zip (map fst fields) (map VarN newVars))
121 let cNew = tipe === record newFields t
123 cs <- zipWithM (constrain env) (map snd fields) (map VarN newVars)
125 return $ cOld /\ ex newVars (and (cNew : cs))
127 Record fields ->
128 do vars <- forM fields $ \_ -> liftIO (var Flexible)
129 cs <- zipWithM (constrain env) (map snd fields) (map VarN vars)
130 let fields' = ST.fieldMap (zip (map fst fields) (map VarN vars))
131 recordType = record fields' (TermN EmptyRecord1)
132 return . ex vars . and $ tipe === recordType : cs
134 Markdown _ _ es ->
135 do vars <- forM es $ \_ -> liftIO (var Flexible)
136 let tvars = map VarN vars
137 cs <- zipWithM (constrain env) es tvars
138 return . ex vars $ and ("Text.markdown" <? tipe : cs)
140 Let defs body ->
141 do c <- constrain env body tipe
142 (schemes, rqs, fqs, header, c2, c1) <-
143 Monad.foldM (constrainDef env)
144 ([], [], [], Map.empty, true, true)
145 (concatMap expandPattern defs)
146 return $ clet schemes
147 (clet [Scheme rqs fqs (clet [monoscheme header] c2) header ]
148 (c1 /\ c))
150 PortIn _ _ -> return true
152 PortOut _ _ signal ->
153 constrain env signal tipe
155constrainDef env info (Definition pattern expr maybeTipe) =
156 let qs = [] -- should come from the def, but I'm not sure what would live there...
157 (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
158 in
159 do rigidVars <- forM qs (\_ -> liftIO $ var Rigid) -- Some mistake may be happening here.
160 -- Currently, qs is always [].
161 case (pattern, maybeTipe) of
162 (P.Var name, Just tipe) -> do
163 flexiVars <- forM qs (\_ -> liftIO $ var Flexible)
164 let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
165 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
166 (vars, typ) <- Env.instantiateType env tipe Map.empty
167 let scheme = Scheme { rigidQuantifiers = [],
168 flexibleQuantifiers = flexiVars ++ vars,
169 constraint = Ann.noneNoDocs CTrue,
170 header = Map.singleton name typ }
171 c <- constrain env' expr typ
172 return ( scheme : schemes
173 , rigidQuantifiers
174 , flexibleQuantifiers
175 , headers
176 , c2
177 , fl rigidVars c /\ c1 )
179 (P.Var name, Nothing) -> do
180 v <- liftIO $ var Flexible
181 let tipe = VarN v
182 inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
183 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
184 c <- constrain env' expr tipe
185 return ( schemes
186 , rigidVars ++ rigidQuantifiers
187 , v : flexibleQuantifiers
188 , Map.insert name tipe headers
189 , c /\ c2
190 , c1 )
192 _ -> error (show pattern)
194expandPattern :: Def -> [Def]
195expandPattern def@(Definition pattern lexpr@(A r _) maybeType) =
196 case pattern of
197 P.Var _ -> [def]
198 _ -> Definition (P.Var x) lexpr maybeType : map toDef vars
199 where
200 vars = P.boundVarList pattern
201 x = "$" ++ concat vars
202 mkVar = A r . rawVar
203 toDef y = Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
205try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
206try region computation = do
207 result <- liftIO $ runErrorT computation
208 case result of
209 Left err -> throwError [err region]
210 Right value -> return value