ecea9ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' into repl-definitions

Conflicts: src/Idris/AbsSyntaxTree.hs src/Idris/REPL.hs

commitecea9adf1ee0b808a9d928549fbf92f83c516935 authorAlyssa Carter <trillionalyssa@gmail.com> dateTue 5 Aug 2014, 13:03 (12 years ago) parentfaf1d39 02f7c64

26 files changed+701−481

compare with master

unifiedsplit

.travis.yml+1

@@ -25,6 +25,7 @@ script:

2525 - make -j2 $TESTS

2626env:

2727 - TESTS="doc"

28+ - TESTS="lib_doc"

2829 - TESTS="test_c"

2930 - TESTS="test_llvm"

3031 - TESTS="test_js"

CHANGELOG+2

@@ -2,6 +2,8 @@ New in 0.9.15:

22--------------

33* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.

44* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.

5+* Stop showing irrelevant and inaccessible internal names in the interactive prover

6+* The proof arguments in the List library functions are now implicit and solved automatically

68New in 0.9.14:

79--------------

libs/prelude/Prelude/List.idr+14−14

@@ -72,9 +72,9 @@ index' _ [] = Nothing

7272

7373||| Get the first element of a non-empty list

7474||| @ ok proof that the list is non-empty

75−head : (l : List a) -> (ok : isCons l = True) -> a

76−head [] refl impossible

77−head (x::xs) p = x

75+head : (l : List a) -> {auto ok : isCons l = True} -> a

76+head [] {ok=refl} impossible

77+head (x::xs) {ok=p} = x

7878

7979||| Attempt to get the first element of a list. If the list is empty, return

8080||| `Nothing`.

@@ -84,9 +84,9 @@ head' (x::xs) = Just x

8484

8585||| Get the tail of a non-empty list.

8686||| @ ok proof that the list is non-empty

87−tail : (l : List a) -> (ok : isCons l = True) -> List a

88−tail [] refl impossible

89−tail (x::xs) p = xs

87+tail : (l : List a) -> {auto ok : isCons l = True} -> List a

88+tail [] {ok=refl} impossible

89+tail (x::xs) {ok=p} = xs

9090

9191||| Attempt to get the tail of a list.

9292|||

@@ -97,10 +97,10 @@ tail' (x::xs) = Just xs

9797

9898||| Retrieve the last element of a non-empty list.

9999||| @ ok proof that the list is non-empty

100−last : (l : List a) -> (ok : isCons l = True) -> a

101−last [] refl impossible

102−last [x] p = x

103−last (x::y::ys) p = last (y::ys) refl

100+last : (l : List a) -> {auto ok : isCons l = True} -> a

101+last [] {ok=refl} impossible

102+last [x] {ok=p} = x

103+last (x::y::ys) {ok=p} = last (y::ys) {ok=refl}

104104

105105||| Attempt to retrieve the last element of a non-empty list.

106106|||

@@ -114,10 +114,10 @@ last' (x::xs) =

114114

115115||| Return all but the last element of a non-empty list.

116116||| @ ok proof that the list is non-empty

117−init : (l : List a) -> (ok : isCons l = True) -> List a

118−init [] refl impossible

119−init [x] p = []

120−init (x::y::ys) p = x :: init (y::ys) refl

117+init : (l : List a) -> {auto ok : isCons l = True} -> List a

118+init [] {ok=refl} impossible

119+init [x] {ok=p} = []

120+init (x::y::ys) {ok=p} = x :: init (y::ys) {ok=refl}

121121

122122||| Attempt to Return all but the last element of a list.

123123|||

src/Idris/AbsSyntax.hs+10−14

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

537537isetPrompt :: String -> Idris ()

538538isetPrompt p = do i <- getIState

539539 case idris_outputmode i of

540− IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

540+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

541541

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

543543isetLoadedRegion :: Idris ()

@@ -546,8 +546,8 @@ isetLoadedRegion = do i <- getIState

546546 case span of

547547 Just fc ->

548548 case idris_outputmode i of

549− IdeSlave n ->

550− runIO . putStrLn $

549+ IdeSlave n h ->

550+ runIO . hPutStrLn h $

551551 convSExp "set-loaded-region" fc n

552552 Nothing -> return ()

553553

@@ -662,10 +662,10 @@ outputTy :: Idris OutputType

662662outputTy = do i <- getIState

663663 return $ opt_outputTy $ idris_options i

664664

665−setIdeSlave :: Bool -> Idris ()

666−setIdeSlave True = do i <- getIState

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

668−setIdeSlave False = return ()

665+setIdeSlave :: Bool -> Handle -> Idris ()

666+setIdeSlave True h = do i <- getIState

667+ putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }

668+setIdeSlave False _ = return ()

669669

670670setTargetTriple :: String -> Idris ()

671671setTargetTriple t = do i <- getIState

@@ -761,10 +761,6 @@ setColourise :: Bool -> Idris ()

761761setColourise b = do i <- getIState

762762 putIState $ i { idris_colourRepl = b }

763763

764−setOutH :: Handle -> Idris ()

765−setOutH h = do i <- getIState

766− putIState $ i { idris_outh = h }

767−

768764impShow :: Idris Bool

769765impShow = do i <- getIState

770766 return (opt_showimp (idris_options i))

@@ -793,10 +789,10 @@ logLvl l str = do i <- getIState

793789 let lvl = opt_logLevel (idris_options i)

794790 when (lvl >= l) $

795791 case idris_outputmode i of

796− RawOutput -> do runIO $ putStrLn str

797− IdeSlave n ->

792+ RawOutput h -> do runIO $ hPutStrLn h str

793+ IdeSlave n h ->

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

799− runIO $ putStrLn $ convSExp "log" good n

795+ runIO . hPutStrLn h $ convSExp "log" good n

800796

801797cmdOptType :: Opt -> Idris Bool

802798cmdOptType x = do i <- getIState

src/Idris/AbsSyntaxTree.hs+8−8

@@ -127,7 +127,9 @@ ppOptionIst = ppOption . idris_options

127127data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

128128

129129-- | The output mode in use

130−data OutputMode = RawOutput | IdeSlave Integer deriving Show

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

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

132+ deriving Show

131133

132134-- | How wide is the console?

133135data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

@@ -192,7 +194,6 @@ data IState = IState {

192194 idris_outputmode :: OutputMode,

193195 idris_colourRepl :: Bool,

194196 idris_colourTheme :: ColourTheme,

195− idris_outh :: Handle,

196197 idris_errorhandlers :: [Name], -- ^ Global error handlers

197198 idris_nameIdx :: (Int, Ctxt (Int, Name)),

198199 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers

@@ -278,8 +279,8 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

278279 emptyContext emptyContext emptyContext emptyContext

279280 emptyContext emptyContext

280281 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

281− [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

282− True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

282+ [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

283+ (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

283284 AutomaticWidth S.empty Nothing Nothing []

284285

285286-- | The monad for the main REPL - reading and processing files and updating

@@ -360,6 +361,7 @@ data Opt = Filename String

360361 | NoBanner

361362 | ColourREPL Bool

362363 | Ideslave

364+ | IdeslaveSocket

363365 | ShowLibs

364366 | ShowLibdir

365367 | ShowIncs

@@ -1637,6 +1639,7 @@ instance Sized PTerm where

16371639 size (PProof tactics) = size tactics

16381640 size (PElabError err) = size err

16391641 size PImpossible = 1

1642+ size _ = 0

16401643

16411644getPArity :: PTerm -> Int

16421645getPArity (PPi _ _ _ sc) = 1 + getPArity sc

@@ -1716,7 +1719,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

17161719 (nub (concatMap (ni env) (map snd os))

17171720 \\ nub (concatMap (ni env) (map fst os)))

17181721 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1719− ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1722+ ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc

17201723 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

17211724 ni env (PRewrite _ l r _) = ni env l ++ ni env r

17221725 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1730,9 +1733,6 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

17301733 ni env (PNoImplicits tm) = ni env tm

17311734 ni env _ = []

17321735

1733− niTacImp env (TacImp _ _ scr) = ni env scr

1734− niTacImp _ _ = []

1735−

17361736-- Return names which are free in the given term.

17371737namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

17381738namesIn uvars ist tm = nub $ ni [] tm

src/Idris/CmdOptions.hs+1

@@ -71,6 +71,7 @@ parseFlags = many $

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

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

7373 <|> flag' Ideslave (long "ideslave")

74+ <|> flag' IdeslaveSocket (long "ideslave-socket")

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

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

7677 <|> flag' NoBasePkgs (long "nobasepkgs")

src/Idris/Core/Elaborate.hs+10−1

@@ -12,7 +12,8 @@ module Idris.Core.Elaborate(module Idris.Core.Elaborate,

1212 module Idris.Core.ProofState) where

1313

1414import Idris.Core.ProofState

15−import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term)

15+import Idris.Core.ProofTerm(bound_in, getProofTerm, mkProofTerm, bound_in_term,

16+ refocus)

1617import Idris.Core.TT

1718import Idris.Core.Evaluate

1819import Idris.Core.Typecheck

@@ -390,6 +391,13 @@ focus n = processTactic' (Focus n)

390391movelast :: Name -> Elab' aux ()

391392movelast n = processTactic' (MoveLast n)

392393

394+-- | Set the zipper in the proof state to point at the current sub term

395+-- (This currently happens automatically, so this will have no effect...)

396+zipHere :: Elab' aux ()

397+zipHere = do ES (ps, a) s m <- get

398+ let pt' = refocus (Just (head (holes ps))) (pterm ps)

399+ put (ES (ps { pterm = pt' }, a) s m)

400+

393401matchProblems :: Bool -> Elab' aux ()

394402matchProblems all = processTactic' (MatchProblems all)

395403

@@ -628,6 +636,7 @@ simple_app fun arg appstr =

628636arg :: Name -> Name -> Elab' aux ()

629637arg n tyhole = do ty <- unique_hole tyhole

630638 claim ty RType

639+ movelast ty

631640 forall n (Var ty)

632641

633642-- try a tactic, if it adds any unification problem, return an error

src/Idris/Core/ProofState.hs+5−3

@@ -216,9 +216,11 @@ unify' ctxt env topx topy =

216216-- ++ show (pterm ps)

217217 ++ "\n----------") $

218218 do let (h, ns) = unified ps

219+ -- solve in results (maybe unify should do this itself...)

220+ let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u

219221 -- if a metavar has multiple solutions, make a new unification

220222 -- problem for each.

221− uns <- mergeSolutions env (u ++ ns)

223+ uns <- mergeSolutions env (u' ++ ns)

222224 ps <- get

223225 let (ns', probs') = updateProblems (context ps) uns

224226 (fails ++ problems ps)

@@ -550,7 +552,7 @@ forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

550552forall n ty ctxt env _ = fail "Can't pi bind here"

551553

552554patvar :: Name -> RunTactic

553−patvar n ctxt env (Bind x (Hole t) sc) =

555+patvar n ctxt env (Bind x (Hole t) sc) =

554556 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $

555557 holes ps \\ [x],

556558 solved = Just (x, P Bound n t),

@@ -900,7 +902,7 @@ processTactic t ps

900902 = case solved ps' of

901903 Just s -> traceWhen (unifylog ps')

902904 ("SOLVED " ++ show s) $

903− updateProblems (context ps')

905+ updateProblems (context ps')

904906 [s] (problems ps')

905907 (injective ps')

906908 (holes ps')

src/Idris/Core/ProofTerm.hs+147−11

@@ -6,7 +6,7 @@

77module Idris.Core.ProofTerm(ProofTerm, Goal(..), mkProofTerm, getProofTerm,

88 updateSolved, updateSolvedTerm,

9− bound_in, bound_in_term,

9+ bound_in, bound_in_term, refocus,

1010 Hole, RunTactic',

1111 goal, atHole) where

1212

@@ -18,20 +18,101 @@ import Control.Monad.State.Strict

1818import Data.List

1919import Debug.Trace

2020

21−newtype ProofTerm = PT Term

21+data TermPath = Top

22+ | AppL TermPath Term

23+ | AppR Term TermPath

24+ | InBind Name BinderPath Term

25+ | InScope Name (Binder Term) TermPath

26+ deriving Show

27+

28+data BinderPath = Binder (Binder TermPath)

29+ | LetT TermPath Term

30+ | LetV Term TermPath

31+ | GuessT TermPath Term

32+ | GuessV Term TermPath

33+ deriving Show

34+

35+replaceTop :: TermPath -> TermPath -> TermPath

36+replaceTop p Top = p

37+replaceTop p (AppL l t) = AppL (replaceTop p l) t

38+replaceTop p (AppR t r) = AppR t (replaceTop p r)

39+replaceTop p (InBind n bp sc) = InBind n (replaceTopB p bp) sc

40+ where

41+ replaceTopB p (Binder b) = Binder (fmap (replaceTop p) b)

42+ replaceTopB p (LetT t v) = LetT (replaceTop p t) v

43+ replaceTopB p (LetV t v) = LetV t (replaceTop p v)

44+ replaceTopB p (GuessT t v) = GuessT (replaceTop p t) v

45+ replaceTopB p (GuessV t v) = GuessV t (replaceTop p v)

46+replaceTop p (InScope n b sc) = InScope n b (replaceTop p sc)

47+

48+rebuildTerm :: Term -> TermPath -> Term

49+rebuildTerm tm Top = tm

50+rebuildTerm tm (AppL p a) = App (rebuildTerm tm p) a

51+rebuildTerm tm (AppR f p) = App f (rebuildTerm tm p)

52+rebuildTerm tm (InScope n b p) = Bind n b (rebuildTerm tm p)

53+rebuildTerm tm (InBind n bp sc) = Bind n (rebuildBinder tm bp) sc

54+

55+rebuildBinder :: Term -> BinderPath -> Binder Term

56+rebuildBinder tm (Binder p) = fmap (rebuildTerm tm) p

57+rebuildBinder tm (LetT p t) = Let (rebuildTerm tm p) t

58+rebuildBinder tm (LetV v p) = Let v (rebuildTerm tm p)

59+rebuildBinder tm (GuessT p t) = Guess (rebuildTerm tm p) t

60+rebuildBinder tm (GuessV v p) = Guess v (rebuildTerm tm p)

61+

62+findHole :: Name -> Env -> Term -> Maybe (TermPath, Env, Term)

63+findHole n env t = fh' env Top t where

64+ fh' env path tm@(Bind x h sc)

65+ | hole h && n == x = Just (path, env, tm)

66+ fh' env path (App f a)

67+ | Just (p, env', tm) <- fh' env path a = Just (AppR f p, env', tm)

68+ | Just (p, env', tm) <- fh' env path f = Just (AppL p a, env', tm)

69+ fh' env path (Bind x b sc)

70+ | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)

71+ | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)

72+ fh' _ _ _ = Nothing

73+

74+ fhB env path (Let t v)

75+ | Just (p, env', tm) <- fh' env path t = Just (LetT p v, env', tm)

76+ | Just (p, env', tm) <- fh' env path v = Just (LetV t p, env', tm)

77+ fhB env path (Guess t v)

78+ | Just (p, env', tm) <- fh' env path t = Just (GuessT p v, env', tm)

79+ | Just (p, env', tm) <- fh' env path v = Just (GuessV t p, env', tm)

80+ fhB env path b

81+ | Just (p, env', tm) <- fh' env path (binderTy b)

82+ = Just (Binder (fmap (\_ -> p) b), env', tm)

83+ fhB _ _ _ = Nothing

84+

85+data ProofTerm = PT { -- wholeterm :: Term,

86+ path :: TermPath,

87+ subterm_env :: Env,

88+ subterm :: Term,

89+ updates :: [(Name, Term)] }

90+ deriving Show

2291

2392type RunTactic' a = Context -> Env -> Term -> StateT a TC Term

2493type Hole = Maybe Name -- Nothing = default hole, first in list in proof state

2594

95+refocus :: Hole -> ProofTerm -> ProofTerm

96+refocus h t = let res = refocus' h t in res

97+-- trace ("OLD: " ++ show t ++ "\n" ++

98+-- "REFOCUSSED " ++ show h ++ ": " ++ show res) res

99+refocus' (Just n) pt@(PT path env tm ups)

100+ | Just (p', env', tm') <- findHole n env tm

101+ = PT (replaceTop p' path) env' tm' ups

102+ | Just (p', env', tm') <- findHole n [] (rebuildTerm tm (updateSolvedPath ups path))

103+ = PT p' env' tm' []

104+ | otherwise = pt

105+refocus' _ pt = pt

106+

26107data Goal = GD { premises :: Env,

27108 goalType :: Binder Term

28109 }

29110

30111mkProofTerm :: Term -> ProofTerm

31−mkProofTerm tm = PT tm

112+mkProofTerm tm = PT Top [] tm []

32113

33114getProofTerm :: ProofTerm -> Term

34−getProofTerm (PT tm) = tm

115+getProofTerm (PT path _ sub ups) = rebuildTerm sub (updateSolvedPath ups path)

35116

36117same Nothing n = True

37118same (Just x) n = x == n

@@ -41,7 +122,14 @@ hole (Guess _ _) = True

41122hole _ = False

42123

43124updateSolvedTerm :: [(Name, Term)] -> Term -> Term

44−updateSolvedTerm xs x = updateSolved' xs x where

125+updateSolvedTerm [] x = x

126+updateSolvedTerm xs x = -- updateSolved' xs x where

127+-- This version below saves allocations, because it doesn't need to reallocate

128+-- the term if there are no updates to do, but costs an extra pass. Below

129+-- version works better on larger terms...

130+ if noneOf (map fst xs) x

131+ then x

132+ else updateSolved' xs x where

45133 updateSolved' [] x = x

46134 updateSolved' xs (Bind n (Hole ty) t)

47135 | Just v <- lookup n xs

@@ -57,11 +145,53 @@ updateSolvedTerm xs x = updateSolved' xs x where

57145 | Just v <- lookup n xs = v

58146 updateSolved' xs t = t

59147

148+ noneOf ns (P _ n _) | n `elem` ns = False

149+ noneOf ns (App f a) = noneOf ns a && noneOf ns f

150+ noneOf ns (Bind n (Hole ty) t) = n `notElem` ns && noneOf ns ty && noneOf ns t

151+ noneOf ns (Bind n b t) = noneOf ns t && noneOfB ns b

152+ where

153+ noneOfB ns (Let t v) = noneOf ns t && noneOf ns v

154+ noneOfB ns (Guess t v) = noneOf ns t && noneOf ns v

155+ noneOfB ns b = noneOf ns (binderTy b)

156+ noneOf ns _ = True

157+

158+updateEnv [] e = e

159+updateEnv ns [] = []

160+updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

161+

162+updateSolvedPath [] t = t

163+updateSolvedPath ns Top = Top

164+updateSolvedPath ns (AppL p r) = AppL p (updateSolvedTerm ns r)

165+updateSolvedPath ns (AppR l p) = AppR (updateSolvedTerm ns l) p

166+updateSolvedPath ns (InBind n b sc)

167+ = InBind n (updateSolvedPathB b) (updateSolvedTerm ns sc)

168+ where

169+ updateSolvedPathB (Binder b) = Binder (fmap (updateSolvedPath ns) b)

170+ updateSolvedPathB (LetT p v) = LetT (updateSolvedPath ns p) (updateSolvedTerm ns v)

171+ updateSolvedPathB (LetV v p) = LetV (updateSolvedTerm ns v) (updateSolvedPath ns p)

172+ updateSolvedPathB (GuessT p v) = GuessT (updateSolvedPath ns p) (updateSolvedTerm ns v)

173+ updateSolvedPathB (GuessV v p) = GuessV (updateSolvedTerm ns v) (updateSolvedPath ns p)

174+updateSolvedPath ns (InScope n (Hole ty) t)

175+ | Just v <- lookup n ns = case ns of

176+ [_] -> updateSolvedPath [(n,v)] t

177+ _ -> updateSolvedPath ns $

178+ updateSolvedPath [(n,v)] t

179+updateSolvedPath ns (InScope n b sc)

180+ = InScope n (fmap (updateSolvedTerm ns) b) (updateSolvedPath ns sc)

181+

60182updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

61−updateSolved xs (PT x) = PT (updateSolvedTerm xs x)

183+updateSolved xs pt@(PT path env sub ups)

184+ = PT path -- (updateSolvedPath xs path)

185+ (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))

186+ (updateSolvedTerm xs sub)

187+ (ups ++ xs)

62188

63189goal :: Hole -> ProofTerm -> TC Goal

64−goal h (PT tm) = g [] tm where

190+goal h pt@(PT path env sub ups)

191+-- | OK ginf <- g env sub = return ginf

192+ | otherwise = g [] (rebuildTerm sub (updateSolvedPath ups path))

193+ where

194+ g :: Env -> Term -> TC Goal

65195 g env (Bind n b@(Guess _ _) sc)

66196 | same h n = return $ GD env b

67197 | otherwise

@@ -69,7 +199,7 @@ goal h (PT tm) = g [] tm where

69199 g env (Bind n b sc) | hole b && same h n = return $ GD env b

70200 | otherwise

71201 = g ((n, b):env) sc `mplus` gb env b

72− g env (App f a) = g env f `mplus` g env a

202+ g env (App f a) = g env a `mplus` g env f

73203 g env t = fail "Can't find hole"

74204

75205 gb env (Let t v) = g env v `mplus` g env t

@@ -78,8 +208,14 @@ goal h (PT tm) = g [] tm where

78208

79209atHole :: Hole -> RunTactic' a -> Context -> Env -> ProofTerm ->

80210 StateT a TC (ProofTerm, Bool)

81−atHole h f c e (PT t) = do (tm, u) <- atH f c e t

82− return (PT tm, u)

211+atHole h f c e pt -- @(PT path env sub)

212+ = do let PT path env sub ups = refocus h pt

213+ (tm, u) <- atH f c env sub

214+ return (PT path env tm ups, u)

215+-- if u then return (PT path env tm ups, u)

216+-- else do let PT path env sub ups = refocus h pt

217+-- (tm, u) <- atH f c env sub

218+-- return (PT path env tm ups, u)

83219 where

84220 updated o = do o' <- o

85221 return (o', True)

@@ -117,7 +253,7 @@ atHole h f c e (PT t) = do (tm, u) <- atH f c e t

117253 return (t { binderTy = ty' }, u)

118254

119255bound_in :: ProofTerm -> [Name]

120−bound_in (PT tm) = bound_in_term tm

256+bound_in (PT path _ tm ups) = bound_in_term (rebuildTerm tm (updateSolvedPath ups path))

121257

122258bound_in_term :: Term -> [Name]

123259bound_in_term (Bind n b sc) = n : bi b ++ bound_in_term sc

src/Idris/Core/Unify.hs+9

@@ -333,6 +333,15 @@ unify ctxt env topx topy inj holes usersupp from =

333333 = unifyTmpFail tx ty

334334 | injective ty && not (holeIn env x || x `elem` holes)

335335 = unifyTmpFail tx ty

336+ -- pick the one bound earliest if both are holes

337+ | tx /= ty && (holeIn env x || x `elem` holes)

338+ && (holeIn env y || y `elem` holes)

339+ = case compare (envPos 0 x env) (envPos 0 y env) of

340+ LT -> do sc 1; checkCycle bnames (x, ty)

341+ _ -> do sc 1; checkCycle bnames (y, tx)

342+ where envPos i n ((n',_):env) | n == n' = i

343+ envPos i n (_:env) = envPos (i+1) n env

344+ envPos _ _ _ = 100000

336345 un' fn bnames xtm@(P _ x _) tm

337346 | pureTerm tm, holeIn env x || x `elem` holes

338347 = do UI s f <- get

src/Idris/ElabTerm.hs+3−2

@@ -17,6 +17,7 @@ import Idris.Core.Unify

1717import Idris.Core.Typecheck (check, recheck)

1818import Idris.ErrReverse (errReverse)

1919import Idris.ElabQuasiquote (extractUnquotes)

20+import qualified Util.Pretty as U

2021

2122import Control.Applicative ((<$>))

2223import Control.Monad

@@ -144,6 +145,7 @@ elab ist info emode opts fn tm

144145 compute -- expand type synonyms, etc

145146 elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)

146147 end_unify

148+ ptm <- get_term

147149 when pattern -- convert remaining holes to pattern vars

148150 (do update_term orderPats

149151 unify_all

@@ -690,7 +692,6 @@ elab ist info emode opts fn tm

690692 (caseBlock fc cname'

691693 (map (isScr scr) (reverse args)) opts)

692694 -- elaborate case

693− env <- get_env

694695 updateAux (newdef : )

695696 -- if we haven't got the type yet, hopefully we'll get it later!

696697 movelast tyn

@@ -905,7 +906,7 @@ elab ist info emode opts fn tm

905906 elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)

906907 = elabArgs ist ina failed fc r f ns force args

907908 elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)

908− = do elabArg argName holeName t

909+ = elabArg argName holeName t

909910 where elabArg argName holeName t =

910911 do now_elaborating fc f argName

911912 wrapErr f argName $ do

src/Idris/Error.hs+2−3

@@ -42,12 +42,11 @@ idrisCatch = catchError

4242

4343setAndReport :: Err -> Idris ()

4444setAndReport e = do ist <- getIState

45− let h = idris_outh ist

4645 case (unwrap e) of

4746 At fc e -> do setErrSpan fc

48− ihWarn h fc $ pprintErr ist e

47+ iWarn fc $ pprintErr ist e

4948 _ -> do setErrSpan (getErrSpan e)

50− ihWarn h emptyFC $ pprintErr ist e

49+ iWarn emptyFC $ pprintErr ist e

5150 where unwrap (ProofSearchFail e) = e -- remove bookkeeping constructor

5251 unwrap e = e

5352

src/Idris/IdeSlave.hs+20−10

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

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

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

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

55import Text.Printf

66import Numeric

@@ -12,12 +12,24 @@ import qualified Data.ByteString.UTF8 as UTF8

1212-- import qualified Data.Text as T

1313import Text.Trifecta hiding (Err)

1414import Text.Trifecta.Delta

15+import System.IO

1516

1617import Idris.Core.TT

1718import Idris.Core.Binary

1819

1920import Control.Applicative hiding (Const)

2021

22+getNChar :: Handle -> Int -> String -> IO (String)

23+getNChar _ 0 s = return (reverse s)

24+getNChar h n s = do c <- hGetChar h

25+ getNChar h (n - 1) (c : s)

26+

27+getLen :: Handle -> IO (Either Err Int)

28+getLen h = do s <- getNChar h 6 ""

29+ case readHex s of

30+ ((num, ""):_) -> return $ Right num

31+ _ -> return $ Left . Msg $ "Couldn't read length " ++ s

32+

2133data SExp = SexpList [SExp]

2234 | StringAtom String

2335 | BoolAtom Bool

@@ -247,19 +259,14 @@ sexpToCommand _

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

248260parseMessage x = case receiveString x of

249261 Right (SexpList [cmd, (IntegerAtom id)]) -> Right (cmd, id)

262+ Right x -> Left . Msg $ "Invalid message " ++ show x

250263 Left err -> Left err

251264

252265receiveString :: String -> Either Err SExp

253266receiveString x =

254− case readHex (take 6 x) of

255− ((num, ""):_) ->

256− let msg = drop 6 x in

257− if (length msg) /= (num - 1)

258− then Left . Msg $ "bad input length"

259− else (case parseSExp msg of

260− Failure _ -> Left . Msg $ "parse failure"

261− Success r -> Right r)

262− _ -> Left . Msg $ "readHex failed"

267+ case parseSExp x of

268+ Failure _ -> Left . Msg $ "parse failure"

269+ Success r -> Right r

263270

264271convSExp :: SExpable a => String -> a -> Integer -> String

265272convSExp pre s id =

@@ -269,3 +276,6 @@ convSExp pre s id =

269276

270277getHexLength :: String -> String

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

279+

280+ideSlaveEpoch :: Int

281+ideSlaveEpoch = 1

src/Idris/Interactive.hs+32−28

@@ -28,11 +28,12 @@ import System.Directory

2828import System.IO

2929import Data.Char

3030import Data.Maybe (fromMaybe)

31+import Data.List (isSuffixOf)

3132

3233import Debug.Trace

3334

34−caseSplitAt :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

35−caseSplitAt h fn updatefile l n

35+caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

36+caseSplitAt fn updatefile l n

3637 = do src <- runIO $ readFile fn

3738 res <- splitOnLine l n fn

3839 iLOG (showSep "\n" (map show res))

@@ -43,11 +44,11 @@ caseSplitAt h fn updatefile l n

4344 then do let fb = fn ++ "~" -- make a backup!

4445 runIO $ writeFile fb (unlines before ++ new ++ unlines later)

4546 runIO $ copyFile fb fn

46− else -- do ihputStrLn h (show res)

47− ihPrintResult h new

47+ else -- do iputStrLn (show res)

48+ iPrintResult new

4849

49−addClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

50−addClauseFrom h fn updatefile l n

50+addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

51+addClauseFrom fn updatefile l n

5152 = do src <- runIO $ readFile fn

5253 let (before, tyline : later) = splitAt (l-1) (lines src)

5354 let indent = getIndent 0 (show n) tyline

@@ -61,15 +62,15 @@ addClauseFrom h fn updatefile l n

6162 cl ++ "\n" ++

6263 unlines rest)

6364 runIO $ copyFile fb fn

64− else ihPrintResult h cl

65+ else iPrintResult cl

6566 where

6667 getIndent i n [] = 0

6768 getIndent i n xs | take 9 xs == "instance " = i

6869 getIndent i n xs | take (length n) xs == n = i

6970 getIndent i n (x : xs) = getIndent (i + 1) n xs

7071

71−addProofClauseFrom :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

72−addProofClauseFrom h fn updatefile l n

72+addProofClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

73+addProofClauseFrom fn updatefile l n

7374 = do src <- runIO $ readFile fn

7475 let (before, tyline : later) = splitAt (l-1) (lines src)

7576 let indent = getIndent 0 (show n) tyline

@@ -83,14 +84,14 @@ addProofClauseFrom h fn updatefile l n

8384 cl ++ "\n" ++

8485 unlines rest)

8586 runIO $ copyFile fb fn

86− else ihPrintResult h cl

87+ else iPrintResult cl

8788 where

8889 getIndent i n [] = 0

8990 getIndent i n xs | take (length n) xs == n = i

9091 getIndent i n (x : xs) = getIndent (i + 1) n xs

9192

92−addMissing :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

93−addMissing h fn updatefile l n

93+addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

94+addMissing fn updatefile l n

9495 = do src <- runIO $ readFile fn

9596 let (before, tyline : later) = splitAt (l-1) (lines src)

9697 let indent = getIndent 0 (show n) tyline

@@ -108,7 +109,7 @@ addMissing h fn updatefile l n

108109 runIO $ writeFile fb (unlines (before ++ nonblank)

109110 ++ extras ++ unlines rest)

110111 runIO $ copyFile fb fn

111− else ihPrintResult h extras

112+ else iPrintResult extras

112113 where showPat = show . stripNS

113114 stripNS tm = mapPT dens tm where

114115 dens (PRef fc n) = PRef fc (nsroot n)

@@ -122,10 +123,13 @@ addMissing h fn updatefile l n

122123 getAppName (PRef _ r) = r

123124 getAppName _ = n

124125

126+ makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '

127+ | otherwise = replicate ind ' '

128+

125129 showNew nm i ind (tm : tms)

126130 = do (nm', i') <- getUniq nm i

127131 rest <- showNew nm i' ind tms

128− return (replicate ind ' ' ++

132+ return (makeIndent ind ++

129133 showPat tm ++ " = ?" ++ nm' ++

130134 "\n" ++ rest)

131135 showNew nm i _ [] = return ""

@@ -135,8 +139,8 @@ addMissing h fn updatefile l n

135139 getIndent i n (x : xs) = getIndent (i + 1) n xs

136140

137141

138−makeWith :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

139−makeWith h fn updatefile l n

142+makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

143+makeWith fn updatefile l n

140144 = do src <- runIO $ readFile fn

141145 let (before, tyline : later) = splitAt (l-1) (lines src)

142146 let ind = getIndent tyline

@@ -151,15 +155,15 @@ makeWith h fn updatefile l n

151155 ++ with ++ "\n" ++

152156 unlines rest)

153157 runIO $ copyFile fb fn

154− else ihPrintResult h with

158+ else iPrintResult with

155159 where getIndent s = length (takeWhile isSpace s)

156160

157161

158−doProofSearch :: Handle -> FilePath -> Bool -> Bool ->

162+doProofSearch :: FilePath -> Bool -> Bool ->

159163 Int -> Name -> [Name] -> Maybe Int -> Idris ()

160−doProofSearch h fn updatefile rec l n hints Nothing

161− = doProofSearch h fn updatefile rec l n hints (Just 10)

162−doProofSearch h fn updatefile rec l n hints (Just depth)

164+doProofSearch fn updatefile rec l n hints Nothing

165+ = doProofSearch fn updatefile rec l n hints (Just 10)

166+doProofSearch fn updatefile rec l n hints (Just depth)

163167 = do src <- runIO $ readFile fn

164168 let (before, tyline : later) = splitAt (l-1) (lines src)

165169 ctxt <- getContext

@@ -192,7 +196,7 @@ doProofSearch h fn updatefile rec l n hints (Just depth)

192196 updateMeta False tyline (show n) newmv ++ "\n"

193197 ++ unlines later)

194198 runIO $ copyFile fb fn

195− else ihPrintResult h newmv

199+ else iPrintResult newmv

196200 where dropCtxt 0 sc = sc

197201 dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

198202 dropCtxt i (PLet _ _ _ sc) = dropCtxt (i - 1) sc

@@ -235,8 +239,8 @@ addBracket True new | any isSpace new = '(' : new ++ ")"

235239 | otherwise = new

236240

237241

238−makeLemma :: Handle -> FilePath -> Bool -> Int -> Name -> Idris ()

239−makeLemma h fn updatefile l n

242+makeLemma :: FilePath -> Bool -> Int -> Name -> Idris ()

243+makeLemma fn updatefile l n

240244 = do src <- runIO $ readFile fn

241245 let (before, tyline : later) = splitAt (l-1) (lines src)

242246

@@ -266,8 +270,8 @@ makeLemma h fn updatefile l n

266270 runIO $ writeFile fb (addLem before tyline lem lem_app later)

267271 runIO $ copyFile fb fn

268272 else case idris_outputmode i of

269− RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app

270− IdeSlave n ->

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

274+ IdeSlave n h ->

271275 let good = SexpList [SymbolAtom "ok",

272276 SexpList [SymbolAtom "metavariable-lemma",

273277 SexpList [SymbolAtom "replace-metavariable",

@@ -284,8 +288,8 @@ makeLemma h fn updatefile l n

284288 runIO $ writeFile fb (addProv before tyline lem_app later)

285289 runIO $ copyFile fb fn

286290 else case idris_outputmode i of

287− RawOutput -> ihPrintResult h $ lem_app

288− IdeSlave n ->

291+ RawOutput _ -> iPrintResult $ lem_app

292+ IdeSlave n h ->

289293 let good = SexpList [SymbolAtom "ok",

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

291295 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+60−63

@@ -24,27 +24,28 @@ pshow ist err = displayDecorated (consoleDecorate ist) .

2424 renderPretty 1.0 80 .

2525 fmap (fancifyAnnots ist) $ pprintErr ist err

2626

27−ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

28−ihWarn h fc err = do i <- getIState

29− case idris_outputmode i of

30− RawOutput ->

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

32− if fc_fname fc /= ""

33− then text (show fc) <> colon <//> err

34− else err

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

36− IdeSlave n ->

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

38− let (str, spans) = displaySpans err'

39− runIO . hPutStrLn h $

40− convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

27+iWarn :: FC -> Doc OutputAnnotation -> Idris ()

28+iWarn fc err =

29+ do i <- getIState

30+ case idris_outputmode i of

31+ RawOutput h ->

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

33+ if fc_fname fc /= ""

34+ then text (show fc) <> colon <//> err

35+ else err

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

37+ IdeSlave n h ->

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

39+ let (str, spans) = displaySpans err'

40+ runIO . hPutStrLn h $

41+ convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

4142

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

4344iRender d = do w <- getWidth

4445 ist <- getIState

4546 let ideSlave = case idris_outputmode ist of

46− IdeSlave _ -> True

47− _ -> False

47+ IdeSlave _ _ -> True

48+ _ -> False

4849 case w of

4950 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

5051 ColsWide n -> return $

@@ -63,37 +64,37 @@ consoleDisplayAnnotated h output = do ist <- getIState

6364 displayDecorated (consoleDecorate ist) $

6465 rendered

6566

66−ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

67−ihPrintTermWithType h tm ty = ihRenderResult h (tm <+> colon <+> align ty)

67+iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

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

6869

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

70−ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

71−ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

72−ihPrintFunTypes h bnd n overloads = do ist <- getIState

73− let ppo = ppOptionIst ist

74− let infixes = idris_infixes ist

75− let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

76− ihRenderResult h output

71+iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

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

73+iPrintFunTypes bnd n overloads = do ist <- getIState

74+ let ppo = ppOptionIst ist

75+ let infixes = idris_infixes ist

76+ let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

77+ iRenderResult output

7778 where fullName n = prettyName True True bnd n

7879 ppOverload ppo infixes n tm =

7980 fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

8081

81−ihRenderOutput :: Handle -> Doc OutputAnnotation -> Idris ()

82−ihRenderOutput h doc =

82+iRenderOutput :: Doc OutputAnnotation -> Idris ()

83+iRenderOutput doc =

8384 do i <- getIState

8485 case idris_outputmode i of

85− RawOutput -> do out <- iRender doc

86− runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

87− IdeSlave n ->

86+ RawOutput h -> do out <- iRender doc

87+ runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

88+ IdeSlave n h ->

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

8990 let out = [toSExp str, toSExp spans]

90− runIO . putStrLn $ convSExp "write-decorated" out n

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

9192

92−ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

93−ihRenderResult h d = do ist <- getIState

94− case idris_outputmode ist of

95− RawOutput -> consoleDisplayAnnotated h d

96− IdeSlave n -> ideSlaveReturnAnnotated n h d

93+iRenderResult :: Doc OutputAnnotation -> Idris ()

94+iRenderResult d = do ist <- getIState

95+ case idris_outputmode ist of

96+ RawOutput h -> consoleDisplayAnnotated h d

97+ IdeSlave n h -> ideSlaveReturnAnnotated n h d

9798

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

99100ideSlaveReturnWithStatus status n h out = do

@@ -111,56 +112,52 @@ ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

111112ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

112113

113114-- | Show an error with semantic highlighting

114−ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

115−ihRenderError h e = do ist <- getIState

116− case idris_outputmode ist of

117− RawOutput -> consoleDisplayAnnotated h e

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

119−

120−ihPrintWithStatus :: String -> Handle -> String -> Idris ()

121−ihPrintWithStatus status h s = do

115+iRenderError :: Doc OutputAnnotation -> Idris ()

116+iRenderError e = do ist <- getIState

117+ case idris_outputmode ist of

118+ RawOutput h -> consoleDisplayAnnotated h e

119+ IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e

120+

121+iPrintWithStatus :: String -> String -> Idris ()

122+iPrintWithStatus status s = do

122123 i <- getIState

123124 case idris_outputmode i of

124− RawOutput -> case s of

125+ RawOutput h -> case s of

125126 "" -> return ()

126127 s -> runIO $ hPutStrLn h s

127− IdeSlave n ->

128+ IdeSlave n h ->

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

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

130131

131132

132−ihPrintResult :: Handle -> String -> Idris ()

133−ihPrintResult = ihPrintWithStatus "ok"

133+iPrintResult :: String -> Idris ()

134+iPrintResult = iPrintWithStatus "ok"

134135

135−ihPrintError :: Handle -> String -> Idris ()

136−ihPrintError = ihPrintWithStatus "error"

136+iPrintError :: String -> Idris ()

137+iPrintError = iPrintWithStatus "error"

137138

138−ihputStrLn :: Handle -> String -> Idris ()

139−ihputStrLn h s = do i <- getIState

140− case idris_outputmode i of

141− RawOutput -> runIO $ hPutStrLn h s

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

139+iputStrLn :: String -> Idris ()

140+iputStrLn s = do i <- getIState

141+ case idris_outputmode i of

142+ RawOutput h -> runIO $ hPutStrLn h s

143+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

143144

144−iputStrLn = ihputStrLn stdout

145−iPrintError = ihPrintError stdout

146−iPrintResult = ihPrintResult stdout

147−iWarn = ihWarn stdout

148145

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

150147ideslavePutSExp cmd info = do i <- getIState

151148 case idris_outputmode i of

152− IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

149+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n

153150 _ -> return ()

154151

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

156153iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

157154iputGoal g = do i <- getIState

158155 case idris_outputmode i of

159− RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

160− IdeSlave n ->

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

157+ IdeSlave n h ->

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

162159 goal = [toSExp str, toSExp spans]

163− in runIO . putStrLn $ convSExp "write-goal" goal n

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

164161

165162-- | Warn about totality problems without failing to compile

166163warnTotality :: Idris ()

src/Idris/ParseHelpers.hs+2−2

@@ -17,7 +17,7 @@ import Idris.Core.TT

1717import Idris.Core.Evaluate

1818import Idris.Delaborate (pprintErr)

1919import Idris.Docstrings

20−import Idris.Output (ihWarn)

20+import Idris.Output (iWarn)

2121

2222import qualified Util.Pretty as Pretty (text)

2323

@@ -79,7 +79,7 @@ clearParserWarnings = do ist <- getIState

7979

8080reportParserWarnings :: Idris ()

8181reportParserWarnings = do ist <- getIState

82− mapM_ (uncurry $ ihWarn (idris_outh ist))

82+ mapM_ (uncurry iWarn)

8383 (map (\ (fc, err) -> (fc, pprintErr ist err)) .

8484 reverse .

8585 nub $

src/Idris/Parser.hs+24−24

@@ -1159,8 +1159,8 @@ parseProg syn fname input mrk

11591159 let (fc, msg) = findFC doc

11601160 i <- getIState

11611161 case idris_outputmode i of

1162− RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)

1163− IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

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

1163+ IdeSlave n h -> iWarn fc (P.text msg)

11641164 putIState (i { errSpan = Just fc })

11651165 return []

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

@@ -1176,17 +1176,17 @@ parseProg syn fname input mrk

11761176 return (ds, i')

11771177

11781178{- | Load idris module and show error if something wrong happens -}

1179−loadModule :: Handle -> FilePath -> Idris String

1180−loadModule outh f

1181− = idrisCatch (loadModule' outh f)

1179+loadModule :: FilePath -> Idris String

1180+loadModule f

1181+ = idrisCatch (loadModule' f)

11821182 (\e -> do setErrSpan (getErrSpan e)

11831183 ist <- getIState

1184− ihWarn outh (getErrSpan e) $ pprintErr ist e

1184+ iWarn (getErrSpan e) $ pprintErr ist e

11851185 return "")

11861186

11871187{- | Load idris module -}

1188−loadModule' :: Handle -> FilePath -> Idris String

1189−loadModule' outh f

1188+loadModule' :: FilePath -> Idris String

1189+loadModule' f

11901190 = do i <- getIState

11911191 let file = takeWhile (/= ' ') f

11921192 ibcsd <- valIBCSubDir i

@@ -1196,21 +1196,21 @@ loadModule' outh f

11961196 then iLOG $ "Already read " ++ file

11971197 else do putIState (i { imported = file : imported i })

11981198 case fp of

1199− IDR fn -> loadSource outh False fn Nothing

1200− LIDR fn -> loadSource outh True fn Nothing

1199+ IDR fn -> loadSource False fn Nothing

1200+ LIDR fn -> loadSource True fn Nothing

12011201 IBC fn src ->

12021202 idrisCatch (loadIBC fn)

12031203 (\c -> do iLOG $ fn ++ " failed " ++ pshow i c

12041204 case src of

1205− IDR sfn -> loadSource outh False sfn Nothing

1206− LIDR sfn -> loadSource outh True sfn Nothing)

1205+ IDR sfn -> loadSource False sfn Nothing

1206+ LIDR sfn -> loadSource True sfn Nothing)

12071207 let (dir, fh) = splitFileName file

12081208 return (dropExtension fh)

12091209

12101210

12111211{- | Load idris code from file -}

1212−loadFromIFile :: Handle -> IFileType -> Maybe Int -> Idris ()

1213−loadFromIFile h i@(IBC fn src) maxline

1212+loadFromIFile :: IFileType -> Maybe Int -> Idris ()

1213+loadFromIFile i@(IBC fn src) maxline

12141214 = do iLOG $ "Skipping " ++ getSrcFile i

12151215 idrisCatch (loadIBC fn)

12161216 (\err -> ierror $ LoadingFailed fn err)

@@ -1219,22 +1219,22 @@ loadFromIFile h i@(IBC fn src) maxline

12191219 getSrcFile (LIDR fn) = fn

12201220 getSrcFile (IBC f src) = getSrcFile src

12211221

1222−loadFromIFile h (IDR fn) maxline = loadSource' h False fn maxline

1223−loadFromIFile h (LIDR fn) maxline = loadSource' h True fn maxline

1222+loadFromIFile (IDR fn) maxline = loadSource' False fn maxline

1223+loadFromIFile (LIDR fn) maxline = loadSource' True fn maxline

12241224

12251225{-| Load idris source code and show error if something wrong happens -}

1226−loadSource' :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()

1227−loadSource' h lidr r maxline

1228− = idrisCatch (loadSource h lidr r maxline)

1226+loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()

1227+loadSource' lidr r maxline

1228+ = idrisCatch (loadSource lidr r maxline)

12291229 (\e -> do setErrSpan (getErrSpan e)

12301230 ist <- getIState

12311231 case e of

1232− At f e' -> ihWarn h f (pprintErr ist e')

1233− _ -> ihWarn h (getErrSpan e) (pprintErr ist e))

1232+ At f e' -> iWarn f (pprintErr ist e')

1233+ _ -> iWarn (getErrSpan e) (pprintErr ist e))

12341234

12351235{- | Load Idris source code-}

1236−loadSource :: Handle -> Bool -> FilePath -> Maybe Int -> Idris ()

1237−loadSource h lidr f toline

1236+loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()

1237+loadSource lidr f toline

12381238 = do iLOG ("Reading " ++ f)

12391239 i <- getIState

12401240 let def_total = default_total i

@@ -1278,7 +1278,7 @@ loadSource h lidr f toline

12781278 logLvl 3 (show (idris_infixes i))

12791279 -- Now add all the declarations to the context

12801280 v <- verbose

1281− when v $ ihputStrLn h $ "Type checking " ++ f

1281+ when v $ iputStrLn $ "Type checking " ++ f

12821282 -- we totality check after every Mutual block, so if

12831283 -- anything is a single definition, wrap it in a

12841284 -- mutual block on its own

src/Idris/Prover.hs+51−45

@@ -19,12 +19,13 @@ import Idris.Parser hiding (params)

1919import Idris.Error

2020import Idris.DataOpts

2121import Idris.Completion

22−import Idris.IdeSlave

22+import qualified Idris.IdeSlave as IdeSlave

2323import Idris.Output

2424import Idris.TypeSearch (searchByType)

2525

2626import Text.Trifecta.Result(Result(..))

2727

28+import System.IO (Handle, stdin, stdout, hPutStrLn)

2829import System.Console.Haskeline

2930import System.Console.Haskeline.History

3031import Control.Monad.State.Strict

@@ -70,8 +71,8 @@ prove opt ctxt lit n ty

7071 iLOG $ "Adding " ++ show tm

7172 i <- getIState

7273 case idris_outputmode i of

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

74− _ -> iputStrLn $ showProof lit n prf

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

75+ _ -> iputStrLn $ showProof lit n prf

7576 let proofs = proof_list i

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

7778 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

@@ -93,9 +94,8 @@ prove opt ctxt lit n ty

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

9495 solveDeferred n

9596 case idris_outputmode i of

96− IdeSlave n ->

97− runIO . putStrLn $

98− convSExp "return" (SymbolAtom "ok", "") n

97+ IdeSlave n h ->

98+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n

9999 _ -> return ()

100100

101101elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

@@ -140,6 +140,8 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

140140 prettyPs bnd [] = empty

141141 prettyPs bnd ((n@(MN _ r), _) : bs)

142142 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

143+ prettyPs bnd ((n@(MN _ _), _) : bs)

144+ | not (n `elem` freeEnvNames bs) = prettyPs bnd bs

143145 prettyPs bnd ((n, Let t v) : bs) =

144146 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

145147 align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs

@@ -168,27 +170,35 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

168170 text "---------- Other goals: ----------" <$$>

169171 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)

170172

173+ freeEnvNames :: Env -> [Name]

174+ freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))

175+

171176lifte :: ElabState [PDecl] -> ElabD a -> Idris a

172177lifte st e = do (v, _) <- elabStep st e

173178 return v

174179

175−receiveInput :: ElabState [PDecl] -> Idris (Maybe String)

176−receiveInput e =

180+receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)

181+receiveInput h e =

177182 do i <- getIState

178− l <- runIO $ getLine

179− (sexp, id) <- case parseMessage l of

183+ let inh = if h == stdout then stdin else h

184+ len' <- runIO $ IdeSlave.getLen inh

185+ len <- case len' of

186+ Left err -> ierror err

187+ Right n -> return n

188+ l <- runIO $ IdeSlave.getNChar inh len ""

189+ (sexp, id) <- case IdeSlave.parseMessage l of

180190 Left err -> ierror err

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

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

183− case sexpToCommand sexp of

184− Just (REPLCompletions prefix) ->

192+ putIState $ i { idris_outputmode = (IdeSlave id h) }

193+ case IdeSlave.sexpToCommand sexp of

194+ Just (IdeSlave.REPLCompletions prefix) ->

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

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

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

187197 ideslavePutSExp "return" good

188− receiveInput e

189− Just (Interpret cmd) -> return (Just cmd)

190− Just (TypeOf str) -> return (Just (":t " ++ str))

191− Just (DocsFor str) -> return (Just (":doc " ++ str))

198+ receiveInput h e

199+ Just (IdeSlave.Interpret cmd) -> return (Just cmd)

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

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

192202 _ -> return Nothing

193203

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

@@ -198,17 +208,18 @@ ploop fn d prompt prf e h

198208 when d $ dumpState i (proof e)

199209 (x, h') <-

200210 case idris_outputmode i of

201− RawOutput -> runInputT (proverSettings e) $

202− -- Manually track the history so that we can use the proof state

203− do _ <- case h of

204− Just history -> putHistory history

205− Nothing -> return ()

206− l <- getInputLine (prompt ++ "> ")

207− h' <- getHistory

208− return (l, Just h')

209− IdeSlave n ->

211+ RawOutput _ ->

212+ runInputT (proverSettings e) $

213+ -- Manually track the history so that we can use the proof state

214+ do case h of

215+ Just history -> putHistory history

216+ Nothing -> return ()

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

218+ h' <- getHistory

219+ return (l, Just h')

220+ IdeSlave _ handle ->

210221 do isetPrompt prompt

211− i <- receiveInput e

222+ i <- receiveInput handle e

212223 return (i, h)

213224 (cmd, step) <- case x of

214225 Nothing -> do iPrintError ""; ifail "Abandoned"

@@ -240,7 +251,8 @@ ploop fn d prompt prf e h

240251 (\err -> return (False, e, False, prf, Left err))

241252 ideslavePutSExp "write-proof-state" (prf', length prf')

242253 case res of

243− Left err -> do iPrintError (pshow i err)

254+ Left err -> do ist <- getIState

255+ iRenderError $ pprintErr ist err

244256 ploop fn d prompt prf' st h'

245257 Right ok ->

246258 if done then do (tm, _) <- elabStep st get_term

@@ -253,8 +265,7 @@ ploop fn d prompt prf e h

253265 ist <- getIState

254266 imp <- impShow

255267 idrisCatch (do

256− let h = idris_outh ist

257− OK env = envAtFocus (proof e)

268+ let OK env = envAtFocus (proof e)

258269 ctxt' = envCtxt env ctxt

259270 bnd = map (\x -> (fst x, False)) env

260271 ist' = ist { tt_ctxt = ctxt' }

@@ -262,8 +273,8 @@ ploop fn d prompt prf e h

262273 -- Unlike the REPL, metavars have no special treatment, to

263274 -- make it easier to see how to prove with them.

264275 let action = case lookupNames n ctxt' of

265− [] -> ihPrintError h $ "No such variable " ++ show n

266− ts -> ihPrintFunTypes h bnd n (map (\n -> (n, delabTy ist' n)) ts)

276+ [] -> iPrintError $ "No such variable " ++ show n

277+ ts -> iPrintFunTypes bnd n (map (\n -> (n, delabTy ist' n)) ts)

267278 putIState ist

268279 return (False, e, False, prf, Right action))

269280 (\err -> do putIState ist ; ierror err)

@@ -278,14 +289,13 @@ ploop fn d prompt prf e h

278289 (tm, ty) <- elabVal recinfo ERHS t

279290 let ppo = ppOptionIst ist

280291 ty' = normaliseC ctxt [] ty

281− h = idris_outh ist

282292 infixes = idris_infixes ist

283293 action = case tm of

284294 TType _ ->

285− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

295+ iPrintTermWithType (prettyImp ppo PType) type1Doc

286296 _ -> let bnd = map (\x -> (fst x, False)) env in

287− ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

288− (pprintPTerm ppo bnd [] infixes (delab ist ty))

297+ iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))

298+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

289299 putIState ist

290300 return (False, e, False, prf, Right action))

291301 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -306,25 +316,21 @@ ploop fn d prompt prf e h

306316 infixes = idris_infixes ist

307317 tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

308318 tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

309− action = ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

319+ action = iPrintTermWithType tmDoc tyDoc

310320 putIState ist

311321 return (False, e, False, prf, Right action))

312322 (\err -> do putIState ist ; ierror err)

313323 docStr :: Either Name Const -> Idris (Bool, ElabState [PDecl], Bool, [String], Either Err (Idris ()))

314324 docStr (Left n) = do ist <- getIState

315− let h = idris_outh ist

316325 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

317326 [] -> return (False, e, False, prf,

318327 Left . Msg $ "No documentation for " ++ show n)

319328 ns -> do toShow <- mapM (showDoc ist) ns

320329 return (False, e, False, prf,

321− Right $ ihRenderResult h (vsep toShow)))

330+ Right $ iRenderResult (vsep toShow)))

322331 (\err -> do putIState ist ; ierror err)

323332 where showDoc ist (n, d) = do doc <- getDocs n

324333 return $ pprintDocs ist doc

325334 docStr (Right c) = do ist <- getIState

326− let h = idris_outh ist

327− return (False, e, False, prf, Right . ihRenderResult h $ pprintConstDocs ist c (constDocs c))

328− search t = do ist <- getIState

329− let h = idris_outh ist

330− return (False, e, False, prf, Right $ searchByType h t)

335+ return (False, e, False, prf, Right . iRenderResult $ pprintConstDocs ist c (constDocs c))

336+ search t = return (False, e, False, prf, Right $ searchByType t)

src/Idris/REPL.hs+266−237

@@ -42,7 +42,7 @@ import Idris.Elab.Value

4242import Version_idris (gitHash)

4343import Util.System

4444import Util.DynamicLinker

45−import Util.Net (listenOnLocalhost)

45+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

4646import Util.Pretty hiding ((</>))

4747

4848import Idris.Core.Evaluate

@@ -93,6 +93,8 @@ import Data.Word (Word)

9393import Data.Either (partitionEithers)

9494import Control.DeepSeq

9595

96+import Numeric ( readHex )

97+

9698import Debug.Trace

9799

98100-- | Run the REPL

@@ -151,7 +153,7 @@ startServer orig fn_in = do tid <- runIO $ forkOS serverLoop

151153 -- TODO: option for port number

152154 serverLoop = withSocketsDo $

153155 do sock <- listenOnLocalhost $ PortNumber 4294

154− loop fn orig sock

156+ loop fn orig { idris_colourRepl = False } sock

155157

156158 fn = case fn_in of

157159 (f:_) -> f

@@ -161,7 +163,10 @@ startServer orig fn_in = do tid <- runIO $ forkOS serverLoop

161163 = do (h,_,_) <- accept sock

162164 hSetEncoding h utf8

163165 cmd <- hGetLine h

164− (ist', fn) <- processNetCmd orig ist h fn cmd

166+ let isth = case idris_outputmode ist of

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

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

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

165170 hClose h

166171 loop fn ist' sock

167172

@@ -187,12 +192,18 @@ processNetCmd orig i h fn cmd

187192 setOutH h

188193 setQuiet True

189194 setVerbose False

190− mods <- loadInputs h [f] toline

195+ mods <- loadInputs [f] toline

191196 ist <- getIState

192197 return (ist, f)

193− processNet fn c = do process h fn c

198+ processNet fn c = do process fn c

194199 ist <- getIState

195200 return (ist, fn)

201+ setOutH :: Handle -> Idris ()

202+ setOutH h =

203+ do ist <- getIState

204+ putIState $ case idris_outputmode ist of

205+ RawOutput _ -> ist {idris_outputmode = RawOutput h}

206+ IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

196207

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

198209runClient :: String -> IO ()

@@ -208,55 +219,73 @@ runClient str = withSocketsDo $ do

208219 else do l <- hGetLine h

209220 hGetResp (acc ++ l ++ "\n") h

210221

222+initIdeslaveSocket :: IO Handle

223+initIdeslaveSocket = do

224+ (sock, port) <- listenOnLocalhostAnyPort

225+ putStrLn $ show port

226+ (h, _, _) <- accept sock

227+ hSetEncoding h utf8

228+ return h

229+

211230-- | Run the IdeSlave

212−ideslaveStart :: IState -> [FilePath] -> Idris ()

213−ideslaveStart orig mods

214− = do i <- getIState

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

232+ideslaveStart s orig mods

233+ = do h <- runIO $ if s then initIdeslaveSocket else return stdout

234+ setIdeSlave True h

235+ i <- getIState

215236 case idris_outputmode i of

216− IdeSlave n ->

217− when (mods /= []) (do isetPrompt (mkPrompt mods))

218− ideslave orig mods

219−

220−

221−ideslave :: IState -> [FilePath] -> Idris ()

222−ideslave orig mods

237+ IdeSlave n h ->

238+ do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n

239+ case mods of

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

241+ _ -> return ()

242+ ideslave h orig mods

243+

244+ideslave :: Handle -> IState -> [FilePath] -> Idris ()

245+ideslave h orig mods

223246 = do idrisCatch

224− (do l <- runIO $ getLine

247+ (do let inh = if h == stdout then stdin else h

248+ len' <- runIO $ IdeSlave.getLen inh

249+ len <- case len' of

250+ Left err -> ierror err

251+ Right n -> return n

252+ l <- runIO $ IdeSlave.getNChar inh len ""

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

226254 Left err -> ierror err

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

228256 i <- getIState

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

257+ putIState $ i { idris_outputmode = (IdeSlave id h) }

230258 idrisCatch -- to report correct id back!

231259 (do let fn = case mods of

232260 (f:_) -> f

233− _ -> ""

261+ _ -> ""

234262 case IdeSlave.sexpToCommand sexp of

235− Just cmd -> runIdeSlaveCommand id orig fn mods cmd

263+ Just cmd -> runIdeSlaveCommand h id orig fn mods cmd

236264 Nothing -> iPrintError "did not understand" )

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

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

239− ideslave orig mods

267+ ideslave h orig mods

240268

241269-- | Run IDESlave commands

242−runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client

270+runIdeSlaveCommand :: Handle -- ^^ The handle for communication

271+ -> Integer -- ^^ The continuation ID for the client

243272 -> IState -- ^^ The original IState

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

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

246275 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

247276 -> Idris ()

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

277+runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

249278 do c <- colourise

250279 i <- getIState

251280 case parseCmd i "(input)" cmd of

252− Failure err -> iPrintError $ show (fixColour c err)

281+ Failure err -> iPrintError $ show (fixColour False err)

253282 Success (Prove n') ->

254283 idrisCatch

255− (do process stdout fn (Prove n')

284+ (do process fn (Prove n')

256285 isetPrompt (mkPrompt mods)

257286 case idris_outputmode i of

258− IdeSlave n -> -- signal completion of proof to ide

259− runIO . hPutStrLn stdout $

287+ IdeSlave n h -> -- signal completion of proof to ide

288+ runIO . hPutStrLn h $

260289 IdeSlave.convSExp "return"

261290 (IdeSlave.SymbolAtom "ok", "")

262291 n

@@ -264,26 +293,26 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

264293 (\e -> do ist <- getIState

265294 isetPrompt (mkPrompt mods)

266295 case idris_outputmode i of

267− IdeSlave n ->

268− runIO . hPutStrLn stdout $

296+ IdeSlave n h ->

297+ runIO . hPutStrLn h $

269298 IdeSlave.convSExp "abandon-proof" "Abandoned" n

270299 _ -> return ()

271− ihRenderError stdout $ pprintErr ist e)

300+ iRenderError $ pprintErr ist e)

272301 Success cmd -> idrisCatch

273302 (ideslaveProcess fn cmd)

274− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

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

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

304+runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =

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

277306 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

278307 IdeSlave.toSExp (map replacement compls,

279308 reverse unused)]

280− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

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

309+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id

310+runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

282311 do i <- getIState

283312 clearErr

284313 putIState (orig { idris_options = idris_options i,

285− idris_outputmode = (IdeSlave id) })

286− loadInputs stdout [filename] toline

314+ idris_outputmode = (IdeSlave id h) })

315+ loadInputs [filename] toline

287316 isetPrompt (mkPrompt [filename])

288317 -- Report either success or failure

289318 i <- getIState

@@ -293,45 +322,45 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

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

294323 IdeSlave.toSExp fc])

295324 (idris_parsedSpan i)

296− in runIO . putStrLn $ IdeSlave.convSExp "return" msg id

325+ in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

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

298− ideslave orig [filename]

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

327+ ideslave h orig [filename]

328+runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =

300329 case splitName name of

301330 Left err -> iPrintError err

302− Right n -> process stdout "(ideslave)"

331+ Right n -> process "(ideslave)"

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

304333 where splitName :: String -> Either String Name

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

306335 [] -> Left ("Didn't understand name '" ++ s ++ "'")

307336 [n] -> Right $ sUN n

308337 (n:ns) -> Right $ sNS (sUN n) ns

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

338+runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =

310339 case parseConst orig name of

311− Success c -> process stdout "(ideslave)" (DocStr (Right c))

340+ Success c -> process "(ideslave)" (DocStr (Right c))

312341 Failure _ ->

313342 case splitName name of

314343 Left err -> iPrintError err

315− Right n -> process stdout "(ideslave)" (DocStr (Left n))

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

317− process stdout fn (CaseSplitAt False line (sUN name))

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

319− process stdout fn (AddClauseFrom False line (sUN name))

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

321− process stdout fn (AddProofClauseFrom False line (sUN name))

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

323− process stdout fn (AddMissing False line (sUN name))

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

325− process stdout fn (MakeWith False line (sUN name))

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

327− doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth

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

344+ Right n -> process "(ideslave)" (DocStr (Left n))

345+runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =

346+ process fn (CaseSplitAt False line (sUN name))

347+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =

348+ process fn (AddClauseFrom False line (sUN name))

349+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =

350+ process fn (AddProofClauseFrom False line (sUN name))

351+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =

352+ process fn (AddMissing False line (sUN name))

353+runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =

354+ process fn (MakeWith False line (sUN name))

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

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

357+runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =

329358 case splitName name of

330359 Left err -> iPrintError err

331− Right n -> process stdout fn (MakeLemma False line n)

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

333− process stdout fn (Apropos a)

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

360+ Right n -> process fn (MakeLemma False line n)

361+runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =

362+ process fn (Apropos a)

363+runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =

335364 do ist <- getIState

336365 let opts = idris_options ist

337366 let impshow = opt_showimp opts

@@ -339,16 +368,16 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

339368 let options = (IdeSlave.SymbolAtom "ok",

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

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

342− runIO . putStrLn $ IdeSlave.convSExp "return" options id

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

371+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id

372+runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

344373 do setImpShow b

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

346− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

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

375+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

376+runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

348377 do setErrContext b

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

350− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

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

379+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

380+runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

352381 do ist <- getIState

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

354383 let ppo = ppOptionIst ist

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

364393 (zip bnds hs),

365394 render ist bnd c pc))

366395 splitMvs

367− runIO . putStrLn $

396+ runIO . hPutStrLn h $

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

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

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

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

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

410439 (show n , out, spans)

411440

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

441+runIdeSlaveCommand h id orig fn mods (IdeSlave.WhoCalls n) =

413442 case splitName n of

414443 Left err -> iPrintError err

415444 Right n -> do calls <- whoCalls n

416445 ist <- getIState

417446 let msg = (IdeSlave.SymbolAtom "ok",

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

419− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

448+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

420449 where pn ist = displaySpans .

421450 renderPretty 0.9 1000 .

422451 fmap (fancifyAnnots ist) .

423452 prettyName True True []

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

453+runIdeSlaveCommand h id orig fn mods (IdeSlave.CallsWho n) =

425454 case splitName n of

426455 Left err -> iPrintError err

427456 Right n -> do calls <- callsWho n

428457 ist <- getIState

429458 let msg = (IdeSlave.SymbolAtom "ok",

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

431− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

460+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

432461 where pn ist = displaySpans .

433462 renderPretty 0.9 1000 .

434463 fmap (fancifyAnnots ist) .

435464 prettyName True True []

436465

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

466+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =

438467 do ctxt <- getContext

439468 ist <- getIState

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

@@ -448,15 +477,15 @@ runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

448477 displaySpans .

449478 renderPretty 0.9 80 .

450479 fmap (fancifyAnnots ist) $ ptm)

451− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

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

453− ideSlaveForceTermImplicits id bnd True tm

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

455− ideSlaveForceTermImplicits id bnd False tm

480+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

481+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

482+ ideSlaveForceTermImplicits h id bnd True tm

483+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

484+ ideSlaveForceTermImplicits h id bnd False tm

456485

457486-- | Show a term for IDESlave with the specified implicitness

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

459−ideSlaveForceTermImplicits id bnd impl tm =

487+ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

488+ideSlaveForceTermImplicits h id bnd impl tm =

460489 do ist <- getIState

461490 let expl = annotate (AnnTerm bnd tm)

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

@@ -466,7 +495,7 @@ ideSlaveForceTermImplicits id bnd impl tm =

466495 displaySpans .

467496 renderPretty 0.9 80 .

468497 fmap (fancifyAnnots ist) $ expl)

469− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

498+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

470499

471500splitName :: String -> Either String Name

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

@@ -475,70 +504,70 @@ splitName s = case reverse $ splitOn "." s of

475504 (n:ns) -> Right $ sNS (sUN n) ns

476505

477506ideslaveProcess :: FilePath -> Command -> Idris ()

478−ideslaveProcess fn Warranty = process stdout fn Warranty

479−ideslaveProcess fn Help = process stdout fn Help

480−ideslaveProcess fn (ChangeDirectory f) = do process stdout fn (ChangeDirectory f)

507+ideslaveProcess fn Warranty = process fn Warranty

508+ideslaveProcess fn Help = process fn Help

509+ideslaveProcess fn (ChangeDirectory f) = do process fn (ChangeDirectory f)

481510 iPrintResult "changed directory to"

482−ideslaveProcess fn (Eval t) = process stdout fn (Eval t)

483−ideslaveProcess fn (NewDefn decls) = do process stdout fn (NewDefn decls)

511+ideslaveProcess fn (Eval t) = process fn (Eval t)

512+ideslaveProcess fn (NewDefn decls) = do process fn (NewDefn decls)

484513 iPrintResult "defined"

485−ideslaveProcess fn (ExecVal t) = process stdout fn (ExecVal t)

486−ideslaveProcess fn (Check (PRef x n)) = process stdout fn (Check (PRef x n))

487−ideslaveProcess fn (Check t) = process stdout fn (Check t)

488−ideslaveProcess fn (DocStr n) = process stdout fn (DocStr n)

489−ideslaveProcess fn Universes = process stdout fn Universes

490−ideslaveProcess fn (Defn n) = do process stdout fn (Defn n)

514+ideslaveProcess fn (ExecVal t) = process fn (ExecVal t)

515+ideslaveProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

516+ideslaveProcess fn (Check t) = process fn (Check t)

517+ideslaveProcess fn (DocStr n) = process fn (DocStr n)

518+ideslaveProcess fn Universes = process fn Universes

519+ideslaveProcess fn (Defn n) = do process fn (Defn n)

491520 iPrintResult ""

492−ideslaveProcess fn (TotCheck n) = process stdout fn (TotCheck n)

493−ideslaveProcess fn (DebugInfo n) = do process stdout fn (DebugInfo n)

521+ideslaveProcess fn (TotCheck n) = process fn (TotCheck n)

522+ideslaveProcess fn (DebugInfo n) = do process fn (DebugInfo n)

494523 iPrintResult ""

495−ideslaveProcess fn (Search t) = process stdout fn (Search t)

496−ideslaveProcess fn (Spec t) = process stdout fn (Spec t)

524+ideslaveProcess fn (Search t) = process fn (Search t)

525+ideslaveProcess fn (Spec t) = process fn (Spec t)

497526-- RmProof and AddProof not supported!

498−ideslaveProcess fn (ShowProof n') = process stdout fn (ShowProof n')

499−ideslaveProcess fn (HNF t) = process stdout fn (HNF t)

500−--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!

501−ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)

527+ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')

528+ideslaveProcess fn (HNF t) = process fn (HNF t)

529+--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!

530+ideslaveProcess fn (TestInline t) = process fn (TestInline t)

502531

503−ideslaveProcess fn Execute = do process stdout fn Execute

532+ideslaveProcess fn Execute = do process fn Execute

504533 iPrintResult ""

505−ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)

534+ideslaveProcess fn (Compile codegen f) = do process fn (Compile codegen f)

506535 iPrintResult ""

507−ideslaveProcess fn (LogLvl i) = do process stdout fn (LogLvl i)

536+ideslaveProcess fn (LogLvl i) = do process fn (LogLvl i)

508537 iPrintResult ""

509−ideslaveProcess fn (Pattelab t) = process stdout fn (Pattelab t)

510−ideslaveProcess fn (Missing n) = process stdout fn (Missing n)

511−ideslaveProcess fn (DynamicLink l) = do process stdout fn (DynamicLink l)

538+ideslaveProcess fn (Pattelab t) = process fn (Pattelab t)

539+ideslaveProcess fn (Missing n) = process fn (Missing n)

540+ideslaveProcess fn (DynamicLink l) = do process fn (DynamicLink l)

512541 iPrintResult ""

513−ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic

542+ideslaveProcess fn ListDynamic = do process fn ListDynamic

514543 iPrintResult ""

515−ideslaveProcess fn Metavars = process stdout fn Metavars

516−ideslaveProcess fn (SetOpt ErrContext) = do process stdout fn (SetOpt ErrContext)

544+ideslaveProcess fn Metavars = process fn Metavars

545+ideslaveProcess fn (SetOpt ErrContext) = do process fn (SetOpt ErrContext)

517546 iPrintResult ""

518−ideslaveProcess fn (UnsetOpt ErrContext) = do process stdout fn (UnsetOpt ErrContext)

547+ideslaveProcess fn (UnsetOpt ErrContext) = do process fn (UnsetOpt ErrContext)

519548 iPrintResult ""

520−ideslaveProcess fn (SetOpt ShowImpl) = do process stdout fn (SetOpt ShowImpl)

549+ideslaveProcess fn (SetOpt ShowImpl) = do process fn (SetOpt ShowImpl)

521550 iPrintResult ""

522−ideslaveProcess fn (UnsetOpt ShowImpl) = do process stdout fn (UnsetOpt ShowImpl)

551+ideslaveProcess fn (UnsetOpt ShowImpl) = do process fn (UnsetOpt ShowImpl)

523552 iPrintResult ""

524−ideslaveProcess fn (SetOpt ShowOrigErr) = do process stdout fn (SetOpt ShowOrigErr)

553+ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)

525554 iPrintResult ""

526−ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)

555+ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)

527556 iPrintResult ""

528−ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

529−ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

530−ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)

531−ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)

532−ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)

533−ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)

534−ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)

535−ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)

536−ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

557+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

558+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

559+ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)

560+ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)

561+ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

562+ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

563+ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

564+ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

565+ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

537566 iPrintResult ""

538−ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

567+ideslaveProcess fn (Apropos a) = do process fn (Apropos a)

539568 iPrintResult ""

540−ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)

541−ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)

569+ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)

570+ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)

542571ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

543572

544573

@@ -570,18 +599,18 @@ processInput cmd orig inputs

570599 , idris_colourTheme = idris_colourTheme i

571600 }

572601 clearErr

573− mods <- loadInputs stdout inputs Nothing

602+ mods <- loadInputs inputs Nothing

574603 return (Just inputs)

575604 Success (Load f toline) ->

576605 do putIState orig { idris_options = idris_options i

577606 , idris_colourTheme = idris_colourTheme i

578607 }

579608 clearErr

580− mod <- loadInputs stdout [f] toline

609+ mod <- loadInputs [f] toline

581610 return (Just [f])

582611 Success (ModImport f) ->

583612 do clearErr

584− fmod <- loadModule stdout f

613+ fmod <- loadModule f

585614 return (Just (inputs ++ [fmod]))

586615 Success Edit -> do -- takeMVar stvar

587616 edit fn orig

@@ -590,7 +619,7 @@ processInput cmd orig inputs

590619 return (Just inputs)

591620 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

592621 return Nothing

593− Success cmd -> do idrisCatch (process stdout fn cmd)

622+ Success cmd -> do idrisCatch (process fn cmd)

594623 (\e -> do msg <- showErr e ; iputStrLn msg)

595624 return (Just inputs)

596625

@@ -626,7 +655,7 @@ edit f orig

626655 putIState $ orig { idris_options = idris_options i

627656 , idris_colourTheme = idris_colourTheme i

628657 }

629− loadInputs stdout [f] Nothing

658+ loadInputs [f] Nothing

630659-- clearOrigPats

631660 iucheck

632661 return ()

@@ -652,13 +681,13 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

652681 = p : "" : prf : xs

653682insertScript prf (x : xs) = x : insertScript prf xs

654683

655−process :: Handle -> FilePath -> Command -> Idris ()

656−process h fn Help = iPrintResult displayHelp

657−process h fn Warranty = iPrintResult warranty

658−process h fn (ChangeDirectory f)

684+process :: FilePath -> Command -> Idris ()

685+process fn Help = iPrintResult displayHelp

686+process fn Warranty = iPrintResult warranty

687+process fn (ChangeDirectory f)

659688 = do runIO $ setCurrentDirectory f

660689 return ()

661−process h fn (Eval t)

690+process fn (Eval t)

662691 = withErrorReflection $ do logLvl 5 $ show t

663692 (tm, ty) <- elabVal recinfo ERHS t

664693 ctxt <- getContext

@@ -671,10 +700,10 @@ process h fn (Eval t)

671700 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

672701 let tmDoc = pprintDelab ist tm'

673702 tyDoc = pprintDelab ist ty'

674− ihPrintTermWithType h tmDoc tyDoc

703+ iPrintTermWithType tmDoc tyDoc

675704

676705

677−process h fn (NewDefn decls) = do

706+process fn (NewDefn decls) = do

678707 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))

679708 mapM_ defineName namedGroups where

680709 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

@@ -732,7 +761,7 @@ process h fn (NewDefn decls) = do

732761 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

733762 fixClauses decl = decl

734763

735−process h fn (Undefine names) = undefine names

764+process fn (Undefine names) = undefine names

736765 where

737766 undefine :: [Name] -> Idris ()

738767 undefine [] = do

@@ -741,7 +770,7 @@ process h fn (Undefine names) = undefine names

741770 -- Keep track of which names you've removed so you can

742771 -- print them out to the user afterward

743772 undefine names = undefine' names []

744− undefine' [] list = do ihputStrLn h (show list)

773+ undefine' [] list = do iputStrLn (show list)

745774 return ()

746775 undefine' (n:names) already = do

747776 allDefined <- idris_repl_defs `fmap` get

@@ -764,7 +793,7 @@ process h fn (Undefine names) = undefine names

764793

765794

766795

767−process h fn (ExecVal t)

796+process fn (ExecVal t)

768797 = do ctxt <- getContext

769798 ist <- getIState

770799 (tm, ty) <- elabVal recinfo ERHS t

@@ -773,19 +802,19 @@ process h fn (ExecVal t)

773802 res <- execute tm

774803 let (resOut, tyOut) = (prettyIst ist (delab ist res),

775804 prettyIst ist (delab ist ty'))

776− ihPrintTermWithType h resOut tyOut

805+ iPrintTermWithType resOut tyOut

777806

778−process h fn (Check (PRef _ n))

807+process fn (Check (PRef _ n))

779808 = do ctxt <- getContext

780809 ist <- getIState

781810 let ppo = ppOptionIst ist

782811 case lookupNames n ctxt of

783812 ts@(t:_) ->

784813 case lookup t (idris_metavars ist) of

785− Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

814+ Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $

786815 showMetavarInfo ppo ist n i

787− Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

788− [] -> ihPrintError h $ "No such variable " ++ show n

816+ Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)

817+ [] -> iPrintError $ "No such variable " ++ show n

789818 where

790819 showMetavarInfo ppo ist n i

791820 = case lookupTy n (tt_ctxt ist) of

@@ -810,7 +839,7 @@ process h fn (Check (PRef _ n))

810839 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

811840

812841

813−process h fn (Check t)

842+process fn (Check t)

814843 = do (tm, ty) <- elabVal recinfo ERHS t

815844 ctxt <- getContext

816845 ist <- getIState

@@ -818,24 +847,24 @@ process h fn (Check t)

818847 ty' = normaliseC ctxt [] ty

819848 case tm of

820849 TType _ ->

821− ihPrintTermWithType h (prettyIst ist PType) type1Doc

822− _ -> ihPrintTermWithType h (pprintDelab ist tm)

823− (pprintDelab ist ty)

850+ iPrintTermWithType (prettyIst ist PType) type1Doc

851+ _ -> iPrintTermWithType (pprintDelab ist tm)

852+ (pprintDelab ist ty)

824853

825−process h fn (DocStr (Left n))

854+process fn (DocStr (Left n))

826855 = do ist <- getIState

827856 case lookupCtxtName n (idris_docstrings ist) of

828857 [] -> iPrintError $ "No documentation for " ++ show n

829858 ns -> do toShow <- mapM (showDoc ist) ns

830− ihRenderResult h (vsep toShow)

859+ iRenderResult (vsep toShow)

831860 where showDoc ist (n, d) = do doc <- getDocs n

832861 return $ pprintDocs ist doc

833862

834−process h fn (DocStr (Right c))

863+process fn (DocStr (Right c))

835864 = do ist <- getIState

836− ihRenderResult h $ pprintConstDocs ist c (constDocs c)

865+ iRenderResult $ pprintConstDocs ist c (constDocs c)

837866

838−process h fn Universes

867+process fn Universes

839868 = do i <- getIState

840869 let cs = idris_constraints i

841870-- iputStrLn $ showSep "\n" (map show cs)

@@ -845,7 +874,7 @@ process h fn Universes

845874 case ucheck cs of

846875 Error e -> iPrintError $ pshow i e

847876 OK _ -> iPrintResult "Universes OK"

848−process h fn (Defn n)

877+process fn (Defn n)

849878 = do i <- getIState

850879 iputStrLn "Compiled patterns:\n"

851880 iputStrLn $ show (lookupDef n (tt_ctxt i))

@@ -860,20 +889,20 @@ process h fn (Defn n)

860889 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

861890 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

862891 showTm i' (delab i rhs))

863−process h fn (TotCheck n)

892+process fn (TotCheck n)

864893 = do i <- getIState

865894 case lookupNameTotal n (tt_ctxt i) of

866− [] -> ihPrintError h $ "Unknown operator " ++ show n

895+ [] -> iPrintError $ "Unknown operator " ++ show n

867896 ts -> do ist <- getIState

868897 c <- colourise

869898 let ppo = ppOptionIst ist

870899 let showN = showName (Just ist) [] ppo c

871− ihPrintResult h . concat . intersperse "\n" .

900+ iPrintResult . concat . intersperse "\n" .

872901 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

873902 ts

874903

875904

876−process h fn (DebugInfo n)

905+process fn (DebugInfo n)

877906 = do i <- getIState

878907 let oi = lookupCtxtName n (idris_optimisation i)

879908 when (not (null oi)) $ iputStrLn (show oi)

@@ -890,29 +919,29 @@ process h fn (DebugInfo n)

890919 iputStrLn $ "Size change: " ++ show sc

891920 when (not (null cg')) $ do iputStrLn "Call graph:\n"

892921 iputStrLn (show cg')

893−process h fn (Search t) = searchByType h t

894−process h fn (CaseSplitAt updatefile l n)

895− = caseSplitAt h fn updatefile l n

896−process h fn (AddClauseFrom updatefile l n)

897− = addClauseFrom h fn updatefile l n

898−process h fn (AddProofClauseFrom updatefile l n)

899− = addProofClauseFrom h fn updatefile l n

900−process h fn (AddMissing updatefile l n)

901− = addMissing h fn updatefile l n

902−process h fn (MakeWith updatefile l n)

903− = makeWith h fn updatefile l n

904−process h fn (MakeLemma updatefile l n)

905− = makeLemma h fn updatefile l n

906−process h fn (DoProofSearch updatefile rec l n hints)

907− = doProofSearch h fn updatefile rec l n hints Nothing

908−process h fn (Spec t)

922+process fn (Search t) = searchByType t

923+process fn (CaseSplitAt updatefile l n)

924+ = caseSplitAt fn updatefile l n

925+process fn (AddClauseFrom updatefile l n)

926+ = addClauseFrom fn updatefile l n

927+process fn (AddProofClauseFrom updatefile l n)

928+ = addProofClauseFrom fn updatefile l n

929+process fn (AddMissing updatefile l n)

930+ = addMissing fn updatefile l n

931+process fn (MakeWith updatefile l n)

932+ = makeWith fn updatefile l n

933+process fn (MakeLemma updatefile l n)

934+ = makeLemma fn updatefile l n

935+process fn (DoProofSearch updatefile rec l n hints)

936+ = doProofSearch fn updatefile rec l n hints Nothing

937+process fn (Spec t)

909938 = do (tm, ty) <- elabVal recinfo ERHS t

910939 ctxt <- getContext

911940 ist <- getIState

912941 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

913942 iPrintResult (show (delab ist tm'))

914943

915−process h fn (RmProof n')

944+process fn (RmProof n')

916945 = do i <- getIState

917946 n <- resolveProof n'

918947 let proofs = proof_list i

@@ -928,7 +957,7 @@ process h fn (RmProof n')

928957 let ms = idris_metavars i

929958 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

930959

931−process h fn' (AddProof prf)

960+process fn' (AddProof prf)

932961 = do fn <- do

933962 let fn'' = takeWhile (/= ' ') fn'

934963 ex <- runIO $ doesFileExist fn''

@@ -958,7 +987,7 @@ process h fn' (AddProof prf)

958987 iputStrLn $ "Added proof " ++ show n

959988 where ls = (lines prog)

960989

961−process h fn (ShowProof n')

990+process fn (ShowProof n')

962991 = do i <- getIState

963992 n <- resolveProof n'

964993 let proofs = proof_list i

@@ -966,7 +995,7 @@ process h fn (ShowProof n')

966995 Nothing -> iPrintError "No proof to show"

967996 Just p -> iPrintResult $ showProof False n p

968997

969−process h fn (Prove n')

998+process fn (Prove n')

970999 = do ctxt <- getContext

9711000 ist <- getIState

9721001 let ns = lookupNames n' ctxt

@@ -984,20 +1013,20 @@ process h fn (Prove n')

9841013 mapM_ checkDeclTotality (idris_totcheck i)

9851014 warnTotality

9861015

987−process h fn (HNF t)

1016+process fn (HNF t)

9881017 = do (tm, ty) <- elabVal recinfo ERHS t

9891018 ctxt <- getContext

9901019 ist <- getIState

9911020 let tm' = hnf ctxt [] tm

9921021 iPrintResult (show (delab ist tm'))

993−process h fn (TestInline t)

1022+process fn (TestInline t)

9941023 = do (tm, ty) <- elabVal recinfo ERHS t

9951024 ctxt <- getContext

9961025 ist <- getIState

9971026 let tm' = inlineTerm ist tm

9981027 c <- colourise

9991028 iPrintResult (showTm ist (delab ist tm'))

1000−process h fn Execute

1029+process fn Execute

10011030 = idrisCatch

10021031 (do ist <- getIState

10031032 (m, _) <- elabVal recinfo ERHS

@@ -1009,33 +1038,33 @@ process h fn Execute

10091038 t <- codegen

10101039 compile t tmpn m

10111040 case idris_outputmode ist of

1012− RawOutput -> do runIO $ system tmpn

1013− return ()

1014− IdeSlave n -> runIO . hPutStrLn h $

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

1016− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

1041+ RawOutput h -> do runIO $ system tmpn

1042+ return ()

1043+ IdeSlave n h -> runIO . hPutStrLn h $

1044+ IdeSlave.convSExp "run-program" tmpn n)

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

10171046 where fc = fileFC "main"

1018−process h fn (Compile codegen f)

1047+process fn (Compile codegen f)

10191048 = do (m, _) <- elabVal recinfo ERHS

10201049 (PApp fc (PRef fc (sUN "run__IO"))

10211050 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

10221051 compile codegen f m

10231052 where fc = fileFC "main"

1024−process h fn (LogLvl i) = setLogLevel i

1053+process fn (LogLvl i) = setLogLevel i

10251054-- Elaborate as if LHS of a pattern (debug command)

1026−process h fn (Pattelab t)

1055+process fn (Pattelab t)

10271056 = do (tm, ty) <- elabVal recinfo ELHS t

10281057 iPrintResult $ show tm ++ "\n\n : " ++ show ty

10291058

1030−process h fn (Missing n)

1059+process fn (Missing n)

10311060 = do i <- getIState

10321061 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

10331062 case lookupCtxt n (idris_patdefs i) of

1034− [] -> ihPrintError h $ "Unknown operator " ++ show n

1063+ [] -> iPrintError $ "Unknown operator " ++ show n

10351064 [(_, tms)] ->

10361065 iPrintResult (showSep "\n" (map (showTm i') tms))

10371066 _ -> iPrintError $ "Ambiguous name"

1038−process h fn (DynamicLink l)

1067+process fn (DynamicLink l)

10391068 = do i <- getIState

10401069 let importdirs = opt_importdirs (idris_options i)

10411070 lib = trim l

@@ -1048,80 +1077,80 @@ process h fn (DynamicLink l)

10481077 return ()

10491078 else putIState $ i { idris_dynamic_libs = x:libs }

10501079 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1051−process h fn ListDynamic

1080+process fn ListDynamic

10521081 = do i <- getIState

10531082 iputStrLn "Dynamic libraries:"

10541083 showLibs $ idris_dynamic_libs i

10551084 where showLibs [] = return ()

10561085 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

1057−process h fn Metavars

1086+process fn Metavars

10581087 = do ist <- getIState

10591088 let mvs = map fst (idris_metavars ist) \\ primDefs

10601089 case mvs of

10611090 [] -> iPrintError "No global metavariables to solve"

10621091 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

1063−process h fn NOP = return ()

1064−

1065−process h fn (SetOpt ErrContext) = setErrContext True

1066−process h fn (UnsetOpt ErrContext) = setErrContext False

1067−process h fn (SetOpt ShowImpl) = setImpShow True

1068−process h fn (UnsetOpt ShowImpl) = setImpShow False

1069−process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

1070−process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1071−process h fn (SetOpt AutoSolve) = setAutoSolve True

1072−process h fn (UnsetOpt AutoSolve) = setAutoSolve False

1073−process h fn (SetOpt NoBanner) = setNoBanner True

1074−process h fn (UnsetOpt NoBanner) = setNoBanner False

1075−process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1076−process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1077−

1078−process h fn (SetOpt _) = iPrintError "Not a valid option"

1079−process h fn (UnsetOpt _) = iPrintError "Not a valid option"

1080−process h fn (SetColour ty c) = setColour ty c

1081−process h fn ColourOn

1092+process fn NOP = return ()

1093+

1094+process fn (SetOpt ErrContext) = setErrContext True

1095+process fn (UnsetOpt ErrContext) = setErrContext False

1096+process fn (SetOpt ShowImpl) = setImpShow True

1097+process fn (UnsetOpt ShowImpl) = setImpShow False

1098+process fn (SetOpt ShowOrigErr) = setShowOrigErr True

1099+process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1100+process fn (SetOpt AutoSolve) = setAutoSolve True

1101+process fn (UnsetOpt AutoSolve) = setAutoSolve False

1102+process fn (SetOpt NoBanner) = setNoBanner True

1103+process fn (UnsetOpt NoBanner) = setNoBanner False

1104+process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1105+process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1106+

1107+process fn (SetOpt _) = iPrintError "Not a valid option"

1108+process fn (UnsetOpt _) = iPrintError "Not a valid option"

1109+process fn (SetColour ty c) = setColour ty c

1110+process fn ColourOn

10821111 = do ist <- getIState

10831112 putIState $ ist { idris_colourRepl = True }

1084−process h fn ColourOff

1113+process fn ColourOff

10851114 = do ist <- getIState

10861115 putIState $ ist { idris_colourRepl = False }

1087−process h fn ListErrorHandlers =

1116+process fn ListErrorHandlers =

10881117 do ist <- getIState

10891118 iPrintResult $ case idris_errorhandlers ist of

10901119 [] -> "No registered error handlers"

10911120 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

1092−process h fn (SetConsoleWidth w) = setWidth w

1121+process fn (SetConsoleWidth w) = setWidth w

10931122

1094−process h fn (Apropos a) =

1123+process fn (Apropos a) =

10951124 do ist <- getIState

10961125 let names = apropos ist (T.pack a)

10971126 let aproposInfo = [ (n,

10981127 delabTy ist n,

10991128 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

11001129 | n <- sort names, isUN n ]

1101− ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1130+ iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)

11021131 where isUN (UN _) = True

11031132 isUN (NS n _) = isUN n

11041133 isUN _ = False

11051134

1106−process h fn (WhoCalls n) =

1135+process fn (WhoCalls n) =

11071136 do calls <- whoCalls n

11081137 ist <- getIState

1109− ihRenderResult h . vsep $

1138+ iRenderResult . vsep $

11101139 map (\(n, ns) ->

11111140 text "Callers of" <+> prettyName True True [] n <$>

11121141 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

11131142 calls

11141143

1115−process h fn (CallsWho n) =

1144+process fn (CallsWho n) =

11161145 do calls <- callsWho n

11171146 ist <- getIState

1118− ihRenderResult h . vsep $

1147+ iRenderResult . vsep $

11191148 map (\(n, ns) ->

11201149 prettyName True True [] n <+> text "calls:" <$>

11211150 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

11221151 calls

11231152-- IdrisDoc

1124−process h fn (MakeDoc s) =

1153+process fn (MakeDoc s) =

11251154 do istate <- getIState

11261155 let names = words s

11271156 parse n | Success x <- runparser name istate fn n = Right x

@@ -1178,8 +1207,8 @@ idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

11781207 [] -> return ()

11791208

11801209

1181−loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()

1182−loadInputs h inputs toline -- furthest line to read in input source files

1210+loadInputs :: [FilePath] -> Maybe Int -> Idris ()

1211+loadInputs inputs toline -- furthest line to read in input source files

11831212 = idrisCatch

11841213 (do ist <- getIState

11851214 -- if we're in --check and not outputting anything, don't bother

@@ -1231,10 +1260,10 @@ loadInputs h inputs toline -- furthest line to read in input source files

12311260 (\e -> do i <- getIState

12321261 case e of

12331262 At f e' -> do setErrSpan f

1234− ihWarn stdout f $ pprintErr i e'

1263+ iWarn f $ pprintErr i e'

12351264 ProgramLineComment -> return () -- fail elsewhere

12361265 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1237− ihWarn stdout emptyFC $ pprintErr i e)

1266+ iWarn emptyFC $ pprintErr i e)

12381267 where -- load all files, stop if any fail

12391268 tryLoad :: Bool -> [IFileType] -> Idris ()

12401269 tryLoad keepstate [] = warnTotality >> return ()

@@ -1251,7 +1280,7 @@ loadInputs h inputs toline -- furthest line to read in input source files

12511280 then Just l

12521281 else Nothing

12531282 _ -> Nothing

1254− loadFromIFile h f maxline

1283+ loadFromIFile f maxline

12551284 inew <- getIState

12561285 -- FIXME: Save these in IBC to avoid this hack! Need to

12571286 -- preserve it all from source inputs

@@ -1299,7 +1328,7 @@ idrisMain opts =

12991328 do let inputs = opt getFile opts

13001329 let quiet = Quiet `elem` opts

13011330 let nobanner = NoBanner `elem` opts

1302− let idesl = Ideslave `elem` opts

1331+ let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts

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

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

13051334 let output = opt getOutput opts

@@ -1336,7 +1365,6 @@ idrisMain opts =

13361365 mapM_ addLangExt (opt getLanguageExt opts)

13371366 setREPL runrepl

13381367 setQuiet (quiet || isJust script || not (null immediate))

1339− setIdeSlave idesl

13401368 setVerbose verbose

13411369 setCmdLine opts

13421370 setOutputTy outty

@@ -1362,9 +1390,9 @@ idrisMain opts =

13621390 addPkgDir "base"

13631391 mapM_ addPkgDir pkgdirs

13641392 elabPrims

1365− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"

1393+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"

13661394 return ()

1367− when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

1395+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

13681396 return ()

13691397

13701398 when (runrepl && not idesl) initScript

@@ -1380,14 +1408,14 @@ idrisMain opts =

13801408 iputStrLn banner

13811409

13821410 orig <- getIState

1383− loadInputs stdout inputs Nothing

1411+ when (not idesl) $ loadInputs inputs Nothing

13841412

13851413 runIO $ hSetBuffering stdout LineBuffering

13861414

13871415 ok <- noErrors

13881416 when ok $ case output of

13891417 [] -> return ()

1390− (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1418+ (o:_) -> idrisCatch (process "" (Compile cgn o))

13911419 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

13921420

13931421 case immediate of

@@ -1398,7 +1426,7 @@ idrisMain opts =

13981426 case parseExpr ist str of

13991427 Failure err -> do iputStrLn $ show (fixColour c err)

14001428 runIO $ exitWith (ExitFailure 1)

1401− Success e -> process stdout "" (Eval e))

1429+ Success e -> process "" (Eval e))

14021430 exprs

14031431 runIO $ exitWith ExitSuccess

14041432

@@ -1420,7 +1448,8 @@ idrisMain opts =

14201448-- clearOrigPats

14211449 startServer orig inputs

14221450 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1423− when (idesl) $ ideslaveStart orig inputs

1451+ let idesock = IdeslaveSocket `elem` opts

1452+ when (idesl) $ ideslaveStart idesock orig inputs

14241453 ok <- noErrors

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

14261455 where

@@ -1482,7 +1511,7 @@ initScript = do script <- getInitScript

14821511 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

14831512 Success Proofs -> proofs i

14841513 Success Quit -> iPrintError "Init scripts cannot quit Idris"

1485− Success cmd -> process stdout [] cmd

1514+ Success cmd -> process [] cmd

14861515

14871516getFile :: Opt -> Maybe String

14881517getFile (Filename str) = Just str

src/Idris/TypeSearch.hs+6−8

@@ -29,14 +29,12 @@ import Idris.Core.Unify (match_unify)

2929import Idris.Delaborate (delabTy)

3030import Idris.Docstrings (noDocs, overview)

3131import Idris.Elab.Type (elabType)

32−import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)

33−

34−import System.IO (Handle)

32+import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)

3533

3634import Util.Pretty (text, char, vsep, (<>), Doc)

3735

38−searchByType :: Handle -> PTerm -> Idris ()

39−searchByType h pterm = do

36+searchByType :: PTerm -> Idris ()

37+searchByType pterm = do

4038 pterm' <- addUsingConstraints syn emptyFC pterm

4139 pterm'' <- implicit toplevel syn n pterm'

4240 i <- getIState

@@ -50,9 +48,9 @@ searchByType h pterm = do

5048 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

5149 | (n, score) <- names']

5250 case idris_outputmode i of

53− RawOutput -> do mapM_ (ihRenderOutput h) docs

54− ihPrintResult h ""

55− IdeSlave n -> ihRenderResult h (vsep docs)

51+ RawOutput _ -> do mapM_ iRenderOutput docs

52+ iPrintResult ""

53+ IdeSlave n h -> iRenderResult (vsep docs)

5654 where

5755 numLimit = 50

5856 syn = defaultSyntax { implicitAllowed = True } -- syntax

src/Pkg/Package.hs+1−1

@@ -144,7 +144,7 @@ documentPkg fp =

144144 setCurrentDirectory $ pkgDir

145145 let run l = runErrorT . (execStateT l)

146146 load [] = return ()

147− load (f:fs) = do loadModule stdout f; load fs

147+ load (f:fs) = do loadModule f; load fs

148148 loader = do idrisMain opts; load fs

149149 idrisInstance <- run loader idrisInit

150150 setCurrentDirectory cd

src/Util/Net.hs+15−2

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

1−module Util.Net (listenOnLocalhost) where

1+module Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort) where

3−import Network

3+import Network hiding (socketPort)

44import Network.Socket hiding (sClose, PortNumber)

55import Network.BSD (getProtocolNumber)

66import Control.Exception (bracketOnError)

@@ -20,3 +20,16 @@ listenOnLocalhost (PortNumber port) = do

2020 return sock

2121 )

2222

23+listenOnLocalhostAnyPort = do

24+ proto <- getProtocolNumber "tcp"

25+ localhost <- inet_addr "127.0.0.1"

26+ bracketOnError

27+ (socket AF_INET Stream proto)

28+ (sClose)

29+ (\sock -> do

30+ setSocketOption sock ReuseAddr 1

31+ bindSocket sock (SockAddrInet aNY_PORT localhost)

32+ listen sock maxListenQueue

33+ port <- socketPort sock

34+ return (sock, port)

35+ )

test/error004/FunErrTest.idr+1−1

@@ -9,7 +9,7 @@ import Language.Reflection.Utils

99total

1010cadr : (xs : List a)

1111 -> {auto cons1 : isCons xs = True}

12− -> {auto cons2 : isCons (tail xs cons1) = True}

12+ -> {auto cons2 : isCons (tail xs) = True}

1313 -> a

1414cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

1515cadr (x :: []) {cons1=refl} {cons2=refl} impossible

test/error004/expected+1−1

@@ -3,4 +3,4 @@ When elaborating argument cons1 to function FunErrTest.cadr:

33 Could not prove that [] has at least two elements.

44FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

55When elaborating argument cons2 to function FunErrTest.cadr:

6− Could not prove that tail [(fromInteger 1)] refl has at least two elements.

6+ Could not prove that tail [(fromInteger 1)] has at least two elements.

test/proof007/DefaultArgUnknownName.idr+7−1

@@ -1,4 +1,10 @@

11module DefaultArgUnknownName

3+-- FIXME: What is the expected behaviour here? Should the type declaration

4+-- not compile?

35funWithBadDefArg : { default sadgjhsag arg : () } -> ()

4−funWithBadDefArg : _ = ()

6+funWithBadDefArg = ()

8+test : ()

9+test = funWithBadDefArg

10+

test/proof007/expected+3−2

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

1−DefaultArgUnknownName.idr:3:18:When elaborating type of DefaultArgUnknownName.funWithBadDefArg:

2−Can't infer type for sadgjhsag

1+DefaultArgUnknownName.idr:5:30:When elaborating right hand side of test:

2+When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3+ No such variable sadgjhsag