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