c918f44 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

c918f44Edwin Brady12 years ago

CHANGELOG+5

compare with master

unifiedsplit

@@ -1,3 +1,8 @@

1+New in 0.9.17:

2+--------------

3+* The --ideslave command line option has been replaced with a --ide-mode

4+ command line option with the same semantics.

1New in 0.9.16:

6New in 0.9.16:

2--------------

7--------------

3* Inductive-inductive definitions are now supported (i.e. simultaneously

8* Inductive-inductive definitions are now supported (i.e. simultaneously

CONTRIBUTORS+3−2

@@ -7,6 +7,8 @@ Jan Bessai

7Michael R. Bernstein

8Nicola Botta

9Edwin Brady

10+Jakob Brünker

11+Alyssa Carter

10David Raymond Christiansen

12David Raymond Christiansen

11Carter Charbonneau

13Carter Charbonneau

12Jason Dagit

14Jason Dagit

@@ -28,6 +30,7 @@ Philip Rasmussen

28Reynir Reynisson

30Reynir Reynisson

29Seo Sanghyeon

31Seo Sanghyeon

30Benjamin Saunders

32Benjamin Saunders

33+Alexander Shabalin

31startling

34startling

32Chetan T

35Chetan T

33Matúš Tejiščák

36Matúš Tejiščák

@@ -35,5 +38,3 @@ Dirk Ullrich

35Leif Warner

38Leif Warner

36Daniel Waterworth

39Daniel Waterworth

37Jonas Westerlund

40Jonas Westerlund

38−Alyssa Carter

39−Alexander Shabalin

idris.cabal+1−1

@@ -685,7 +685,7 @@ Library

685 , Idris.ErrReverse

686 , Idris.Help

687 , Idris.IBC

688− , Idris.IdeSlave

688+ , Idris.IdeMode

689 , Idris.IdrisDoc

690 , Idris.Imports

691 , Idris.Inliner

libs/base/Data/Sign.idr+1−1

@@ -1,7 +1,7 @@

1module Data.Sign

3||| A representation of signs for signed datatypes such as `ZZ`

4−data Sign = Plus | Minus

4+data Sign = Plus | Zero | Minus

6||| Discover the sign of some type

7class Signed t where

libs/base/Data/ZZ.idr+1

@@ -15,6 +15,7 @@ import Data.Sign

15data ZZ = Pos Nat | NegS Nat

17instance Signed ZZ where

18+ sign (Pos Z) = Zero

18 sign (Pos _) = Plus

19 sign (Pos _) = Plus

19 sign (NegS _) = Minus

20 sign (NegS _) = Minus

libs/base/Network/Socket.idr+1−1

@@ -31,7 +31,7 @@ data SocketFamily =

31instance Show SocketFamily where

32 show AF_UNSPEC = "AF_UNSPEC"

33 show AF_INET = "AF_INET"

34− show AF_INET6 = "AF_INET4"

34+ show AF_INET6 = "AF_INET6"

36instance ToCode SocketFamily where

37 toCode AF_UNSPEC = 0

src/Idris/AbsSyntax.hs+15−9

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

10import Idris.AbsSyntaxTree

11import Idris.Colours

12import Idris.Docstrings

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

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

14import IRTS.CodegenCommon

15import Util.DynamicLinker

@@ -601,7 +601,7 @@ type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "

601isetPrompt :: String -> Idris ()

602isetPrompt p = do i <- getIState

603 case idris_outputmode i of

604− IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

604+ IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

605

606-- | Tell clients how much was parsed and loaded

607isetLoadedRegion :: Idris ()

@@ -610,7 +610,7 @@ isetLoadedRegion = do i <- getIState

610 case span of

611 Just fc ->

612 case idris_outputmode i of

613− IdeSlave n h ->

613+ IdeMode n h ->

614 runIO . hPutStrLn h $

615 convSExp "set-loaded-region" fc n

616 Nothing -> return ()

@@ -752,10 +752,12 @@ outputTy :: Idris OutputType

752outputTy = do i <- getIState

753 return $ opt_outputTy $ idris_options i

754

755−setIdeSlave :: Bool -> Handle -> Idris ()

755+setIdeMode :: Bool -> Handle -> Idris ()

756−setIdeSlave True h = do i <- getIState

756+setIdeMode True h = do i <- getIState

757− putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }

757+ putIState $ i { idris_outputmode = IdeMode 0 h

758+ , idris_colourRepl = False

759+ }

758−setIdeSlave False _ = return ()

760+setIdeMode False _ = return ()

759

761

760setTargetTriple :: String -> Idris ()

762setTargetTriple :: String -> Idris ()

761setTargetTriple t = do i <- getIState

763setTargetTriple t = do i <- getIState

@@ -870,7 +872,7 @@ logLvl l str = do i <- getIState

870 when (lvl >= l) $

872 when (lvl >= l) $

871 case idris_outputmode i of

873 case idris_outputmode i of

872 RawOutput h -> do runIO $ hPutStrLn h str

874 RawOutput h -> do runIO $ hPutStrLn h str

873− IdeSlave n h ->

875+ IdeMode n h ->

874 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]

876 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]

875 runIO . hPutStrLn h $ convSExp "log" good n

877 runIO . hPutStrLn h $ convSExp "log" good n

876

878

@@ -1734,7 +1736,11 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1734 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

1736 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

1735 = Placeholder

1737 = Placeholder

1736 su (PApp fc f@(PRef _ fn) args)

1738 su (PApp fc f@(PRef _ fn) args)

1737− | isDConName fn ctxt

1739+ -- here we use canBeDConName because the impossible pattern

1740+ -- check will not necessarily fully resolve constructor names,

1741+ -- and these bare names will otherwise get in the way of

1742+ -- impossbility checking.

1743+ | canBeDConName fn ctxt

1738 = PApp fc f (fmap (fmap su) args)

1744 = PApp fc f (fmap (fmap su) args)

1739 su (PApp fc f args)

1745 su (PApp fc f args)

1740 = PHidden (PApp fc f args)

1746 = PHidden (PApp fc f args)

src/Idris/AbsSyntaxTree.hs+18−4

@@ -26,6 +26,7 @@ import qualified Control.Monad.Trans.Class as Trans (lift)

27import Data.Data (Data)

28import Data.Function (on)

29+import Data.Generics.Uniplate.Data (universe)

29import Data.List hiding (group)

30import Data.List hiding (group)

30import Data.Char

31import Data.Char

31import qualified Data.Map.Strict as M

32import qualified Data.Map.Strict as M

@@ -143,7 +144,7 @@ data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord

143

144

144-- | The output mode in use

145-- | The output mode in use

145data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

146data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

146− | IdeSlave Integer Handle -- ^ Send IDE output for some request ID to the handle

147+ | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle

147 deriving Show

148 deriving Show

148

149

149-- | How wide is the console?

150-- | How wide is the console?

@@ -404,8 +405,8 @@ data Opt = Filename String

404 | Quiet

405 | Quiet

405 | NoBanner

406 | NoBanner

406 | ColourREPL Bool

407 | ColourREPL Bool

407− | Ideslave

408+ | Idemode

408− | IdeslaveSocket

409+ | IdemodeSocket

409 | ShowLibs

410 | ShowLibs

410 | ShowLibdir

411 | ShowLibdir

411 | ShowIncs

412 | ShowIncs

@@ -1376,6 +1377,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1376 where

1377 where

1377 startPrec = 0

1378 startPrec = 0

1378 funcAppPrec = 10

1379 funcAppPrec = 10

1380+

1379 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1381 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1380 prettySe p bnd (PQuote r) =

1382 prettySe p bnd (PQuote r) =

1381 text "![" <> pretty r <> text "]"

1383 text "![" <> pretty r <> text "]"

@@ -1641,6 +1643,16 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1641 getFixity :: String -> Maybe Fixity

1643 getFixity :: String -> Maybe Fixity

1642 getFixity = flip M.lookup fixities

1644 getFixity = flip M.lookup fixities

1643

1645

1646+-- | Determine whether a name was the one inserted for a hole or

1647+-- guess by the delaborator

1648+isHoleName :: Name -> Bool

1649+isHoleName (UN n) = n == T.pack "[__]"

1650+isHoleName _ = False

1651+

1652+-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess

1653+containsHole :: PTerm -> Bool

1654+containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]

1655+

1644-- | Pretty-printer helper for the binding site of a name

1656-- | Pretty-printer helper for the binding site of a name

1645bindingOf :: Name -- ^^ the bound name

1657bindingOf :: Name -- ^^ the bound name

1646 -> Bool -- ^^ whether the name is implicit

1658 -> Bool -- ^^ whether the name is implicit

@@ -1656,7 +1668,7 @@ prettyName

1656 -> Doc OutputAnnotation

1668 -> Doc OutputAnnotation

1657prettyName infixParen showNS bnd n

1669prettyName infixParen showNS bnd n

1658 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

1670 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"

1659− | (UN n') <- n, isPrefixOf "_" $ T.unpack n' = text "_"

1671+ | (UN n') <- n, T.unpack n' == "_" = text "_"

1660 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName

1672 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName

1661 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

1673 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName

1662 where fullName = text nameSpace <> parenthesise (text (baseName n))

1674 where fullName = text nameSpace <> parenthesise (text (baseName n))

@@ -1728,6 +1740,8 @@ getShowArgs :: [PArg] -> [PArg]

1728getShowArgs [] = []

1740getShowArgs [] = []

1729getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs

1741getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs

1730getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs

1742getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs

1743+ | PImp _ _ _ _ tm <- e

1744+ , containsHole tm = e : getShowArgs xs

1731getShowArgs (_ : xs) = getShowArgs xs

1745getShowArgs (_ : xs) = getShowArgs xs

1732

1746

1733getConsts :: [PArg] -> [PTerm]

1747getConsts :: [PArg] -> [PTerm]

src/Idris/CmdOptions.hs+4−2

@@ -71,8 +71,10 @@ parseFlags :: Parser [Opt]

71parseFlags = many $

72 flag' NoBanner (long "nobanner" <> help "Suppress the banner")

73 <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

74− <|> flag' Ideslave (long "ideslave")

74+ <|> flag' Idemode (long "ide-mode" <> help "Run the Idris REPL with machine-readable syntax")

75− <|> flag' IdeslaveSocket (long "ideslave-socket")

75+ <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on")

76+ <|> flag' Idemode (long "ideslave" <> help "Deprecated version of --ide-mode") -- TODO: Remove in v0.9.18

77+ <|> flag' IdemodeSocket (long "ideslave-socket" <> help "Deprecated version of --ide-mode-socket") -- TODO: Remove in v0.9.18

76 <|> (Client <$> strOption (long "client"))

78 <|> (Client <$> strOption (long "client"))

77 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

79 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

78 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

80 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

src/Idris/Core/Elaborate.hs+14−13

@@ -173,30 +173,30 @@ elaborating_app = do ES (ps, _) _ _ <- get

173

174-- Some handy gadgets for pulling out bits of state

175

176−-- get the global context

176+-- | Get the global context

177get_context :: Elab' aux Context

178get_context = do ES p _ _ <- get

179 return $! (context (fst p))

180

181−-- update the context

181+-- | Update the context.

182-- (should only be used for adding temporary definitions or all sorts of

183-- stuff could go wrong)

184set_context :: Context -> Elab' aux ()

185set_context ctxt = do ES (p, a) logs prev <- get

186 put (ES (p { context = ctxt }, a) logs prev)

187

188−-- get the proof term

188+-- | get the proof term

189get_term :: Elab' aux Term

190get_term = do ES p _ _ <- get

191 return $! (getProofTerm (pterm (fst p)))

192

193−-- get the proof term

193+-- | get the proof term

194update_term :: (Term -> Term) -> Elab' aux ()

195update_term f = do ES (p,a) logs prev <- get

196 let p' = p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }

197 put (ES (p', a) logs prev)

198

199−-- get the local context at the currently in focus hole

199+-- | get the local context at the currently in focus hole

200get_env :: Elab' aux Env

201get_env = do ES p _ _ <- get

202 lift $ envAtFocus (fst p)

@@ -213,14 +213,14 @@ get_probs :: Elab' aux Fails

213get_probs = do ES p _ _ <- get

214 return $! (problems (fst p))

215

216−-- Return recently solved names (that is, the names solved since the

216+-- | Return recently solved names (that is, the names solved since the

217-- last call to get_recents)

218get_recents :: Elab' aux [Name]

219get_recents = do ES (p, a) l prev <- get

220 put (ES (p { recents = [] }, a) l prev)

221 return (recents p)

222

223−-- get the current goal type

223+-- | get the current goal type

224goal :: Elab' aux Type

225goal = do ES p _ _ <- get

226 b <- lift $ goalAtFocus (fst p)

@@ -233,7 +233,7 @@ is_guess = do ES p _ _ <- get

233 Guess _ _ -> return True

234 _ -> return False

235

236−-- Get the guess at the current hole, if there is one

236+-- | Get the guess at the current hole, if there is one

237get_guess :: Elab' aux Term

238get_guess = do ES p _ _ <- get

239 b <- lift $ goalAtFocus (fst p)

@@ -241,7 +241,7 @@ get_guess = do ES p _ _ <- get

241 Guess t v -> return $! v

242 _ -> fail "Not a guess"

243

244−-- typecheck locally

244+-- | Typecheck locally

245get_type :: Raw -> Elab' aux Type

246get_type tm = do ctxt <- get_context

247 env <- get_env

@@ -254,7 +254,7 @@ get_type_val tm = do ctxt <- get_context

254 (val, ty) <- lift $ check ctxt env tm

255 return $! (finalise val, finalise ty)

256

257−-- get holes we've deferred for later definition

257+-- | get holes we've deferred for later definition

258get_deferred :: Elab' aux [Name]

259get_deferred = do ES p _ _ <- get

260 return $! (deferred (fst p))

@@ -271,17 +271,18 @@ checkInjective (tm, l, r) = do ctxt <- get_context

271 isInj ctxt (Bind _ (Pi _ _ _) sc) = True

272 isInj ctxt _ = False

273

274−-- get instance argument names

274+-- | get instance argument names

275get_instances :: Elab' aux [Name]

276get_instances = do ES p _ _ <- get

277 return $! (instances (fst p))

278

279−-- get auto argument names

279+-- | get auto argument names

280get_autos :: Elab' aux [(Name, [Name])]

281get_autos = do ES p _ _ <- get

282 return $! (autos (fst p))

283

284−-- given a desired hole name, return a unique hole name

284+-- | given a desired hole name, return a unique hole name

285+unique_hole :: Name -> Elab' aux Name

285unique_hole = unique_hole' False

286unique_hole = unique_hole' False

286

287

287unique_hole' :: Bool -> Name -> Elab' aux Name

288unique_hole' :: Bool -> Name -> Elab' aux Name

src/Idris/Core/Evaluate.hs+29−24

@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

12 lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,

13 mapDefCtxt,

14− lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, isTConName, isConName, isFnName,

14+ lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,

15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,

16 isUniverse) where

@@ -971,47 +971,52 @@ isConName n ctxt = isTConName n ctxt || isDConName n ctxt

971

972isTConName :: Name -> Context -> Bool

973isTConName n ctxt

974− = or $ do def <- lookupCtxt n (definitions ctxt)

974+ = case lookupDefExact n ctxt of

975− case tfst def of

976− (TyDecl (TCon _ _) _) -> return True

975+ Just (TyDecl (TCon _ _) _) -> True

977− _ -> return False

976+ _ -> False

978

977

978+-- | Check whether a resolved name is certainly a data constructor

979isDConName :: Name -> Context -> Bool

980isDConName n ctxt

981+ = case lookupDefExact n ctxt of

982+ Just (TyDecl (DCon _ _ _) _) -> True

983+ _ -> False

984+

985+-- | Check whether any overloading of a name is a data constructor

986+canBeDConName :: Name -> Context -> Bool

987+canBeDConName n ctxt

981 = or $ do def <- lookupCtxt n (definitions ctxt)

988 = or $ do def <- lookupCtxt n (definitions ctxt)

982 case tfst def of

989 case tfst def of

983− (TyDecl (DCon _ _ _) _) -> return True

990+ (TyDecl (DCon _ _ _) _) -> return True

984− _ -> return False

991+ _ -> return False

985

992

986isFnName :: Name -> Context -> Bool

993isFnName :: Name -> Context -> Bool

987isFnName n ctxt

994isFnName n ctxt

988− = let def = lookupCtxtExact n (definitions ctxt) in

995+ = case lookupDefExact n ctxt of

989− case def of

990− Just (Function _ _, _, _, _) -> True

996+ Just (Function _ _) -> True

991− Just (Operator _ _ _, _, _, _) -> True

997+ Just (Operator _ _ _) -> True

992− Just (CaseOp _ _ _ _ _ _, _, _, _) -> True

998+ Just (CaseOp _ _ _ _ _ _) -> True

993− _ -> False

999+ _ -> False

994

1000

995isTCDict :: Name -> Context -> Bool

1001isTCDict :: Name -> Context -> Bool

996isTCDict n ctxt

1002isTCDict n ctxt

997− = let def = lookupCtxtExact n (definitions ctxt) in

1003+ = case lookupDefExact n ctxt of

998− case def of

999− Just (Function _ _, _, _, _) -> False

1004+ Just (Function _ _) -> False

1000− Just (Operator _ _ _, _, _, _) -> False

1005+ Just (Operator _ _ _) -> False

1001− Just (CaseOp ci _ _ _ _ _, _, _, _) -> tc_dictionary ci

1006+ Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci

1002− _ -> False

1007+ _ -> False

1003

1008

1004lookupP :: Name -> Context -> [Term]

1009lookupP :: Name -> Context -> [Term]

1005lookupP n ctxt

1010lookupP n ctxt

1006 = do def <- lookupCtxt n (definitions ctxt)

1011 = do def <- lookupCtxt n (definitions ctxt)

1007 p <- case def of

1012 p <- case def of

1008− (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1013+ (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1009− (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1014+ (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1010 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1015 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1011− (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1016+ (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1012 case snd p of

1017 case snd p of

1013− Hidden -> []

1018+ Hidden -> []

1014− _ -> return (fst p)

1019+ _ -> return (fst p)

1015

1020

1016lookupDefExact :: Name -> Context -> Maybe Def

1021lookupDefExact :: Name -> Context -> Maybe Def

1017lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

1022lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

src/Idris/Coverage.hs+10−11

@@ -18,18 +18,18 @@ import Debug.Trace

19import Control.Monad.State.Strict

21−-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the

21+-- | Generate a pattern from an 'impossible' LHS.

22+--

23+-- We need this to eliminate the pattern clauses which have been

22−-- pattern clauses which have been provided explicitly from new clause

24+-- provided explicitly from new clause generation.

23−-- generation.)

24−

25mkPatTm :: PTerm -> Idris Term

26mkPatTm t = do i <- getIState

27 let timp = addImpl' True [] [] i t

28 evalStateT (toTT (mapPT deNS timp)) 0

29 where

30 toTT (PRef _ n) = do i <- lift getIState

31− case lookupDef n (tt_ctxt i) of

31+ case lookupNameDef n (tt_ctxt i) of

32− [TyDecl nt _] -> return $ P nt n Erased

32+ [(n', TyDecl nt _)] -> return $ P nt n' Erased

33 _ -> return $ P Ref n Erased

34 toTT (PApp _ t args) = do t' <- toTT t

35 args' <- mapM (toTT . getTm) args

@@ -44,13 +44,12 @@ mkPatTm t = do i <- getIState

44 deNS (PRef f (NS n _)) = PRef f n

45 deNS t = t

47−-- Given a list of LHSs, generate a extra clauses which cover the remaining

47+-- | Given a list of LHSs, generate a extra clauses which cover the remaining

48−-- cases. The ones which haven't been provided are marked 'absurd' so that the

48+-- cases. The ones which haven't been provided are marked 'absurd' so

49−-- checker will make sure they can't happen.

49+-- that the checker will make sure they can't happen.

50−

50+--

51-- This will only work after the given clauses have been typechecked and the

52-- names are fully explicit!

53−

54genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

53genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

55genClauses fc n xs given

54genClauses fc n xs given

56 = do i <- getIState

55 = do i <- getIState

src/Idris/Delaborate.hs+2−2

@@ -308,7 +308,7 @@ pprintErr' i (ElaboratingArg f x _ e)

308 where whatIsName = let ctxt = tt_ctxt i

309 in if isTConName f ctxt

310 then text "type constructor" <> space

311− else if isConName f ctxt

311+ else if isDConName f ctxt

312 then text "constructor" <> space

313 else if isFnName f ctxt

314 then text "function" <> space

@@ -488,7 +488,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

488 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

489 _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

490 _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

491− _ | otherwise -> annot

491+ _ | otherwise -> annot

492 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

493 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

494 let o = overview (fst docs)

src/Idris/Elab/Provider.hs+16−10

@@ -74,9 +74,9 @@ elabProvider info syn fc what n

74 (e, et) <- case what of

75 ProvTerm _ tm -> elabVal info ERHS tm

76 ProvPostulate tm -> elabVal info ERHS tm

77− unless (isProviderOf (normalise ctxt [] ty') et) $

77+ unless (isProviderOf ctxt ty' et) $

78− ifail $ "Expected provider type IO (Provider (" ++

78+ ifail $ "Expected provider type " ++ show (providerOf ty') ++

79− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

79+ ", got " ++ show et ++ " instead."

81 -- Execute the type provider and normalise the result

82 -- use 'run__provider' to convert to a primitive IO action

@@ -107,11 +107,17 @@ elabProvider info syn fc what n

107 isTType (TType _) = True

108 isTType _ = False

109

110+ -- Note: IO (Providers.Provider ty) is used instead of IO'

111+ -- (MkFFI C_FFI) (Providers.Provider ty) in hopes of better

112+ -- error messages with less normalisation

113+ providerOf :: Type -> Type

114+ providerOf ty = App (P Ref (sUN "IO") Erased) $

115+ App (P Ref (sNS (sUN "Provider") ["Providers"]) Erased)

116+ ty

117+

110− isProviderOf :: TT Name -> TT Name -> Bool

118+ isProviderOf :: Context -> TT Name -> TT Name -> Bool

111− isProviderOf tp prov

119+ isProviderOf ctxt tp prov =

112− | (P _ (UN io) _, [prov']) <- unApply prov

120+ case converts ctxt [] (providerOf tp) prov of

113− , (P _ (NS (UN prov) [provs]) _, [tp']) <- unApply prov'

121+ OK _ -> True

114− , tp == tp', io == txt "IO"

115− , prov == txt "Provider" && provs == txt "Providers" = True

116− isProviderOf _ _ = False

122+ _ -> False

117

123

src/Idris/IdeSlave.hs → src/Idris/IdeMode.hsrenamed+29−29

@@ -2,7 +2,7 @@

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

5−module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where

5+module Idris.IdeMode(parseMessage, convSExp, IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

7import Text.Printf

8import Numeric

@@ -206,32 +206,32 @@ parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

206

207data Opt = ShowImpl | ErrContext deriving Show

208

209−data IdeSlaveCommand = REPLCompletions String

209+data IdeModeCommand = REPLCompletions String

210− | Interpret String

210+ | Interpret String

211− | TypeOf String

211+ | TypeOf String

212− | CaseSplit Int String

212+ | CaseSplit Int String

213− | AddClause Int String

213+ | AddClause Int String

214− | AddProofClause Int String

214+ | AddProofClause Int String

215− | AddMissing Int String

215+ | AddMissing Int String

216− | MakeWithBlock Int String

216+ | MakeWithBlock Int String

217− | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

217+ | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

218− | MakeLemma Int String

218+ | MakeLemma Int String

219− | LoadFile String (Maybe Int)

219+ | LoadFile String (Maybe Int)

220− | DocsFor String

220+ | DocsFor String

221− | Apropos String

221+ | Apropos String

222− | GetOpts

222+ | GetOpts

223− | SetOpt Opt Bool

223+ | SetOpt Opt Bool

224− | Metavariables Int -- ^^ the Int is the column count for pretty-printing

224+ | Metavariables Int -- ^^ the Int is the column count for pretty-printing

225− | WhoCalls String

225+ | WhoCalls String

226− | CallsWho String

226+ | CallsWho String

227− | TermNormalise [(Name, Bool)] Term

227+ | TermNormalise [(Name, Bool)] Term

228− | TermShowImplicits [(Name, Bool)] Term

228+ | TermShowImplicits [(Name, Bool)] Term

229− | TermNoImplicits [(Name, Bool)] Term

229+ | TermNoImplicits [(Name, Bool)] Term

230− | PrintDef String

230+ | PrintDef String

231− | ErrString Err

231+ | ErrString Err

232− | ErrPPrint Err

232+ | ErrPPrint Err

233−

233+

234−sexpToCommand :: SExp -> Maybe IdeSlaveCommand

234+sexpToCommand :: SExp -> Maybe IdeModeCommand

235sexpToCommand (SexpList (x:[])) = sexpToCommand x

236sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

237sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

@@ -298,5 +298,5 @@ convSExp pre s id =

298getHexLength :: String -> String

299getHexLength s = printf "%06x" (1 + (length s))

300

301−ideSlaveEpoch :: Int

301+ideModeEpoch :: Int

302−ideSlaveEpoch = 1

302+ideModeEpoch = 1

src/Idris/Interactive.hs+3−3

@@ -16,7 +16,7 @@ import Idris.ElabTerm

16import Idris.Error

17import Idris.Delaborate

18import Idris.Output

19−import Idris.IdeSlave hiding (IdeSlaveCommand(..))

19+import Idris.IdeMode hiding (IdeModeCommand(..))

21import Idris.Elab.Value

@@ -271,7 +271,7 @@ makeLemma fn updatefile l n

271 runIO $ copyFile fb fn

272 else case idris_outputmode i of

273 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app

274− IdeSlave n h ->

274+ IdeMode n h ->

275 let good = SexpList [SymbolAtom "ok",

276 SexpList [SymbolAtom "metavariable-lemma",

277 SexpList [SymbolAtom "replace-metavariable",

@@ -289,7 +289,7 @@ makeLemma fn updatefile l n

289 runIO $ copyFile fb fn

290 else case idris_outputmode i of

291 RawOutput _ -> iPrintResult $ lem_app

292− IdeSlave n h ->

292+ IdeMode n h ->

293 let good = SexpList [SymbolAtom "ok",

294 SexpList [SymbolAtom "provisional-definition-lemma",

295 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+18−18

@@ -8,7 +8,7 @@ import Idris.Core.Evaluate (isDConName, isTConName, isFnName, normaliseAll)

8import Idris.AbsSyntax

9import Idris.Delaborate

10import Idris.Docstrings

11−import Idris.IdeSlave

11+import Idris.IdeMode

13import Util.Pretty

14import Util.ScreenSize (getScreenWidth)

@@ -43,7 +43,7 @@ iWarn fc err =

43 then text (show fc) <> colon <//> err

44 else err

45 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

46− IdeSlave n h ->

46+ IdeMode n h ->

47 do err' <- iRender . fmap (fancifyAnnots i) $ err

48 let (str, spans) = displaySpans err'

49 runIO . hPutStrLn h $

@@ -52,8 +52,8 @@ iWarn fc err =

52iRender :: Doc a -> Idris (SimpleDoc a)

53iRender d = do w <- getWidth

54 ist <- getIState

55− let ideSlave = case idris_outputmode ist of

55+ let ideMode = case idris_outputmode ist of

56− IdeSlave _ _ -> True

56+ IdeMode _ _ -> True

57 _ -> False

58 case w of

59 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

@@ -61,7 +61,7 @@ iRender d = do w <- getWidth

61 if n < 1

62 then renderPretty 1.0 1000000000 d

63 else renderPretty 0.8 n d

64− AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d

64+ AutomaticWidth | ideMode -> return $ renderPretty 1.0 1000000000 d

65 | otherwise -> do width <- runIO getScreenWidth

66 return $ renderPretty 0.8 width d

@@ -76,7 +76,7 @@ consoleDisplayAnnotated h output = do ist <- getIState

76iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

77iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

79−-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

79+-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name

80iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()

81iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n

82iPrintFunTypes bnd n overloads = do ist <- getIState

@@ -94,7 +94,7 @@ iRenderOutput doc =

94 case idris_outputmode i of

95 RawOutput h -> do out <- iRender doc

96 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

97− IdeSlave n h ->

97+ IdeMode n h ->

98 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

99 let out = [toSExp str, toSExp spans]

100 runIO . hPutStrLn h $ convSExp "write-decorated" out n

@@ -103,10 +103,10 @@ iRenderResult :: Doc OutputAnnotation -> Idris ()

103iRenderResult d = do ist <- getIState

104 case idris_outputmode ist of

105 RawOutput h -> consoleDisplayAnnotated h d

106− IdeSlave n h -> ideSlaveReturnAnnotated n h d

106+ IdeMode n h -> ideModeReturnAnnotated n h d

107

108−ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

108+ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

109−ideSlaveReturnWithStatus status n h out = do

109+ideModeReturnWithStatus status n h out = do

110 ist <- getIState

111 (str, spans) <- fmap displaySpans .

112 iRender .

@@ -116,16 +116,16 @@ ideSlaveReturnWithStatus status n h out = do

116 runIO . hPutStrLn h $ convSExp "return" good n

117

118

119−-- | Write pretty-printed output to IDESlave with semantic annotations

119+-- | Write pretty-printed output to IDEMode with semantic annotations

120−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

120+ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

121−ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

121+ideModeReturnAnnotated = ideModeReturnWithStatus "ok"

122

123-- | Show an error with semantic highlighting

124iRenderError :: Doc OutputAnnotation -> Idris ()

125iRenderError e = do ist <- getIState

126 case idris_outputmode ist of

127 RawOutput h -> consoleDisplayAnnotated h e

128− IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e

128+ IdeMode n h -> ideModeReturnWithStatus "error" n h e

129

130iPrintWithStatus :: String -> String -> Idris ()

131iPrintWithStatus status s = do

@@ -134,7 +134,7 @@ iPrintWithStatus status s = do

134 RawOutput h -> case s of

135 "" -> return ()

136 s -> runIO $ hPutStrLn h s

137− IdeSlave n h ->

137+ IdeMode n h ->

138 let good = SexpList [SymbolAtom status, toSExp s] in

139 runIO $ hPutStrLn h $ convSExp "return" good n

140

@@ -149,13 +149,13 @@ iputStrLn :: String -> Idris ()

149iputStrLn s = do i <- getIState

150 case idris_outputmode i of

151 RawOutput h -> runIO $ hPutStrLn h s

152− IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

152+ IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

153

154

155ideslavePutSExp :: SExpable a => String -> a -> Idris ()

156ideslavePutSExp cmd info = do i <- getIState

157 case idris_outputmode i of

158− IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n

158+ IdeMode n h -> runIO . hPutStrLn h $ convSExp cmd info n

159 _ -> return ()

160

161-- TODO: send structured output similar to the metavariable list

@@ -163,7 +163,7 @@ iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

163iputGoal g = do i <- getIState

164 case idris_outputmode i of

165 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)

166− IdeSlave n h ->

166+ IdeMode n h ->

167 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g

168 goal = [toSExp str, toSExp spans]

169 in runIO . hPutStrLn h $ convSExp "write-goal" goal n

src/Idris/ParseHelpers.hs+4−2

@@ -224,7 +224,7 @@ float = Tok.double

224idrisStyle :: MonadicParsing m => IdentifierStyle m

225idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier

226 where _styleName = "Idris"

227− _styleStart = satisfy isAlpha

227+ _styleStart = satisfy isAlpha <|> oneOf "_"

228 _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

229 _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",

230 "do", "dsl", "import", "impossible",

@@ -262,7 +262,9 @@ reservedOp name = token $ try $

262

263-- | Parses an identifier as a token

264identifier :: MonadicParsing m => m String

265−identifier = token $ Tok.ident idrisStyle

265+identifier = try(do i <- token $ Tok.ident idrisStyle

266+ when (i == "_") $ unexpected "wildcard"

267+ return i)

266

268

267-- | Parses an identifier with possible namespace as a name

269-- | Parses an identifier with possible namespace as a name

268iName :: MonadicParsing m => [String] -> m Name

270iName :: MonadicParsing m => [String] -> m Name

src/Idris/Parser.hs+1−1

@@ -1192,7 +1192,7 @@ parseProg syn fname input mrk

1192 i <- getIState

1193 case idris_outputmode i of

1194 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1195− IdeSlave n h -> iWarn fc (P.text msg)

1195+ IdeMode n h -> iWarn fc (P.text msg)

1196 putIState (i { errSpan = Just fc })

1197 return []

1198 Success (x, i) -> do putIState i

src/Idris/Prover.hs+15−15

@@ -20,7 +20,7 @@ import Idris.Parser hiding (params)

20import Idris.Error

21import Idris.DataOpts

22import Idris.Completion

23−import qualified Idris.IdeSlave as IdeSlave

23+import qualified Idris.IdeMode as IdeMode

24import Idris.Output

25import Idris.TypeSearch (searchByType)

@@ -72,7 +72,7 @@ prove opt ctxt lit n ty

72 iLOG $ "Adding " ++ show tm

73 i <- getIState

74 case idris_outputmode i of

75− IdeSlave _ _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

75+ IdeMode _ _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

76 _ -> iputStrLn $ showProof lit n prf

77 let proofs = proof_list i

78 putIState (i { proof_list = (n, prf) : proofs })

@@ -95,8 +95,8 @@ prove opt ctxt lit n ty

95 [([], P Ref n ty, ptm')] ty)

96 solveDeferred n

97 case idris_outputmode i of

98− IdeSlave n h ->

98+ IdeMode n h ->

99− runIO . hPutStrLn h $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n

99+ runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n

100 _ -> return ()

101

102elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)

@@ -185,24 +185,24 @@ receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)

185receiveInput h e =

186 do i <- getIState

187 let inh = if h == stdout then stdin else h

188− len' <- runIO $ IdeSlave.getLen inh

188+ len' <- runIO $ IdeMode.getLen inh

189 len <- case len' of

190 Left err -> ierror err

191 Right n -> return n

192− l <- runIO $ IdeSlave.getNChar inh len ""

192+ l <- runIO $ IdeMode.getNChar inh len ""

193− (sexp, id) <- case IdeSlave.parseMessage l of

193+ (sexp, id) <- case IdeMode.parseMessage l of

194 Left err -> ierror err

195 Right (sexp, id) -> return (sexp, id)

196− putIState $ i { idris_outputmode = (IdeSlave id h) }

196+ putIState $ i { idris_outputmode = (IdeMode id h) }

197− case IdeSlave.sexpToCommand sexp of

197+ case IdeMode.sexpToCommand sexp of

198− Just (IdeSlave.REPLCompletions prefix) ->

198+ Just (IdeMode.REPLCompletions prefix) ->

199 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

200− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

200+ let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]

201 ideslavePutSExp "return" good

202 receiveInput h e

203− Just (IdeSlave.Interpret cmd) -> return (Just cmd)

203+ Just (IdeMode.Interpret cmd) -> return (Just cmd)

204− Just (IdeSlave.TypeOf str) -> return (Just (":t " ++ str))

204+ Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))

205− Just (IdeSlave.DocsFor str) -> return (Just (":doc " ++ str))

205+ Just (IdeMode.DocsFor str) -> return (Just (":doc " ++ str))

206 _ -> return Nothing

207

208ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

@@ -221,7 +221,7 @@ ploop fn d prompt prf e h

221 l <- getInputLine (prompt ++ "> ")

222 h' <- getHistory

223 return (l, Just h')

224− IdeSlave _ handle ->

224+ IdeMode _ handle ->

225 do isetPrompt prompt

226 i <- receiveInput handle e

227 return (i, h)

src/Idris/REPL.hs+94−89

@@ -22,7 +22,7 @@ import Idris.Primitives

22import Idris.Coverage

23import Idris.Docs hiding (Doc)

24import Idris.Completion

25−import qualified Idris.IdeSlave as IdeSlave

25+import qualified Idris.IdeMode as IdeMode

26import Idris.Chaser

27import Idris.Imports

28import Idris.Colours hiding (colourise)

@@ -165,7 +165,7 @@ startServer port orig fn_in = do tid <- runIO $ forkOS (serverLoop port)

165 cmd <- hGetLine h

166 let isth = case idris_outputmode ist of

167 RawOutput _ -> ist {idris_outputmode = RawOutput h}

168− IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

168+ IdeMode n _ -> ist {idris_outputmode = IdeMode n h}

169 (ist', fn) <- processNetCmd orig isth h fn cmd

170 hClose h

171 loop fn ist' sock

@@ -204,7 +204,7 @@ processNetCmd orig i h fn cmd

204 do ist <- getIState

205 putIState $ case idris_outputmode ist of

206 RawOutput _ -> ist {idris_outputmode = RawOutput h}

207− IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

207+ IdeMode n _ -> ist {idris_outputmode = IdeMode n h}

208

209-- | Run a command on the server on localhost

210runClient :: PortID -> String -> IO ()

@@ -232,25 +232,25 @@ runClient port str = withSocketsDo $ do

232 putStrLn "Unable to connect to a running Idris repl"

233

234

235−initIdeslaveSocket :: IO Handle

235+initIdemodeSocket :: IO Handle

236−initIdeslaveSocket = do

236+initIdemodeSocket = do

237 (sock, port) <- listenOnLocalhostAnyPort

238 putStrLn $ show port

239 (h, _, _) <- accept sock

240 hSetEncoding h utf8

241 return h

242

243−-- | Run the IdeSlave

243+-- | Run the IdeMode

244ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()

245ideslaveStart s orig mods

246− = do h <- runIO $ if s then initIdeslaveSocket else return stdout

246+ = do h <- runIO $ if s then initIdemodeSocket else return stdout

247− setIdeSlave True h

247+ setIdeMode True h

248 i <- getIState

249 case idris_outputmode i of

250− IdeSlave n h ->

250+ IdeMode n h ->

251− do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n

251+ do runIO $ hPutStrLn h $ IdeMode.convSExp "protocol-version" IdeMode.ideModeEpoch n

252 case mods of

253− a:_ -> runIdeSlaveCommand h n i "" [] (IdeSlave.LoadFile a Nothing)

253+ a:_ -> runIdeModeCommand h n i "" [] (IdeMode.LoadFile a Nothing)

254 _ -> return ()

255 ideslave h orig mods

256

@@ -258,36 +258,36 @@ ideslave :: Handle -> IState -> [FilePath] -> Idris ()

258ideslave h orig mods

259 = do idrisCatch

260 (do let inh = if h == stdout then stdin else h

261− len' <- runIO $ IdeSlave.getLen inh

261+ len' <- runIO $ IdeMode.getLen inh

262 len <- case len' of

263 Left err -> ierror err

264 Right n -> return n

265− l <- runIO $ IdeSlave.getNChar inh len ""

265+ l <- runIO $ IdeMode.getNChar inh len ""

266− (sexp, id) <- case IdeSlave.parseMessage l of

266+ (sexp, id) <- case IdeMode.parseMessage l of

267 Left err -> ierror err

268 Right (sexp, id) -> return (sexp, id)

269 i <- getIState

270− putIState $ i { idris_outputmode = (IdeSlave id h) }

270+ putIState $ i { idris_outputmode = (IdeMode id h) }

271 idrisCatch -- to report correct id back!

272 (do let fn = case mods of

273 (f:_) -> f

274 _ -> ""

275− case IdeSlave.sexpToCommand sexp of

275+ case IdeMode.sexpToCommand sexp of

276− Just cmd -> runIdeSlaveCommand h id orig fn mods cmd

276+ Just cmd -> runIdeModeCommand h id orig fn mods cmd

277 Nothing -> iPrintError "did not understand" )

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

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

280 ideslave h orig mods

281

282−-- | Run IDESlave commands

282+-- | Run IDEMode commands

283−runIdeSlaveCommand :: Handle -- ^^ The handle for communication

283+runIdeModeCommand :: Handle -- ^^ The handle for communication

284 -> Integer -- ^^ The continuation ID for the client

285 -> IState -- ^^ The original IState

286 -> FilePath -- ^^ The current open file

287 -> [FilePath] -- ^^ The currently loaded modules

288− -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

288+ -> IdeMode.IdeModeCommand -- ^^ The command to process

289 -> Idris ()

290−runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

290+runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

291 do c <- colourise

292 i <- getIState

293 case parseCmd i "(input)" cmd of

@@ -297,96 +297,96 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

297 (do process fn (Prove n')

298 isetPrompt (mkPrompt mods)

299 case idris_outputmode i of

300− IdeSlave n h -> -- signal completion of proof to ide

300+ IdeMode n h -> -- signal completion of proof to ide

301 runIO . hPutStrLn h $

302− IdeSlave.convSExp "return"

302+ IdeMode.convSExp "return"

303− (IdeSlave.SymbolAtom "ok", "")

303+ (IdeMode.SymbolAtom "ok", "")

304 n

305 _ -> return ())

306 (\e -> do ist <- getIState

307 isetPrompt (mkPrompt mods)

308 case idris_outputmode i of

309− IdeSlave n h ->

309+ IdeMode n h ->

310 runIO . hPutStrLn h $

311− IdeSlave.convSExp "abandon-proof" "Abandoned" n

311+ IdeMode.convSExp "abandon-proof" "Abandoned" n

312 _ -> return ()

313 iRenderError $ pprintErr ist e)

314 Success (Right cmd) -> idrisCatch

315 (ideslaveProcess fn cmd)

316 (\e -> getIState >>= iRenderError . flip pprintErr e)

317 Success (Left err) -> iPrintError err

318−runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =

318+runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

319 do (unused, compls) <- replCompletion (reverse str, "")

320− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

320+ let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

321− IdeSlave.toSExp (map replacement compls,

321+ IdeMode.toSExp (map replacement compls,

322 reverse unused)]

323− runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id

323+ runIO . hPutStrLn h $ IdeMode.convSExp "return" good id

324−runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

324+runIdeModeCommand h id orig fn mods (IdeMode.LoadFile filename toline) =

325 do i <- getIState

326 clearErr

327 putIState (orig { idris_options = idris_options i,

328− idris_outputmode = (IdeSlave id h) })

328+ idris_outputmode = (IdeMode id h) })

329 mods <- loadInputs [filename] toline

330 isetPrompt (mkPrompt mods)

331 -- Report either success or failure

332 i <- getIState

333 case (errSpan i) of

334− Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

334+ Nothing -> let msg = maybe (IdeMode.SexpList [IdeMode.SymbolAtom "ok",

335− IdeSlave.SexpList []])

335+ IdeMode.SexpList []])

336− (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

336+ (\fc -> IdeMode.SexpList [IdeMode.SymbolAtom "ok",

337− IdeSlave.toSExp fc])

337+ IdeMode.toSExp fc])

338 (idris_parsedSpan i)

339− in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

339+ in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

340 Just x -> iPrintError $ "didn't load " ++ filename

341 ideslave h orig mods

342−runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =

342+runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

343 case splitName name of

344 Left err -> iPrintError err

345 Right n -> process "(ideslave)"

346 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

347−runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =

347+runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name) =

348 case parseConst orig name of

349 Success c -> process "(ideslave)" (DocStr (Right c))

350 Failure _ ->

351 case splitName name of

352 Left err -> iPrintError err

353 Right n -> process "(ideslave)" (DocStr (Left n))

354−runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =

354+runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

355 process fn (CaseSplitAt False line (sUN name))

356−runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =

356+runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

357 process fn (AddClauseFrom False line (sUN name))

358−runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =

358+runIdeModeCommand h id orig fn mods (IdeMode.AddProofClause line name) =

359 process fn (AddProofClauseFrom False line (sUN name))

360−runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =

360+runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =

361 process fn (AddMissing False line (sUN name))

362−runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =

362+runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =

363 process fn (MakeWith False line (sUN name))

364−runIdeSlaveCommand h id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

364+runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =

365 doProofSearch fn False r line (sUN name) (map sUN hints) depth

366−runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =

366+runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =

367 case splitName name of

368 Left err -> iPrintError err

369 Right n -> process fn (MakeLemma False line n)

370−runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =

370+runIdeModeCommand h id orig fn mods (IdeMode.Apropos a) =

371 process fn (Apropos [] a)

372−runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =

372+runIdeModeCommand h id orig fn mods (IdeMode.GetOpts) =

373 do ist <- getIState

374 let opts = idris_options ist

375 let impshow = opt_showimp opts

376 let errCtxt = opt_errContext opts

377− let options = (IdeSlave.SymbolAtom "ok",

377+ let options = (IdeMode.SymbolAtom "ok",

378− [(IdeSlave.SymbolAtom "show-implicits", impshow),

378+ [(IdeMode.SymbolAtom "show-implicits", impshow),

379− (IdeSlave.SymbolAtom "error-context", errCtxt)])

379+ (IdeMode.SymbolAtom "error-context", errCtxt)])

380− runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id

380+ runIO . hPutStrLn h $ IdeMode.convSExp "return" options id

381−runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

381+runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ShowImpl b) =

382 do setImpShow b

383− let msg = (IdeSlave.SymbolAtom "ok", b)

383+ let msg = (IdeMode.SymbolAtom "ok", b)

384− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

384+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

385−runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

385+runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ErrContext b) =

386 do setErrContext b

387− let msg = (IdeSlave.SymbolAtom "ok", b)

387+ let msg = (IdeMode.SymbolAtom "ok", b)

388− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

388+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

389−runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

389+runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

390 do ist <- getIState

391 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

392 let ppo = ppOptionIst ist

@@ -403,7 +403,7 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

403 render ist bnd c pc))

404 splitMvs

405 runIO . hPutStrLn h $

406− IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id

406+ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

407 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

408 mapSnd f xs = zip (map fst xs) (map (f . snd) xs)

409

@@ -447,32 +447,32 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

447 let (out, spans) = render ist bnd t pt in

448 (show n , out, spans)

449

450−runIdeSlaveCommand h id orig fn mods (IdeSlave.WhoCalls n) =

450+runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =

451 case splitName n of

452 Left err -> iPrintError err

453 Right n -> do calls <- whoCalls n

454 ist <- getIState

455− let msg = (IdeSlave.SymbolAtom "ok",

455+ let msg = (IdeMode.SymbolAtom "ok",

456 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

457− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

457+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

458 where pn ist = displaySpans .

459 renderPretty 0.9 1000 .

460 fmap (fancifyAnnots ist) .

461 prettyName True True []

462−runIdeSlaveCommand h id orig fn mods (IdeSlave.CallsWho n) =

462+runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

463 case splitName n of

464 Left err -> iPrintError err

465 Right n -> do calls <- callsWho n

466 ist <- getIState

467− let msg = (IdeSlave.SymbolAtom "ok",

467+ let msg = (IdeMode.SymbolAtom "ok",

468 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

469− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

469+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

470 where pn ist = displaySpans .

471 renderPretty 0.9 1000 .

472 fmap (fancifyAnnots ist) .

473 prettyName True True []

474

475−runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =

475+runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

476 do ctxt <- getContext

477 ist <- getIState

478 let tm' = force (normaliseAll ctxt [] tm)

@@ -482,46 +482,46 @@ runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =

482 []

483 (idris_infixes ist)

484 (delab ist tm'))

485− msg = (IdeSlave.SymbolAtom "ok",

485+ msg = (IdeMode.SymbolAtom "ok",

486 displaySpans .

487 renderPretty 0.9 80 .

488 fmap (fancifyAnnots ist) $ ptm)

489− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

489+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

490−runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

490+runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =

491− ideSlaveForceTermImplicits h id bnd True tm

491+ ideModeForceTermImplicits h id bnd True tm

492−runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

492+runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =

493− ideSlaveForceTermImplicits h id bnd False tm

493+ ideModeForceTermImplicits h id bnd False tm

494−runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =

494+runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =

495 case splitName name of

496 Left err -> iPrintError err

497 Right n -> process "(ideslave)" (PrintDef n)

498−runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrString e) =

498+runIdeModeCommand h id orig fn modes (IdeMode.ErrString e) =

499 do ist <- getIState

500 let out = displayS . renderPretty 1.0 60 $ pprintErr ist e

501− msg = (IdeSlave.SymbolAtom "ok", IdeSlave.StringAtom $ out "")

501+ msg = (IdeMode.SymbolAtom "ok", IdeMode.StringAtom $ out "")

502− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

502+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

503−runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrPPrint e) =

503+runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =

504 do ist <- getIState

505 let (out, spans) =

506 displaySpans .

507 renderPretty 0.9 80 .

508 fmap (fancifyAnnots ist) $ pprintErr ist e

509− msg = (IdeSlave.SymbolAtom "ok", out, spans)

509+ msg = (IdeMode.SymbolAtom "ok", out, spans)

510− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

510+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

511

512−-- | Show a term for IDESlave with the specified implicitness

512+-- | Show a term for IDEMode with the specified implicitness

513−ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

513+ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

514−ideSlaveForceTermImplicits h id bnd impl tm =

514+ideModeForceTermImplicits h id bnd impl tm =

515 do ist <- getIState

516 let expl = annotate (AnnTerm bnd tm)

517 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })

518 bnd [] (idris_infixes ist)

519 (delab ist tm))

520− msg = (IdeSlave.SymbolAtom "ok",

520+ msg = (IdeMode.SymbolAtom "ok",

521 displaySpans .

522 renderPretty 0.9 80 .

523 fmap (fancifyAnnots ist) $ expl)

524− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

524+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

525

526splitName :: String -> Either String Name

527splitName s = case reverse $ splitOn "." s of

@@ -537,6 +537,7 @@ ideslaveProcess fn Warranty = process fn Warranty

537ideslaveProcess fn Help = process fn Help

538ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

539 iPrintResult "changed directory to"

540+ideslaveProcess fn (ModImport f) = process fn (ModImport f)

540ideslaveProcess fn (Eval t) = process fn (Eval t)

541ideslaveProcess fn (Eval t) = process fn (Eval t)

541ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)

542ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)

542 iPrintResult "defined"

543 iPrintResult "defined"

@@ -722,6 +723,10 @@ process fn Warranty = iPrintResult warranty

722process fn (ChangeDirectory f)

723process fn (ChangeDirectory f)

723 = do runIO $ setCurrentDirectory f

724 = do runIO $ setCurrentDirectory f

724 return ()

725 return ()

726+process fn (ModImport f) = do fmod <- loadModule f

727+ case fmod of

728+ Just pr -> isetPrompt pr

729+ Nothing -> iPrintError $ "Can't find import " ++ f

725process fn (Eval t)

730process fn (Eval t)

726 = withErrorReflection $ do logLvl 5 $ show t

731 = withErrorReflection $ do logLvl 5 $ show t

727 getIState >>= flip warnDisamb t

732 getIState >>= flip warnDisamb t

@@ -1096,8 +1101,8 @@ process fn Execute

1096 case idris_outputmode ist of

1101 case idris_outputmode ist of

1097 RawOutput h -> do runIO $ rawSystem tmpn []

1102 RawOutput h -> do runIO $ rawSystem tmpn []

1098 return ()

1103 return ()

1099− IdeSlave n h -> runIO . hPutStrLn h $

1104+ IdeMode n h -> runIO . hPutStrLn h $

1100− IdeSlave.convSExp "run-program" tmpn n)

1105+ IdeMode.convSExp "run-program" tmpn n)

1101 (\e -> getIState >>= iRenderError . flip pprintErr e)

1106 (\e -> getIState >>= iRenderError . flip pprintErr e)

1102 where fc = fileFC "main"

1107 where fc = fileFC "main"

1103process fn (Compile codegen f)

1108process fn (Compile codegen f)

@@ -1482,7 +1487,7 @@ idrisMain opts =

1482 do let inputs = opt getFile opts

1487 do let inputs = opt getFile opts

1483 let quiet = Quiet `elem` opts

1488 let quiet = Quiet `elem` opts

1484 let nobanner = NoBanner `elem` opts

1489 let nobanner = NoBanner `elem` opts

1485− let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts

1490+ let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

1486 let runrepl = not (NoREPL `elem` opts)

1491 let runrepl = not (NoREPL `elem` opts)

1487 let verbose = runrepl || Verbose `elem` opts

1492 let verbose = runrepl || Verbose `elem` opts

1488 let output = opt getOutput opts

1493 let output = opt getOutput opts

@@ -1607,7 +1612,7 @@ idrisMain opts =

1607-- clearOrigPats

1612-- clearOrigPats

1608 startServer port orig mods

1613 startServer port orig mods

1609 runInputT (replSettings (Just historyFile)) $ repl orig mods efile

1614 runInputT (replSettings (Just historyFile)) $ repl orig mods efile

1610− let idesock = IdeslaveSocket `elem` opts

1615+ let idesock = IdemodeSocket `elem` opts

1611 when (idesl) $ ideslaveStart idesock orig inputs

1616 when (idesl) $ ideslaveStart idesock orig inputs

1612 ok <- noErrors

1617 ok <- noErrors

1613 when (not ok) $ runIO (exitWith (ExitFailure 1))

1618 when (not ok) $ runIO (exitWith (ExitFailure 1))

src/Idris/TypeSearch.hs+1−1

@@ -57,7 +57,7 @@ searchByType pkgs pterm = do

57 case idris_outputmode i of

58 RawOutput _ -> do mapM_ iRenderOutput docs

59 iPrintResult ""

60− IdeSlave _ _ -> iRenderResult (vsep docs)

60+ IdeMode _ _ -> iRenderResult (vsep docs)

61 putIState i -- don't actually make any changes

62 where

63 numLimit = 50

test/totality006/expected+1

@@ -1,2 +1,3 @@

1totality006.idr:8:1:Main.prf is not total as there are missing cases

2totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

3+totality006b.idr:10:1:totality006b.blargh is not total as there are missing cases

test/totality006/run+1

@@ -1,4 +1,5 @@

1#!/usr/bin/env bash

2idris $@ totality006.idr --check

3idris $@ totality006a.idr --check

4+idris $@ totality006b.idr --check

4rm -f *.ibc

5rm -f *.ibc

test/totality006/totality006b.idrnew file+14

@@ -0,0 +1,14 @@

1+module totality006b

3+import Data.So

6+-- There are approaches to impossibility checking that break on this

7+-- case but not on test006.idr, due to the extra computation.

8+total

9+blargh : (xs, ys : List a) -> So (length xs > length ys) -> GT (length xs) (length ys)

10+blargh [] [] Oh impossible

11+blargh [] (y :: xs) so = absurd so

12+blargh (y :: xs) [] Oh = LTESucc LTEZero

13+

14+-- Missing: blargh (y :: xs) (z :: ys) x = ?blargh_rhs_3