306a7ee · elk · git.iko.soy

1+{-# OPTIONS_GHC -Wall #-}

1module Type.Constrain.Expression where

2module Type.Constrain.Expression where

2

3

3import Control.Applicative ((<$>))

4import Control.Applicative ((<$>))

5import Control.Monad.Error

6import Control.Monad.Error

6import qualified Data.List as List

7import qualified Data.List as List

7import qualified Data.Map as Map

8import qualified Data.Map as Map

9+import Prelude hiding (and)

8import qualified Text.PrettyPrint as PP

10import qualified Text.PrettyPrint as PP

9

11

10−import AST.Literal as Lit

12+import qualified AST.Literal as Lit

11import AST.Annotation as Ann

13import AST.Annotation as Ann

12import AST.Expression.General

14import AST.Expression.General

13import qualified AST.Expression.Canonical as Canonical

15import qualified AST.Expression.Canonical as Canonical

15import qualified AST.Type as ST

17import qualified AST.Type as ST

16import qualified AST.Variable as V

18import qualified AST.Variable as V

17import Type.Type hiding (Descriptor(..))

19import Type.Type hiding (Descriptor(..))

18−import Type.Fragment

20+import qualified Type.Fragment as Fragment

19import qualified Type.Environment as Env

21import qualified Type.Environment as Env

20import qualified Type.Constrain.Literal as Literal

22import qualified Type.Constrain.Literal as Literal

21import qualified Type.Constrain.Pattern as Pattern

23import qualified Type.Constrain.Pattern as Pattern

26 -> Canonical.Expr

28 -> Canonical.Expr

27 -> Type

29 -> Type

28 -> ErrorT [PP.Doc] IO TypeConstraint

30 -> ErrorT [PP.Doc] IO TypeConstraint

29−constrain env (A region expr) tipe =

31+constrain env (A region expression) tipe =

30 let list t = Env.get env Env.types "List" <| t

32 let list t = Env.get env Env.types "List" <| t

31 and = A region . CAnd

33 and = A region . CAnd

32 true = A region CTrue

34 true = A region CTrue

34 x <? t = A region (CInstance x t)

36 x <? t = A region (CInstance x t)

35 clet schemes c = A region (CLet schemes c)

37 clet schemes c = A region (CLet schemes c)

36 in

38 in

37− case expr of

39+ case expression of

40+ Literal lit ->

38− Literal lit -> liftIO $ Literal.constrain env region lit tipe

41+ liftIO $ Literal.constrain env region lit tipe

39

42

40 GLShader _uid _src gltipe ->

43 GLShader _uid _src gltipe ->

41 exists $ \attr ->

44 exists $ \attr ->

51 attribute = makeRec Lit.attribute attr

54 attribute = makeRec Lit.attribute attr

52 uniform = makeRec Lit.uniform unif

55 uniform = makeRec Lit.uniform unif

53 varying = makeRec Lit.varying (termN EmptyRecord1)

56 varying = makeRec Lit.varying (termN EmptyRecord1)

57+ in

54− in return . A region $ CEqual tipe (shaderTipe attribute uniform varying)

58+ return . A region $ CEqual tipe (shaderTipe attribute uniform varying)

55

59

56 Var var

60 Var var

57 | name == saveEnvName -> return (A region CSaveEnv)

61 | name == saveEnvName -> return (A region CSaveEnv)

60 name = V.toString var

64 name = V.toString var

61

65

62 Range lo hi ->

66 Range lo hi ->

63− existsNumber $ \n -> do

67+ existsNumber $ \n ->

64− clo <- constrain env lo n

68+ do clo <- constrain env lo n

65− chi <- constrain env hi n

69+ chi <- constrain env hi n

66− return $ and [clo, chi, list n === tipe]

70+ return $ and [clo, chi, list n === tipe]

67

71

68 ExplicitList exprs ->

72 ExplicitList exprs ->

69− exists $ \x -> do

73+ exists $ \x ->

70− cs <- mapM (\e -> constrain env e x) exprs

74+ do constraints <- mapM (\e -> constrain env e x) exprs

71− return . and $ list x === tipe : cs

75+ return . and $ list x === tipe : constraints

72

76

73 Binop op e1 e2 ->

77 Binop op e1 e2 ->

74 exists $ \t1 ->

78 exists $ \t1 ->

75− exists $ \t2 -> do

79+ exists $ \t2 ->

76− c1 <- constrain env e1 t1

80+ do c1 <- constrain env e1 t1

77− c2 <- constrain env e2 t2

81+ c2 <- constrain env e2 t2

78− return $ and [ c1, c2, V.toString op <? (t1 ==> t2 ==> tipe) ]

82+ return $ and [ c1, c2, V.toString op <? (t1 ==> t2 ==> tipe) ]

79

83

80 Lambda p e ->

84 Lambda p e ->

81 exists $ \t1 ->

85 exists $ \t1 ->

82− exists $ \t2 -> do

86+ exists $ \t2 ->

83− fragment <- try region $ Pattern.constrain env p t1

87+ do fragment <- try region $ Pattern.constrain env p t1

84− c2 <- constrain env e t2

88+ c2 <- constrain env e t2

89+ let c = ex (Fragment.vars fragment)

85− let c = ex (vars fragment) (clet [monoscheme (typeEnv fragment)]

90+ (clet [monoscheme (Fragment.typeEnv fragment)]

86− (typeConstraint fragment /\ c2 ))

91+ (Fragment.typeConstraint fragment /\ c2)

92+ )

87− return $ c /\ tipe === (t1 ==> t2)

93+ return $ c /\ tipe === (t1 ==> t2)

88

94

89 App e1 e2 ->

95 App e1 e2 ->

90− exists $ \t -> do

96+ exists $ \t ->

91− c1 <- constrain env e1 (t ==> tipe)

97+ do c1 <- constrain env e1 (t ==> tipe)

92− c2 <- constrain env e2 t

98+ c2 <- constrain env e2 t

93− return $ c1 /\ c2

99+ return $ c1 /\ c2

94−

100+

101+ MultiIf branches ->

95− MultiIf branches -> and <$> mapM constrain' branches

102+ and <$> mapM constrain' branches

96− where

103+ where

97− bool = Env.get env Env.types "Bool"

104+ bool = Env.get env Env.types "Bool"

105+

98− constrain' (b,e) = do

106+ constrain' (cond, expr) =

99− cb <- constrain env b bool

107+ do cb <- constrain env cond bool

100− ce <- constrain env e tipe

108+ ce <- constrain env expr tipe

101 return (cb /\ ce)

109 return (cb /\ ce)

102

110

103− Case exp branches ->

111+ Case expr branches ->

104− exists $ \t -> do

112+ exists $ \t ->

105− ce <- constrain env exp t

113+ do ce <- constrain env expr t

106− let branch (p,e) = do

114+ and . (:) ce <$> mapM (branch t) branches

115+ where

116+ branch t (pattern, branchExpr) =

107− fragment <- try region $ Pattern.constrain env p t

117+ do fragment <- try region $ Pattern.constrain env pattern t

108− clet [toScheme fragment] <$> constrain env e tipe

118+ clet [Fragment.toScheme fragment] <$> constrain env branchExpr tipe

109− and . (:) ce <$> mapM branch branches

110

119

111 Data name exprs ->

120 Data name exprs ->

112− do vars <- forM exprs $ \_ -> liftIO (variable Flexible)

121+ do vars <- forM exprs $ \_ -> liftIO (variable Flexible)

113− let pairs = zip exprs (map varN vars)

122+ let pairs = zip exprs (map varN vars)

114− (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)

123+ (ctipe, cs) <- Monad.foldM step (tipe,true) (reverse pairs)

115− return $ ex vars (cs /\ name <? ctipe)

124+ return $ ex vars (cs /\ name <? ctipe)

116 where

125 where

117− step (t,c) (e,x) = do

126+ step (t,c) (e,x) =

118− c' <- constrain env e x

127+ do c' <- constrain env e x

119− return (x ==> t, c /\ c')

128+ return (x ==> t, c /\ c')

120

129

121− Access e label ->

130+ Access expr label ->

122 exists $ \t ->

131 exists $ \t ->

123− constrain env e (record (Map.singleton label [tipe]) t)

132+ constrain env expr (record (Map.singleton label [tipe]) t)

124

133

125− Remove e label ->

134+ Remove expr label ->

126 exists $ \t ->

135 exists $ \t ->

127− constrain env e (record (Map.singleton label [t]) tipe)

136+ constrain env expr (record (Map.singleton label [t]) tipe)

128

137

129− Insert e label value ->

138+ Insert expr label value ->

130 exists $ \tVal ->

139 exists $ \tVal ->

131− exists $ \tRec -> do

140+ exists $ \tRec ->

132− cVal <- constrain env value tVal

141+ do cVal <- constrain env value tVal

133− cRec <- constrain env e tRec

142+ cRec <- constrain env expr tRec

134− let c = tipe === record (Map.singleton label [tVal]) tRec

143+ let c = tipe === record (Map.singleton label [tVal]) tRec

135− return (and [cVal, cRec, c])

144+ return (and [cVal, cRec, c])

136

145

137− Modify e fields ->

146+ Modify expr fields ->

138− exists $ \t -> do

147+ exists $ \t ->

139− oldVars <- forM fields $ \_ -> liftIO (variable Flexible)

148+ do oldVars <- forM fields $ \_ -> liftIO (variable Flexible)

140− let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))

149+ let oldFields = ST.fieldMap (zip (map fst fields) (map varN oldVars))

141− cOld <- ex oldVars <$> constrain env e (record oldFields t)

150+ cOld <- ex oldVars <$> constrain env expr (record oldFields t)

142

151

143− newVars <- forM fields $ \_ -> liftIO (variable Flexible)

152+ newVars <- forM fields $ \_ -> liftIO (variable Flexible)

144− let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))

153+ let newFields = ST.fieldMap (zip (map fst fields) (map varN newVars))

145− let cNew = tipe === record newFields t

154+ let cNew = tipe === record newFields t

146

155

147− cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)

156+ cs <- zipWithM (constrain env) (map snd fields) (map varN newVars)

148

157

149− return $ cOld /\ ex newVars (and (cNew : cs))

158+ return $ cOld /\ ex newVars (and (cNew : cs))

150

159

151 Record fields ->

160 Record fields ->

152− do vars <- forM fields $ \_ -> liftIO (variable Flexible)

161+ do vars <- forM fields $ \_ -> liftIO (variable Flexible)

153− cs <- zipWithM (constrain env) (map snd fields) (map varN vars)

162+ cs <- zipWithM (constrain env) (map snd fields) (map varN vars)

154− let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))

163+ let fields' = ST.fieldMap (zip (map fst fields) (map varN vars))

155− recordType = record fields' (termN EmptyRecord1)

164+ let recordType = record fields' (termN EmptyRecord1)

156− return . ex vars . and $ tipe === recordType : cs

165+ return . ex vars . and $ tipe === recordType : cs

157

166

158 Let defs body ->

167 Let defs body ->

159− do c <- constrain env body tipe

168+ 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))

167

169

168− Port _ _ ->

170+ (Info schemes rqs fqs headers c2 c1) <-

169− return true

171+ Monad.foldM

172+ (constrainDef env)

173+ (Info [] [] [] Map.empty true true)

174+ (concatMap expandPattern defs)

170

175

176+ let letScheme = [ Scheme rqs fqs (clet [monoscheme headers] c2) headers ]

171

177

172−constrainDef env info (Canonical.Definition pattern expr maybeTipe) =

178+ return $ clet schemes (clet letScheme (c1 /\ c))

173− let qs = [] -- should come from the def, but I'm not sure what would live there...

179+

174− (schemes, rigidQuantifiers, flexibleQuantifiers, headers, c2, c1) = info

180+ Port _ _ ->

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 )

195−

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

181+ return true

203− , rigidVars ++ rigidQuantifiers

204− , v : flexibleQuantifiers

205− , Map.insert name tipe headers

206− , c /\ c2

207− , c1 )

208−

209− _ -> error ("problem in constrainDef with " ++ show pattern)

210

182

211

183

212expandPattern :: Canonical.Def -> [Canonical.Def]

184expandPattern :: Canonical.Def -> [Canonical.Def]

213expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =

185expandPattern def@(Canonical.Definition pattern lexpr@(A r _) maybeType) =

214 case pattern of

186 case pattern of

215− P.Var _ -> [def]

187+ P.Var _ ->

188+ [def]

189+ _ ->

216− _ -> Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars

190+ Canonical.Definition (P.Var x) lexpr maybeType : map toDef vars

217− where

191+ where

218− vars = P.boundVarList pattern

192+ vars = P.boundVarList pattern

219− x = "$" ++ concat vars

193+ x = "$" ++ concat vars

220− mkVar = A r . localVar

194+ mkVar = A r . localVar

221− toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing

195+ toDef y = Canonical.Definition (P.Var y) (A r $ Case (mkVar x) [(pattern, mkVar y)]) Nothing

222

196

223

197

224try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a

198try :: Region -> ErrorT (Region -> PP.Doc) IO a -> ErrorT [PP.Doc] IO a

227 case result of

201 case result of

228 Left err -> throwError [err region]

202 Left err -> throwError [err region]

229 Right value -> return value

203 Right value -> return value

204+

205+

206+-- CONSTRAIN DEFINITIONS

207+

208+data Info = Info

209+ { iSchemes :: [TypeScheme]

210+ , iRigid :: [Variable]

211+ , iFlex :: [Variable]

212+ , iHeaders :: Map.Map String Type

213+ , iC2 :: TypeConstraint

214+ , iC1 :: TypeConstraint

215+ }

216+

217+

218+constrainDef :: Env.Environment -> Info -> Canonical.Def -> ErrorT [PP.Doc] IO Info

219+constrainDef env info (Canonical.Definition pattern expr maybeTipe) =

220+ let qs = [] -- should come from the def, but I'm not sure what would live there...

221+ in

222+ case (pattern, maybeTipe) of

223+ (P.Var name, Just tipe) ->

224+ constrainAnnotatedDef env info qs name expr tipe

225+

226+ (P.Var name, Nothing) ->

227+ constrainUnannotatedDef env info qs name expr

228+

229+ _ -> error ("problem in constrainDef with " ++ show pattern)

230+

231+

232+constrainAnnotatedDef

233+ :: Env.Environment

234+ -> Info

235+ -> [String]

236+ -> String

237+ -> Canonical.Expr

238+ -> ST.CanonicalType

239+ -> ErrorT [PP.Doc] IO Info

240+constrainAnnotatedDef env info qs name expr tipe =

241+ do -- Some mistake may be happening here. Currently, qs is always [].

242+ rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)

243+

244+ flexiVars <- forM qs (\_ -> liftIO $ variable Flexible)

245+

246+ let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs flexiVars

247+

248+ let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }

249+

250+ (vars, typ) <- Env.instantiateType env tipe Map.empty

251+

252+ let scheme =

253+ Scheme

254+ { rigidQuantifiers = []

255+ , flexibleQuantifiers = flexiVars ++ vars

256+ , constraint = Ann.noneNoDocs CTrue

257+ , header = Map.singleton name typ

258+ }

259+

260+ c <- constrain env' expr typ

261+

262+ return $ info

263+ { iSchemes = scheme : iSchemes info

264+ , iC1 = fl rigidVars c /\ iC1 info

265+ }

266+

267+

268+constrainUnannotatedDef

269+ :: Env.Environment

270+ -> Info

271+ -> [String]

272+ -> String

273+ -> Canonical.Expr

274+ -> ErrorT [PP.Doc] IO Info

275+constrainUnannotatedDef env info qs name expr =

276+ do -- Some mistake may be happening here. Currently, qs is always [].

277+ rigidVars <- forM qs (\_ -> liftIO $ variable Rigid)

278+

279+ v <- liftIO $ variable Flexible

280+

281+ let tipe = varN v

282+

283+ let inserts = zipWith (\arg typ -> Map.insert arg (varN typ)) qs rigidVars

284+

285+ let env' = env { Env.value = List.foldl' (\x f -> f x) (Env.value env) inserts }

286+

287+ c <- constrain env' expr tipe

288+

289+ return $ info

290+ { iRigid = rigidVars ++ iRigid info

291+ , iFlex = v : iFlex info

292+ , iHeaders = Map.insert name tipe (iHeaders info)

293+ , iC2 = c /\ iC2 info

294+ }