cc9895d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'improve-universe-solver' of https://github.com/ozgurakgun/Idris-dev into ozgurakgun-improve-universe-solver

Conflicts: src/Idris/Core/Constraints.hs

commitcc9895d3d732cadfd0eecac3933c3afa0c39c835 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 22 Mar 2015, 12:24 (12 years ago) parentd57d60a baad761

4 files changed+152−62

compare with master

unifiedsplit

src/Idris/Core/Constraints.hs+72−22 src/Idris/Core/Typecheck.hs+62−30 src/Idris/Elab/Data.hs+13−4 test/error001/expected+5−6

src/Idris/Core/Constraints.hs+72−22

@@ -62,14 +62,34 @@ solve maxUniverseLevel ucs =

6262 ]

6363 }

6464

65− -- | a map from variables to the list of constraints the variable occurs in.

66− constraints :: M.Map Var (S.Set ConstraintFC)

67− constraints = M.fromListWith S.union

68− [ (v, S.singleton (ConstraintFC c fc))

69− | ConstraintFC c fc <- inpConstraints

65+ lhs (ULT (UVar x) _) = Just (Var x)

66+ lhs (ULE (UVar x) _) = Just (Var x)

67+ lhs _ = Nothing

68+

69+ rhs (ULT _ (UVar x)) = Just (Var x)

70+ rhs (ULE _ (UVar x)) = Just (Var x)

71+ rhs _ = Nothing

72+

73+ -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)

74+ constraintsLHS :: M.Map Var (S.Set (UConstraint, FC))

75+ constraintsLHS = M.fromListWith S.union

76+ [ (v, S.singleton (c,fc))

77+ | (c, fc) <- inpConstraints

7078 , let vars = varsIn c

7179 , length vars > 1 -- do not register unary constraints

7280 , v <- vars

81+ , lhs c == Just v

82+ ]

83+

84+ -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)

85+ constraintsRHS :: M.Map Var (S.Set (UConstraint, FC))

86+ constraintsRHS = M.fromListWith S.union

87+ [ (v, S.singleton (c,fc))

88+ | (c, fc) <- inpConstraints

89+ , let vars = varsIn c

90+ , length vars > 1 -- do not register unary constraints

91+ , v <- vars

92+ , rhs c == Just v

7393 ]

7494

7595 -- | this is where the actual work is done.

@@ -87,15 +107,15 @@ solve maxUniverseLevel ucs =

87107 ULE a b -> do

88108 Domain lowerA upperA <- domainOf a

89109 Domain lowerB upperB <- domainOf b

90− when (upperB < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB)

91− when (lowerA > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA upperB)

110+ when (upperB < upperA) $ updateUpperBoundOf (cons, fc) a upperB

111+ when (lowerA > lowerB) $ updateLowerBoundOf (cons, fc) b lowerA

92112 ULT a b -> do

93113 Domain lowerA upperA <- domainOf a

94114 Domain lowerB upperB <- domainOf b

95115 let upperB_pred = pred upperB

96116 let lowerA_succ = succ lowerA

97− when (upperB_pred < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB_pred)

98− when (lowerA_succ > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA_succ upperB)

117+ when (upperB_pred < upperA) $ updateUpperBoundOf (cons, fc) a upperB_pred

118+ when (lowerA_succ > lowerB) $ updateLowerBoundOf (cons, fc) b lowerA_succ

99119 propagate

100120

101121 -- | extract a solution from the state.

@@ -121,13 +141,12 @@ solve maxUniverseLevel ucs =

121141 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)

122142 domainOf (UVal val) = return (Domain val val)

123143

124− -- | updates the domain of a variable.

125− -- this function is also where we fail, inc ase of a domain wipe-out.

126− updateDomainOf :: ConstraintFC -> UExp -> Domain -> StateT SolverState TC ()

127− updateDomainOf suspect (UVar var) newDom = do

144+ updateUpperBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()

145+ updateUpperBoundOf suspect (UVar var) upper = do

128146 doms <- gets domainStore

129− let (oldDom, suspects) = doms M.! Var var

130− when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines

147+ let (oldDom@(Domain lower _), suspects) = doms M.! Var var

148+ let newDom = Domain lower upper

149+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines

131150 $ "Universe inconsistency."

132151 : ("Working on: " ++ show (UVar var))

133152 : ("Old domain: " ++ show oldDom)

@@ -135,17 +154,48 @@ solve maxUniverseLevel ucs =

135154 : "Involved constraints: "

136155 : map (("\t"++) . show) (suspect : S.toList suspects)

137156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

138− addToQueue (Var var)

139− updateDomainOf _ UVal{} _ = return ()

157+ addToQueueRHS (fst suspect) (Var var)

158+ updateUpperBoundOf _ UVal{} _ = return ()

159+

160+ updateLowerBoundOf :: (UConstraint, FC) -> UExp -> Int -> StateT SolverState TC ()

161+ updateLowerBoundOf suspect (UVar var) lower = do

162+ doms <- gets domainStore

163+ let (oldDom@(Domain _ upper), suspects) = doms M.! Var var

164+ let newDom = Domain lower upper

165+ when (wipeOut newDom) $ lift $ Error $ At (snd suspect) $ Msg $ unlines

166+ $ "Universe inconsistency."

167+ : ("Working on: " ++ show (UVar var))

168+ : ("Old domain: " ++ show oldDom)

169+ : ("New domain: " ++ show newDom)

170+ : "Involved constraints: "

171+ : map (("\t"++) . show) (suspect : S.toList suspects)

172+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }

173+ addToQueueLHS (fst suspect) (Var var)

174+ updateLowerBoundOf _ UVal{} _ = return ()

175+

176+ -- | add all constraints (with the given var on the lhs) to the queue

177+ addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()

178+ addToQueueLHS thisCons var =

179+ case M.lookup var constraintsLHS of

180+ Nothing -> return ()

181+ Just cs -> do

182+ Queue list set <- gets queue

183+ let set' = S.insert thisCons set

184+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]

185+ if null newCons

186+ then return ()

187+ else modify $ \ st -> st { queue = Queue (list ++ newCons)

188+ (S.union set (S.fromList (map fst newCons))) }

140189

141− -- | add all constraints related to a variable.

142− addToQueue :: MonadState SolverState m => Var -> m ()

143− addToQueue var =

144− case M.lookup var constraints of

190+ -- | add all constraints (with the given var on the rhs) to the queue

191+ addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()

192+ addToQueueRHS thisCons var =

193+ case M.lookup var constraintsRHS of

145194 Nothing -> return ()

146195 Just cs -> do

147196 Queue list set <- gets queue

148− let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set ]

197+ let set' = S.insert thisCons set

198+ let newCons = [ c | c <- S.toList cs, fst c `S.notMember` set' ]

149199 if null newCons

150200 then return ()

151201 else modify $ \ st -> st { queue = Queue (list ++ newCons)

src/Idris/Core/Typecheck.hs+62−30

@@ -69,7 +69,7 @@ check ctxt env tm

6969 = evalStateT (check' True ctxt env tm) (0, []) -- Holes allowed

7070

7171check' :: Bool -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

72−check' holes ctxt env top = chk (TType (UVar (-5))) env top where

72+check' holes ctxt env top = chk (TType (UVar (-5))) Nothing env top where

7373

7474 smaller (UType NullType) _ = UType NullType

7575 smaller _ (UType NullType) = UType NullType

@@ -78,23 +78,47 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

7878 smaller x _ = x

7979

8080 chk :: Type -> -- uniqueness level

81+ Maybe UExp -> -- maximum universe level, if known

8182 Env -> Raw -> StateT UCs TC (Term, Type)

82− chk u env (Var n)

83+ chk u maxu env (Var n)

8384 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

8485 -- If we're elaborating, we don't want the private names; if we're

8586 -- checking an already elaborated term, we do

8687 | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt

8788 = return (P nt n' ty, ty)

8889 | otherwise = do lift $ tfail $ NoSuchVariable n

89− chk u env ap@(RApp f a)

90− = do (fv, fty) <- chk u env f

91− (av, aty) <- chk u env a

90+ chk u maxu env ap@(RApp f RType) | not holes

91+ -- special case to reduce constraintss

92+ = do (fv, fty) <- chk u maxu env f

9293 let fty' = case uniqueBinders (map fst env) (finalise fty) of

9394 ty@(Bind x (Pi i s k) t) -> ty

9495 _ -> uniqueBinders (map fst env)

9596 $ case hnf ctxt env fty of

9697 ty@(Bind x (Pi i s k) t) -> ty

9798 _ -> normalise ctxt env fty

99+ case fty' of

100+ Bind x (Pi i (TType v') k) t ->

101+ do (v, cs) <- get

102+ put (v+1, ULT (UVar v) v' : cs)

103+ let apty = simplify initContext env

104+ (Bind x (Let (TType v') (TType (UVar v))) t)

105+ return (App fv (TType (UVar v)), apty)

106+ Bind x (Pi i s k) t ->

107+ do (av, aty) <- chk u maxu env RType

108+ convertsC ctxt env aty s

109+ let apty = simplify initContext env

110+ (Bind x (Let aty av) t)

111+ return (App fv av, apty)

112+ t -> lift $ tfail $ NonFunctionType fv fty

113+ chk u maxu env ap@(RApp f a)

114+ = do (fv, fty) <- chk u maxu env f

115+ let fty' = case uniqueBinders (map fst env) (finalise fty) of

116+ ty@(Bind x (Pi i s k) t) -> ty

117+ _ -> uniqueBinders (map fst env)

118+ $ case hnf ctxt env fty of

119+ ty@(Bind x (Pi i s k) t) -> ty

120+ _ -> normalise ctxt env fty

121+ (av, aty) <- chk u maxu env a

98122 case fty' of

99123 Bind x (Pi i s k) t ->

100124 do convertsC ctxt env aty s

@@ -102,13 +126,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

102126 (Bind x (Let aty av) t)

103127 return (App fv av, apty)

104128 t -> lift $ tfail $ NonFunctionType fv fty

105− chk u env RType

129+ chk u maxu env RType

106130 | holes = return (TType (UVal 0), TType (UVal 0))

107131 | otherwise = do (v, cs) <- get

108132 let c = ULT (UVar v) (UVar (v+1))

109133 put (v+2, (c:cs))

110134 return (TType (UVar v), TType (UVar (v+1)))

111− chk u env (RUType un)

135+ chk u maxu env (RUType un)

112136 | holes = return (UType un, TType (UVal 0))

113137 | otherwise = do -- TODO! Issue #1715 on the issue tracker.

114138 -- https://github.com/idris-lang/Idris-dev/issues/1715

@@ -117,8 +141,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

117141 -- put (v+2, (c:cs))

118142 -- return (TType (UVar v), TType (UVar (v+1)))

119143 return (UType un, TType (UVal 0))

120− chk u env (RConstant Forgot) = return (Erased, Erased)

121− chk u env (RConstant c) = return (Constant c, constType c)

144+ chk u maxu env (RConstant Forgot) = return (Erased, Erased)

145+ chk u maxu env (RConstant c) = return (Constant c, constType c)

122146 where constType (I _) = Constant (AType (ATInt ITNative))

123147 constType (BI _) = Constant (AType (ATInt ITBig))

124148 constType (Fl _) = Constant (AType ATFloat)

@@ -135,17 +159,25 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

135159 constType TheWorld = Constant WorldType

136160 constType Forgot = Erased

137161 constType _ = TType (UVal 0)

138− chk u env (RForce t) = do (_, ty) <- chk u env t

139− return (Erased, ty)

140− chk u env (RBind n (Pi i s k) t)

141− = do (sv, st) <- chk u env s

142− (kv, kt) <- chk u env k

143− (tv, tt) <- chk st ((n, Pi i sv kv) : env) t

162+ chk u maxu env (RForce t) = do (_, ty) <- chk u maxu env t

163+ return (Erased, ty)

164+ chk u maxu env (RBind n (Pi i s k) t)

165+ = do (sv, st) <- chk u Nothing env s

166+ vcs <- get

167+ (kv, kt) <- chk u Nothing env k

168+ put vcs -- no need to validate these constraints, they are independent

144169 (v, cs) <- get

170+ nmaxu <- case maxu of

171+ Nothing -> do put (v+1, cs)

172+ return (UVar v)

173+ Just m -> return m

174+ (tv, tt) <- chk st (Just nmaxu) ((n, Pi i sv kv) : env) t

145175 case (normalise ctxt env st, normalise ctxt env tt) of

146176 (TType su, TType tu) -> do

147− when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)

148− let k' = st `smaller` kv `smaller` TType (UVar v) `smaller` u

177+ when (not holes) $ do (v, cs) <- get

178+ put (v, ULE su nmaxu :

179+ ULE tu nmaxu : cs)

180+ let k' = TType (UVar v) `smaller` st `smaller` kv `smaller` u

149181 return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

150182 (pToV n tv), k')

151183 (un, un') ->

@@ -168,27 +200,27 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

168200 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)

169201 mostUnique (_ : es) k = mostUnique es k

170202

171− chk u env (RBind n b sc)

203+ chk u maxu env (RBind n b sc)

172204 = do (b', bt') <- checkBinder b

173− (scv, sct) <- chk (smaller bt' u) ((n, b'):env) sc

205+ (scv, sct) <- chk (smaller bt' u) maxu ((n, b'):env) sc

174206 discharge n b' bt' (pToV n scv) (pToV n sct)

175207 where checkBinder (Lam t)

176− = do (tv, tt) <- chk u env t

208+ = do (tv, tt) <- chk u maxu env t

177209 let tv' = normalise ctxt env tv

178210 let tt' = normalise ctxt env tt

179211 lift $ isType ctxt env tt'

180212 return (Lam tv, tt')

181213 checkBinder (Let t v)

182− = do (tv, tt) <- chk u env t

183− (vv, vt) <- chk u env v

214+ = do (tv, tt) <- chk u maxu env t

215+ (vv, vt) <- chk u maxu env v

184216 let tv' = normalise ctxt env tv

185217 let tt' = normalise ctxt env tt

186218 convertsC ctxt env vt tv

187219 lift $ isType ctxt env tt'

188220 return (Let tv vv, tt')

189221 checkBinder (NLet t v)

190− = do (tv, tt) <- chk u env t

191− (vv, vt) <- chk u env v

222+ = do (tv, tt) <- chk u maxu env t

223+ (vv, vt) <- chk u maxu env v

192224 let tv' = normalise ctxt env tv

193225 let tt' = normalise ctxt env tt

194226 convertsC ctxt env vt tv

@@ -197,13 +229,13 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

197229 checkBinder (Hole t)

198230 | not holes = lift $ tfail (IncompleteTerm undefined)

199231 | otherwise

200− = do (tv, tt) <- chk u env t

232+ = do (tv, tt) <- chk u maxu env t

201233 let tv' = normalise ctxt env tv

202234 let tt' = normalise ctxt env tt

203235 lift $ isType ctxt env tt'

204236 return (Hole tv, tt')

205237 checkBinder (GHole i t)

206− = do (tv, tt) <- chk u env t

238+ = do (tv, tt) <- chk u maxu env t

207239 let tv' = normalise ctxt env tv

208240 let tt' = normalise ctxt env tt

209241 lift $ isType ctxt env tt'

@@ -211,15 +243,15 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

211243 checkBinder (Guess t v)

212244 | not holes = lift $ tfail (IncompleteTerm undefined)

213245 | otherwise

214− = do (tv, tt) <- chk u env t

215− (vv, vt) <- chk u env v

246+ = do (tv, tt) <- chk u maxu env t

247+ (vv, vt) <- chk u maxu env v

216248 let tv' = normalise ctxt env tv

217249 let tt' = normalise ctxt env tt

218250 convertsC ctxt env vt tv

219251 lift $ isType ctxt env tt'

220252 return (Guess tv vv, tt')

221253 checkBinder (PVar t)

222− = do (tv, tt) <- chk u env t

254+ = do (tv, tt) <- chk u maxu env t

223255 let tv' = normalise ctxt env tv

224256 let tt' = normalise ctxt env tt

225257 lift $ isType ctxt env tt'

@@ -227,7 +259,7 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

227259 -- to tell if it's a collapsible variable)

228260 return (PVar tv, tt')

229261 checkBinder (PVTy t)

230− = do (tv, tt) <- chk u env t

262+ = do (tv, tt) <- chk u maxu env t

231263 let tv' = normalise ctxt env tv

232264 let tt' = normalise ctxt env tt

233265 lift $ isType ctxt env tt'

src/Idris/Elab/Data.hs+13−4

@@ -64,7 +64,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

6464 = do let codata = Codata `elem` opts

6565 iLOG (show fc)

6666 undef <- isUndefined fc n

67− (cty, _, t, inacc) <- buildType info syn fc [] n t_in

67+ (cty, ckind, t, inacc) <- buildType info syn fc [] n t_in

6868 -- if n is defined already, make sure it is just a type declaration

6969 -- with the same type we've just elaborated, and no constructors

7070 -- yet

@@ -76,7 +76,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

7676 let unique = case getRetTy cty of

7777 UType UniqueType -> True

7878 _ -> False

79− cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

79+ cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty) ckind) dcons

8080 ttag <- getName

8181 i <- getIState

8282 let as = map (const (Left (Msg ""))) (getArgTys cty)

@@ -210,16 +210,18 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

210210 }

211211

212212elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

213− Type -> -- for kind checking

213+ Type -> -- for unique kind checking

214+ Type -> -- data type's kind

214215 (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->

215216 Idris (Name, Type)

216−elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217+elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

217218 = do checkUndefined fc n

218219 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

219220 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

220221 ctxt <- getContext

221222 let cty' = normalise ctxt [] cty

222223 checkUniqueKind ckind expkind

224+ addDataConstraint ckind dkind

223225

224226 -- Check that the constructor type is, in fact, a part of the family being defined

225227 tyIs n cty'

@@ -280,6 +282,13 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

280282 checkUniqueKind (UType AllTypes) _ = return ()

281283 checkUniqueKind _ _ = return ()

282284

285+ -- Constructor's kind must be <= expected kind

286+ addDataConstraint (TType con) (TType exp)

287+ = do ctxt <- getContext

288+ let v = next_tvar ctxt

289+ addConstraints fc (v, [ULT con exp])

290+ addDataConstraint _ _ = return ()

291+

283292type EliminatorState = StateT (Map.Map String Int) Idris

284293

285294-- -- Issue #1616 in the issue tracker.

test/error001/expected+5−6

@@ -1,10 +1,9 @@

11test002.idr:5:6:Universe inconsistency.

2−Working on: f2

3−Old domain: Domain 7 7

4−New domain: Domain 7 6

2+Working on: e2

3+Old domain: Domain 4 4

4+New domain: Domain 4 3

55Involved constraints:

6− (f2 <= i1,test002.idr:5:6)

76 (e2 < f2,test002.idr:5:6)

8− (j1 <= f2,test002.idr:5:6)

9− (f2 <= i1,test002.idr:5:6)

7+ (e2 < f2,test002.idr:5:6)

8+ (i1 <= e2,test002.idr:5:6)

109