git.iko.soy/elk
on 63243ca help sign in
elk/compiler/Type/Constrain/Expression.hs
209 lines 8.3 kB history raw
1{-# OPTIONS_GHC -W #-}
2module Type.Constrain.Expression where
4import qualified Data.List as List
5import qualified Data.Map as Map
6import qualified Data.Set as Set
7import Control.Applicative ((<$>))
8import qualified Control.Monad as Monad
9import Control.Monad.Error
10import qualified Text.PrettyPrint as PP
12import SourceSyntax.Location as Loc
13import SourceSyntax.Pattern (Pattern(PVar), boundVars)
14import SourceSyntax.Expression
15import qualified SourceSyntax.Type as SrcT
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 -> LExpr -> Type -> ErrorT [PP.Doc] IO TypeConstraint
23constrain env (L span expr) tipe =
24 let list t = Env.get env Env.types "_List" <| t
25 and = L span . CAnd
26 true = L span CTrue
27 t1 === t2 = L span (CEqual t1 t2)
28 x <? t = L span (CInstance x t)
29 clet schemes c = L span (CLet schemes c)
30 in
31 case expr of
32 Literal lit -> liftIO $ Literal.constrain env span lit tipe
34 Var name | name == saveEnvName -> return (L span CSaveEnv)
35 | otherwise -> return (name <? tipe)
37 Range lo hi ->
38 exists $ \x -> do
39 clo <- constrain env lo x
40 chi <- constrain env hi x
41 return $ and [clo, chi, list x === tipe]
43 ExplicitList exprs ->
44 exists $ \x -> do
45 cs <- mapM (\e -> constrain env e x) exprs
46 return . and $ list x === tipe : cs
48 Binop op e1 e2 ->
49 exists $ \t1 ->
50 exists $ \t2 -> do
51 c1 <- constrain env e1 t1
52 c2 <- constrain env e2 t2
53 return $ and [ c1, c2, op <? (t1 ==> t2 ==> tipe) ]
55 Lambda p e ->
56 exists $ \t1 ->
57 exists $ \t2 -> do
58 fragment <- try span $ Pattern.constrain env p t1
59 c2 <- constrain env e t2
60 let c = ex (vars fragment) (clet [monoscheme (typeEnv fragment)]
61 (typeConstraint fragment /\ c2 ))
62 return $ c /\ tipe === (t1 ==> t2)
64 App e1 e2 ->
65 exists $ \t -> do
66 c1 <- constrain env e1 (t ==> tipe)
67 c2 <- constrain env e2 t
68 return $ c1 /\ c2
70 MultiIf branches -> and <$> mapM constrain' branches
71 where
72 bool = Env.get env Env.types "Bool"
73 constrain' (b,e) = do
74 cb <- constrain env b bool
75 ce <- constrain env e tipe
76 return (cb /\ ce)
78 Case exp branches ->
79 exists $ \t -> do
80 ce <- constrain env exp t
81 let branch (p,e) = do
82 fragment <- try span $ Pattern.constrain env p t
83 clet [toScheme fragment] <$> constrain env e tipe
84 and . (:) ce <$> mapM branch branches
86 Data name exprs ->
87 do vars <- forM exprs $ \_ -> liftIO (var Flexible)
88 let pairs = zip exprs (map VarN vars)
89 (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)
90 return $ ex vars (cs /\ name <? ctipe)
91 where
92 step (t,c) (e,x) = do
93 c' <- constrain env e x
94 return (x ==> t, c /\ c')
96 Access e label ->
97 exists $ \t ->
98 constrain env e (record (Map.singleton label [tipe]) t)
100 Remove e label ->
101 exists $ \t ->
102 constrain env e (record (Map.singleton label [t]) tipe)
104 Insert e label value ->
105 exists $ \tVal ->
106 exists $ \tRec -> do
107 cVal <- constrain env value tVal
108 cRec <- constrain env e tRec
109 let c = tipe === record (Map.singleton label [tVal]) tRec
110 return (and [cVal, cRec, c])
112 Modify e fields ->
113 exists $ \t -> do
114 oldVars <- forM fields $ \_ -> liftIO (var Flexible)
115 let oldFields = SrcT.fieldMap (zip (map fst fields) (map VarN oldVars))
116 cOld <- ex oldVars <$> constrain env e (record oldFields t)
118 newVars <- forM fields $ \_ -> liftIO (var Flexible)
119 let newFields = SrcT.fieldMap (zip (map fst fields) (map VarN newVars))
120 let cNew = tipe === record newFields t
122 cs <- zipWithM (constrain env) (map snd fields) (map VarN newVars)
124 return $ cOld /\ ex newVars (and (cNew : cs))
126 Record fields ->
127 do vars <- forM fields $ \_ -> liftIO (var Flexible)
128 cs <- zipWithM (constrain env) (map snd fields) (map VarN vars)
129 let fields' = SrcT.fieldMap (zip (map fst fields) (map VarN vars))
130 recordType = record fields' (TermN EmptyRecord1)
131 return . ex vars . and $ tipe === recordType : cs
133 Markdown _ _ es ->
134 do vars <- forM es $ \_ -> liftIO (var Flexible)
135 let tvars = map VarN vars
136 cs <- zipWithM (constrain env) es tvars
137 return . ex vars $ and ("Text.markdown" <? tipe : cs)
139 Let defs body ->
140 do c <- constrain env body tipe
141 (schemes, rqs, fqs, header, c2, c1) <-
142 Monad.foldM (constrainDef env)
143 ([], [], [], Map.empty, true, true)
144 (concatMap expandPattern defs)
145 return $ clet schemes
146 (clet [Scheme rqs fqs (clet [monoscheme header] c2) header ]
147 (c1 /\ c))
149 PortIn _ _ -> return true
151 PortOut _ _ signal ->
152 constrain env signal tipe
154constrainDef env info (Definition pattern expr maybeTipe) =
155 let qs = [] -- should come from the def, but I'm not sure what would live there...
156 (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info
157 in
158 do rigidVars <- forM qs (\_ -> liftIO $ var Rigid) -- Some mistake may be happening here.
159 -- Currently, qs is always [].
160 case (pattern, maybeTipe) of
161 (PVar name, Just tipe) -> do
162 flexiVars <- forM qs (\_ -> liftIO $ var Flexible)
163 let inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs flexiVars
164 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
165 (vars, typ) <- Env.instantiateType env tipe Map.empty
166 let scheme = Scheme { rigidQuantifiers = [],
167 flexibleQuantifiers = flexiVars ++ vars,
168 constraint = Loc.noneNoDocs CTrue,
169 header = Map.singleton name typ }
170 c <- constrain env' expr typ
171 return ( scheme : schemes
172 , rigidQuantifiers
173 , flexibleQuantifiers
174 , headers
175 , c2
176 , fl rigidVars c /\ c1 )
178 (PVar name, Nothing) -> do
179 v <- liftIO $ var Flexible
180 let tipe = VarN v
181 inserts = zipWith (\arg typ -> Map.insert arg (VarN typ)) qs rigidVars
182 env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }
183 c <- constrain env' expr tipe
184 return ( schemes
185 , rigidVars ++ rigidQuantifiers
186 , v : flexibleQuantifiers
187 , Map.insert name tipe headers
188 , c /\ c2
189 , c1 )
191 _ -> error (show pattern)
193expandPattern :: Def -> [Def]
194expandPattern def@(Definition pattern lexpr@(L s _) maybeType) =
195 case pattern of
196 PVar _ -> [def]
197 _ -> Definition (PVar x) lexpr maybeType : map toDef vars
198 where
199 vars = Set.toList $ boundVars pattern
200 x = "$" ++ concat vars
201 mkVar = L s . Var
202 toDef y = Definition (PVar y) (L s $ Case (mkVar x) [(pattern, mkVar y)]) Nothing
204try :: SrcSpan -> ErrorT (SrcSpan -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a
205try span computation = do
206 result <- liftIO $ runErrorT computation
207 case result of
208 Left err -> throwError [err span]
209 Right value -> return value