c918f44 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Conflicts: src/Idris/Core/Elaborate.hs

commitc918f44d4b297d68dd288e1ef99208fa74dee147 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Feb 2015, 14:05 (12 years ago) parent26cfbe9 807d623

25 files changed+301−238

compare with master

unifiedsplit

CHANGELOG+5

@@ -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.

16New in 0.9.16:

27--------------

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

CONTRIBUTORS+3−2

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

77Michael R. Bernstein

88Nicola Botta

99Edwin Brady

10+Jakob Brünker

11+Alyssa Carter

1012David Raymond Christiansen

1113Carter Charbonneau

1214Jason Dagit

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

2830Reynir Reynisson

2931Seo Sanghyeon

3032Benjamin Saunders

33+Alexander Shabalin

3134startling

3235Chetan T

3336Matúš Tejiščák

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

3538Leif Warner

3639Daniel Waterworth

3740Jonas Westerlund

38−Alyssa Carter

39−Alexander Shabalin

idris.cabal+1−1

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

685685 , Idris.ErrReverse

686686 , Idris.Help

687687 , Idris.IBC

688− , Idris.IdeSlave

688+ , Idris.IdeMode

689689 , Idris.IdrisDoc

690690 , Idris.Imports

691691 , Idris.Inliner

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

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

11module Data.Sign

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

4−data Sign = Plus | Minus

4+data Sign = Plus | Zero | Minus

66||| Discover the sign of some type

77class Signed t where

libs/base/Data/ZZ.idr+1

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

1515data ZZ = Pos Nat | NegS Nat

1616

1717instance Signed ZZ where

18+ sign (Pos Z) = Zero

1819 sign (Pos _) = Plus

1920 sign (NegS _) = Minus

2021

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

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

3131instance Show SocketFamily where

3232 show AF_UNSPEC = "AF_UNSPEC"

3333 show AF_INET = "AF_INET"

34− show AF_INET6 = "AF_INET4"

34+ show AF_INET6 = "AF_INET6"

3535

3636instance ToCode SocketFamily where

3737 toCode AF_UNSPEC = 0

src/Idris/AbsSyntax.hs+15−9

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

1010import Idris.AbsSyntaxTree

1111import Idris.Colours

1212import Idris.Docstrings

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

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

1414import IRTS.CodegenCommon

1515import Util.DynamicLinker

1616

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

601601isetPrompt :: String -> Idris ()

602602isetPrompt p = do i <- getIState

603603 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

605605

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

607607isetLoadedRegion :: Idris ()

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

610610 case span of

611611 Just fc ->

612612 case idris_outputmode i of

613− IdeSlave n h ->

613+ IdeMode n h ->

614614 runIO . hPutStrLn h $

615615 convSExp "set-loaded-region" fc n

616616 Nothing -> return ()

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

752752outputTy = do i <- getIState

753753 return $ opt_outputTy $ idris_options i

754754

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

756−setIdeSlave True h = do i <- getIState

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

758−setIdeSlave False _ = return ()

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

756+setIdeMode True h = do i <- getIState

757+ putIState $ i { idris_outputmode = IdeMode 0 h

758+ , idris_colourRepl = False

759+ }

760+setIdeMode False _ = return ()

759761

760762setTargetTriple :: String -> Idris ()

761763setTargetTriple t = do i <- getIState

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

870872 when (lvl >= l) $

871873 case idris_outputmode i of

872874 RawOutput h -> do runIO $ hPutStrLn h str

873− IdeSlave n h ->

875+ IdeMode n h ->

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

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

876878

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

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

17351737 = Placeholder

17361738 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

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

17391745 su (PApp fc f args)

17401746 = PHidden (PApp fc f args)

src/Idris/AbsSyntaxTree.hs+18−4

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

2626

2727import Data.Data (Data)

2828import Data.Function (on)

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

2930import Data.List hiding (group)

3031import Data.Char

3132import qualified Data.Map.Strict as M

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

143144

144145-- | The output mode in use

145146data 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

147148 deriving Show

148149

149150-- | How wide is the console?

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

404405 | Quiet

405406 | NoBanner

406407 | ColourREPL Bool

407− | Ideslave

408− | IdeslaveSocket

408+ | Idemode

409+ | IdemodeSocket

409410 | ShowLibs

410411 | ShowLibdir

411412 | ShowIncs

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

13761377 where

13771378 startPrec = 0

13781379 funcAppPrec = 10

1380+

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

13801382 prettySe p bnd (PQuote r) =

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

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

16411643 getFixity :: String -> Maybe Fixity

16421644 getFixity = flip M.lookup fixities

16431645

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+

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

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

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

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

16561668 -> Doc OutputAnnotation

16571669prettyName infixParen showNS bnd n

16581670 | (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 "_"

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

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

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

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

17281740getShowArgs [] = []

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

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

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

1744+ , containsHole tm = e : getShowArgs xs

17311745getShowArgs (_ : xs) = getShowArgs xs

17321746

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

src/Idris/CmdOptions.hs+4−2

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

7171parseFlags = many $

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

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

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

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

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

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

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

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

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

173173

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

175175

176−-- get the global context

176+-- | Get the global context

177177get_context :: Elab' aux Context

178178get_context = do ES p _ _ <- get

179179 return $! (context (fst p))

180180

181−-- update the context

181+-- | Update the context.

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

183183-- stuff could go wrong)

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

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

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

187187

188−-- get the proof term

188+-- | get the proof term

189189get_term :: Elab' aux Term

190190get_term = do ES p _ _ <- get

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

192192

193−-- get the proof term

193+-- | get the proof term

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

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

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

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

198198

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

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

200200get_env :: Elab' aux Env

201201get_env = do ES p _ _ <- get

202202 lift $ envAtFocus (fst p)

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

213213get_probs = do ES p _ _ <- get

214214 return $! (problems (fst p))

215215

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

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

217217-- last call to get_recents)

218218get_recents :: Elab' aux [Name]

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

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

221221 return (recents p)

222222

223−-- get the current goal type

223+-- | get the current goal type

224224goal :: Elab' aux Type

225225goal = do ES p _ _ <- get

226226 b <- lift $ goalAtFocus (fst p)

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

233233 Guess _ _ -> return True

234234 _ -> return False

235235

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

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

237237get_guess :: Elab' aux Term

238238get_guess = do ES p _ _ <- get

239239 b <- lift $ goalAtFocus (fst p)

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

241241 Guess t v -> return $! v

242242 _ -> fail "Not a guess"

243243

244−-- typecheck locally

244+-- | Typecheck locally

245245get_type :: Raw -> Elab' aux Type

246246get_type tm = do ctxt <- get_context

247247 env <- get_env

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

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

255255 return $! (finalise val, finalise ty)

256256

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

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

258258get_deferred :: Elab' aux [Name]

259259get_deferred = do ES p _ _ <- get

260260 return $! (deferred (fst p))

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

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

272272 isInj ctxt _ = False

273273

274−-- get instance argument names

274+-- | get instance argument names

275275get_instances :: Elab' aux [Name]

276276get_instances = do ES p _ _ <- get

277277 return $! (instances (fst p))

278278

279−-- get auto argument names

279+-- | get auto argument names

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

281281get_autos = do ES p _ _ <- get

282282 return $! (autos (fst p))

283283

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

285286unique_hole = unique_hole' False

286287

287288unique_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,

1111 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,

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

1313 mapDefCtxt,

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

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

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

1616 isUniverse) where

1717

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

971971

972972isTConName :: Name -> Context -> Bool

973973isTConName n ctxt

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

975− case tfst def of

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

977− _ -> return False

974+ = case lookupDefExact n ctxt of

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

976+ _ -> False

978977

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

979979isDConName :: Name -> Context -> Bool

980980isDConName 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

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

982989 case tfst def of

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

984− _ -> return False

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

991+ _ -> return False

985992

986993isFnName :: Name -> Context -> Bool

987994isFnName n ctxt

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

989− case def of

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

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

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

993− _ -> False

995+ = case lookupDefExact n ctxt of

996+ Just (Function _ _) -> True

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

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

999+ _ -> False

9941000

9951001isTCDict :: Name -> Context -> Bool

9961002isTCDict n ctxt

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

998− case def of

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

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

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

1002− _ -> False

1003+ = case lookupDefExact n ctxt of

1004+ Just (Function _ _) -> False

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

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

1007+ _ -> False

10031008

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

10051010lookupP n ctxt

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

10071012 p <- case def of

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

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

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

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

10101015 (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)

10121017 case snd p of

1013− Hidden -> []

1014− _ -> return (fst p)

1018+ Hidden -> []

1019+ _ -> return (fst p)

10151020

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

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

src/Idris/Coverage.hs+10−11

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

1818

1919import Control.Monad.State.Strict

2020

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

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

23−-- generation.)

24−

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

22+--

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

24+-- provided explicitly from new clause generation.

2525mkPatTm :: PTerm -> Idris Term

2626mkPatTm t = do i <- getIState

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

2828 evalStateT (toTT (mapPT deNS timp)) 0

2929 where

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

31− case lookupDef n (tt_ctxt i) of

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

31+ case lookupNameDef n (tt_ctxt i) of

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

3333 _ -> return $ P Ref n Erased

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

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

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

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

4545 deNS t = t

4646

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

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

50−

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

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

50+--

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

5252-- names are fully explicit!

53−

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

5554genClauses fc n xs given

5655 = do i <- getIState

src/Idris/Delaborate.hs+2−2

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

308308 where whatIsName = let ctxt = tt_ctxt i

309309 in if isTConName f ctxt

310310 then text "type constructor" <> space

311− else if isConName f ctxt

311+ else if isDConName f ctxt

312312 then text "constructor" <> space

313313 else if isFnName f ctxt

314314 then text "function" <> space

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

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

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

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

491− _ | otherwise -> annot

491+ _ | otherwise -> annot

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

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

494494 let o = overview (fst docs)

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

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

7474 (e, et) <- case what of

7575 ProvTerm _ tm -> elabVal info ERHS tm

7676 ProvPostulate tm -> elabVal info ERHS tm

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

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

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

77+ unless (isProviderOf ctxt ty' et) $

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

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

8080

8181 -- Execute the type provider and normalise the result

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

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

107107 isTType (TType _) = True

108108 isTType _ = False

109109

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

111− isProviderOf tp prov

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

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

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

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

116− isProviderOf _ _ = False

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+

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

119+ isProviderOf ctxt tp prov =

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

121+ OK _ -> True

122+ _ -> False

117123

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

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

33{-# 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

77import Text.Printf

88import Numeric

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

206206

207207data Opt = ShowImpl | ErrContext deriving Show

208208

209−data IdeSlaveCommand = REPLCompletions String

210− | Interpret String

211− | TypeOf String

212− | CaseSplit Int String

213− | AddClause Int String

214− | AddProofClause Int String

215− | AddMissing Int String

216− | MakeWithBlock Int String

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

218− | MakeLemma Int String

219− | LoadFile String (Maybe Int)

220− | DocsFor String

221− | Apropos String

222− | GetOpts

223− | SetOpt Opt Bool

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

225− | WhoCalls String

226− | CallsWho String

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

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

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

230− | PrintDef String

231− | ErrString Err

232− | ErrPPrint Err

233−

234−sexpToCommand :: SExp -> Maybe IdeSlaveCommand

209+data IdeModeCommand = REPLCompletions String

210+ | Interpret String

211+ | TypeOf String

212+ | CaseSplit Int String

213+ | AddClause Int String

214+ | AddProofClause Int String

215+ | AddMissing Int String

216+ | MakeWithBlock Int String

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

218+ | MakeLemma Int String

219+ | LoadFile String (Maybe Int)

220+ | DocsFor String

221+ | Apropos String

222+ | GetOpts

223+ | SetOpt Opt Bool

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

225+ | WhoCalls String

226+ | CallsWho String

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

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

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

230+ | PrintDef String

231+ | ErrString Err

232+ | ErrPPrint Err

233+

234+sexpToCommand :: SExp -> Maybe IdeModeCommand

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

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

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

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

298298getHexLength :: String -> String

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

300300

301−ideSlaveEpoch :: Int

302−ideSlaveEpoch = 1

301+ideModeEpoch :: Int

302+ideModeEpoch = 1

src/Idris/Interactive.hs+3−3

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

1616import Idris.Error

1717import Idris.Delaborate

1818import Idris.Output

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

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

2020

2121import Idris.Elab.Value

2222

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

271271 runIO $ copyFile fb fn

272272 else case idris_outputmode i of

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

274− IdeSlave n h ->

274+ IdeMode n h ->

275275 let good = SexpList [SymbolAtom "ok",

276276 SexpList [SymbolAtom "metavariable-lemma",

277277 SexpList [SymbolAtom "replace-metavariable",

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

289289 runIO $ copyFile fb fn

290290 else case idris_outputmode i of

291291 RawOutput _ -> iPrintResult $ lem_app

292− IdeSlave n h ->

292+ IdeMode n h ->

293293 let good = SexpList [SymbolAtom "ok",

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

295295 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+18−18

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

88import Idris.AbsSyntax

99import Idris.Delaborate

1010import Idris.Docstrings

11−import Idris.IdeSlave

11+import Idris.IdeMode

1212

1313import Util.Pretty

1414import Util.ScreenSize (getScreenWidth)

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

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

4444 else err

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

46− IdeSlave n h ->

46+ IdeMode n h ->

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

4848 let (str, spans) = displaySpans err'

4949 runIO . hPutStrLn h $

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

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

5353iRender d = do w <- getWidth

5454 ist <- getIState

55− let ideSlave = case idris_outputmode ist of

56− IdeSlave _ _ -> True

55+ let ideMode = case idris_outputmode ist of

56+ IdeMode _ _ -> True

5757 _ -> False

5858 case w of

5959 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

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

6161 if n < 1

6262 then renderPretty 1.0 1000000000 d

6363 else renderPretty 0.8 n d

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

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

6565 | otherwise -> do width <- runIO getScreenWidth

6666 return $ renderPretty 0.8 width d

6767

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

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

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

7878

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

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

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

8282iPrintFunTypes bnd n overloads = do ist <- getIState

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

9494 case idris_outputmode i of

9595 RawOutput h -> do out <- iRender doc

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

97− IdeSlave n h ->

97+ IdeMode n h ->

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

9999 let out = [toSExp str, toSExp spans]

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

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

103103iRenderResult d = do ist <- getIState

104104 case idris_outputmode ist of

105105 RawOutput h -> consoleDisplayAnnotated h d

106− IdeSlave n h -> ideSlaveReturnAnnotated n h d

106+ IdeMode n h -> ideModeReturnAnnotated n h d

107107

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

109−ideSlaveReturnWithStatus status n h out = do

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

109+ideModeReturnWithStatus status n h out = do

110110 ist <- getIState

111111 (str, spans) <- fmap displaySpans .

112112 iRender .

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

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

117117

118118

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

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

121−ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

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

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

121+ideModeReturnAnnotated = ideModeReturnWithStatus "ok"

122122

123123-- | Show an error with semantic highlighting

124124iRenderError :: Doc OutputAnnotation -> Idris ()

125125iRenderError e = do ist <- getIState

126126 case idris_outputmode ist of

127127 RawOutput h -> consoleDisplayAnnotated h e

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

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

129129

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

131131iPrintWithStatus status s = do

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

134134 RawOutput h -> case s of

135135 "" -> return ()

136136 s -> runIO $ hPutStrLn h s

137− IdeSlave n h ->

137+ IdeMode n h ->

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

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

140140

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

149149iputStrLn s = do i <- getIState

150150 case idris_outputmode i of

151151 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

153153

154154

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

156156ideslavePutSExp cmd info = do i <- getIState

157157 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

159159 _ -> return ()

160160

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

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

163163iputGoal g = do i <- getIState

164164 case idris_outputmode i of

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

166− IdeSlave n h ->

166+ IdeMode n h ->

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

168168 goal = [toSExp str, toSExp spans]

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

src/Idris/ParseHelpers.hs+4−2

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

224224idrisStyle :: MonadicParsing m => IdentifierStyle m

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

226226 where _styleName = "Idris"

227− _styleStart = satisfy isAlpha

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

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

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

230230 "do", "dsl", "import", "impossible",

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

262262

263263-- | Parses an identifier as a token

264264identifier :: 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)

266268

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

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

src/Idris/Parser.hs+1−1

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

11921192 i <- getIState

11931193 case idris_outputmode i of

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

11961196 putIState (i { errSpan = Just fc })

11971197 return []

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

src/Idris/Prover.hs+15−15

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

2020import Idris.Error

2121import Idris.DataOpts

2222import Idris.Completion

23−import qualified Idris.IdeSlave as IdeSlave

23+import qualified Idris.IdeMode as IdeMode

2424import Idris.Output

2525import Idris.TypeSearch (searchByType)

2626

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

7272 iLOG $ "Adding " ++ show tm

7373 i <- getIState

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

7676 _ -> iputStrLn $ showProof lit n prf

7777 let proofs = proof_list i

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

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

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

9696 solveDeferred n

9797 case idris_outputmode i of

98− IdeSlave n h ->

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

98+ IdeMode n h ->

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

100100 _ -> return ()

101101

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

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

185185receiveInput h e =

186186 do i <- getIState

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

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

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

189189 len <- case len' of

190190 Left err -> ierror err

191191 Right n -> return n

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

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

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

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

194194 Left err -> ierror err

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

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

197− case IdeSlave.sexpToCommand sexp of

198− Just (IdeSlave.REPLCompletions prefix) ->

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

197+ case IdeMode.sexpToCommand sexp of

198+ Just (IdeMode.REPLCompletions prefix) ->

199199 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)]

201201 ideslavePutSExp "return" good

202202 receiveInput h e

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

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

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

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

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

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

206206 _ -> return Nothing

207207

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

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

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

222222 h' <- getHistory

223223 return (l, Just h')

224− IdeSlave _ handle ->

224+ IdeMode _ handle ->

225225 do isetPrompt prompt

226226 i <- receiveInput handle e

227227 return (i, h)

src/Idris/REPL.hs+94−89

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

2222import Idris.Coverage

2323import Idris.Docs hiding (Doc)

2424import Idris.Completion

25−import qualified Idris.IdeSlave as IdeSlave

25+import qualified Idris.IdeMode as IdeMode

2626import Idris.Chaser

2727import Idris.Imports

2828import Idris.Colours hiding (colourise)

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

165165 cmd <- hGetLine h

166166 let isth = case idris_outputmode ist of

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

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

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

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

170170 hClose h

171171 loop fn ist' sock

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

204204 do ist <- getIState

205205 putIState $ case idris_outputmode ist of

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

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

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

208208

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

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

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

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

233233

234234

235−initIdeslaveSocket :: IO Handle

236−initIdeslaveSocket = do

235+initIdemodeSocket :: IO Handle

236+initIdemodeSocket = do

237237 (sock, port) <- listenOnLocalhostAnyPort

238238 putStrLn $ show port

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

240240 hSetEncoding h utf8

241241 return h

242242

243−-- | Run the IdeSlave

243+-- | Run the IdeMode

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

245245ideslaveStart s orig mods

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

247− setIdeSlave True h

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

247+ setIdeMode True h

248248 i <- getIState

249249 case idris_outputmode i of

250− IdeSlave n h ->

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

250+ IdeMode n h ->

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

252252 case mods of

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

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

254254 _ -> return ()

255255 ideslave h orig mods

256256

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

258258ideslave h orig mods

259259 = do idrisCatch

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

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

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

262262 len <- case len' of

263263 Left err -> ierror err

264264 Right n -> return n

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

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

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

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

267267 Left err -> ierror err

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

269269 i <- getIState

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

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

271271 idrisCatch -- to report correct id back!

272272 (do let fn = case mods of

273273 (f:_) -> f

274274 _ -> ""

275− case IdeSlave.sexpToCommand sexp of

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

275+ case IdeMode.sexpToCommand sexp of

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

277277 Nothing -> iPrintError "did not understand" )

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

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

280280 ideslave h orig mods

281281

282−-- | Run IDESlave commands

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

282+-- | Run IDEMode commands

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

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

285285 -> IState -- ^^ The original IState

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

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

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

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

289289 -> Idris ()

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

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

291291 do c <- colourise

292292 i <- getIState

293293 case parseCmd i "(input)" cmd of

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

297297 (do process fn (Prove n')

298298 isetPrompt (mkPrompt mods)

299299 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

301301 runIO . hPutStrLn h $

302− IdeSlave.convSExp "return"

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

302+ IdeMode.convSExp "return"

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

304304 n

305305 _ -> return ())

306306 (\e -> do ist <- getIState

307307 isetPrompt (mkPrompt mods)

308308 case idris_outputmode i of

309− IdeSlave n h ->

309+ IdeMode n h ->

310310 runIO . hPutStrLn h $

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

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

312312 _ -> return ()

313313 iRenderError $ pprintErr ist e)

314314 Success (Right cmd) -> idrisCatch

315315 (ideslaveProcess fn cmd)

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

317317 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) =

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

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

321− IdeSlave.toSExp (map replacement compls,

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

321+ IdeMode.toSExp (map replacement compls,

322322 reverse unused)]

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

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

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

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

325325 do i <- getIState

326326 clearErr

327327 putIState (orig { idris_options = idris_options i,

328− idris_outputmode = (IdeSlave id h) })

328+ idris_outputmode = (IdeMode id h) })

329329 mods <- loadInputs [filename] toline

330330 isetPrompt (mkPrompt mods)

331331 -- Report either success or failure

332332 i <- getIState

333333 case (errSpan i) of

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

335− IdeSlave.SexpList []])

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

337− IdeSlave.toSExp fc])

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

335+ IdeMode.SexpList []])

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

337+ IdeMode.toSExp fc])

338338 (idris_parsedSpan i)

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

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

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

341341 ideslave h orig mods

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

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

343343 case splitName name of

344344 Left err -> iPrintError err

345345 Right n -> process "(ideslave)"

346346 (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) =

348348 case parseConst orig name of

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

350350 Failure _ ->

351351 case splitName name of

352352 Left err -> iPrintError err

353353 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) =

355355 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) =

357357 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) =

359359 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) =

361361 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) =

363363 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) =

365365 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) =

367367 case splitName name of

368368 Left err -> iPrintError err

369369 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) =

371371 process fn (Apropos [] a)

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

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

373373 do ist <- getIState

374374 let opts = idris_options ist

375375 let impshow = opt_showimp opts

376376 let errCtxt = opt_errContext opts

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

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

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

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

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

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

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

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

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

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

382382 do setImpShow b

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

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

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

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

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

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

386386 do setErrContext b

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

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

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

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

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

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

390390 do ist <- getIState

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

392392 let ppo = ppOptionIst ist

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

403403 render ist bnd c pc))

404404 splitMvs

405405 runIO . hPutStrLn h $

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

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

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

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

409409

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

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

448448 (show n , out, spans)

449449

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

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

451451 case splitName n of

452452 Left err -> iPrintError err

453453 Right n -> do calls <- whoCalls n

454454 ist <- getIState

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

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

456456 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

458458 where pn ist = displaySpans .

459459 renderPretty 0.9 1000 .

460460 fmap (fancifyAnnots ist) .

461461 prettyName True True []

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

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

463463 case splitName n of

464464 Left err -> iPrintError err

465465 Right n -> do calls <- callsWho n

466466 ist <- getIState

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

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

468468 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

470470 where pn ist = displaySpans .

471471 renderPretty 0.9 1000 .

472472 fmap (fancifyAnnots ist) .

473473 prettyName True True []

474474

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

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

476476 do ctxt <- getContext

477477 ist <- getIState

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

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

482482 []

483483 (idris_infixes ist)

484484 (delab ist tm'))

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

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

486486 displaySpans .

487487 renderPretty 0.9 80 .

488488 fmap (fancifyAnnots ist) $ ptm)

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

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

491− ideSlaveForceTermImplicits h id bnd True tm

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

493− ideSlaveForceTermImplicits h id bnd False tm

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

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

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

491+ ideModeForceTermImplicits h id bnd True tm

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

493+ ideModeForceTermImplicits h id bnd False tm

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

495495 case splitName name of

496496 Left err -> iPrintError err

497497 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) =

499499 do ist <- getIState

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

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

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

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

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

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

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

504504 do ist <- getIState

505505 let (out, spans) =

506506 displaySpans .

507507 renderPretty 0.9 80 .

508508 fmap (fancifyAnnots ist) $ pprintErr ist e

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

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

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

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

511511

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

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

514−ideSlaveForceTermImplicits h id bnd impl tm =

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

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

514+ideModeForceTermImplicits h id bnd impl tm =

515515 do ist <- getIState

516516 let expl = annotate (AnnTerm bnd tm)

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

518518 bnd [] (idris_infixes ist)

519519 (delab ist tm))

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

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

521521 displaySpans .

522522 renderPretty 0.9 80 .

523523 fmap (fancifyAnnots ist) $ expl)

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

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

525525

526526splitName :: String -> Either String Name

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

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

537537ideslaveProcess fn Help = process fn Help

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

539539 iPrintResult "changed directory to"

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

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

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

542543 iPrintResult "defined"

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

722723process fn (ChangeDirectory f)

723724 = do runIO $ setCurrentDirectory f

724725 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

725730process fn (Eval t)

726731 = withErrorReflection $ do logLvl 5 $ show t

727732 getIState >>= flip warnDisamb t

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

10961101 case idris_outputmode ist of

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

10981103 return ()

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

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

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

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

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

11021107 where fc = fileFC "main"

11031108process fn (Compile codegen f)

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

14821487 do let inputs = opt getFile opts

14831488 let quiet = Quiet `elem` opts

14841489 let nobanner = NoBanner `elem` opts

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

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

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

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

14881493 let output = opt getOutput opts

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

16071612-- clearOrigPats

16081613 startServer port orig mods

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

1610− let idesock = IdeslaveSocket `elem` opts

1615+ let idesock = IdemodeSocket `elem` opts

16111616 when (idesl) $ ideslaveStart idesock orig inputs

16121617 ok <- noErrors

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

src/Idris/TypeSearch.hs+1−1

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

5757 case idris_outputmode i of

5858 RawOutput _ -> do mapM_ iRenderOutput docs

5959 iPrintResult ""

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

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

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

6262 where

6363 numLimit = 50

test/totality006/expected+1

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

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

22totality006a.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 @@

11#!/usr/bin/env bash

22idris $@ totality006.idr --check

33idris $@ totality006a.idr --check

4+idris $@ totality006b.idr --check

45rm -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