ecea9ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' into repl-definitions

ecea9adAlyssa Carter12 years ago

.travis.yml+1

compare with master

unifiedsplit

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

25 - make -j2 $TESTS

26env:

27 - TESTS="doc"

28+ - TESTS="lib_doc"

28 - TESTS="test_c"

29 - TESTS="test_c"

29 - TESTS="test_llvm"

30 - TESTS="test_llvm"

30 - TESTS="test_js"

31 - TESTS="test_js"

CHANGELOG+2

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

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

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

4* 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

6New in 0.9.14:

8New in 0.9.14:

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

9--------------

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

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

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

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

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

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

76−head [] refl impossible

76+head [] {ok=refl} impossible

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

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

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

80||| `Nothing`.

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

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

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

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

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

88−tail [] refl impossible

88+tail [] {ok=refl} impossible

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

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

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

92|||

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

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

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

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

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

101−last [] refl impossible

101+last [] {ok=refl} impossible

102−last [x] p = x

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

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

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

104

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

106|||

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

114

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

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

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

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

118−init [] refl impossible

118+init [] {ok=refl} impossible

119−init [x] p = []

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

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

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

121

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

123|||

src/Idris/AbsSyntax.hs+10−14

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

537isetPrompt :: String -> Idris ()

538isetPrompt p = do i <- getIState

539 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

541

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

543isetLoadedRegion :: Idris ()

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

546 case span of

547 Just fc ->

548 case idris_outputmode i of

549− IdeSlave n ->

549+ IdeSlave n h ->

550− runIO . putStrLn $

550+ runIO . hPutStrLn h $

551 convSExp "set-loaded-region" fc n

552 Nothing -> return ()

553

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

662outputTy = do i <- getIState

663 return $ opt_outputTy $ idris_options i

664

665−setIdeSlave :: Bool -> Idris ()

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

666−setIdeSlave True = do i <- getIState

666+setIdeSlave True h = do i <- getIState

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

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

668−setIdeSlave False = return ()

668+setIdeSlave False _ = return ()

669

670setTargetTriple :: String -> Idris ()

671setTargetTriple t = do i <- getIState

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

761setColourise b = do i <- getIState

762 putIState $ i { idris_colourRepl = b }

763

764−setOutH :: Handle -> Idris ()

765−setOutH h = do i <- getIState

766− putIState $ i { idris_outh = h }

767−

768impShow :: Idris Bool

764impShow :: Idris Bool

769impShow = do i <- getIState

765impShow = do i <- getIState

770 return (opt_showimp (idris_options i))

766 return (opt_showimp (idris_options i))

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

793 let lvl = opt_logLevel (idris_options i)

789 let lvl = opt_logLevel (idris_options i)

794 when (lvl >= l) $

790 when (lvl >= l) $

795 case idris_outputmode i of

791 case idris_outputmode i of

796− RawOutput -> do runIO $ putStrLn str

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

797− IdeSlave n ->

793+ IdeSlave n h ->

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

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

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

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

800

796

801cmdOptType :: Opt -> Idris Bool

797cmdOptType :: Opt -> Idris Bool

802cmdOptType x = do i <- getIState

798cmdOptType x = do i <- getIState

src/Idris/AbsSyntaxTree.hs+8−8

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

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

128

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

131

133

132-- | How wide is the console?

134-- | How wide is the console?

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

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

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

192 idris_outputmode :: OutputMode,

194 idris_outputmode :: OutputMode,

193 idris_colourRepl :: Bool,

195 idris_colourRepl :: Bool,

194 idris_colourTheme :: ColourTheme,

196 idris_colourTheme :: ColourTheme,

195− idris_outh :: Handle,

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

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

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

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

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

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

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

278 emptyContext emptyContext emptyContext emptyContext

279 emptyContext emptyContext emptyContext emptyContext

279 emptyContext emptyContext

280 emptyContext emptyContext

280 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

281 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

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

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

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

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

283 AutomaticWidth S.empty Nothing Nothing []

284 AutomaticWidth S.empty Nothing Nothing []

284

285

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

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

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

360 | NoBanner

361 | NoBanner

361 | ColourREPL Bool

362 | ColourREPL Bool

362 | Ideslave

363 | Ideslave

364+ | IdeslaveSocket

363 | ShowLibs

365 | ShowLibs

364 | ShowLibdir

366 | ShowLibdir

365 | ShowIncs

367 | ShowIncs

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

1637 size (PProof tactics) = size tactics

1639 size (PProof tactics) = size tactics

1638 size (PElabError err) = size err

1640 size (PElabError err) = size err

1639 size PImpossible = 1

1641 size PImpossible = 1

1642+ size _ = 0

1640

1643

1641getPArity :: PTerm -> Int

1644getPArity :: PTerm -> Int

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

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

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

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

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

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

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

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

1721 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

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

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

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

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

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

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

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

1730 ni env (PNoImplicits tm) = ni env tm

1733 ni env (PNoImplicits tm) = ni env tm

1731 ni env _ = []

1734 ni env _ = []

1732

1735

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

1734− niTacImp _ _ = []

1735−

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

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

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

src/Idris/CmdOptions.hs+1

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

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

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

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

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

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

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

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

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

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

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

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

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

12 module Idris.Core.ProofState) where

14import 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)

16import Idris.Core.TT

17import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Core.Evaluate

18import Idris.Core.Typecheck

19import Idris.Core.Typecheck

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

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

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

391movelast n = processTactic' (MoveLast n)

392movelast n = processTactic' (MoveLast n)

392

393

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+

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

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

394matchProblems all = processTactic' (MatchProblems all)

402matchProblems all = processTactic' (MatchProblems all)

395

403

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

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

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

629arg n tyhole = do ty <- unique_hole tyhole

637arg n tyhole = do ty <- unique_hole tyhole

630 claim ty RType

638 claim ty RType

639+ movelast ty

631 forall n (Var ty)

640 forall n (Var ty)

632

641

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

642-- 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 =

216-- ++ show (pterm ps)

217 ++ "\n----------") $

218 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

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

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

220 -- problem for each.

222 -- problem for each.

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

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

222 ps <- get

224 ps <- get

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

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

224 (fails ++ problems ps)

226 (fails ++ problems ps)

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

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

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

551

553

552patvar :: Name -> RunTactic

554patvar :: Name -> RunTactic

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

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

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

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

555 holes ps \\ [x],

557 holes ps \\ [x],

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

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

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

900 = case solved ps' of

902 = case solved ps' of

901 Just s -> traceWhen (unifylog ps')

903 Just s -> traceWhen (unifylog ps')

902 ("SOLVED " ++ show s) $

904 ("SOLVED " ++ show s) $

903− updateProblems (context ps')

905+ updateProblems (context ps')

904 [s] (problems ps')

906 [s] (problems ps')

905 (injective ps')

907 (injective ps')

906 (holes ps')

908 (holes ps')

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

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

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

8 updateSolved, updateSolvedTerm,

9− bound_in, bound_in_term,

9+ bound_in, bound_in_term, refocus,

10 Hole, RunTactic',

11 goal, atHole) where

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

18import Data.List

19import Debug.Trace

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+

21−newtype ProofTerm = PT Term

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

86+ path :: TermPath,

87+ subterm_env :: Env,

88+ subterm :: Term,

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

90+ deriving Show

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

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

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

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

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+

26data Goal = GD { premises :: Env,

107data Goal = GD { premises :: Env,

27 goalType :: Binder Term

108 goalType :: Binder Term

28 }

109 }

110

30mkProofTerm :: Term -> ProofTerm

111mkProofTerm :: Term -> ProofTerm

31−mkProofTerm tm = PT tm

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

113

33getProofTerm :: ProofTerm -> Term

114getProofTerm :: ProofTerm -> Term

34−getProofTerm (PT tm) = tm

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

116

36same Nothing n = True

117same Nothing n = True

37same (Just x) n = x == n

118same (Just x) n = x == n

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

41hole _ = False

122hole _ = False

123

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

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

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

44−updateSolvedTerm xs x = updateSolved' xs x where

132+ else updateSolved' xs x where

45 updateSolved' [] x = x

133 updateSolved' [] x = x

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

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

47 | Just v <- lookup n xs

135 | Just v <- lookup n xs

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

57 | Just v <- lookup n xs = v

145 | Just v <- lookup n xs = v

58 updateSolved' xs t = t

146 updateSolved' xs t = t

147

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+

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

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

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

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

186+ (updateSolvedTerm xs sub)

187+ (ups ++ xs)

188

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

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

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

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

193+ where

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

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

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

66 | same h n = return $ GD env b

196 | same h n = return $ GD env b

67 | otherwise

197 | otherwise

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

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

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

70 | otherwise

200 | otherwise

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

201 = 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

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

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

204

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

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

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

208

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

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

80 StateT a TC (ProofTerm, Bool)

210 StateT a TC (ProofTerm, Bool)

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

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

82− return (PT tm, u)

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

83 where

219 where

84 updated o = do o' <- o

220 updated o = do o' <- o

85 return (o', True)

221 return (o', True)

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

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

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

118

254

119bound_in :: ProofTerm -> [Name]

255bound_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))

121

257

122bound_in_term :: Term -> [Name]

258bound_in_term :: Term -> [Name]

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

259bound_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 =

333 = unifyTmpFail tx ty

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

335 = 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

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

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

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

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

338 = do UI s f <- get

347 = do UI s f <- get

src/Idris/ElabTerm.hs+3−2

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

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

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20+import qualified Util.Pretty as U

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

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

22import Control.Monad

23import Control.Monad

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

144 compute -- expand type synonyms, etc

145 compute -- expand type synonyms, etc

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

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

146 end_unify

147 end_unify

148+ ptm <- get_term

147 when pattern -- convert remaining holes to pattern vars

149 when pattern -- convert remaining holes to pattern vars

148 (do update_term orderPats

150 (do update_term orderPats

149 unify_all

151 unify_all

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

690 (caseBlock fc cname'

692 (caseBlock fc cname'

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

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

692 -- elaborate case

694 -- elaborate case

693− env <- get_env

694 updateAux (newdef : )

695 updateAux (newdef : )

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

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

696 movelast tyn

697 movelast tyn

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

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

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

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

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

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

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

908− = do elabArg argName holeName t

909+ = elabArg argName holeName t

909 where elabArg argName holeName t =

910 where elabArg argName holeName t =

910 do now_elaborating fc f argName

911 do now_elaborating fc f argName

911 wrapErr f argName $ do

912 wrapErr f argName $ do

src/Idris/Error.hs+2−3

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

43setAndReport :: Err -> Idris ()

44setAndReport e = do ist <- getIState

45− let h = idris_outh ist

46 case (unwrap e) of

45 case (unwrap e) of

47 At fc e -> do setErrSpan fc

46 At fc e -> do setErrSpan fc

48− ihWarn h fc $ pprintErr ist e

47+ iWarn fc $ pprintErr ist e

49 _ -> do setErrSpan (getErrSpan e)

48 _ -> do setErrSpan (getErrSpan e)

50− ihWarn h emptyFC $ pprintErr ist e

49+ iWarn emptyFC $ pprintErr ist e

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

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

52 unwrap e = e

51 unwrap e = e

src/Idris/IdeSlave.hs+20−10

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

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

5import Text.Printf

6import Numeric

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

12-- import qualified Data.Text as T

13import Text.Trifecta hiding (Err)

14import Text.Trifecta.Delta

15+import System.IO

16import Idris.Core.TT

17import Idris.Core.TT

17import Idris.Core.Binary

18import Idris.Core.Binary

19import Control.Applicative hiding (Const)

20import Control.Applicative hiding (Const)

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+

21data SExp = SexpList [SExp]

33data SExp = SexpList [SExp]

22 | StringAtom String

34 | StringAtom String

23 | BoolAtom Bool

35 | BoolAtom Bool

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

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

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

248parseMessage x = case receiveString x of

260parseMessage x = case receiveString x of

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

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

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

250 Left err -> Left err

263 Left err -> Left err

251

264

252receiveString :: String -> Either Err SExp

265receiveString :: String -> Either Err SExp

253receiveString x =

266receiveString 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

267+ case parseSExp x of

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

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

261− Success r -> Right r)

269+ Success r -> Right r

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

263

270

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

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

265convSExp pre s id =

272convSExp pre s id =

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

269

276

270getHexLength :: String -> String

277getHexLength :: String -> String

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

278getHexLength 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

28import System.IO

29import Data.Char

30import Data.Maybe (fromMaybe)

31+import Data.List (isSuffixOf)

32import Debug.Trace

33import Debug.Trace

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

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

35−caseSplitAt h fn updatefile l n

36+caseSplitAt fn updatefile l n

36 = do src <- runIO $ readFile fn

37 = do src <- runIO $ readFile fn

37 res <- splitOnLine l n fn

38 res <- splitOnLine l n fn

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

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

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

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

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

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

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

45 runIO $ copyFile fb fn

46 runIO $ copyFile fb fn

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

47+ else -- do iputStrLn (show res)

47− ihPrintResult h new

48+ iPrintResult new

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

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

50−addClauseFrom h fn updatefile l n

51+addClauseFrom fn updatefile l n

51 = do src <- runIO $ readFile fn

52 = do src <- runIO $ readFile fn

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

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

53 let indent = getIndent 0 (show n) tyline

54 let indent = getIndent 0 (show n) tyline

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

61 cl ++ "\n" ++

62 cl ++ "\n" ++

62 unlines rest)

63 unlines rest)

63 runIO $ copyFile fb fn

64 runIO $ copyFile fb fn

64− else ihPrintResult h cl

65+ else iPrintResult cl

65 where

66 where

66 getIndent i n [] = 0

67 getIndent i n [] = 0

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

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

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

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

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

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

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

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

72−addProofClauseFrom h fn updatefile l n

73+addProofClauseFrom fn updatefile l n

73 = do src <- runIO $ readFile fn

74 = do src <- runIO $ readFile fn

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

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

75 let indent = getIndent 0 (show n) tyline

76 let indent = getIndent 0 (show n) tyline

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

83 cl ++ "\n" ++

84 cl ++ "\n" ++

84 unlines rest)

85 unlines rest)

85 runIO $ copyFile fb fn

86 runIO $ copyFile fb fn

86− else ihPrintResult h cl

87+ else iPrintResult cl

87 where

88 where

88 getIndent i n [] = 0

89 getIndent i n [] = 0

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

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

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

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

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

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

93−addMissing h fn updatefile l n

94+addMissing fn updatefile l n

94 = do src <- runIO $ readFile fn

95 = do src <- runIO $ readFile fn

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

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

96 let indent = getIndent 0 (show n) tyline

97 let indent = getIndent 0 (show n) tyline

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

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

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

109 ++ extras ++ unlines rest)

110 ++ extras ++ unlines rest)

110 runIO $ copyFile fb fn

111 runIO $ copyFile fb fn

111− else ihPrintResult h extras

112+ else iPrintResult extras

112 where showPat = show . stripNS

113 where showPat = show . stripNS

113 stripNS tm = mapPT dens tm where

114 stripNS tm = mapPT dens tm where

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

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

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

122 getAppName (PRef _ r) = r

123 getAppName (PRef _ r) = r

123 getAppName _ = n

124 getAppName _ = n

124

125

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

127+ | otherwise = replicate ind ' '

128+

125 showNew nm i ind (tm : tms)

129 showNew nm i ind (tm : tms)

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

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

127 rest <- showNew nm i' ind tms

131 rest <- showNew nm i' ind tms

128− return (replicate ind ' ' ++

132+ return (makeIndent ind ++

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

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

130 "\n" ++ rest)

134 "\n" ++ rest)

131 showNew nm i _ [] = return ""

135 showNew nm i _ [] = return ""

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

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

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

136

140

137

141

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

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

139−makeWith h fn updatefile l n

143+makeWith fn updatefile l n

140 = do src <- runIO $ readFile fn

144 = do src <- runIO $ readFile fn

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

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

142 let ind = getIndent tyline

146 let ind = getIndent tyline

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

151 ++ with ++ "\n" ++

155 ++ with ++ "\n" ++

152 unlines rest)

156 unlines rest)

153 runIO $ copyFile fb fn

157 runIO $ copyFile fb fn

154− else ihPrintResult h with

158+ else iPrintResult with

155 where getIndent s = length (takeWhile isSpace s)

159 where getIndent s = length (takeWhile isSpace s)

156

160

157

161

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

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

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

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

160−doProofSearch h fn updatefile rec l n hints Nothing

164+doProofSearch fn updatefile rec l n hints Nothing

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

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

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

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

163 = do src <- runIO $ readFile fn

167 = do src <- runIO $ readFile fn

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

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

165 ctxt <- getContext

169 ctxt <- getContext

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

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

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

193 ++ unlines later)

197 ++ unlines later)

194 runIO $ copyFile fb fn

198 runIO $ copyFile fb fn

195− else ihPrintResult h newmv

199+ else iPrintResult newmv

196 where dropCtxt 0 sc = sc

200 where dropCtxt 0 sc = sc

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

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

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

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

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

235 | otherwise = new

239 | otherwise = new

236

240

237

241

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

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

239−makeLemma h fn updatefile l n

243+makeLemma fn updatefile l n

240 = do src <- runIO $ readFile fn

244 = do src <- runIO $ readFile fn

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

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

242

246

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

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

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

267 runIO $ copyFile fb fn

271 runIO $ copyFile fb fn

268 else case idris_outputmode i of

272 else case idris_outputmode i of

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

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

270− IdeSlave n ->

274+ IdeSlave n h ->

271 let good = SexpList [SymbolAtom "ok",

275 let good = SexpList [SymbolAtom "ok",

272 SexpList [SymbolAtom "metavariable-lemma",

276 SexpList [SymbolAtom "metavariable-lemma",

273 SexpList [SymbolAtom "replace-metavariable",

277 SexpList [SymbolAtom "replace-metavariable",

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

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

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

285 runIO $ copyFile fb fn

289 runIO $ copyFile fb fn

286 else case idris_outputmode i of

290 else case idris_outputmode i of

287− RawOutput -> ihPrintResult h $ lem_app

291+ RawOutput _ -> iPrintResult $ lem_app

288− IdeSlave n ->

292+ IdeSlave n h ->

289 let good = SexpList [SymbolAtom "ok",

293 let good = SexpList [SymbolAtom "ok",

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

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

291 SexpList [SymbolAtom "definition-clause",

295 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+60−63

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

24 renderPretty 1.0 80 .

25 fmap (fancifyAnnots ist) $ pprintErr ist err

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

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

28+iWarn fc err =

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

29+ do i <- getIState

29− case idris_outputmode i of

30+ case idris_outputmode i of

30− RawOutput ->

31+ RawOutput h ->

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

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

32− if fc_fname fc /= ""

33+ if fc_fname fc /= ""

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

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

34− else err

35+ else err

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

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

36− IdeSlave n ->

37+ IdeSlave n h ->

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

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

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

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

39− runIO . hPutStrLn h $

40+ runIO . hPutStrLn h $

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

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

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

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

43iRender d = do w <- getWidth

44iRender d = do w <- getWidth

44 ist <- getIState

45 ist <- getIState

45 let ideSlave = case idris_outputmode ist of

46 let ideSlave = case idris_outputmode ist of

46− IdeSlave _ -> True

47+ IdeSlave _ _ -> True

47− _ -> False

48+ _ -> False

48 case w of

49 case w of

49 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

50 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

50 ColsWide n -> return $

51 ColsWide n -> return $

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

63 displayDecorated (consoleDecorate ist) $

64 displayDecorated (consoleDecorate ist) $

64 rendered

65 rendered

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

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

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

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

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

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

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

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

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

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

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

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

73− let ppo = ppOptionIst ist

74+ let ppo = ppOptionIst ist

74− let infixes = idris_infixes ist

75+ let infixes = idris_infixes ist

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

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

76− ihRenderResult h output

77+ iRenderResult output

77 where fullName n = prettyName True True bnd n

78 where fullName n = prettyName True True bnd n

78 ppOverload ppo infixes n tm =

79 ppOverload ppo infixes n tm =

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

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

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

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

82−ihRenderOutput h doc =

83+iRenderOutput doc =

83 do i <- getIState

84 do i <- getIState

84 case idris_outputmode i of

85 case idris_outputmode i of

85− RawOutput -> do out <- iRender doc

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

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

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

87− IdeSlave n ->

88+ IdeSlave n h ->

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

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

89 let out = [toSExp str, toSExp spans]

90 let out = [toSExp str, toSExp spans]

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

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

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

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

93−ihRenderResult h d = do ist <- getIState

94+iRenderResult d = do ist <- getIState

94− case idris_outputmode ist of

95+ case idris_outputmode ist of

95− RawOutput -> consoleDisplayAnnotated h d

96+ RawOutput h -> consoleDisplayAnnotated h d

96− IdeSlave n -> ideSlaveReturnAnnotated n h d

97+ IdeSlave n h -> ideSlaveReturnAnnotated n h d

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

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

99ideSlaveReturnWithStatus status n h out = do

100ideSlaveReturnWithStatus status n h out = do

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

111ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

112ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

112

113

113-- | Show an error with semantic highlighting

114-- | Show an error with semantic highlighting

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

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

115−ihRenderError h e = do ist <- getIState

116+iRenderError e = do ist <- getIState

116− case idris_outputmode ist of

117+ case idris_outputmode ist of

117− RawOutput -> consoleDisplayAnnotated h e

118+ RawOutput h -> consoleDisplayAnnotated h e

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

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

119−

120+

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

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

121−ihPrintWithStatus status h s = do

122+iPrintWithStatus status s = do

122 i <- getIState

123 i <- getIState

123 case idris_outputmode i of

124 case idris_outputmode i of

124− RawOutput -> case s of

125+ RawOutput h -> case s of

125 "" -> return ()

126 "" -> return ()

126 s -> runIO $ hPutStrLn h s

127 s -> runIO $ hPutStrLn h s

127− IdeSlave n ->

128+ IdeSlave n h ->

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

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

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

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

130

131

132

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

133+iPrintResult :: String -> Idris ()

133−ihPrintResult = ihPrintWithStatus "ok"

134+iPrintResult = iPrintWithStatus "ok"

134

135

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

136+iPrintError :: String -> Idris ()

136−ihPrintError = ihPrintWithStatus "error"

137+iPrintError = iPrintWithStatus "error"

137

138

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

139+iputStrLn :: String -> Idris ()

139−ihputStrLn h s = do i <- getIState

140+iputStrLn s = do i <- getIState

140− case idris_outputmode i of

141+ case idris_outputmode i of

141− RawOutput -> runIO $ hPutStrLn h s

142+ RawOutput h -> runIO $ hPutStrLn h s

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

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

143

144

144−iputStrLn = ihputStrLn stdout

145−iPrintError = ihPrintError stdout

146−iPrintResult = ihPrintResult stdout

147−iWarn = ihWarn stdout

148

145

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

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

150ideslavePutSExp cmd info = do i <- getIState

147ideslavePutSExp cmd info = do i <- getIState

151 case idris_outputmode i of

148 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

153 _ -> return ()

150 _ -> return ()

154

151

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

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

156iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

153iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

157iputGoal g = do i <- getIState

154iputGoal g = do i <- getIState

158 case idris_outputmode i of

155 case idris_outputmode i of

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

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

160− IdeSlave n ->

157+ IdeSlave n h ->

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

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

162 goal = [toSExp str, toSExp spans]

159 goal = [toSExp str, toSExp spans]

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

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

164

161

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

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

166warnTotality :: Idris ()

163warnTotality :: Idris ()

src/Idris/ParseHelpers.hs+2−2

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

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19import Idris.Docstrings

20−import Idris.Output (ihWarn)

20+import Idris.Output (iWarn)

22import qualified Util.Pretty as Pretty (text)

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

80reportParserWarnings :: Idris ()

81reportParserWarnings = do ist <- getIState

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

82+ mapM_ (uncurry iWarn)

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

84 reverse .

85 nub $

src/Idris/Parser.hs+24−24

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

1159 let (fc, msg) = findFC doc

1160 i <- getIState

1161 case idris_outputmode i of

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

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

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

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

1164 putIState (i { errSpan = Just fc })

1165 return []

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

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

1176 return (ds, i')

1177

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

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

1179+loadModule :: FilePath -> Idris String

1180−loadModule outh f

1180+loadModule f

1181− = idrisCatch (loadModule' outh f)

1181+ = idrisCatch (loadModule' f)

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

1183 ist <- getIState

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

1184+ iWarn (getErrSpan e) $ pprintErr ist e

1185 return "")

1186

1187{- | Load idris module -}

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

1188+loadModule' :: FilePath -> Idris String

1189−loadModule' outh f

1189+loadModule' f

1190 = do i <- getIState

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

1192 ibcsd <- valIBCSubDir i

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

1196 then iLOG $ "Already read " ++ file

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

1198 case fp of

1199− IDR fn -> loadSource outh False fn Nothing

1199+ IDR fn -> loadSource False fn Nothing

1200− LIDR fn -> loadSource outh True fn Nothing

1200+ LIDR fn -> loadSource True fn Nothing

1201 IBC fn src ->

1202 idrisCatch (loadIBC fn)

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

1204 case src of

1205− IDR sfn -> loadSource outh False sfn Nothing

1205+ IDR sfn -> loadSource False sfn Nothing

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

1206+ LIDR sfn -> loadSource True sfn Nothing)

1207 let (dir, fh) = splitFileName file

1208 return (dropExtension fh)

1209

1210

1211{- | Load idris code from file -}

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

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

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

1213+loadFromIFile i@(IBC fn src) maxline

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

1215 idrisCatch (loadIBC fn)

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

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

1219 getSrcFile (LIDR fn) = fn

1220 getSrcFile (IBC f src) = getSrcFile src

1221

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

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

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

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

1224

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

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

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

1227−loadSource' h lidr r maxline

1227+loadSource' lidr r maxline

1228− = idrisCatch (loadSource h lidr r maxline)

1228+ = idrisCatch (loadSource lidr r maxline)

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

1230 ist <- getIState

1231 case e of

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

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

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

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

1234

1235{- | Load Idris source code-}

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

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

1237−loadSource h lidr f toline

1237+loadSource lidr f toline

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

1239 i <- getIState

1240 let def_total = default_total i

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

1278 logLvl 3 (show (idris_infixes i))

1279 -- Now add all the declarations to the context

1280 v <- verbose

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

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

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

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

1284 -- mutual block on its own

src/Idris/Prover.hs+51−45

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

19import Idris.Error

20import Idris.DataOpts

21import Idris.Completion

22−import Idris.IdeSlave

22+import qualified Idris.IdeSlave as IdeSlave

23import Idris.Output

24import Idris.TypeSearch (searchByType)

26import Text.Trifecta.Result(Result(..))

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

28import System.Console.Haskeline

29import System.Console.Haskeline

29import System.Console.Haskeline.History

30import System.Console.Haskeline.History

30import Control.Monad.State.Strict

31import Control.Monad.State.Strict

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

70 iLOG $ "Adding " ++ show tm

71 iLOG $ "Adding " ++ show tm

71 i <- getIState

72 i <- getIState

72 case idris_outputmode i of

73 case idris_outputmode i of

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

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

74− _ -> iputStrLn $ showProof lit n prf

75+ _ -> iputStrLn $ showProof lit n prf

75 let proofs = proof_list i

76 let proofs = proof_list i

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

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

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

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

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

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

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

94 solveDeferred n

95 solveDeferred n

95 case idris_outputmode i of

96 case idris_outputmode i of

96− IdeSlave n ->

97+ IdeSlave n h ->

97− runIO . putStrLn $

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

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

99 _ -> return ()

100

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

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

140 prettyPs bnd [] = empty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

170

172

173+ freeEnvNames :: Env -> [Name]

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

175+

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

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

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

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

173 return v

178 return v

174

179

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

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

176−receiveInput e =

181+receiveInput h e =

177 do i <- getIState

182 do i <- getIState

178− l <- runIO $ getLine

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

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

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

180 Left err -> ierror err

190 Left err -> ierror err

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

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

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

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

183− case sexpToCommand sexp of

193+ case IdeSlave.sexpToCommand sexp of

184− Just (REPLCompletions prefix) ->

194+ Just (IdeSlave.REPLCompletions prefix) ->

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

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

187 ideslavePutSExp "return" good

197 ideslavePutSExp "return" good

188− receiveInput e

198+ receiveInput h e

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

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

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

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

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

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

192 _ -> return Nothing

202 _ -> return Nothing

193

203

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

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

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

198 when d $ dumpState i (proof e)

208 when d $ dumpState i (proof e)

199 (x, h') <-

209 (x, h') <-

200 case idris_outputmode i of

210 case idris_outputmode i of

211+ RawOutput _ ->

201− RawOutput -> runInputT (proverSettings e) $

212+ runInputT (proverSettings e) $

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

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

203− do _ <- case h of

214+ do case h of

204− Just history -> putHistory history

215+ Just history -> putHistory history

205− Nothing -> return ()

216+ Nothing -> return ()

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

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

207− h' <- getHistory

218+ h' <- getHistory

208− return (l, Just h')

219+ return (l, Just h')

209− IdeSlave n ->

220+ IdeSlave _ handle ->

210 do isetPrompt prompt

221 do isetPrompt prompt

211− i <- receiveInput e

222+ i <- receiveInput handle e

212 return (i, h)

223 return (i, h)

213 (cmd, step) <- case x of

224 (cmd, step) <- case x of

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

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

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

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

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

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

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

242 case res of

253 case res of

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

254+ Left err -> do ist <- getIState

255+ iRenderError $ pprintErr ist err

244 ploop fn d prompt prf' st h'

256 ploop fn d prompt prf' st h'

245 Right ok ->

257 Right ok ->

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

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

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

253 ist <- getIState

265 ist <- getIState

254 imp <- impShow

266 imp <- impShow

255 idrisCatch (do

267 idrisCatch (do

256− let h = idris_outh ist

257− OK env = envAtFocus (proof e)

268+ let OK env = envAtFocus (proof e)

258 ctxt' = envCtxt env ctxt

269 ctxt' = envCtxt env ctxt

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

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

260 ist' = ist { tt_ctxt = ctxt' }

271 ist' = ist { tt_ctxt = ctxt' }

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

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

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

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

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

264 let action = case lookupNames n ctxt' of

275 let action = case lookupNames n ctxt' of

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

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

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

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

267 putIState ist

278 putIState ist

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

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

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

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

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

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

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

279 let ppo = ppOptionIst ist

290 let ppo = ppOptionIst ist

280 ty' = normaliseC ctxt [] ty

291 ty' = normaliseC ctxt [] ty

281− h = idris_outh ist

282 infixes = idris_infixes ist

292 infixes = idris_infixes ist

283 action = case tm of

293 action = case tm of

284 TType _ ->

294 TType _ ->

285− ihPrintTermWithType h (prettyImp ppo PType) type1Doc

295+ iPrintTermWithType (prettyImp ppo PType) type1Doc

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

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

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

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

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

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

289 putIState ist

299 putIState ist

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

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

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

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

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

306 infixes = idris_infixes ist

316 infixes = idris_infixes ist

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

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

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

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

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

319+ action = iPrintTermWithType tmDoc tyDoc

310 putIState ist

320 putIState ist

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

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

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

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

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

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

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

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

315− let h = idris_outh ist

316 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

325 idrisCatch (case lookupCtxtName n (idris_docstrings ist) of

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

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

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

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

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

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

320 return (False, e, False, prf,

329 return (False, e, False, prf,

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

330+ Right $ iRenderResult (vsep toShow)))

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

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

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

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

324 return $ pprintDocs ist doc

333 return $ pprintDocs ist doc

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

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

335+ return (False, e, False, prf, Right . iRenderResult $ 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)

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

42import Version_idris (gitHash)

43import Util.System

44import Util.DynamicLinker

45−import Util.Net (listenOnLocalhost)

45+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

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

48import Idris.Core.Evaluate

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

93import Data.Either (partitionEithers)

94import Control.DeepSeq

96+import Numeric ( readHex )

97+

96import Debug.Trace

98import Debug.Trace

98-- | Run the REPL

100-- | Run the REPL

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

151 -- TODO: option for port number

153 -- TODO: option for port number

152 serverLoop = withSocketsDo $

154 serverLoop = withSocketsDo $

153 do sock <- listenOnLocalhost $ PortNumber 4294

155 do sock <- listenOnLocalhost $ PortNumber 4294

154− loop fn orig sock

156+ loop fn orig { idris_colourRepl = False } sock

155

157

156 fn = case fn_in of

158 fn = case fn_in of

157 (f:_) -> f

159 (f:_) -> f

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

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

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

162 hSetEncoding h utf8

164 hSetEncoding h utf8

163 cmd <- hGetLine h

165 cmd <- hGetLine h

166+ let isth = case idris_outputmode ist of

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

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

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

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

165 hClose h

170 hClose h

166 loop fn ist' sock

171 loop fn ist' sock

167

172

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

187 setOutH h

192 setOutH h

188 setQuiet True

193 setQuiet True

189 setVerbose False

194 setVerbose False

190− mods <- loadInputs h [f] toline

195+ mods <- loadInputs [f] toline

191 ist <- getIState

196 ist <- getIState

192 return (ist, f)

197 return (ist, f)

193− processNet fn c = do process h fn c

198+ processNet fn c = do process fn c

194 ist <- getIState

199 ist <- getIState

195 return (ist, fn)

200 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}

196

207

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

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

198runClient :: String -> IO ()

209runClient :: String -> IO ()

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

208 else do l <- hGetLine h

219 else do l <- hGetLine h

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

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

210

221

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+

211-- | Run the IdeSlave

230-- | Run the IdeSlave

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

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

213−ideslaveStart orig mods

232+ideslaveStart s orig mods

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

234+ setIdeSlave True h

214− = do i <- getIState

235+ i <- getIState

215 case idris_outputmode i of

236 case idris_outputmode i of

216− IdeSlave n ->

237+ IdeSlave n h ->

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

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

218− ideslave orig mods

242+ ideslave h orig mods

219−

243+

220−

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

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

222−ideslave orig mods

245+ideslave h orig mods

223 = do idrisCatch

246 = 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 ""

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

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

226 Left err -> ierror err

254 Left err -> ierror err

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

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

228 i <- getIState

256 i <- getIState

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

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

230 idrisCatch -- to report correct id back!

258 idrisCatch -- to report correct id back!

231 (do let fn = case mods of

259 (do let fn = case mods of

232 (f:_) -> f

260 (f:_) -> f

233− _ -> ""

261+ _ -> ""

234 case IdeSlave.sexpToCommand sexp of

262 case IdeSlave.sexpToCommand sexp of

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

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

236 Nothing -> iPrintError "did not understand" )

264 Nothing -> iPrintError "did not understand" )

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

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

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

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

239− ideslave orig mods

267+ ideslave h orig mods

240

268

241-- | Run IDESlave commands

269-- | Run IDESlave commands

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

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

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

243 -> IState -- ^^ The original IState

272 -> IState -- ^^ The original IState

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

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

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

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

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

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

247 -> Idris ()

276 -> Idris ()

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

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

249 do c <- colourise

278 do c <- colourise

250 i <- getIState

279 i <- getIState

251 case parseCmd i "(input)" cmd of

280 case parseCmd i "(input)" cmd of

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

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

253 Success (Prove n') ->

282 Success (Prove n') ->

254 idrisCatch

283 idrisCatch

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

284+ (do process fn (Prove n')

256 isetPrompt (mkPrompt mods)

285 isetPrompt (mkPrompt mods)

257 case idris_outputmode i of

286 case idris_outputmode i of

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

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

259− runIO . hPutStrLn stdout $

288+ runIO . hPutStrLn h $

260 IdeSlave.convSExp "return"

289 IdeSlave.convSExp "return"

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

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

262 n

291 n

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

264 (\e -> do ist <- getIState

293 (\e -> do ist <- getIState

265 isetPrompt (mkPrompt mods)

294 isetPrompt (mkPrompt mods)

266 case idris_outputmode i of

295 case idris_outputmode i of

267− IdeSlave n ->

296+ IdeSlave n h ->

268− runIO . hPutStrLn stdout $

297+ runIO . hPutStrLn h $

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

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

270 _ -> return ()

299 _ -> return ()

271− ihRenderError stdout $ pprintErr ist e)

300+ iRenderError $ pprintErr ist e)

272 Success cmd -> idrisCatch

301 Success cmd -> idrisCatch

273 (ideslaveProcess fn cmd)

302 (ideslaveProcess fn cmd)

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

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

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

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

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

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

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

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

278 IdeSlave.toSExp (map replacement compls,

307 IdeSlave.toSExp (map replacement compls,

279 reverse unused)]

308 reverse unused)]

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

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

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

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

282 do i <- getIState

311 do i <- getIState

283 clearErr

312 clearErr

284 putIState (orig { idris_options = idris_options i,

313 putIState (orig { idris_options = idris_options i,

285− idris_outputmode = (IdeSlave id) })

314+ idris_outputmode = (IdeSlave id h) })

286− loadInputs stdout [filename] toline

315+ loadInputs [filename] toline

287 isetPrompt (mkPrompt [filename])

316 isetPrompt (mkPrompt [filename])

288 -- Report either success or failure

317 -- Report either success or failure

289 i <- getIState

318 i <- getIState

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

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

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

294 IdeSlave.toSExp fc])

323 IdeSlave.toSExp fc])

295 (idris_parsedSpan i)

324 (idris_parsedSpan i)

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

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

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

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

298− ideslave orig [filename]

327+ ideslave h orig [filename]

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

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

300 case splitName name of

329 case splitName name of

301 Left err -> iPrintError err

330 Left err -> iPrintError err

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

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

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

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

304 where splitName :: String -> Either String Name

333 where splitName :: String -> Either String Name

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

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

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

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

307 [n] -> Right $ sUN n

336 [n] -> Right $ sUN n

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

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

310 case parseConst orig name of

339 case parseConst orig name of

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

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

312 Failure _ ->

341 Failure _ ->

313 case splitName name of

342 case splitName name of

314 Left err -> iPrintError err

343 Left err -> iPrintError err

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

329 case splitName name of

358 case splitName name of

330 Left err -> iPrintError err

359 Left err -> iPrintError err

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

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

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

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

333− process stdout fn (Apropos a)

362+ process fn (Apropos a)

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

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

335 do ist <- getIState

364 do ist <- getIState

336 let opts = idris_options ist

365 let opts = idris_options ist

337 let impshow = opt_showimp opts

366 let impshow = opt_showimp opts

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

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

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

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

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

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

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

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

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

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

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

344 do setImpShow b

373 do setImpShow b

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

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

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

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

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

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

348 do setErrContext b

377 do setErrContext b

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

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

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

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

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

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

352 do ist <- getIState

381 do ist <- getIState

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

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

354 let ppo = ppOptionIst ist

383 let ppo = ppOptionIst ist

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

364 (zip bnds hs),

393 (zip bnds hs),

365 render ist bnd c pc))

394 render ist bnd c pc))

366 splitMvs

395 splitMvs

367− runIO . putStrLn $

396+ runIO . hPutStrLn h $

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

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

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

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

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

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

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

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

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

410 (show n , out, spans)

439 (show n , out, spans)

411

440

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

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

413 case splitName n of

442 case splitName n of

414 Left err -> iPrintError err

443 Left err -> iPrintError err

415 Right n -> do calls <- whoCalls n

444 Right n -> do calls <- whoCalls n

416 ist <- getIState

445 ist <- getIState

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

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

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

447 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

420 where pn ist = displaySpans .

449 where pn ist = displaySpans .

421 renderPretty 0.9 1000 .

450 renderPretty 0.9 1000 .

422 fmap (fancifyAnnots ist) .

451 fmap (fancifyAnnots ist) .

423 prettyName True True []

452 prettyName True True []

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

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

425 case splitName n of

454 case splitName n of

426 Left err -> iPrintError err

455 Left err -> iPrintError err

427 Right n -> do calls <- callsWho n

456 Right n -> do calls <- callsWho n

428 ist <- getIState

457 ist <- getIState

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

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

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

459 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

432 where pn ist = displaySpans .

461 where pn ist = displaySpans .

433 renderPretty 0.9 1000 .

462 renderPretty 0.9 1000 .

434 fmap (fancifyAnnots ist) .

463 fmap (fancifyAnnots ist) .

435 prettyName True True []

464 prettyName True True []

436

465

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

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

438 do ctxt <- getContext

467 do ctxt <- getContext

439 ist <- getIState

468 ist <- getIState

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

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

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

448 displaySpans .

477 displaySpans .

449 renderPretty 0.9 80 .

478 renderPretty 0.9 80 .

450 fmap (fancifyAnnots ist) $ ptm)

479 fmap (fancifyAnnots ist) $ ptm)

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

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

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

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

453− ideSlaveForceTermImplicits id bnd True tm

482+ ideSlaveForceTermImplicits h id bnd True tm

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

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

455− ideSlaveForceTermImplicits id bnd False tm

484+ ideSlaveForceTermImplicits h id bnd False tm

456

485

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

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

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

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

459−ideSlaveForceTermImplicits id bnd impl tm =

488+ideSlaveForceTermImplicits h id bnd impl tm =

460 do ist <- getIState

489 do ist <- getIState

461 let expl = annotate (AnnTerm bnd tm)

490 let expl = annotate (AnnTerm bnd tm)

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

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

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

466 displaySpans .

495 displaySpans .

467 renderPretty 0.9 80 .

496 renderPretty 0.9 80 .

468 fmap (fancifyAnnots ist) $ expl)

497 fmap (fancifyAnnots ist) $ expl)

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

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

470

499

471splitName :: String -> Either String Name

500splitName :: String -> Either String Name

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

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

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

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

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

476

505

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

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

478−ideslaveProcess fn Warranty = process stdout fn Warranty

507+ideslaveProcess fn Warranty = process fn Warranty

479−ideslaveProcess fn Help = process stdout fn Help

508+ideslaveProcess fn Help = process fn Help

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

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

481 iPrintResult "changed directory to"

510 iPrintResult "changed directory to"

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

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

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

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

484 iPrintResult "defined"

513 iPrintResult "defined"

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

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

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

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

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

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

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

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

489−ideslaveProcess fn Universes = process stdout fn Universes

518+ideslaveProcess fn Universes = process fn Universes

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

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

491 iPrintResult ""

520 iPrintResult ""

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

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

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

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

494 iPrintResult ""

523 iPrintResult ""

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

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

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

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

497-- RmProof and AddProof not supported!

526-- RmProof and AddProof not supported!

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

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

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

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

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

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

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

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

502

531

503−ideslaveProcess fn Execute = do process stdout fn Execute

532+ideslaveProcess fn Execute = do process fn Execute

504 iPrintResult ""

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

506 iPrintResult ""

535 iPrintResult ""

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

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

508 iPrintResult ""

537 iPrintResult ""

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

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

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

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

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

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

512 iPrintResult ""

541 iPrintResult ""

513−ideslaveProcess fn ListDynamic = do process stdout fn ListDynamic

542+ideslaveProcess fn ListDynamic = do process fn ListDynamic

514 iPrintResult ""

543 iPrintResult ""

515−ideslaveProcess fn Metavars = process stdout fn Metavars

544+ideslaveProcess fn Metavars = process fn Metavars

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

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

517 iPrintResult ""

546 iPrintResult ""

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

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

519 iPrintResult ""

548 iPrintResult ""

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

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

521 iPrintResult ""

550 iPrintResult ""

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

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

523 iPrintResult ""

552 iPrintResult ""

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

553+ideslaveProcess fn (SetOpt ShowOrigErr) = do process fn (SetOpt ShowOrigErr)

525 iPrintResult ""

554 iPrintResult ""

526−ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process stdout fn (UnsetOpt ShowOrigErr)

555+ideslaveProcess fn (UnsetOpt ShowOrigErr) = do process fn (UnsetOpt ShowOrigErr)

527 iPrintResult ""

556 iPrintResult ""

528−ideslaveProcess fn (SetOpt x) = process stdout fn (SetOpt x)

557+ideslaveProcess fn (SetOpt x) = process fn (SetOpt x)

529−ideslaveProcess fn (UnsetOpt x) = process stdout fn (UnsetOpt x)

558+ideslaveProcess fn (UnsetOpt x) = process fn (UnsetOpt x)

530−ideslaveProcess fn (CaseSplitAt False pos str) = process stdout fn (CaseSplitAt False pos str)

559+ideslaveProcess fn (CaseSplitAt False pos str) = process fn (CaseSplitAt False pos str)

531−ideslaveProcess fn (AddProofClauseFrom False pos str) = process stdout fn (AddProofClauseFrom False pos str)

560+ideslaveProcess fn (AddProofClauseFrom False pos str) = process fn (AddProofClauseFrom False pos str)

532−ideslaveProcess fn (AddClauseFrom False pos str) = process stdout fn (AddClauseFrom False pos str)

561+ideslaveProcess fn (AddClauseFrom False pos str) = process fn (AddClauseFrom False pos str)

533−ideslaveProcess fn (AddMissing False pos str) = process stdout fn (AddMissing False pos str)

562+ideslaveProcess fn (AddMissing False pos str) = process fn (AddMissing False pos str)

534−ideslaveProcess fn (MakeWith False pos str) = process stdout fn (MakeWith False pos str)

563+ideslaveProcess fn (MakeWith False pos str) = process fn (MakeWith False pos str)

535−ideslaveProcess fn (DoProofSearch False r pos str xs) = process stdout fn (DoProofSearch False r pos str xs)

564+ideslaveProcess fn (DoProofSearch False r pos str xs) = process fn (DoProofSearch False r pos str xs)

536−ideslaveProcess fn (SetConsoleWidth w) = do process stdout fn (SetConsoleWidth w)

565+ideslaveProcess fn (SetConsoleWidth w) = do process fn (SetConsoleWidth w)

537 iPrintResult ""

566 iPrintResult ""

538−ideslaveProcess fn (Apropos a) = do process stdout fn (Apropos a)

567+ideslaveProcess fn (Apropos a) = do process fn (Apropos a)

539 iPrintResult ""

568 iPrintResult ""

540−ideslaveProcess fn (WhoCalls n) = process stdout fn (WhoCalls n)

569+ideslaveProcess fn (WhoCalls n) = process fn (WhoCalls n)

541−ideslaveProcess fn (CallsWho n) = process stdout fn (CallsWho n)

570+ideslaveProcess fn (CallsWho n) = process fn (CallsWho n)

542ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

571ideslaveProcess fn _ = iPrintError "command not recognized or not supported"

543

572

544

573

@@ -570,18 +599,18 @@ processInput cmd orig inputs

570 , idris_colourTheme = idris_colourTheme i

599 , idris_colourTheme = idris_colourTheme i

571 }

600 }

572 clearErr

601 clearErr

573− mods <- loadInputs stdout inputs Nothing

602+ mods <- loadInputs inputs Nothing

574 return (Just inputs)

603 return (Just inputs)

575 Success (Load f toline) ->

604 Success (Load f toline) ->

576 do putIState orig { idris_options = idris_options i

605 do putIState orig { idris_options = idris_options i

577 , idris_colourTheme = idris_colourTheme i

606 , idris_colourTheme = idris_colourTheme i

578 }

607 }

579 clearErr

608 clearErr

580− mod <- loadInputs stdout [f] toline

609+ mod <- loadInputs [f] toline

581 return (Just [f])

610 return (Just [f])

582 Success (ModImport f) ->

611 Success (ModImport f) ->

583 do clearErr

612 do clearErr

584− fmod <- loadModule stdout f

613+ fmod <- loadModule f

585 return (Just (inputs ++ [fmod]))

614 return (Just (inputs ++ [fmod]))

586 Success Edit -> do -- takeMVar stvar

615 Success Edit -> do -- takeMVar stvar

587 edit fn orig

616 edit fn orig

@@ -590,7 +619,7 @@ processInput cmd orig inputs

590 return (Just inputs)

619 return (Just inputs)

591 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

620 Success Quit -> do when (not quiet) (iputStrLn "Bye bye")

592 return Nothing

621 return Nothing

593− Success cmd -> do idrisCatch (process stdout fn cmd)

622+ Success cmd -> do idrisCatch (process fn cmd)

594 (\e -> do msg <- showErr e ; iputStrLn msg)

623 (\e -> do msg <- showErr e ; iputStrLn msg)

595 return (Just inputs)

624 return (Just inputs)

596

625

@@ -626,7 +655,7 @@ edit f orig

626 putIState $ orig { idris_options = idris_options i

655 putIState $ orig { idris_options = idris_options i

627 , idris_colourTheme = idris_colourTheme i

656 , idris_colourTheme = idris_colourTheme i

628 }

657 }

629− loadInputs stdout [f] Nothing

658+ loadInputs [f] Nothing

630-- clearOrigPats

659-- clearOrigPats

631 iucheck

660 iucheck

632 return ()

661 return ()

@@ -652,13 +681,13 @@ insertScript prf (p@"---------- Proofs ----------" : "" : xs)

652 = p : "" : prf : xs

681 = p : "" : prf : xs

653insertScript prf (x : xs) = x : insertScript prf xs

682insertScript prf (x : xs) = x : insertScript prf xs

654

683

655−process :: Handle -> FilePath -> Command -> Idris ()

684+process :: FilePath -> Command -> Idris ()

656−process h fn Help = iPrintResult displayHelp

685+process fn Help = iPrintResult displayHelp

657−process h fn Warranty = iPrintResult warranty

686+process fn Warranty = iPrintResult warranty

658−process h fn (ChangeDirectory f)

687+process fn (ChangeDirectory f)

659 = do runIO $ setCurrentDirectory f

688 = do runIO $ setCurrentDirectory f

660 return ()

689 return ()

661−process h fn (Eval t)

690+process fn (Eval t)

662 = withErrorReflection $ do logLvl 5 $ show t

691 = withErrorReflection $ do logLvl 5 $ show t

663 (tm, ty) <- elabVal recinfo ERHS t

692 (tm, ty) <- elabVal recinfo ERHS t

664 ctxt <- getContext

693 ctxt <- getContext

@@ -671,10 +700,10 @@ process h fn (Eval t)

671 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

700 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

672 let tmDoc = pprintDelab ist tm'

701 let tmDoc = pprintDelab ist tm'

673 tyDoc = pprintDelab ist ty'

702 tyDoc = pprintDelab ist ty'

674− ihPrintTermWithType h tmDoc tyDoc

703+ iPrintTermWithType tmDoc tyDoc

675

704

676

705

677−process h fn (NewDefn decls) = do

706+process fn (NewDefn decls) = do

678 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))

707 logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))

679 mapM_ defineName namedGroups where

708 mapM_ defineName namedGroups where

680 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

709 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

@@ -732,7 +761,7 @@ process h fn (NewDefn decls) = do

732 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

761 PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

733 fixClauses decl = decl

762 fixClauses decl = decl

734

763

735−process h fn (Undefine names) = undefine names

764+process fn (Undefine names) = undefine names

736 where

765 where

737 undefine :: [Name] -> Idris ()

766 undefine :: [Name] -> Idris ()

738 undefine [] = do

767 undefine [] = do

@@ -741,7 +770,7 @@ process h fn (Undefine names) = undefine names

741 -- Keep track of which names you've removed so you can

770 -- Keep track of which names you've removed so you can

742 -- print them out to the user afterward

771 -- print them out to the user afterward

743 undefine names = undefine' names []

772 undefine names = undefine' names []

744− undefine' [] list = do ihputStrLn h (show list)

773+ undefine' [] list = do iputStrLn (show list)

745 return ()

774 return ()

746 undefine' (n:names) already = do

775 undefine' (n:names) already = do

747 allDefined <- idris_repl_defs `fmap` get

776 allDefined <- idris_repl_defs `fmap` get

@@ -764,7 +793,7 @@ process h fn (Undefine names) = undefine names

764

793

765

794

766

795

767−process h fn (ExecVal t)

796+process fn (ExecVal t)

768 = do ctxt <- getContext

797 = do ctxt <- getContext

769 ist <- getIState

798 ist <- getIState

770 (tm, ty) <- elabVal recinfo ERHS t

799 (tm, ty) <- elabVal recinfo ERHS t

@@ -773,19 +802,19 @@ process h fn (ExecVal t)

773 res <- execute tm

802 res <- execute tm

774 let (resOut, tyOut) = (prettyIst ist (delab ist res),

803 let (resOut, tyOut) = (prettyIst ist (delab ist res),

775 prettyIst ist (delab ist ty'))

804 prettyIst ist (delab ist ty'))

776− ihPrintTermWithType h resOut tyOut

805+ iPrintTermWithType resOut tyOut

777

806

778−process h fn (Check (PRef _ n))

807+process fn (Check (PRef _ n))

779 = do ctxt <- getContext

808 = do ctxt <- getContext

780 ist <- getIState

809 ist <- getIState

781 let ppo = ppOptionIst ist

810 let ppo = ppOptionIst ist

782 case lookupNames n ctxt of

811 case lookupNames n ctxt of

783 ts@(t:_) ->

812 ts@(t:_) ->

784 case lookup t (idris_metavars ist) of

813 case lookup t (idris_metavars ist) of

785− Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

814+ Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $

786 showMetavarInfo ppo ist n i

815 showMetavarInfo ppo ist n i

787− Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

816+ Nothing -> iPrintFunTypes [] n (map (\n -> (n, delabTy ist n)) ts)

788− [] -> ihPrintError h $ "No such variable " ++ show n

817+ [] -> iPrintError $ "No such variable " ++ show n

789 where

818 where

790 showMetavarInfo ppo ist n i

819 showMetavarInfo ppo ist n i

791 = case lookupTy n (tt_ctxt ist) of

820 = case lookupTy n (tt_ctxt ist) of

@@ -810,7 +839,7 @@ process h fn (Check (PRef _ n))

810 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

839 tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

811

840

812

841

813−process h fn (Check t)

842+process fn (Check t)

814 = do (tm, ty) <- elabVal recinfo ERHS t

843 = do (tm, ty) <- elabVal recinfo ERHS t

815 ctxt <- getContext

844 ctxt <- getContext

816 ist <- getIState

845 ist <- getIState

@@ -818,24 +847,24 @@ process h fn (Check t)

818 ty' = normaliseC ctxt [] ty

847 ty' = normaliseC ctxt [] ty

819 case tm of

848 case tm of

820 TType _ ->

849 TType _ ->

821− ihPrintTermWithType h (prettyIst ist PType) type1Doc

850+ iPrintTermWithType (prettyIst ist PType) type1Doc

822− _ -> ihPrintTermWithType h (pprintDelab ist tm)

851+ _ -> iPrintTermWithType (pprintDelab ist tm)

823− (pprintDelab ist ty)

852+ (pprintDelab ist ty)

824

853

825−process h fn (DocStr (Left n))

854+process fn (DocStr (Left n))

826 = do ist <- getIState

855 = do ist <- getIState

827 case lookupCtxtName n (idris_docstrings ist) of

856 case lookupCtxtName n (idris_docstrings ist) of

828 [] -> iPrintError $ "No documentation for " ++ show n

857 [] -> iPrintError $ "No documentation for " ++ show n

829 ns -> do toShow <- mapM (showDoc ist) ns

858 ns -> do toShow <- mapM (showDoc ist) ns

830− ihRenderResult h (vsep toShow)

859+ iRenderResult (vsep toShow)

831 where showDoc ist (n, d) = do doc <- getDocs n

860 where showDoc ist (n, d) = do doc <- getDocs n

832 return $ pprintDocs ist doc

861 return $ pprintDocs ist doc

833

862

834−process h fn (DocStr (Right c))

863+process fn (DocStr (Right c))

835 = do ist <- getIState

864 = do ist <- getIState

836− ihRenderResult h $ pprintConstDocs ist c (constDocs c)

865+ iRenderResult $ pprintConstDocs ist c (constDocs c)

837

866

838−process h fn Universes

867+process fn Universes

839 = do i <- getIState

868 = do i <- getIState

840 let cs = idris_constraints i

869 let cs = idris_constraints i

841-- iputStrLn $ showSep "\n" (map show cs)

870-- iputStrLn $ showSep "\n" (map show cs)

@@ -845,7 +874,7 @@ process h fn Universes

845 case ucheck cs of

874 case ucheck cs of

846 Error e -> iPrintError $ pshow i e

875 Error e -> iPrintError $ pshow i e

847 OK _ -> iPrintResult "Universes OK"

876 OK _ -> iPrintResult "Universes OK"

848−process h fn (Defn n)

877+process fn (Defn n)

849 = do i <- getIState

878 = do i <- getIState

850 iputStrLn "Compiled patterns:\n"

879 iputStrLn "Compiled patterns:\n"

851 iputStrLn $ show (lookupDef n (tt_ctxt i))

880 iputStrLn $ show (lookupDef n (tt_ctxt i))

@@ -860,20 +889,20 @@ process h fn (Defn n)

860 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

889 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

861 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

890 in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

862 showTm i' (delab i rhs))

891 showTm i' (delab i rhs))

863−process h fn (TotCheck n)

892+process fn (TotCheck n)

864 = do i <- getIState

893 = do i <- getIState

865 case lookupNameTotal n (tt_ctxt i) of

894 case lookupNameTotal n (tt_ctxt i) of

866− [] -> ihPrintError h $ "Unknown operator " ++ show n

895+ [] -> iPrintError $ "Unknown operator " ++ show n

867 ts -> do ist <- getIState

896 ts -> do ist <- getIState

868 c <- colourise

897 c <- colourise

869 let ppo = ppOptionIst ist

898 let ppo = ppOptionIst ist

870 let showN = showName (Just ist) [] ppo c

899 let showN = showName (Just ist) [] ppo c

871− ihPrintResult h . concat . intersperse "\n" .

900+ iPrintResult . concat . intersperse "\n" .

872 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

901 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

873 ts

902 ts

874

903

875

904

876−process h fn (DebugInfo n)

905+process fn (DebugInfo n)

877 = do i <- getIState

906 = do i <- getIState

878 let oi = lookupCtxtName n (idris_optimisation i)

907 let oi = lookupCtxtName n (idris_optimisation i)

879 when (not (null oi)) $ iputStrLn (show oi)

908 when (not (null oi)) $ iputStrLn (show oi)

@@ -890,29 +919,29 @@ process h fn (DebugInfo n)

890 iputStrLn $ "Size change: " ++ show sc

919 iputStrLn $ "Size change: " ++ show sc

891 when (not (null cg')) $ do iputStrLn "Call graph:\n"

920 when (not (null cg')) $ do iputStrLn "Call graph:\n"

892 iputStrLn (show cg')

921 iputStrLn (show cg')

893−process h fn (Search t) = searchByType h t

922+process fn (Search t) = searchByType t

894−process h fn (CaseSplitAt updatefile l n)

923+process fn (CaseSplitAt updatefile l n)

895− = caseSplitAt h fn updatefile l n

924+ = caseSplitAt fn updatefile l n

896−process h fn (AddClauseFrom updatefile l n)

925+process fn (AddClauseFrom updatefile l n)

897− = addClauseFrom h fn updatefile l n

926+ = addClauseFrom fn updatefile l n

898−process h fn (AddProofClauseFrom updatefile l n)

927+process fn (AddProofClauseFrom updatefile l n)

899− = addProofClauseFrom h fn updatefile l n

928+ = addProofClauseFrom fn updatefile l n

900−process h fn (AddMissing updatefile l n)

929+process fn (AddMissing updatefile l n)

901− = addMissing h fn updatefile l n

930+ = addMissing fn updatefile l n

902−process h fn (MakeWith updatefile l n)

931+process fn (MakeWith updatefile l n)

903− = makeWith h fn updatefile l n

932+ = makeWith fn updatefile l n

904−process h fn (MakeLemma updatefile l n)

933+process fn (MakeLemma updatefile l n)

905− = makeLemma h fn updatefile l n

934+ = makeLemma fn updatefile l n

906−process h fn (DoProofSearch updatefile rec l n hints)

935+process fn (DoProofSearch updatefile rec l n hints)

907− = doProofSearch h fn updatefile rec l n hints Nothing

936+ = doProofSearch fn updatefile rec l n hints Nothing

908−process h fn (Spec t)

937+process fn (Spec t)

909 = do (tm, ty) <- elabVal recinfo ERHS t

938 = do (tm, ty) <- elabVal recinfo ERHS t

910 ctxt <- getContext

939 ctxt <- getContext

911 ist <- getIState

940 ist <- getIState

912 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

941 let tm' = simplify ctxt [] {- (idris_statics ist) -} tm

913 iPrintResult (show (delab ist tm'))

942 iPrintResult (show (delab ist tm'))

914

943

915−process h fn (RmProof n')

944+process fn (RmProof n')

916 = do i <- getIState

945 = do i <- getIState

917 n <- resolveProof n'

946 n <- resolveProof n'

918 let proofs = proof_list i

947 let proofs = proof_list i

@@ -928,7 +957,7 @@ process h fn (RmProof n')

928 let ms = idris_metavars i

957 let ms = idris_metavars i

929 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

958 putIState $ i { idris_metavars = (n, (Nothing, 0, False)) : ms }

930

959

931−process h fn' (AddProof prf)

960+process fn' (AddProof prf)

932 = do fn <- do

961 = do fn <- do

933 let fn'' = takeWhile (/= ' ') fn'

962 let fn'' = takeWhile (/= ' ') fn'

934 ex <- runIO $ doesFileExist fn''

963 ex <- runIO $ doesFileExist fn''

@@ -958,7 +987,7 @@ process h fn' (AddProof prf)

958 iputStrLn $ "Added proof " ++ show n

987 iputStrLn $ "Added proof " ++ show n

959 where ls = (lines prog)

988 where ls = (lines prog)

960

989

961−process h fn (ShowProof n')

990+process fn (ShowProof n')

962 = do i <- getIState

991 = do i <- getIState

963 n <- resolveProof n'

992 n <- resolveProof n'

964 let proofs = proof_list i

993 let proofs = proof_list i

@@ -966,7 +995,7 @@ process h fn (ShowProof n')

966 Nothing -> iPrintError "No proof to show"

995 Nothing -> iPrintError "No proof to show"

967 Just p -> iPrintResult $ showProof False n p

996 Just p -> iPrintResult $ showProof False n p

968

997

969−process h fn (Prove n')

998+process fn (Prove n')

970 = do ctxt <- getContext

999 = do ctxt <- getContext

971 ist <- getIState

1000 ist <- getIState

972 let ns = lookupNames n' ctxt

1001 let ns = lookupNames n' ctxt

@@ -984,20 +1013,20 @@ process h fn (Prove n')

984 mapM_ checkDeclTotality (idris_totcheck i)

1013 mapM_ checkDeclTotality (idris_totcheck i)

985 warnTotality

1014 warnTotality

986

1015

987−process h fn (HNF t)

1016+process fn (HNF t)

988 = do (tm, ty) <- elabVal recinfo ERHS t

1017 = do (tm, ty) <- elabVal recinfo ERHS t

989 ctxt <- getContext

1018 ctxt <- getContext

990 ist <- getIState

1019 ist <- getIState

991 let tm' = hnf ctxt [] tm

1020 let tm' = hnf ctxt [] tm

992 iPrintResult (show (delab ist tm'))

1021 iPrintResult (show (delab ist tm'))

993−process h fn (TestInline t)

1022+process fn (TestInline t)

994 = do (tm, ty) <- elabVal recinfo ERHS t

1023 = do (tm, ty) <- elabVal recinfo ERHS t

995 ctxt <- getContext

1024 ctxt <- getContext

996 ist <- getIState

1025 ist <- getIState

997 let tm' = inlineTerm ist tm

1026 let tm' = inlineTerm ist tm

998 c <- colourise

1027 c <- colourise

999 iPrintResult (showTm ist (delab ist tm'))

1028 iPrintResult (showTm ist (delab ist tm'))

1000−process h fn Execute

1029+process fn Execute

1001 = idrisCatch

1030 = idrisCatch

1002 (do ist <- getIState

1031 (do ist <- getIState

1003 (m, _) <- elabVal recinfo ERHS

1032 (m, _) <- elabVal recinfo ERHS

@@ -1009,33 +1038,33 @@ process h fn Execute

1009 t <- codegen

1038 t <- codegen

1010 compile t tmpn m

1039 compile t tmpn m

1011 case idris_outputmode ist of

1040 case idris_outputmode ist of

1012− RawOutput -> do runIO $ system tmpn

1041+ RawOutput h -> do runIO $ system tmpn

1013− return ()

1042+ return ()

1014− IdeSlave n -> runIO . hPutStrLn h $

1043+ IdeSlave n h -> runIO . hPutStrLn h $

1015− IdeSlave.convSExp "run-program" tmpn n)

1044+ IdeSlave.convSExp "run-program" tmpn n)

1016− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

1045+ (\e -> getIState >>= iRenderError . flip pprintErr e)

1017 where fc = fileFC "main"

1046 where fc = fileFC "main"

1018−process h fn (Compile codegen f)

1047+process fn (Compile codegen f)

1019 = do (m, _) <- elabVal recinfo ERHS

1048 = do (m, _) <- elabVal recinfo ERHS

1020 (PApp fc (PRef fc (sUN "run__IO"))

1049 (PApp fc (PRef fc (sUN "run__IO"))

1021 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1050 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1022 compile codegen f m

1051 compile codegen f m

1023 where fc = fileFC "main"

1052 where fc = fileFC "main"

1024−process h fn (LogLvl i) = setLogLevel i

1053+process fn (LogLvl i) = setLogLevel i

1025-- Elaborate as if LHS of a pattern (debug command)

1054-- Elaborate as if LHS of a pattern (debug command)

1026−process h fn (Pattelab t)

1055+process fn (Pattelab t)

1027 = do (tm, ty) <- elabVal recinfo ELHS t

1056 = do (tm, ty) <- elabVal recinfo ELHS t

1028 iPrintResult $ show tm ++ "\n\n : " ++ show ty

1057 iPrintResult $ show tm ++ "\n\n : " ++ show ty

1029

1058

1030−process h fn (Missing n)

1059+process fn (Missing n)

1031 = do i <- getIState

1060 = do i <- getIState

1032 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

1061 let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

1033 case lookupCtxt n (idris_patdefs i) of

1062 case lookupCtxt n (idris_patdefs i) of

1034− [] -> ihPrintError h $ "Unknown operator " ++ show n

1063+ [] -> iPrintError $ "Unknown operator " ++ show n

1035 [(_, tms)] ->

1064 [(_, tms)] ->

1036 iPrintResult (showSep "\n" (map (showTm i') tms))

1065 iPrintResult (showSep "\n" (map (showTm i') tms))

1037 _ -> iPrintError $ "Ambiguous name"

1066 _ -> iPrintError $ "Ambiguous name"

1038−process h fn (DynamicLink l)

1067+process fn (DynamicLink l)

1039 = do i <- getIState

1068 = do i <- getIState

1040 let importdirs = opt_importdirs (idris_options i)

1069 let importdirs = opt_importdirs (idris_options i)

1041 lib = trim l

1070 lib = trim l

@@ -1048,80 +1077,80 @@ process h fn (DynamicLink l)

1048 return ()

1077 return ()

1049 else putIState $ i { idris_dynamic_libs = x:libs }

1078 else putIState $ i { idris_dynamic_libs = x:libs }

1050 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1079 where trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace

1051−process h fn ListDynamic

1080+process fn ListDynamic

1052 = do i <- getIState

1081 = do i <- getIState

1053 iputStrLn "Dynamic libraries:"

1082 iputStrLn "Dynamic libraries:"

1054 showLibs $ idris_dynamic_libs i

1083 showLibs $ idris_dynamic_libs i

1055 where showLibs [] = return ()

1084 where showLibs [] = return ()

1056 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

1085 showLibs ((Lib name _):ls) = do iputStrLn $ "\t" ++ name; showLibs ls

1057−process h fn Metavars

1086+process fn Metavars

1058 = do ist <- getIState

1087 = do ist <- getIState

1059 let mvs = map fst (idris_metavars ist) \\ primDefs

1088 let mvs = map fst (idris_metavars ist) \\ primDefs

1060 case mvs of

1089 case mvs of

1061 [] -> iPrintError "No global metavariables to solve"

1090 [] -> iPrintError "No global metavariables to solve"

1062 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

1091 _ -> iPrintResult $ "Global metavariables:\n\t" ++ show mvs

1063−process h fn NOP = return ()

1092+process fn NOP = return ()

1064−

1093+

1065−process h fn (SetOpt ErrContext) = setErrContext True

1094+process fn (SetOpt ErrContext) = setErrContext True

1066−process h fn (UnsetOpt ErrContext) = setErrContext False

1095+process fn (UnsetOpt ErrContext) = setErrContext False

1067−process h fn (SetOpt ShowImpl) = setImpShow True

1096+process fn (SetOpt ShowImpl) = setImpShow True

1068−process h fn (UnsetOpt ShowImpl) = setImpShow False

1097+process fn (UnsetOpt ShowImpl) = setImpShow False

1069−process h fn (SetOpt ShowOrigErr) = setShowOrigErr True

1098+process fn (SetOpt ShowOrigErr) = setShowOrigErr True

1070−process h fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1099+process fn (UnsetOpt ShowOrigErr) = setShowOrigErr False

1071−process h fn (SetOpt AutoSolve) = setAutoSolve True

1100+process fn (SetOpt AutoSolve) = setAutoSolve True

1072−process h fn (UnsetOpt AutoSolve) = setAutoSolve False

1101+process fn (UnsetOpt AutoSolve) = setAutoSolve False

1073−process h fn (SetOpt NoBanner) = setNoBanner True

1102+process fn (SetOpt NoBanner) = setNoBanner True

1074−process h fn (UnsetOpt NoBanner) = setNoBanner False

1103+process fn (UnsetOpt NoBanner) = setNoBanner False

1075−process h fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1104+process fn (SetOpt WarnReach) = fmodifyState opts_idrisCmdline $ nub . (WarnReach:)

1076−process h fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1105+process fn (UnsetOpt WarnReach) = fmodifyState opts_idrisCmdline $ delete WarnReach

1077−

1106+

1078−process h fn (SetOpt _) = iPrintError "Not a valid option"

1107+process fn (SetOpt _) = iPrintError "Not a valid option"

1079−process h fn (UnsetOpt _) = iPrintError "Not a valid option"

1108+process fn (UnsetOpt _) = iPrintError "Not a valid option"

1080−process h fn (SetColour ty c) = setColour ty c

1109+process fn (SetColour ty c) = setColour ty c

1081−process h fn ColourOn

1110+process fn ColourOn

1082 = do ist <- getIState

1111 = do ist <- getIState

1083 putIState $ ist { idris_colourRepl = True }

1112 putIState $ ist { idris_colourRepl = True }

1084−process h fn ColourOff

1113+process fn ColourOff

1085 = do ist <- getIState

1114 = do ist <- getIState

1086 putIState $ ist { idris_colourRepl = False }

1115 putIState $ ist { idris_colourRepl = False }

1087−process h fn ListErrorHandlers =

1116+process fn ListErrorHandlers =

1088 do ist <- getIState

1117 do ist <- getIState

1089 iPrintResult $ case idris_errorhandlers ist of

1118 iPrintResult $ case idris_errorhandlers ist of

1090 [] -> "No registered error handlers"

1119 [] -> "No registered error handlers"

1091 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

1120 handlers -> "Registered error handlers: " ++ (concat . intersperse ", " . map show) handlers

1092−process h fn (SetConsoleWidth w) = setWidth w

1121+process fn (SetConsoleWidth w) = setWidth w

1093

1122

1094−process h fn (Apropos a) =

1123+process fn (Apropos a) =

1095 do ist <- getIState

1124 do ist <- getIState

1096 let names = apropos ist (T.pack a)

1125 let names = apropos ist (T.pack a)

1097 let aproposInfo = [ (n,

1126 let aproposInfo = [ (n,

1098 delabTy ist n,

1127 delabTy ist n,

1099 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1128 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1100 | n <- sort names, isUN n ]

1129 | n <- sort names, isUN n ]

1101− ihRenderResult h $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1130+ iRenderResult $ vsep (map (prettyDocumentedIst ist) aproposInfo)

1102 where isUN (UN _) = True

1131 where isUN (UN _) = True

1103 isUN (NS n _) = isUN n

1132 isUN (NS n _) = isUN n

1104 isUN _ = False

1133 isUN _ = False

1105

1134

1106−process h fn (WhoCalls n) =

1135+process fn (WhoCalls n) =

1107 do calls <- whoCalls n

1136 do calls <- whoCalls n

1108 ist <- getIState

1137 ist <- getIState

1109− ihRenderResult h . vsep $

1138+ iRenderResult . vsep $

1110 map (\(n, ns) ->

1139 map (\(n, ns) ->

1111 text "Callers of" <+> prettyName True True [] n <$>

1140 text "Callers of" <+> prettyName True True [] n <$>

1112 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

1141 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

1113 calls

1142 calls

1114

1143

1115−process h fn (CallsWho n) =

1144+process fn (CallsWho n) =

1116 do calls <- callsWho n

1145 do calls <- callsWho n

1117 ist <- getIState

1146 ist <- getIState

1118− ihRenderResult h . vsep $

1147+ iRenderResult . vsep $

1119 map (\(n, ns) ->

1148 map (\(n, ns) ->

1120 prettyName True True [] n <+> text "calls:" <$>

1149 prettyName True True [] n <+> text "calls:" <$>

1121 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

1150 indent 1 (vsep (map ((text "*" <+>) . align . prettyName True True []) ns)))

1122 calls

1151 calls

1123-- IdrisDoc

1152-- IdrisDoc

1124−process h fn (MakeDoc s) =

1153+process fn (MakeDoc s) =

1125 do istate <- getIState

1154 do istate <- getIState

1126 let names = words s

1155 let names = words s

1127 parse n | Success x <- runparser name istate fn n = Right x

1156 parse n | Success x <- runparser name istate fn n = Right x

@@ -1178,8 +1207,8 @@ idris opts = do res <- runErrorT $ execStateT totalMain idrisInit

1178 [] -> return ()

1207 [] -> return ()

1179

1208

1180

1209

1181−loadInputs :: Handle -> [FilePath] -> Maybe Int -> Idris ()

1210+loadInputs :: [FilePath] -> Maybe Int -> Idris ()

1182−loadInputs h inputs toline -- furthest line to read in input source files

1211+loadInputs inputs toline -- furthest line to read in input source files

1183 = idrisCatch

1212 = idrisCatch

1184 (do ist <- getIState

1213 (do ist <- getIState

1185 -- if we're in --check and not outputting anything, don't bother

1214 -- 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

1231 (\e -> do i <- getIState

1260 (\e -> do i <- getIState

1232 case e of

1261 case e of

1233 At f e' -> do setErrSpan f

1262 At f e' -> do setErrSpan f

1234− ihWarn stdout f $ pprintErr i e'

1263+ iWarn f $ pprintErr i e'

1235 ProgramLineComment -> return () -- fail elsewhere

1264 ProgramLineComment -> return () -- fail elsewhere

1236 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1265 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1237− ihWarn stdout emptyFC $ pprintErr i e)

1266+ iWarn emptyFC $ pprintErr i e)

1238 where -- load all files, stop if any fail

1267 where -- load all files, stop if any fail

1239 tryLoad :: Bool -> [IFileType] -> Idris ()

1268 tryLoad :: Bool -> [IFileType] -> Idris ()

1240 tryLoad keepstate [] = warnTotality >> return ()

1269 tryLoad keepstate [] = warnTotality >> return ()

@@ -1251,7 +1280,7 @@ loadInputs h inputs toline -- furthest line to read in input source files

1251 then Just l

1280 then Just l

1252 else Nothing

1281 else Nothing

1253 _ -> Nothing

1282 _ -> Nothing

1254− loadFromIFile h f maxline

1283+ loadFromIFile f maxline

1255 inew <- getIState

1284 inew <- getIState

1256 -- FIXME: Save these in IBC to avoid this hack! Need to

1285 -- FIXME: Save these in IBC to avoid this hack! Need to

1257 -- preserve it all from source inputs

1286 -- preserve it all from source inputs

@@ -1299,7 +1328,7 @@ idrisMain opts =

1299 do let inputs = opt getFile opts

1328 do let inputs = opt getFile opts

1300 let quiet = Quiet `elem` opts

1329 let quiet = Quiet `elem` opts

1301 let nobanner = NoBanner `elem` opts

1330 let nobanner = NoBanner `elem` opts

1302− let idesl = Ideslave `elem` opts

1331+ let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts

1303 let runrepl = not (NoREPL `elem` opts)

1332 let runrepl = not (NoREPL `elem` opts)

1304 let verbose = runrepl || Verbose `elem` opts

1333 let verbose = runrepl || Verbose `elem` opts

1305 let output = opt getOutput opts

1334 let output = opt getOutput opts

@@ -1336,7 +1365,6 @@ idrisMain opts =

1336 mapM_ addLangExt (opt getLanguageExt opts)

1365 mapM_ addLangExt (opt getLanguageExt opts)

1337 setREPL runrepl

1366 setREPL runrepl

1338 setQuiet (quiet || isJust script || not (null immediate))

1367 setQuiet (quiet || isJust script || not (null immediate))

1339− setIdeSlave idesl

1340 setVerbose verbose

1368 setVerbose verbose

1341 setCmdLine opts

1369 setCmdLine opts

1342 setOutputTy outty

1370 setOutputTy outty

@@ -1362,9 +1390,9 @@ idrisMain opts =

1362 addPkgDir "base"

1390 addPkgDir "base"

1363 mapM_ addPkgDir pkgdirs

1391 mapM_ addPkgDir pkgdirs

1364 elabPrims

1392 elabPrims

1365− when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"

1393+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule "Builtins"

1366 return ()

1394 return ()

1367− when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"

1395+ when (not (NoPrelude `elem` opts)) $ do x <- loadModule "Prelude"

1368 return ()

1396 return ()

1369

1397

1370 when (runrepl && not idesl) initScript

1398 when (runrepl && not idesl) initScript

@@ -1380,14 +1408,14 @@ idrisMain opts =

1380 iputStrLn banner

1408 iputStrLn banner

1381

1409

1382 orig <- getIState

1410 orig <- getIState

1383− loadInputs stdout inputs Nothing

1411+ when (not idesl) $ loadInputs inputs Nothing

1384

1412

1385 runIO $ hSetBuffering stdout LineBuffering

1413 runIO $ hSetBuffering stdout LineBuffering

1386

1414

1387 ok <- noErrors

1415 ok <- noErrors

1388 when ok $ case output of

1416 when ok $ case output of

1389 [] -> return ()

1417 [] -> return ()

1390− (o:_) -> idrisCatch (process stdout "" (Compile cgn o))

1418+ (o:_) -> idrisCatch (process "" (Compile cgn o))

1391 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1419 (\e -> do ist <- getIState ; iputStrLn $ pshow ist e)

1392

1420

1393 case immediate of

1421 case immediate of

@@ -1398,7 +1426,7 @@ idrisMain opts =

1398 case parseExpr ist str of

1426 case parseExpr ist str of

1399 Failure err -> do iputStrLn $ show (fixColour c err)

1427 Failure err -> do iputStrLn $ show (fixColour c err)

1400 runIO $ exitWith (ExitFailure 1)

1428 runIO $ exitWith (ExitFailure 1)

1401− Success e -> process stdout "" (Eval e))

1429+ Success e -> process "" (Eval e))

1402 exprs

1430 exprs

1403 runIO $ exitWith ExitSuccess

1431 runIO $ exitWith ExitSuccess

1404

1432

@@ -1420,7 +1448,8 @@ idrisMain opts =

1420-- clearOrigPats

1448-- clearOrigPats

1421 startServer orig inputs

1449 startServer orig inputs

1422 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1450 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1451+ let idesock = IdeslaveSocket `elem` opts

1423− when (idesl) $ ideslaveStart orig inputs

1452+ when (idesl) $ ideslaveStart idesock orig inputs

1424 ok <- noErrors

1453 ok <- noErrors

1425 when (not ok) $ runIO (exitWith (ExitFailure 1))

1454 when (not ok) $ runIO (exitWith (ExitFailure 1))

1426 where

1455 where

@@ -1482,7 +1511,7 @@ initScript = do script <- getInitScript

1482 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

1511 Success Edit -> iPrintError "Init scripts cannot invoke the editor"

1483 Success Proofs -> proofs i

1512 Success Proofs -> proofs i

1484 Success Quit -> iPrintError "Init scripts cannot quit Idris"

1513 Success Quit -> iPrintError "Init scripts cannot quit Idris"

1485− Success cmd -> process stdout [] cmd

1514+ Success cmd -> process [] cmd

1486

1515

1487getFile :: Opt -> Maybe String

1516getFile :: Opt -> Maybe String

1488getFile (Filename str) = Just str

1517getFile (Filename str) = Just str

src/Idris/TypeSearch.hs+6−8

@@ -29,14 +29,12 @@ import Idris.Core.Unify (match_unify)

29import Idris.Delaborate (delabTy)

30import Idris.Docstrings (noDocs, overview)

31import Idris.Elab.Type (elabType)

32−import Idris.Output (ihRenderOutput, ihPrintResult, ihRenderResult)

32+import Idris.Output (iRenderOutput, iPrintResult, iRenderResult)

33−

34−import System.IO (Handle)

36import Util.Pretty (text, char, vsep, (<>), Doc)

34import Util.Pretty (text, char, vsep, (<>), Doc)

38−searchByType :: Handle -> PTerm -> Idris ()

36+searchByType :: PTerm -> Idris ()

39−searchByType h pterm = do

37+searchByType pterm = do

40 pterm' <- addUsingConstraints syn emptyFC pterm

38 pterm' <- addUsingConstraints syn emptyFC pterm

41 pterm'' <- implicit toplevel syn n pterm'

39 pterm'' <- implicit toplevel syn n pterm'

42 i <- getIState

40 i <- getIState

@@ -50,9 +48,9 @@ searchByType h pterm = do

50 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

48 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

51 | (n, score) <- names']

49 | (n, score) <- names']

52 case idris_outputmode i of

50 case idris_outputmode i of

53− RawOutput -> do mapM_ (ihRenderOutput h) docs

51+ RawOutput _ -> do mapM_ iRenderOutput docs

54− ihPrintResult h ""

52+ iPrintResult ""

55− IdeSlave n -> ihRenderResult h (vsep docs)

53+ IdeSlave n h -> iRenderResult (vsep docs)

56 where

54 where

57 numLimit = 50

55 numLimit = 50

58 syn = defaultSyntax { implicitAllowed = True } -- syntax

56 syn = defaultSyntax { implicitAllowed = True } -- syntax

src/Pkg/Package.hs+1−1

@@ -144,7 +144,7 @@ documentPkg fp =

144 setCurrentDirectory $ pkgDir

145 let run l = runErrorT . (execStateT l)

146 load [] = return ()

147− load (f:fs) = do loadModule stdout f; load fs

147+ load (f:fs) = do loadModule f; load fs

148 loader = do idrisMain opts; load fs

149 idrisInstance <- run loader idrisInit

150 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)

4import Network.Socket hiding (sClose, PortNumber)

5import Network.BSD (getProtocolNumber)

6import Control.Exception (bracketOnError)

@@ -20,3 +20,16 @@ listenOnLocalhost (PortNumber port) = do

20 return sock

21 )

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

9total

10cadr : (xs : List a)

11 -> {auto cons1 : isCons xs = True}

12− -> {auto cons2 : isCons (tail xs cons1) = True}

12+ -> {auto cons2 : isCons (tail xs) = True}

13 -> a

14cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

15cadr (x :: []) {cons1=refl} {cons2=refl} impossible

test/error004/expected+1−1

@@ -3,4 +3,4 @@ When elaborating argument cons1 to function FunErrTest.cadr:

3 Could not prove that [] has at least two elements.

4FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

5When 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 @@

1module DefaultArgUnknownName

3+-- FIXME: What is the expected behaviour here? Should the type declaration

4+-- not compile?

3funWithBadDefArg : { default sadgjhsag arg : () } -> ()

5funWithBadDefArg : { 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:

1+DefaultArgUnknownName.idr:5:30:When elaborating right hand side of test:

2−Can't infer type for sadgjhsag

2+When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3+ No such variable sadgjhsag