d763c9c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use postulates for decEq primitive proofs

d763c9cEdwin Brady13 years ago

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

compare with master

unifiedsplit

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

190--------------------------------------------------------------------------------

191

192instance DecEq Int where

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

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

194− else No (really_believe_me _|_)

194+ where postulate primitiveEq : x = y

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

195

196

196--------------------------------------------------------------------------------

197--------------------------------------------------------------------------------

197-- Char

198-- Char

198--------------------------------------------------------------------------------

199--------------------------------------------------------------------------------

199

200

200instance DecEq Char where

201instance DecEq Char where

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

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

202− else No (really_believe_me _|_)

203+ where postulate primitiveEq : x = y

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

203

205

204--------------------------------------------------------------------------------

206--------------------------------------------------------------------------------

205-- Integer

207-- Integer

206--------------------------------------------------------------------------------

208--------------------------------------------------------------------------------

207

209

208instance DecEq Integer where

210instance DecEq Integer where

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

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

210− else No (really_believe_me _|_)

212+ where postulate primitiveEq : x = y

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

211

214

212--------------------------------------------------------------------------------

215--------------------------------------------------------------------------------

213-- Float

216-- Float

214--------------------------------------------------------------------------------

217--------------------------------------------------------------------------------

215

218

216instance DecEq Float where

219instance DecEq Float where

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

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

218− else No (really_believe_me _|_)

221+ where postulate primitiveEq : x = y

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

219

223

220--------------------------------------------------------------------------------

224--------------------------------------------------------------------------------

221-- String

225-- String

222--------------------------------------------------------------------------------

226--------------------------------------------------------------------------------

223

227

224instance DecEq String where

228instance DecEq String where

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

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

226− else No (really_believe_me _|_)

230+ where postulate primitiveEq : x = y

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

227

232

228

233

src/IRTS/Compiler.hs+1−1

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

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

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

165mkLDecl 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

167

168instance ToIR (TT Name) where

169 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)

1458

1459 logLvl 5 "DONE CHECK"

1460 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)

1462 def' <- checkDef fc defer

1463 def' <- checkDef fc defer

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

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

1464 addDeferred def''

1465 addDeferred def''