87b4ffc · tix · git.iko.soy

git.iko.soy/tix

on master help sign in

Greatly simplified (delayed) substitutions.

87b4ffciko6 years ago

src/Tix/Typechecker.hs+52−92

compare with master

unifiedsplit

@@ -56,13 +56,13 @@ import Prelude as P

57getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [InferError], [UnifyingError], [PredicateError], A.Object)

58getType r =

59− let ((((((((t, traceTree), inf), predicate), unifying), errs), _srcs), subs), _) =

59+ let ((((((t, traceTree), inf), predicate), unifying), errs), _srcs) =

60 run

61 . runReader nullSpan

62 . evalState @(MKM.Map Pred) mempty

63 . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))

64 . evalState (M.empty :: VariableMap)

65− . runConstraintEnv

65+ . evalState @Substitution mempty

66 . runState @[(TypeVariable, SrcSpan)] []

67 . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))

68 . runSeqWriter @[(SrcSpan, Errors)]

@@ -72,31 +72,7 @@ getType r =

72 . runFreshSrc

73 . runTreeTracer

74 $ inferGeneral r

75− in (sub subs t, errs, inf, unifying, predicate, traceTree)

75+ in (t, errs, inf, unifying, predicate, traceTree)

76−

77−runConstraintEnv ::

78− Members '[State VariableMap, State (MKM.Map Pred)] effs =>

79− Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : effs) a ->

80− Eff effs ((a, Substitution), Seq Constraint)

81−runConstraintEnv f = do

82− ((x, subs), cs) <-

83− runState @(Seq Constraint) Empty

84− . interpret @(Writer Constraint) (\(Tell x) -> modify (x :<|))

85− . runWriter @Substitution

86− . interpret @SubstituteEnv

87− ( \(SubstituteEnv x) -> do

88− -- modify @(Seq Constraint) (sub x <$>)

89− -- TODone: I have a feeling that variables in the env should already be closed over.

90− -- (aka this is redundant)

91− --

92− -- No, they can have type variables. E g when they are arguments in a function.

93− modify @VariableMap (sub x <$>)

94− modify @(MKM.Map Pred) (sub x)

95− tell x

96− return ()

97− )

98− $ f

99− return ((x, subs), sub subs <$> cs)

100

101runFreshSrc ::

77runFreshSrc ::

102 Members '[Reader SrcSpan, Writer (TypeVariable, SrcSpan)] eff =>

78 Members '[Reader SrcSpan, Writer (TypeVariable, SrcSpan)] eff =>

@@ -113,27 +89,6 @@ runFreshSrc =

113 MinFreshFromNow -> send MinFreshFromNow

89 MinFreshFromNow -> send MinFreshFromNow

114 )

90 )

115

116−captureSubstitutions ::

117− Members '[SubstituteEnv] effs =>

118− Eff (Writer Substitution : effs) a ->

119− Eff effs (a, Substitution)

120−captureSubstitutions f = do

121− (x, s) <-

122− runWriter @Substitution

123− . interpose @SubstituteEnv

124− ( \(SubstituteEnv x) -> do

125− tell x

126− subEnv x

127− )

128− $ f

129− return (x, s)

130−

131−data SubstituteEnv a where

132− SubstituteEnv :: Substitution -> SubstituteEnv ()

133−

134−subEnv :: Member SubstituteEnv r => Substitution -> Eff r ()

135−subEnv = send . SubstituteEnv

136−

137data Constraint = !NType :~ !NType

92data Constraint = !NType :~ !NType

138 deriving stock (Eq, Ord, Show)

93 deriving stock (Eq, Ord, Show)

139

@@ -178,6 +133,10 @@ instance Free a => Free [a] where

178 free = foldMap free

133 free = foldMap free

179 sub s = fmap (sub s)

134 sub s = fmap (sub s)

180

135

136+instance Free a => Free (Seq a) where

137+ free = foldMap free

138+ sub s = fmap (sub s)

139+

181instance Free Substitution where

140instance Free Substitution where

182 free (Substitution s) = free . M.elems $ s

141 free (Substitution s) = free . M.elems $ s

183 sub new old = old <> new

142 sub new old = old <> new

@@ -200,7 +159,6 @@ newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}

200prettySubstitution :: Substitution -> A.Value

159prettySubstitution :: Substitution -> A.Value

201prettySubstitution = A.toJSON . M.mapKeysMonotonic (TL.pack . show) . fmap renderPretty . unSubstitution

160prettySubstitution = A.toJSON . M.mapKeysMonotonic (TL.pack . show) . fmap renderPretty . unSubstitution

202

161

203−-- | @older <> newer@

204instance Semigroup Substitution where

162instance Semigroup Substitution where

205 x'@(Substitution x) <> y'@(Substitution y) = Substitution (M.unionWithKey (error "invariant") (fmap (sub y') x) (fmap (sub x') y))

163 x'@(Substitution x) <> y'@(Substitution y) = Substitution (M.unionWithKey (error "invariant") (fmap (sub y') x) (fmap (sub x') y))

206

164

@@ -214,22 +172,23 @@ instance Free Constraint where

214(<<-) ::

172(<<-) ::

215 TypeVariable ->

173 TypeVariable ->

216 NType ->

174 NType ->

217− UnifyM Substitution

175+ UnifyM ()

218−v <<- (NTypeVariable x) | v == x = return mempty

176+v <<- (NTypeVariable x) | v == x = pure ()

219v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty

177v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty

220 where

178 where

221 occursIn :: Free x => TypeVariable -> x -> Bool

179 occursIn :: Free x => TypeVariable -> x -> Bool

222 occursIn t u = t `S.member` free u

180 occursIn t u = t `S.member` free u

223−v <<- x = return $ Substitution $ M.singleton v x

181+v <<- x = modify (Substitution (M.singleton v x) <>)

224

182

225unifyWithPriority ::

183unifyWithPriority ::

226 -- | The range of type variables to interpret as being lower

184 -- | The range of type variables to interpret as being lower

227 -- priority (try to replace them if possible)

185 -- priority (try to replace them if possible)

228 RS.RSet TypeVariable ->

186 RS.RSet TypeVariable ->

229 Constraint ->

187 Constraint ->

230− UnifyM Substitution

188+ UnifyM ()

231−unifyWithPriority range (lhs :~ rhs) =

189+unifyWithPriority range (lhs :~ rhs) = do

190+ s <- get

232− case (lhs, rhs) of

191+ case sub s (lhs, rhs) of

233 (x, y) | x == y -> return mempty

192 (x, y) | x == y -> return mempty

234 (NTypeVariable x, NTypeVariable y) -> do

193 (NTypeVariable x, NTypeVariable y) -> do

235 if y `RS.member` range

194 if y `RS.member` range

@@ -242,30 +201,29 @@ unifyWithPriority range (lhs :~ rhs) =

242 assertSetsMatch (tell . KeysDontMatch) (M.keysSet x) (M.keysSet y)

201 assertSetsMatch (tell . KeysDontMatch) (M.keysSet x) (M.keysSet y)

243 unifySchemes range . M.elems $ M.intersectionWith (,) x y

202 unifySchemes range . M.elems $ M.intersectionWith (,) x y

244 (x1 :-> y1, x2 :-> y2) -> do

203 (x1 :-> y1, x2 :-> y2) -> do

245− s <- unifyWithPriority range (x1 :~ x2)

204+ unifyWithPriority range (x1 :~ x2)

246− s' <- unifyWithPriority range $ sub s $ y1 :~ y2

205+ unifyWithPriority range $ y1 :~ y2

247− return $ s' <> s

248− (x, y) -> tell (CanNotUnify x y) >> return mempty

206+ (x, y) -> tell (CanNotUnify x y)

249

207

250−unifySchemes :: RS.RSet TypeVariable -> [(Scheme, Scheme)] -> UnifyM Substitution

208+unifySchemes :: RS.RSet TypeVariable -> [(Scheme, Scheme)] -> UnifyM ()

251unifySchemes _ [] = pure mempty

209unifySchemes _ [] = pure mempty

252unifySchemes range ((x, y) : rest) = do

210unifySchemes range ((x, y) : rest) = do

253− s <- unifyScheme range x y

211+ unifyScheme range x y

254− sub s <$> unifySchemes range (sub s rest)

212+ unifySchemes range rest

255

213

256−unifyScheme :: RS.RSet TypeVariable -> Scheme -> Scheme -> UnifyM Substitution

214+unifyScheme :: RS.RSet TypeVariable -> Scheme -> Scheme -> UnifyM ()

257unifyScheme range (xs :=> x) (ys :=> y) = do

215unifyScheme range (xs :=> x) (ys :=> y) = do

258− s <- solveWithPriority range (pure (x :~ y))

216+ solveWithPriority range (pure (x :~ y))

217+ s <- get

259 let f = S.fromList . sub s

218 let f = S.fromList . sub s

260 assertSetsMatch (tell . ConstraintsDontMatch) (f xs) (f ys)

219 assertSetsMatch (tell . ConstraintsDontMatch) (f xs) (f ys)

261− return s

262

220

263assertSetsMatch :: Ord x => Applicative f => (Set x -> f ()) -> Set x -> Set x -> f ()

221assertSetsMatch :: Ord x => Applicative f => (Set x -> f ()) -> Set x -> Set x -> f ()

264assertSetsMatch f x y = case (x S.\\ y, y S.\\ x) of

222assertSetsMatch f x y = case (x S.\\ y, y S.\\ x) of

265 (a, b) | S.null a, S.null b -> pure ()

223 (a, b) | S.null a, S.null b -> pure ()

266 (a, b) -> f $ a <> b

224 (a, b) -> f $ a <> b

267

225

268−solve :: Seq Constraint -> UnifyM Substitution

226+solve :: Seq Constraint -> UnifyM ()

269solve = solveWithPriority mempty

227solve = solveWithPriority mempty

270

228

271solveWithPriority ::

229solveWithPriority ::

@@ -273,11 +231,11 @@ solveWithPriority ::

273 -- priority (try to replace them if possible)

231 -- priority (try to replace them if possible)

274 RS.RSet TypeVariable ->

232 RS.RSet TypeVariable ->

275 Seq Constraint ->

233 Seq Constraint ->

276− UnifyM Substitution

234+ UnifyM ()

277solveWithPriority _ Empty = return mempty

235solveWithPriority _ Empty = return mempty

278solveWithPriority range (rest :|> c) = do

236solveWithPriority range (rest :|> c) = do

279− s <- unifyWithPriority range c

237+ unifyWithPriority range c

280− sub s <$> solveWithPriority range (fmap (sub s) rest)

238+ solveWithPriority range rest

281

239

282data Errors

240data Errors

283 = UndefinedVariable VarName

241 = UndefinedVariable VarName

@@ -300,12 +258,11 @@ data InferError

300 = ConflictingBindingDefinitions (NormalizedBinding' NExprLoc) (NormalizedBinding' NExprLoc)

258 = ConflictingBindingDefinitions (NormalizedBinding' NExprLoc) (NormalizedBinding' NExprLoc)

301 deriving stock (Show)

259 deriving stock (Show)

302

260

303−type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x

261+type UnifyM x = forall r. Members '[Writer UnifyingError, State Substitution] r => Eff r x

304

262

305type InferEffs =

263type InferEffs =

306 '[ Fresh,

264 '[ Fresh,

307 Reader SrcSpan,

265 Reader SrcSpan,

308− Writer Constraint,

309 Writer (SrcSpan, Errors),

266 Writer (SrcSpan, Errors),

310 Writer PredicateError,

267 Writer PredicateError,

311 Writer Pred,

268 Writer Pred,

@@ -313,12 +270,14 @@ type InferEffs =

313 State VariableMap,

270 State VariableMap,

314 Writer UnifyingError,

271 Writer UnifyingError,

315 Writer InferError,

272 Writer InferError,

316− SubstituteEnv,

273+ State Substitution,

317 TreeTracer

274 TreeTracer

318 ]

275 ]

319

276

320type InferM x = forall r. Members InferEffs r => Eff r x

277type InferM x = forall r. Members InferEffs r => Eff r x

321

278

279+type InferM' x = forall r. Members (Writer Constraint : InferEffs) r => Eff r x

280+

322runSeqWriter :: forall s w r a. (IsSequence s, Element s ~ w) => Eff (Writer w ': r) a -> Eff r (a, s)

281runSeqWriter :: forall s w r a. (IsSequence s, Element s ~ w) => Eff (Writer w ': r) a -> Eff r (a, s)

323runSeqWriter = handleRelayS mempty (\s x -> return (x, s)) $ \s (Tell w) k -> k (cons w s) ()

282runSeqWriter = handleRelayS mempty (\s x -> return (x, s)) $ \s (Tell w) k -> k (cons w s) ()

324

283

@@ -385,7 +344,7 @@ instantiate s = do

385 modify (M.insert db t)

344 modify (M.insert db t)

386 return t

345 return t

387

346

388−infer :: NExprLoc -> InferM NType

347+infer :: NExprLoc -> InferM' NType

389infer (Fix (Compose (Ann src x))) = local (const src) $ case x of

348infer (Fix (Compose (Ann src x))) = local (const src) $ case x of

390 NConstant a -> return . NAtomic $ case a of

349 NConstant a -> return . NAtomic $ case a of

391 NURI {} -> URI

350 NURI {} -> URI

@@ -623,11 +582,9 @@ inferComponents n ((S.toList -> paths) : otherComponents) = do

623 -- TODO: There should probably be some smarter predicate filtering

582 -- TODO: There should probably be some smarter predicate filtering

624 schemes <- types & traverse . traverse %%~ (\t -> solveAndClose p $ sub s $ preds :=> t)

583 schemes <- types & traverse . traverse %%~ (\t -> solveAndClose p $ sub s $ preds :=> t)

625

584

626− (otherBindings, s') <-

585+ otherBindings <-

627− captureSubstitutions $

628− withBindings (toScheme' <$> schemes) $

629− inferComponents n otherComponents

586+ withBindings (toScheme' <$> schemes) $ inferComponents n otherComponents

630− return $ M.unionWith mergeBindings (fmap (sub s') <$> schemes) otherBindings

587+ return $ M.unionWith mergeBindings schemes otherBindings

631 where

588 where

632 bindingToNExpr :: NonEmpty VarName -> NExprLoc -> Binding NExpr

589 bindingToNExpr :: NonEmpty VarName -> NExprLoc -> Binding NExpr

633 bindingToNExpr name expr = NamedVar (StaticKey <$> name) (stripAnnotation expr) nullPos

590 bindingToNExpr name expr = NamedVar (StaticKey <$> name) (stripAnnotation expr) nullPos

@@ -730,33 +687,36 @@ showExpr :: NExpr -> Text

730showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix

687showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix

731

688

732inferGeneral :: NExprLoc -> InferM Scheme

689inferGeneral :: NExprLoc -> InferM Scheme

690+inferGeneral x@(Fix (Compose (Ann src _))) =

733−inferGeneral x@(Fix (Compose (Ann src _))) = local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do

691+ local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do

734− (t, p, keep, s) <- inferGeneral' id $ infer x

692+ (t, p, keep, s) <- inferGeneral' id $ infer x

735− solveAndClose p $ sub s $ keep :=> t

693+ solveAndClose p $ sub s $ keep :=> t

736

694

737inferGeneral' ::

695inferGeneral' ::

738 (Members InferEffs r, Pretty y) =>

696 (Members InferEffs r, Pretty y) =>

739 (x -> y) ->

697 (x -> y) ->

740− Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : r) x ->

698+ Eff (Writer Constraint : r) x ->

741 Eff r (x, RS.RSet TypeVariable, [Pred], Substitution)

699 Eff r (x, RS.RSet TypeVariable, [Pred], Substitution)

742inferGeneral' toPretty f = do

700inferGeneral' toPretty f = do

743− (((x, subs), cs), range) <-

701+ ((x, cs), range) <-

744− traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ f

702+ traceSubtree "subexpressions" . registerTypeVariables . runSeqWriter @(Seq Constraint) $ f

745 traceSubtree "received" $ do

703 traceSubtree "received" $ do

746 traceValue "type" $ renderPretty $ toPretty x

704 traceValue "type" $ renderPretty $ toPretty x

747− traceValue "substitutions" $ prettySubstitution subs

705+ get >>= traceValue "substitutions" . prettySubstitution

748 traceValue "constraints" $ fmap renderPretty cs

706 traceValue "constraints" $ fmap renderPretty cs

749 traceValue "range" $ T.pack . show $ range

707 traceValue "range" $ T.pack . show $ range

750 get @(MKM.Map Pred) >>= traceValue "preds" . showPreds

708 get @(MKM.Map Pred) >>= traceValue "preds" . showPreds

751− s' <- solveWithPriority range cs

709+ solveWithPriority range cs

752− traceValue "substitutions_after_solving" $ prettySubstitution s'

710+ get >>= traceValue "substitutions_after_solving" . prettySubstitution

753− let s = subs <> s'

711+ (s, returnedS) <-

712+ get @Substitution

713+ <&> join bimap Substitution . M.partitionWithKey (\k _ -> k `RS.member` range) . unSubstitution

714+ put returnedS

754− returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s

715+ -- modify @Substitution $ Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution

755− traceValue "composed_substitution" $ prettySubstitution s

716+ -- returnedS <- get @Substitution

756 traceSubtree "returned" $ do

717 traceSubtree "returned" $ do

757 traceValue "substitutions" $ prettySubstitution returnedS

718 traceValue "substitutions" $ prettySubstitution returnedS

758 -- Filter for optimization purposes

719 -- Filter for optimization purposes

759− subEnv returnedS

760 preds <- get @(MKM.Map Pred)

720 preds <- get @(MKM.Map Pred)

761 traceValue "subbed_preds" $ showPreds preds

721 traceValue "subbed_preds" $ showPreds preds

762 let newRange = range RS.\\ rangeFromSet (free returnedS)

722 let newRange = range RS.\\ rangeFromSet (free returnedS)

@@ -796,7 +756,7 @@ solveAndClose range (cs :=> t) = do

796 case (constraints, collectedPreds) of

756 case (constraints, collectedPreds) of

797 (Empty, []) -> return . close newRange $ solvedPreds :=> t

757 (Empty, []) -> return . close newRange $ solvedPreds :=> t

798 _ -> do

758 _ -> do

799− s <- solveWithPriority newRange constraints

759+ ((), s) <- runState @Substitution mempty $ solveWithPriority newRange constraints

800 solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t

760 solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t

801

761

802solveConstraints ::

762solveConstraints ::