d763c9c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Use postulates for decEq primitive proofs

This means we can assert there is a proof at compile-time, but we're not going to rely on the structure of that proof anywhere (which can cause problems if they are relied on elsewhere). Fixes #1005

commitd763c9c3e32be57ffecfe8a694e324185f9f1d8d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 26 Mar 2014, 23:11 (13 years ago) parentdfb3982

3 files changed+18−12

compare with master

unifiedsplit

libs/prelude/Decidable/Equality.idr+15−10 src/IRTS/Compiler.hs+1−1 src/Idris/ElabDecls.hs+2−1

libs/prelude/Decidable/Equality.idr+15−10

@@ -190,39 +190,44 @@ instance DecEq a => DecEq (Vect n a) where

190190--------------------------------------------------------------------------------

191191

192192instance DecEq Int where

193− decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

194− else No (really_believe_me _|_)

193+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

194+ where postulate primitiveEq : x = y

195+ postulate primitiveNotEq : x = y -> _|_

195196

196197--------------------------------------------------------------------------------

197198-- Char

198199--------------------------------------------------------------------------------

199200

200201instance DecEq Char where

201− decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

202− else No (really_believe_me _|_)

202+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

203+ where postulate primitiveEq : x = y

204+ postulate primitiveNotEq : x = y -> _|_

203205

204206--------------------------------------------------------------------------------

205207-- Integer

206208--------------------------------------------------------------------------------

207209

208210instance DecEq Integer where

209− decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

210− else No (really_believe_me _|_)

211+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

212+ where postulate primitiveEq : x = y

213+ postulate primitiveNotEq : x = y -> _|_

211214

212215--------------------------------------------------------------------------------

213216-- Float

214217--------------------------------------------------------------------------------

215218

216219instance DecEq Float where

217− decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

218− else No (really_believe_me _|_)

220+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

221+ where postulate primitiveEq : x = y

222+ postulate primitiveNotEq : x = y -> _|_

219223

220224--------------------------------------------------------------------------------

221225-- String

222226--------------------------------------------------------------------------------

223227

224228instance DecEq String where

225− decEq x y = if x == y then Yes (really_believe_me {a = x=x} {b = x=y} refl)

226− else No (really_believe_me _|_)

229+ decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

230+ where postulate primitiveEq : x = y

231+ postulate primitiveNotEq : x = y -> _|_

227232

228233

src/IRTS/Compiler.hs+1−1

@@ -163,7 +163,7 @@ mkLDecl n (CaseOp ci _ _ _ pats cd)

163163 return (declArgs [] (case_inlinable ci) n e)

164164mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a

165165mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a

166−mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)))

166+mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run

167167

168168instance ToIR (TT Name) where

169169 ir tm = ir' [] tm where

src/Idris/ElabDecls.hs+2−1

@@ -1458,7 +1458,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

14581458

14591459 logLvl 5 "DONE CHECK"

14601460 logLvl 2 $ "---> " ++ show rhs'

1461− when (not (null defer)) $ iLOG $ "DEFERRED " ++ show (map fst defer)

1461+ when (not (null defer)) $ iLOG $ "DEFERRED " ++

1462+ show (map (\ (n, (_,_,t)) -> (n, t)) defer)

14621463 def' <- checkDef fc defer

14631464 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

14641465 addDeferred def''