5401872 · Idris-dev · git.iko.soy

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/AbsSyntax.hs+1−1

@@ -10,7 +10,7 @@ import Idris.Core.Typecheck

10import Idris.AbsSyntaxTree

11import Idris.Colours

12import Idris.Docstrings

13−import Idris.IdeSlave

13+import Idris.IdeSlave hiding (Opt(..))

14import IRTS.CodegenCommon

15import Util.DynamicLinker

16

src/Idris/Core/CaseTree.hs+2−2

@@ -159,7 +159,7 @@ directUse fn@(App f a)

159 | (P Ref (UN pfk) _, [App e w]) <- unApply fn,

160 pfk == txt "prim_fork"

161 = directUse e ++ directUse w -- HACK so that fork works

162− | (P Ref (UN fce) _, [_, a]) <- unApply fn,

162+ | (P Ref (UN fce) _, [_, _, a]) <- unApply fn,

163 fce == txt "Force"

164 = directUse a -- forcing a value counts as a use

165 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

@@ -626,7 +626,7 @@ prune proj (Case n alts)

626

627 forceTm n arg t = subst arg (forceArg n) t

628

629− forceArg n = App (App (P Ref (sUN "Force") Erased) Erased)

629+ forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

630 (P Bound n Erased)

631

632 mkProj n i [] sc = prune proj sc

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''

src/Idris/IdeSlave.hs+9−1

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

1{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

2

3−module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable) where

3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..)) where

4

5import Text.Printf

6import Numeric

@@ -130,6 +130,8 @@ quotedChar = try (string "\\\\" >> return '\\')

130parseSExp :: String -> Result SExp

131parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

132

133+data Opt = ShowImpl | ErrContext deriving Show

134+

133data IdeSlaveCommand = REPLCompletions String

135data IdeSlaveCommand = REPLCompletions String

134 | Interpret String

136 | Interpret String

135 | TypeOf String

137 | TypeOf String

@@ -142,6 +144,8 @@ data IdeSlaveCommand = REPLCompletions String

142 | LoadFile String

144 | LoadFile String

143 | DocsFor String

145 | DocsFor String

144 | Apropos String

146 | Apropos String

147+ | GetOpts

148+ | SetOpt Opt Bool

145 deriving Show

149 deriving Show

146

150

147sexpToCommand :: SExp -> Maybe IdeSlaveCommand

151sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -161,6 +165,10 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

161 _ -> Nothing)

165 _ -> Nothing)

162sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

166sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

163sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

167sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

168+sexpToCommand (SymbolAtom "get-options") = Just GetOpts

169+sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

170+ | Just opt <- lookup s opts = Just (SetOpt opt b)

171+ where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

164sexpToCommand _ = Nothing

172sexpToCommand _ = Nothing

165

173

166parseMessage :: String -> Either Err (SExp, Integer)

174parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+17

@@ -270,6 +270,23 @@ ideslave orig mods

270 process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

271 Just (IdeSlave.Apropos a) ->

272 process stdout fn (Apropos a)

273+ Just (IdeSlave.GetOpts) ->

274+ do ist <- getIState

275+ let opts = idris_options ist

276+ let impshow = opt_showimp opts

277+ let errCtxt = opt_errContext opts

278+ let options = (IdeSlave.SymbolAtom "ok",

279+ [(IdeSlave.SymbolAtom "show-implicits", impshow),

280+ (IdeSlave.SymbolAtom "error-context", errCtxt)])

281+ runIO . putStrLn $ IdeSlave.convSExp "return" options id

282+ Just (IdeSlave.SetOpt IdeSlave.ShowImpl b) ->

283+ do setImpShow b

284+ let msg = (IdeSlave.SymbolAtom "ok", b)

285+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

286+ Just (IdeSlave.SetOpt IdeSlave.ErrContext b) ->

287+ do setErrContext b

288+ let msg = (IdeSlave.SymbolAtom "ok", b)

289+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

273 Nothing -> do iPrintError "did not understand")

290 Nothing -> do iPrintError "did not understand")

274 (\e -> do iPrintError $ show e))

291 (\e -> do iPrintError $ show e))

275 (\e -> do iPrintError $ show e)

292 (\e -> do iPrintError $ show e)