5401872 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'upstream/master' into idrisdoc

commit54018726cb1582e215675c7c0a21b2fdc1f58192 authorPhilip Rasmussen <pjor@itu.dk> dateFri 28 Mar 2014, 17:06 (13 years ago) parent7762a35 d763c9c

7 files changed+47−16

compare with master

unifiedsplit

libs/prelude/Decidable/Equality.idr+15−10 src/IRTS/Compiler.hs+1−1 src/Idris/AbsSyntax.hs+1−1 src/Idris/Core/CaseTree.hs+2−2 src/Idris/ElabDecls.hs+2−1 src/Idris/IdeSlave.hs+9−1 src/Idris/REPL.hs+17

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

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

1010import Idris.AbsSyntaxTree

1111import Idris.Colours

1212import Idris.Docstrings

13−import Idris.IdeSlave

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

1414import IRTS.CodegenCommon

1515import Util.DynamicLinker

1616

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

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

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

160160 pfk == txt "prim_fork"

161161 = 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,

163163 fce == txt "Force"

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

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

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

626626

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

628628

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

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

630630 (P Bound n Erased)

631631

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

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

src/Idris/IdeSlave.hs+9−1

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

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

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

55import Text.Printf

66import Numeric

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

130130parseSExp :: String -> Result SExp

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

132132

133+data Opt = ShowImpl | ErrContext deriving Show

134+

133135data IdeSlaveCommand = REPLCompletions String

134136 | Interpret String

135137 | TypeOf String

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

142144 | LoadFile String

143145 | DocsFor String

144146 | Apropos String

147+ | GetOpts

148+ | SetOpt Opt Bool

145149 deriving Show

146150

147151sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

161165 _ -> Nothing)

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

163167sexpToCommand (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

164172sexpToCommand _ = Nothing

165173

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

src/Idris/REPL.hs+17

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

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

271271 Just (IdeSlave.Apropos a) ->

272272 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

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

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

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