a854972 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Small reduction in constraint generation

Also prune the set before solving to remove constraints which won't affect the result. Effects needs to have --typeintype set (for the moment) due to the type level list which may contain types, which may themselves be lists.

commita8549728b82e985befa1ff7ba5ad1a48830cdbc1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 9 Jun 2016, 11:06 (10 years ago) parentdc7da6b

11 files changed+99−60

compare with master

unifiedsplit

libs/effects/Effects.idr+4−4 libs/effects/effects.ipkg+1−1 src/Idris/AbsSyntax.hs+7−5 src/Idris/Core/Constraints.hs+31−1 src/Idris/Core/Typecheck.hs+33−30 src/Idris/Elab/Clause.hs+2−1 src/Idris/Elab/Data.hs+9−7 src/Idris/Elab/Utils.hs+3−1 src/Idris/REPL.hs+1−1 test/totality014/expected+3−4 test/universes002/expected+5−5

libs/effects/Effects.idr+4−4

@@ -448,19 +448,19 @@ runEnv env prog = eff env prog (\r, env => pure (r ** env))

448448

449449-- ----------------------------------------------- [ some higher order things ]

450450

451−mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)

451+mapE : (a -> EffM m b xs (\_ => xs)) -> List a -> EffM m (List b) xs (\_ => xs)

452452mapE f [] = pure []

453453mapE f (x :: xs) = [| f x :: mapE f xs |]

454454

455455

456−mapVE : (a -> {xs} EffM m b) ->

456+mapVE : (a -> EffM m b xs (\_ => xs)) ->

457457 Vect n a ->

458− {xs} EffM m (Vect n b)

458+ EffM m (Vect n b) xs (\_ => xs)

459459mapVE f [] = pure []

460460mapVE f (x :: xs) = [| f x :: mapVE f xs |]

461461

462462

463−when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()

463+when : Bool -> Lazy (EffM m () xs (\_ => xs)) -> EffM m () xs (\_ => xs)

464464when True e = Force e

465465when False e = pure ()

466466

libs/effects/effects.ipkg+1−1

@@ -1,6 +1,6 @@

11package effects

3−opts = "--nobasepkgs -i ../prelude -i ../base"

3+opts = "--nobasepkgs --typeintype -i ../prelude -i ../base"

55modules = Effects

66 , Effect.Default

src/Idris/AbsSyntax.hs+7−5

@@ -693,11 +693,13 @@ updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) }

693693

694694addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()

695695addConstraints fc (v, cs)

696− = do i <- getIState

697− let ctxt = tt_ctxt i

698− let ctxt' = ctxt { next_tvar = v }

699− let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)

700− putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

696+ = do tit <- typeInType

697+ when (not tit) $ do

698+ i <- getIState

699+ let ctxt = tt_ctxt i

700+ let ctxt' = ctxt { next_tvar = v }

701+ let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)

702+ putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

701703 where

702704 insertAll [] c = c

703705 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics

src/Idris/Core/Constraints.hs+31−1

@@ -15,16 +15,46 @@ import Control.Monad.State.Strict

1515import Data.List ( partition )

1616import qualified Data.Map.Strict as M

1717import qualified Data.Set as S

18+import Debug.Trace

1819

1920-- | Check that a list of universe constraints can be satisfied.

2021ucheck :: S.Set ConstraintFC -> TC ()

21−ucheck = void . solve 10 . S.filter (not . ignore)

22+ucheck = void . solve 10 . S.filter (not . ignore) . dropUnused

2223 where

2324 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

2425 ignore (ConstraintFC c _) | any (== Var [] (-1)) (varsIn c) = True

2526 ignore (ConstraintFC (ULE a b) _) = a == b

2627 ignore _ = False

2728

29+dropUnused :: S.Set ConstraintFC -> S.Set ConstraintFC

30+dropUnused xs = let cs = S.toList xs

31+ onlhs = countLHS M.empty cs in

32+ addIfUsed S.empty onlhs cs

33+ where

34+ -- Count the number of times a variable occurs on the LHS of a constraint

35+ countLHS ms [] = ms

36+ countLHS ms (c : cs) = let lhvar = getLHS (uconstraint c)

37+ num = case M.lookup lhvar ms of

38+ Nothing -> 1

39+ Just v -> v + 1 in

40+ countLHS (M.insert lhvar num ms) cs

41+

42+ -- Only keep a constraint if the variable on the RHS is used elsewhere

43+ -- on the LHS of a constraint

44+ addIfUsed cs' lhs [] = cs'

45+ addIfUsed cs' lhs (c : cs)

46+ = let rhvar = getRHS (uconstraint c) in

47+ case M.lookup rhvar lhs of

48+ Nothing -> addIfUsed cs' lhs cs

49+ Just v -> addIfUsed (S.insert c cs') lhs cs

50+

51+ getLHS (ULT x _) = x

52+ getLHS (ULE x _) = x

53+

54+ getRHS (ULT _ x) = x

55+ getRHS (ULE _ x) = x

56+

57+

2858data Var = Var String Int

2959 deriving (Eq, Ord, Show)

3060

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

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

8686 = evalStateT (check' True [] ctxt env tm) (0, [])

8787

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

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

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

9090

9191 smaller (UType NullType) _ = UType NullType

9292 smaller _ (UType NullType) = UType NullType

@@ -98,8 +98,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

9898 | otherwise = Complete

9999

100100 chk :: Type -> -- uniqueness level

101+ Maybe UExp -> -- universe for kind

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

102− chk u env (Var n)

103+ chk u lvl env (Var n)

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

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

105106 -- checking an already elaborated term, we do

@@ -109,9 +110,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

109110 | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

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

111112 | otherwise = do lift $ tfail $ NoSuchVariable n

112− chk u env ap@(RApp f RType) | not holes

113+ chk u lvl env ap@(RApp f RType) | not holes

113114 -- special case to reduce constraintss

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

115+ = do (fv, fty) <- chk u Nothing env f

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

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

117118 _ -> uniqueBinders (map fst env)

@@ -126,21 +127,21 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

126127 (Bind x (Let (TType v') (TType (UVar tcns v))) t)

127128 return (App Complete fv (TType (UVar tcns v)), apty)

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

129− do (av, aty) <- chk u env RType

130+ do (av, aty) <- chk u Nothing env RType

130131 convertsC ctxt env aty s

131132 let apty = simplify initContext env

132133 (Bind x (Let aty av) t)

133134 return (App astate fv av, apty)

134135 t -> lift $ tfail $ NonFunctionType fv fty

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

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

136+ chk u lvl env ap@(RApp f a)

137+ = do (fv, fty) <- chk u Nothing env f

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

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

139140 _ -> uniqueBinders (map fst env)

140141 $ case hnf ctxt env fty of

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

142143 _ -> normalise ctxt env fty

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

144+ (av, aty) <- chk u Nothing env a

144145 case fty' of

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

146147 do convertsC ctxt env aty s

@@ -148,13 +149,13 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

148149 (Bind x (Let aty av) t)

149150 return (App astate fv av, apty)

150151 t -> lift $ tfail $ NonFunctionType fv fty

151− chk u env RType

152+ chk u lvl env RType

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

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

154155 let c = ULT (UVar tcns v) (UVar tcns (v+1))

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

156157 return (TType (UVar tcns v), TType (UVar tcns (v+1)))

157− chk u env (RUType un)

158+ chk u lvl env (RUType un)

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

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

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

@@ -163,8 +164,8 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

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

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

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

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

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

167+ chk u lvl env (RConstant Forgot) = return (Erased, Erased)

168+ chk u lvl env (RConstant c) = return (Constant c, constType c)

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

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

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

@@ -177,13 +178,15 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

177178 constType TheWorld = Constant WorldType

178179 constType Forgot = Erased

179180 constType _ = TType (UVal 0)

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

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

181+ chk u lvl env (RBind n (Pi i s k) t)

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

182183 (v, cs) <- get

183− (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent

184+ (kv, kt) <- chk u Nothing env k -- no need to validate these constraints, they are independent

184185 put (v+1, cs)

185− let maxu = UVar tcns v

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

186+ let maxu = case lvl of

187+ Nothing -> UVar tcns v

188+ Just v' -> v'

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

187190

188191-- convertsC ctxt env st (TType maxu)

189192-- convertsC ctxt env tt (TType maxu)

@@ -219,25 +222,25 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

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

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

221224

222− chk u env (RBind n b sc)

225+ chk u lvl env (RBind n b sc)

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

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

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

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

226229 where checkBinder (Lam t)

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

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

228231 let tv' = normalise ctxt env tv

229232 convType tcns ctxt env tt

230233 return (Lam tv, tt)

231234 checkBinder (Let t v)

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

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

235+ = do (tv, tt) <- chk u Nothing env t

236+ (vv, vt) <- chk u Nothing env v

234237 let tv' = normalise ctxt env tv

235238 convertsC ctxt env vt tv

236239 convType tcns ctxt env tt

237240 return (Let tv vv, tt)

238241 checkBinder (NLet t v)

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

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

242+ = do (tv, tt) <- chk u Nothing env t

243+ (vv, vt) <- chk u Nothing env v

241244 let tv' = normalise ctxt env tv

242245 convertsC ctxt env vt tv

243246 convType tcns ctxt env tt

@@ -245,33 +248,33 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

245248 checkBinder (Hole t)

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

247250 | otherwise

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

251+ = do (tv, tt) <- chk u Nothing env t

249252 let tv' = normalise ctxt env tv

250253 convType tcns ctxt env tt

251254 return (Hole tv, tt)

252255 checkBinder (GHole i ns t)

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

256+ = do (tv, tt) <- chk u Nothing env t

254257 let tv' = normalise ctxt env tv

255258 convType tcns ctxt env tt

256259 return (GHole i ns tv, tt)

257260 checkBinder (Guess t v)

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

259262 | otherwise

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

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

263+ = do (tv, tt) <- chk u Nothing env t

264+ (vv, vt) <- chk u Nothing env v

262265 let tv' = normalise ctxt env tv

263266 convertsC ctxt env vt tv

264267 convType tcns ctxt env tt

265268 return (Guess tv vv, tt)

266269 checkBinder (PVar t)

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

270+ = do (tv, tt) <- chk u Nothing env t

268271 let tv' = normalise ctxt env tv

269272 convType tcns ctxt env tt

270273 -- Normalised version, for erasure purposes (it's easier

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

272275 return (PVar tv, tt)

273276 checkBinder (PVTy t)

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

277+ = do (tv, tt) <- chk u Nothing env t

275278 let tv' = normalise ctxt env tv

276279 convType tcns ctxt env tt

277280 return (PVTy tv, tt)

src/Idris/Elab/Clause.hs+2−1

@@ -735,8 +735,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

735735

736736 ctxt <- getContext

737737 let constv = next_tvar ctxt

738+ tit <- typeInType

738739 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

739− OK (_, cs) -> when (PEGenerated `notElem` opts) $ do

740+ OK (_, cs) -> when (PEGenerated `notElem` opts && not tit) $ do

740741 addConstraints fc cs

741742 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

742743 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

src/Idris/Elab/Data.hs+9−7

@@ -281,13 +281,15 @@ addParamConstraints fc ps cty cons

281281 where

282282 constraintTy (Bind n (Pi _ ty _) sc)

283283 = case getRetTy ty of

284− TType avar -> do ctxt <- getContext

285− let tv = next_tvar ctxt

286− let con = if n `elem` pnames

287− then ULE avar cvar

288− else ULT avar cvar

289− addConstraints fc (tv, [con])

290− addIBC (IBCConstraint fc con)

284+ TType avar -> do tit <- typeInType

285+ when (not tit) $ do

286+ ctxt <- getContext

287+ let tv = next_tvar ctxt

288+ let con = if n `elem` pnames

289+ then ULE avar cvar

290+ else ULT avar cvar

291+ addConstraints fc (tv, [con])

292+ addIBC (IBCConstraint fc con)

291293 _ -> return ()

292294 constraintTy t = return ()

293295

src/Idris/Elab/Utils.hs+3−1

@@ -46,7 +46,9 @@ recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

4646 Error e -> tfail (At fc (mkerr e))

4747 OK x -> return x

4848 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

49− when addConstrs $ do addConstraints fc cs

49+ tit <- typeInType

50+ when (not tit && addConstrs) $

51+ do addConstraints fc cs

5052 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

5153 mapM_ (checkDeprecated fc) (allTTNames tm)

5254 mapM_ (checkDeprecated fc) (allTTNames ty)

src/Idris/REPL.hs+1−1

@@ -1047,7 +1047,7 @@ process fn Universes

10471047 let cs = idris_constraints i

10481048 let cslist = S.toAscList cs

10491049-- iputStrLn $ showSep "\n" (map show cs)

1050− iputStrLn $ show (map uconstraint cslist)

1050+ iputStrLn $ showSep "\n" (map show cslist)

10511051 let n = length cslist

10521052 iputStrLn $ "(" ++ show n ++ " constraints)"

10531053 case ucheck cs of

test/totality014/expected+3−4

@@ -1,9 +1,8 @@

1−totality014.idr:6:9:Universe inconsistency.

2− Working on: ./totality014.idr.u

1+totality014.idr:1:6:Universe inconsistency.

2+ Working on: ./totality014.idr.w

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

7− ConstraintFC {uconstraint = ./totality014.idr.u < ./totality014.idr.v, ufc = totality014.idr:1:6}

6+ ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

87 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

98 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

test/universes002/expected+5−5

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

11universes002.idr:45:9:Universe inconsistency.

2− Working on: ./universes002.idr.c7

2+ Working on: ./universes002.idr.b1

33 Old domain: (5,5)

44 New domain: (5,4)

55 Involved constraints:

6− ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}

7− ConstraintFC {uconstraint = ./universes002.idr.c7 < ./universes002.idr.d7, ufc = universes002.idr:15:6}

8− ConstraintFC {uconstraint = ./universes002.idr.e7 < ./universes002.idr.c7, ufc = universes002.idr:15:6}

9− ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}

6+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9}

7+ ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6}

8+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9}

9+ ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6}