c03fa21 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3415 from steshaw/interactive-indentation-config

c03fa21Ahmad Salim Al-Sibahi10 years ago

src/Idris/AbsSyntax.hs+69−61

compare with master

unifiedsplit

@@ -5,8 +5,8 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,

9+{-# LANGUAGE DeriveFunctor, PatternGuards #-}

9− PatternGuards, TypeSynonymInstances #-}

11module Idris.AbsSyntax(

12 module Idris.AbsSyntax

@@ -15,37 +15,32 @@ module Idris.AbsSyntax(

16import Idris.AbsSyntaxTree

17import Idris.Colours

18−import Idris.Core.Elaborate hiding (Tactic(..))

19import Idris.Core.Evaluate

18import Idris.Core.Evaluate

20import Idris.Core.TT

19import Idris.Core.TT

21−import Idris.Core.Typecheck

22import Idris.Docstrings

20import Idris.Docstrings

23import Idris.IdeMode hiding (Opt(..))

21import Idris.IdeMode hiding (Opt(..))

24import IRTS.CodegenCommon

22import IRTS.CodegenCommon

26−import Util.DynamicLinker

24+import System.Directory (canonicalizePath, doesFileExist)

27−import Util.Pretty

28−import Util.ScreenSize

29−import Util.System

25+import System.IO

31import Control.Applicative

27import Control.Applicative

32−import Control.Monad (liftM3)

33import Control.Monad.State

28import Control.Monad.State

34−import Data.Char

29+import Prelude hiding (Applicative, Foldable, Traversable, (<$>))

30+

35import Data.Either

31import Data.Either

36−import Data.Generics.Uniplate.Data (descend, descendM)

37import Data.List hiding (insert, union)

32import Data.List hiding (insert, union)

38import qualified Data.Map as M

33import qualified Data.Map as M

39import Data.Maybe

34import Data.Maybe

40import qualified Data.Set as S

35import qualified Data.Set as S

41import qualified Data.Text as T

36import qualified Data.Text as T

42−import Data.Word (Word)

43−import Debug.Trace

44−import Network (PortID(PortNumber))

45−import System.Console.Haskeline

46−import System.Directory (canonicalizePath, doesFileExist)

47−import System.IO

48−import System.IO.Error (ioeGetErrorString, isUserError, tryIOError)

37+import System.IO.Error (tryIOError)

38+

39+import Data.Generics.Uniplate.Data (descend, descendM)

40+

41+import Util.DynamicLinker

42+import Util.Pretty

43+import Util.System

50getContext :: Idris Context

45getContext :: Idris Context

51getContext = do i <- getIState; return (tt_ctxt i)

46getContext = do i <- getIState; return (tt_ctxt i)

@@ -91,9 +86,9 @@ addDyLib libs = do i <- getIState

91 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }

86 Just x -> do putIState $ i { idris_dynamic_libs = x:ls }

92 return (Left x)

87 return (Left x)

93 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib

88 where findDyLib :: [DynamicLib] -> String -> Maybe DynamicLib

94− findDyLib [] l = Nothing

89+ findDyLib [] _ = Nothing

95− findDyLib (lib:libs) l | l == lib_name lib = Just lib

90+ findDyLib (lib:libs') l | l == lib_name lib = Just lib

96− | otherwise = findDyLib libs l

91+ | otherwise = findDyLib libs' l

98getAutoImports :: Idris [FilePath]

93getAutoImports :: Idris [FilePath]

99getAutoImports = do i <- getIState

94getAutoImports = do i <- getIState

@@ -102,7 +97,6 @@ getAutoImports = do i <- getIState

102addAutoImport :: FilePath -> Idris ()

97addAutoImport :: FilePath -> Idris ()

103addAutoImport fp = do i <- getIState

98addAutoImport fp = do i <- getIState

104 let opts = idris_options i

99 let opts = idris_options i

105− let autoimps = opt_autoImport opts

106 put (i { idris_options = opts { opt_autoImport =

100 put (i { idris_options = opts { opt_autoImport =

107 fp : opt_autoImport opts } } )

101 fp : opt_autoImport opts } } )

108

102

@@ -250,7 +244,7 @@ getCoercionsTo i ty =

250 let cs = idris_coercions i

244 let cs = idris_coercions i

251 (fn,_) = unApply (getRetTy ty) in

245 (fn,_) = unApply (getRetTy ty) in

252 findCoercions fn cs

246 findCoercions fn cs

253− where findCoercions t [] = []

247+ where findCoercions _ [] = []

254 findCoercions t (n : ns) =

248 findCoercions t (n : ns) =

255 let ps = case lookupTy n (tt_ctxt i) of

249 let ps = case lookupTy n (tt_ctxt i) of

256 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of

250 [ty'] -> case unApply (getRetTy (normalise (tt_ctxt i) [] ty')) of

@@ -322,10 +316,10 @@ addTyInfConstraints fc ts = do logLvl 2 $ "TI missing: " ++ show ts

322 do let (fx, _) = unApply x

316 do let (fx, _) = unApply x

323 let (fy, _) = unApply y

317 let (fy, _) = unApply y

324 case (fx, fy) of

318 case (fx, fy) of

325− (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n)

319+ (P (TCon _ _) n _, P (TCon _ _) n' _) -> errWhen (n/=n) -- XXX: n' is unused. Should this be errWhen (n /= n')?

326 (P (TCon _ _) n _, Constant _) -> errWhen True

320 (P (TCon _ _) n _, Constant _) -> errWhen True

327 (Constant _, P (TCon _ _) n' _) -> errWhen True

321 (Constant _, P (TCon _ _) n' _) -> errWhen True

328− (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n)

322+ (P (DCon _ _ _) n _, P (DCon _ _ _) n' _) -> errWhen (n/=n) -- XXX: n' is unused. Should this be errWhen (n /= n')?

329 _ -> return ()

323 _ -> return ()

330

324

331 where errWhen True

325 where errWhen True

@@ -353,12 +347,6 @@ addFunctionErrorHandlers f arg hs =

353 -- will always be one of those two, thus no extra case

347 -- will always be one of those two, thus no extra case

354 putIState $ i { idris_function_errorhandlers = newHandlers }

348 putIState $ i { idris_function_errorhandlers = newHandlers }

355

349

356−getFunctionErrorHandlers :: Name -> Name -> Idris [Name]

357−getFunctionErrorHandlers f arg = do i <- getIState

358− return . maybe [] S.toList $

359− undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)

360−

361−

362-- | Trace all the names in a call graph starting at the given name

350-- | Trace all the names in a call graph starting at the given name

363getAllNames :: Name -> Idris [Name]

351getAllNames :: Name -> Idris [Name]

364getAllNames n = do i <- getIState

352getAllNames n = do i <- getIState

@@ -414,7 +402,7 @@ addNameHint ty n

414 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }

402 putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }

415

403

416getNameHints :: IState -> Name -> [Name]

404getNameHints :: IState -> Name -> [Name]

417−getNameHints i (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]

405+getNameHints _ (UN arr) | arr == txt "->" = [sUN "f",sUN "g"]

418getNameHints i n =

406getNameHints i n =

419 case lookupCtxt n (idris_namehints i) of

407 case lookupCtxt n (idris_namehints i) of

420 [ns] -> ns

408 [ns] -> ns

@@ -430,7 +418,6 @@ getDeprecated n = do

430 i <- getIState

418 i <- getIState

431 return $ lookupCtxtExact n (idris_deprecated i)

419 return $ lookupCtxtExact n (idris_deprecated i)

432

420

433−

434addFragile :: Name -> String -> Idris ()

421addFragile :: Name -> String -> Idris ()

435addFragile n reason = do

422addFragile n reason = do

436 i <- getIState

423 i <- getIState

@@ -442,15 +429,15 @@ getFragile n = do

442 return $ lookupCtxtExact n (idris_fragile i)

429 return $ lookupCtxtExact n (idris_fragile i)

443

430

444push_estack :: Name -> Bool -> Idris ()

431push_estack :: Name -> Bool -> Idris ()

445−push_estack n impl

432+push_estack n implementation

446 = do i <- getIState

433 = do i <- getIState

447− putIState (i { elab_stack = (n, impl) : elab_stack i })

434+ putIState (i { elab_stack = (n, implementation) : elab_stack i })

448

435

449pop_estack :: Idris ()

436pop_estack :: Idris ()

450pop_estack = do i <- getIState

437pop_estack = do i <- getIState

451 putIState (i { elab_stack = ptail (elab_stack i) })

438 putIState (i { elab_stack = ptail (elab_stack i) })

452 where ptail [] = []

439 where ptail [] = []

453− ptail (x : xs) = xs

440+ ptail (_ : xs) = xs

454

441

455-- | Add an interface implementation function.

442-- | Add an interface implementation function.

456--

443--

@@ -546,7 +533,7 @@ addIBC ibc@(IBCDef n)

546 when (notDef (ibc_write i)) $

533 when (notDef (ibc_write i)) $

547 putIState $ i { ibc_write = ibc : ibc_write i }

534 putIState $ i { ibc_write = ibc : ibc_write i }

548 where notDef [] = True

535 where notDef [] = True

549− notDef (IBCDef n': is) | n == n' = False

536+ notDef (IBCDef n': _) | n == n' = False

550 notDef (_ : is) = notDef is

537 notDef (_ : is) = notDef is

551addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

538addIBC ibc = do i <- getIState; putIState $ i { ibc_write = ibc : ibc_write i }

552

539

@@ -683,7 +670,7 @@ clearPTypes :: Idris ()

683clearPTypes = do i <- get

670clearPTypes = do i <- get

684 let ctxt = tt_ctxt i

671 let ctxt = tt_ctxt i

685 put (i { tt_ctxt = mapDefCtxt pErase ctxt })

672 put (i { tt_ctxt = mapDefCtxt pErase ctxt })

686− where pErase (CaseOp c t tys orig tot cds)

673+ where pErase (CaseOp c t tys orig _ cds)

687 = CaseOp c t tys orig [] (pErase' cds)

674 = CaseOp c t tys orig [] (pErase' cds)

688 pErase x = x

675 pErase x = x

689 pErase' (CaseDefs (cs, c) rs)

676 pErase' (CaseDefs (cs, c) rs)

@@ -699,7 +686,7 @@ checkUndefined fc n

699 _ -> return ()

686 _ -> return ()

700

687

701isUndefined :: FC -> Name -> Idris Bool

688isUndefined :: FC -> Name -> Idris Bool

702−isUndefined fc n

689+isUndefined _ n

703 = do i <- getContext

690 = do i <- getContext

704 case lookupTyExact n i of

691 case lookupTyExact n i of

705 Just _ -> return False

692 Just _ -> return False

@@ -756,7 +743,7 @@ addDeferred' nt ns

756 tidyNames used (Bind n b sc)

743 tidyNames used (Bind n b sc)

757 = let n' = uniqueNameSet n used in

744 = let n' = uniqueNameSet n used in

758 Bind n' b $ tidyNames (S.insert n' used) sc

745 Bind n' b $ tidyNames (S.insert n' used) sc

759− tidyNames used b = b

746+ tidyNames _ b = b

760

747

761solveDeferred :: FC -> Name -> Idris ()

748solveDeferred :: FC -> Name -> Idris ()

762solveDeferred fc n

749solveDeferred fc n

@@ -1144,7 +1131,6 @@ setColour ct c = do i <- getIState

1144 setColour' PromptColour c t = t { promptColour = c }

1131 setColour' PromptColour c t = t { promptColour = c }

1145 setColour' PostulateColour c t = t { postulateColour = c }

1132 setColour' PostulateColour c t = t { postulateColour = c }

1146

1133

1147−

1148logLvl :: Int -> String -> Idris ()

1134logLvl :: Int -> String -> Idris ()

1149logLvl = logLvlCats []

1135logLvl = logLvlCats []

1150

1136

@@ -1178,7 +1164,7 @@ logLvlCats :: [LogCat] -- ^ The categories that the message should appear under.

1178 -> Int -- ^ The Logging level the message should appear.

1164 -> Int -- ^ The Logging level the message should appear.

1179 -> String -- ^ The message to show the developer.

1165 -> String -- ^ The message to show the developer.

1180 -> Idris ()

1166 -> Idris ()

1181−logLvlCats cs l str = do

1167+logLvlCats cs l msg = do

1182 i <- getIState

1168 i <- getIState

1183 let lvl = opt_logLevel (idris_options i)

1169 let lvl = opt_logLevel (idris_options i)

1184 let cats = opt_logcats (idris_options i)

1170 let cats = opt_logcats (idris_options i)

@@ -1186,9 +1172,9 @@ logLvlCats cs l str = do

1186 when (inCat cs cats || null cats) $

1172 when (inCat cs cats || null cats) $

1187 case idris_outputmode i of

1173 case idris_outputmode i of

1188 RawOutput h -> do

1174 RawOutput h -> do

1189− runIO $ hPutStrLn h str

1175+ runIO $ hPutStrLn h msg

1190 IdeMode n h -> do

1176 IdeMode n h -> do

1191− let good = SexpList [IntegerAtom (toInteger l), toSExp str]

1177+ let good = SexpList [IntegerAtom (toInteger l), toSExp msg]

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

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

1193 where

1179 where

1194 inCat :: [LogCat] -> [LogCat] -> Bool

1180 inCat :: [LogCat] -> [LogCat] -> Bool

@@ -1210,6 +1196,29 @@ setTypeCase t = do i <- getIState

1210 let opt' = opts { opt_typecase = t }

1196 let opt' = opts { opt_typecase = t }

1211 putIState $ i { idris_options = opt' }

1197 putIState $ i { idris_options = opt' }

1212

1198

1199+getIndentWith :: Idris Int

1200+getIndentWith = do

1201+ i <- getIState

1202+ return $ interactiveOpts_indentWith (idris_interactiveOpts i)

1203+

1204+setIndentWith :: Int -> Idris ()

1205+setIndentWith indentWith = do

1206+ i <- getIState

1207+ let opts = idris_interactiveOpts i

1208+ let opts' = opts { interactiveOpts_indentWith = indentWith }

1209+ putIState $ i { idris_interactiveOpts = opts' }

1210+

1211+getIndentClause :: Idris Int

1212+getIndentClause = do

1213+ i <- getIState

1214+ return $ interactiveOpts_indentClause (idris_interactiveOpts i)

1215+

1216+setIndentClause :: Int -> Idris ()

1217+setIndentClause indentClause = do

1218+ i <- getIState

1219+ let opts = idris_interactiveOpts i

1220+ let opts' = opts { interactiveOpts_indentClause = indentClause }

1221+ putIState $ i { idris_interactiveOpts = opts' }

1213

1222

1214-- Dealing with parameters

1223-- Dealing with parameters

1215

1224

@@ -2226,9 +2235,10 @@ instance Applicative (EitherErr a) where

2226instance Monad (EitherErr a) where

2235instance Monad (EitherErr a) where

2227 return = RightOK

2236 return = RightOK

2228

2237

2229− (LeftErr e) >>= k = LeftErr e

2238+ (LeftErr e) >>= _ = LeftErr e

2230 RightOK v >>= k = k v

2239 RightOK v >>= k = k v

2231

2240

2241+toEither :: EitherErr a b -> Either a b

2232toEither (LeftErr e) = Left e

2242toEither (LeftErr e) = Left e

2233toEither (RightOK ho) = Right ho

2243toEither (RightOK ho) = Right ho

2234

2244

@@ -2439,7 +2449,7 @@ mkUniqueNames env shadows tm

2439 -- looking for too long...)

2449 -- looking for too long...)

2440 initN (UN n) l = UN $ txt (str n ++ show l)

2450 initN (UN n) l = UN $ txt (str n ++ show l)

2441 initN (MN i s) l = MN (i+l) s

2451 initN (MN i s) l = MN (i+l) s

2442− initN n l = n

2452+ initN n _ = n

2443

2453

2444 -- FIXME: Probably ought to do this for completeness! It's fine as

2454 -- FIXME: Probably ought to do this for completeness! It's fine as

2445 -- long as there are no bindings inside tactics though.

2455 -- long as there are no bindings inside tactics though.

@@ -2547,50 +2557,49 @@ mkUniqueNames env shadows tm

2547

2557

2548 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2558 mkUniq ql nmap tm = descendM (mkUniq ql nmap) tm

2549

2559

2550−

2551getFile :: Opt -> Maybe String

2560getFile :: Opt -> Maybe String

2552−getFile (Filename str) = Just str

2561+getFile (Filename s) = Just s

2553getFile _ = Nothing

2562getFile _ = Nothing

2554

2563

2555getBC :: Opt -> Maybe String

2564getBC :: Opt -> Maybe String

2556−getBC (BCAsm str) = Just str

2565+getBC (BCAsm s) = Just s

2557getBC _ = Nothing

2566getBC _ = Nothing

2558

2567

2559getOutput :: Opt -> Maybe String

2568getOutput :: Opt -> Maybe String

2560−getOutput (Output str) = Just str

2569+getOutput (Output s) = Just s

2561getOutput _ = Nothing

2570getOutput _ = Nothing

2562

2571

2563getIBCSubDir :: Opt -> Maybe String

2572getIBCSubDir :: Opt -> Maybe String

2564−getIBCSubDir (IBCSubDir str) = Just str

2573+getIBCSubDir (IBCSubDir s) = Just s

2565getIBCSubDir _ = Nothing

2574getIBCSubDir _ = Nothing

2566

2575

2567getImportDir :: Opt -> Maybe String

2576getImportDir :: Opt -> Maybe String

2568−getImportDir (ImportDir str) = Just str

2577+getImportDir (ImportDir s) = Just s

2569getImportDir _ = Nothing

2578getImportDir _ = Nothing

2570

2579

2571getSourceDir :: Opt -> Maybe String

2580getSourceDir :: Opt -> Maybe String

2572−getSourceDir (SourceDir str) = Just str

2581+getSourceDir (SourceDir s) = Just s

2573getSourceDir _ = Nothing

2582getSourceDir _ = Nothing

2574

2583

2575getPkgDir :: Opt -> Maybe String

2584getPkgDir :: Opt -> Maybe String

2576−getPkgDir (Pkg str) = Just str

2585+getPkgDir (Pkg s) = Just s

2577getPkgDir _ = Nothing

2586getPkgDir _ = Nothing

2578

2587

2579getPkg :: Opt -> Maybe (Bool, String)

2588getPkg :: Opt -> Maybe (Bool, String)

2580−getPkg (PkgBuild str) = Just (False, str)

2589+getPkg (PkgBuild s) = Just (False, s)

2581−getPkg (PkgInstall str) = Just (True, str)

2590+getPkg (PkgInstall s) = Just (True, s)

2582getPkg _ = Nothing

2591getPkg _ = Nothing

2583

2592

2584getPkgClean :: Opt -> Maybe String

2593getPkgClean :: Opt -> Maybe String

2585−getPkgClean (PkgClean str) = Just str

2594+getPkgClean (PkgClean s) = Just s

2586getPkgClean _ = Nothing

2595getPkgClean _ = Nothing

2587

2596

2588getPkgREPL :: Opt -> Maybe String

2597getPkgREPL :: Opt -> Maybe String

2589−getPkgREPL (PkgREPL str) = Just str

2598+getPkgREPL (PkgREPL s) = Just s

2590getPkgREPL _ = Nothing

2599getPkgREPL _ = Nothing

2591

2600

2592getPkgCheck :: Opt -> Maybe String

2601getPkgCheck :: Opt -> Maybe String

2593−getPkgCheck (PkgCheck str) = Just str

2602+getPkgCheck (PkgCheck s) = Just s

2594getPkgCheck _ = Nothing

2603getPkgCheck _ = Nothing

2595

2604

2596-- | Returns None if given an Opt which is not PkgMkDoc

2605-- | Returns None if given an Opt which is not PkgMkDoc

@@ -2618,7 +2627,6 @@ getConsoleWidth :: Opt -> Maybe ConsoleWidth

2618getConsoleWidth (UseConsoleWidth x) = Just x

2627getConsoleWidth (UseConsoleWidth x) = Just x

2619getConsoleWidth _ = Nothing

2628getConsoleWidth _ = Nothing

2620

2629

2621−

2622getExecScript :: Opt -> Maybe String

2630getExecScript :: Opt -> Maybe String

2623getExecScript (InterpretScript expr) = Just expr

2631getExecScript (InterpretScript expr) = Just expr

2624getExecScript _ = Nothing

2632getExecScript _ = Nothing

@@ -2667,7 +2675,7 @@ getClient _ = Nothing

2667-- Get the first valid port

2675-- Get the first valid port

2668getPort :: [Opt] -> Maybe REPLPort

2676getPort :: [Opt] -> Maybe REPLPort

2669getPort [] = Nothing

2677getPort [] = Nothing

2670−getPort (Port p : xs) = Just p

2678+getPort (Port p : _ ) = Just p

2671getPort (_ : xs) = getPort xs

2679getPort (_ : xs) = getPort xs

2672

2680

2673opt :: (Opt -> Maybe a) -> [Opt] -> [a]

2681opt :: (Opt -> Maybe a) -> [Opt] -> [a]

src/Idris/AbsSyntaxTree.hs+42−20

@@ -5,24 +5,25 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8−{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,

9+{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}

9− FlexibleInstances, MultiParamTypeClasses, PatternGuards,

10− TypeSynonymInstances #-}

12module Idris.AbsSyntaxTree where

11module Idris.AbsSyntaxTree where

14−import Idris.Colours

15import Idris.Core.Elaborate hiding (Tactic(..))

13import Idris.Core.Elaborate hiding (Tactic(..))

16import Idris.Core.Evaluate

14import Idris.Core.Evaluate

17import Idris.Core.TT

15import Idris.Core.TT

18−import Idris.Core.Typecheck

19import Idris.Docstrings

16import Idris.Docstrings

20import IRTS.CodegenCommon

17import IRTS.CodegenCommon

21import IRTS.Lang

18import IRTS.Lang

22import Util.DynamicLinker

19import Util.DynamicLinker

23import Util.Pretty

20import Util.Pretty

22+import Idris.Colours

23+

24+import System.IO

25+

25−import Prelude hiding ((<$>))

26+import Prelude hiding (Foldable, Traversable, (<$>))

27import Control.Applicative ((<|>))

28import Control.Applicative ((<|>))

28import qualified Control.Monad.Trans.Class as Trans (lift)

29import qualified Control.Monad.Trans.Class as Trans (lift)

@@ -30,24 +31,20 @@ import Control.Monad.Trans.Except

30import Control.Monad.Trans.State.Strict

31import Control.Monad.Trans.State.Strict

31import Data.Char

32import Data.Char

32import Data.Data (Data)

33import Data.Data (Data)

33−import Data.Either

34+

34import Data.Foldable (Foldable)

35import Data.Foldable (Foldable)

35import Data.Function (on)

36import Data.Function (on)

36import Data.Generics.Uniplate.Data (children, universe)

37import Data.Generics.Uniplate.Data (children, universe)

37import Data.List hiding (group)

38import Data.List hiding (group)

38import qualified Data.Map.Strict as M

39import qualified Data.Map.Strict as M

39−import Data.Maybe (fromMaybe, mapMaybe, maybeToList)

40+import Data.Maybe (mapMaybe, maybeToList)

40import qualified Data.Set as S

41import qualified Data.Set as S

41import qualified Data.Text as T

42import qualified Data.Text as T

42import Data.Traversable (Traversable)

43import Data.Traversable (Traversable)

43import Data.Typeable

44import Data.Typeable

44−import Data.Word (Word)

45−import Debug.Trace

46import GHC.Generics (Generic)

45import GHC.Generics (Generic)

47import Network.Socket (PortNumber)

46import Network.Socket (PortNumber)

48−import System.Console.Haskeline

47+

49−import System.IO

50−import Text.PrettyPrint.Annotated.Leijen

52data ElabWhat = ETypes | EDefns | EAll

49data ElabWhat = ETypes | EDefns | EAll

53 deriving (Show, Eq)

50 deriving (Show, Eq)

@@ -112,6 +109,7 @@ data IOption = IOption {

112 , opt_autoimpls :: Bool

109 , opt_autoimpls :: Bool

113 } deriving (Show, Eq, Generic)

110 } deriving (Show, Eq, Generic)

114

111

112+defaultOpts :: IOption

115defaultOpts = IOption { opt_logLevel = 0

113defaultOpts = IOption { opt_logLevel = 0

116 , opt_logcats = []

114 , opt_logcats = []

117 , opt_typecase = False

115 , opt_typecase = False

@@ -151,6 +149,7 @@ data PPOption = PPOption {

151data Optimisation = PETransform -- ^ partial eval and associated transforms

149data Optimisation = PETransform -- ^ partial eval and associated transforms

152 deriving (Show, Eq, Generic)

150 deriving (Show, Eq, Generic)

153

151

152+defaultOptimise :: [Optimisation]

154defaultOptimise = [PETransform]

153defaultOptimise = [PETransform]

155

154

156-- | Pretty printing options with default verbosity.

155-- | Pretty printing options with default verbosity.

@@ -206,6 +205,12 @@ data DefaultTotality = DefaultCheckingTotal -- ^ Total

206 | DefaultCheckingCovering -- ^Total coverage, but may diverge

205 | DefaultCheckingCovering -- ^Total coverage, but may diverge

207 deriving (Show, Eq, Generic)

206 deriving (Show, Eq, Generic)

208

207

208+-- | Configuration options for interactive editing.

209+data InteractiveOpts = InteractiveOpts {

210+ interactiveOpts_indentWith :: Int

211+ , interactiveOpts_indentClause :: Int

212+} deriving (Show, Generic)

213+

209-- | The global state used in the Idris monad

214-- | The global state used in the Idris monad

210data IState = IState {

215data IState = IState {

211 tt_ctxt :: Context -- ^ All the currently defined names and their terms

216 tt_ctxt :: Context -- ^ All the currently defined names and their terms

@@ -294,7 +299,7 @@ data IState = IState {

294 , idris_repl_defs :: [Name]

299 , idris_repl_defs :: [Name]

295

300

296 -- | Stack of names currently being elaborated, Bool set if it's an

301 -- | Stack of names currently being elaborated, Bool set if it's an

297− -- implementation (implementations appear twice; also as a funtion name)

302+ -- implementation (implementations appear twice; also as a function name)

298 , elab_stack :: [(Name, Bool)]

303 , elab_stack :: [(Name, Bool)]

299

304

300

305

@@ -306,8 +311,8 @@ data IState = IState {

306 , idris_inmodule :: S.Set Name -- ^ Names defined in current module

311 , idris_inmodule :: S.Set Name -- ^ Names defined in current module

307 , idris_ttstats :: M.Map Term (Int, Term)

312 , idris_ttstats :: M.Map Term (Int, Term)

308 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

313 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.

309− }

314+ , idris_interactiveOpts :: InteractiveOpts

310− deriving Generic

315+ } deriving Generic

311

316

312-- Required for parsers library, and therefore trifecta

317-- Required for parsers library, and therefore trifecta

313instance Show IState where

318instance Show IState where

@@ -332,6 +337,7 @@ data CGInfo = CGInfo {

332deriving instance Binary CGInfo

337deriving instance Binary CGInfo

333!-}

338!-}

334

339

340+primDefs :: [Name]

335primDefs = [ sUN "unsafePerformPrimIO"

341primDefs = [ sUN "unsafePerformPrimIO"

336 , sUN "mkLazyForeignPrim"

342 , sUN "mkLazyForeignPrim"

337 , sUN "mkForeignPrim"

343 , sUN "mkForeignPrim"

@@ -390,6 +396,12 @@ data IBCWrite = IBCFix FixDecl

390 | IBCConstraint FC UConstraint

396 | IBCConstraint FC UConstraint

391 deriving (Show, Generic)

397 deriving (Show, Generic)

392

398

399+initialInteractiveOpts :: InteractiveOpts

400+initialInteractiveOpts = InteractiveOpts {

401+ interactiveOpts_indentWith = 2

402+ , interactiveOpts_indentClause = 2

403+}

404+

393-- | The initial state for the compiler

405-- | The initial state for the compiler

394idrisInit :: IState

406idrisInit :: IState

395idrisInit = IState initContext S.empty []

407idrisInit = IState initContext S.empty []

@@ -402,7 +414,7 @@ idrisInit = IState initContext S.empty []

402 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

414 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

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

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

404 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

416 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []

405− emptyContext S.empty M.empty emptyContext

417+ emptyContext S.empty M.empty emptyContext initialInteractiveOpts

406

418

407

419

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

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

@@ -488,6 +500,8 @@ data Opt = Filename String

488 | ColourREPL Bool

500 | ColourREPL Bool

489 | Idemode

501 | Idemode

490 | IdemodeSocket

502 | IdemodeSocket

503+ | IndentWith Int

504+ | IndentClause Int

491 | ShowAll

505 | ShowAll

492 | ShowLibs

506 | ShowLibs

493 | ShowLibDir

507 | ShowLibDir

@@ -627,19 +641,27 @@ is_scoped (Imp _ _ _ s _ _) = s

627is_scoped _ = Nothing

641is_scoped _ = Nothing

628

642

629-- Top level implicit

643-- Top level implicit

644+impl :: Plicity

630impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW

645impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW

631-- Machine generated top level implicit

646-- Machine generated top level implicit

647+impl_gen :: Plicity

632impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW

648impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW

633

649

634-- Scoped implicits

650-- Scoped implicits

651+forall_imp :: Plicity

635forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW

652forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW

653+forall_constraint :: Plicity

636forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW

654forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW

637

655

656+expl :: Plicity

638expl = Exp [] Dynamic False RigW

657expl = Exp [] Dynamic False RigW

658+expl_param :: Plicity

639expl_param = Exp [] Dynamic True RigW

659expl_param = Exp [] Dynamic True RigW

640

660

661+constraint :: Plicity

641constraint = Constraint [] Static RigW

662constraint = Constraint [] Static RigW

642

663

664+tacimpl :: PTerm -> Plicity

643tacimpl t = TacImp [] Dynamic t RigW

665tacimpl t = TacImp [] Dynamic t RigW

644

666

645data FnOpt = Inlinable -- ^ always evaluate when simplifying

667data FnOpt = Inlinable -- ^ always evaluate when simplifying

@@ -1410,7 +1432,7 @@ highestFC (PAppImpl t _) = highestFC t

1410-- Interface data

1432-- Interface data

1411

1433

1412data InterfaceInfo = CI {

1434data InterfaceInfo = CI {

1413− implementationCtorName :: Name

1435+ implementationCtorName :: Name

1414 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method

1436 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method

1415 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl

1437 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl

1416 , interface_default_super_interfaces :: [PDecl]

1438 , interface_default_super_interfaces :: [PDecl]

@@ -2269,7 +2291,7 @@ getExps (_ : xs) = getExps xs

2269

2291

2270getShowArgs :: [PArg] -> [PArg]

2292getShowArgs :: [PArg] -> [PArg]

2271getShowArgs [] = []

2293getShowArgs [] = []

2272−getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs

2294+getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs

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

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

2274 | PImp _ _ _ _ tm <- e

2296 | PImp _ _ _ _ tm <- e

2275 , containsHole tm = e : getShowArgs xs

2297 , containsHole tm = e : getShowArgs xs

@@ -2586,5 +2608,5 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm

2586getErasureInfo :: IState -> Name -> [Int]

2608getErasureInfo :: IState -> Name -> [Int]

2587getErasureInfo ist n =

2609getErasureInfo ist n =

2588 case lookupCtxtExact n (idris_optimisation ist) of

2610 case lookupCtxtExact n (idris_optimisation ist) of

2589− Just (Optimise inacc detag force) -> map fst inacc

2611+ Just (Optimise inacc _ _) -> map fst inacc

2590 Nothing -> []

2612 Nothing -> []

src/Idris/CaseSplit.hs+19−27

@@ -15,8 +15,8 @@ resolve other dependencies.

15Finally, merge the generated patterns with the original, by matching.

16Always take the "more specific" argument when there is a discrepancy, i.e.

17names over '_', patterns over names, etc.

18−

19-}

18-}

19+

20{-# LANGUAGE PatternGuards #-}

22module Idris.CaseSplit(

@@ -28,10 +28,8 @@ module Idris.CaseSplit(

28 ) where

30import Idris.AbsSyntax

31−import Idris.AbsSyntaxTree (IState, Idris, PTerm)

32import Idris.Core.Evaluate

31import Idris.Core.Evaluate

33import Idris.Core.TT

32import Idris.Core.TT

34−import Idris.Core.Typecheck

35import Idris.Delaborate

33import Idris.Delaborate

36import Idris.Elab.Term

34import Idris.Elab.Term

37import Idris.Elab.Value

35import Idris.Elab.Value

@@ -39,18 +37,11 @@ import Idris.ElabDecls

39import Idris.Error

37import Idris.Error

40import Idris.Output

38import Idris.Output

41import Idris.Parser

39import Idris.Parser

42−import Idris.Parser.Helpers

44import Control.Monad

41import Control.Monad

45import Control.Monad.State.Strict

42import Control.Monad.State.Strict

46import Data.Char

43import Data.Char

47import Data.List (isPrefixOf, isSuffixOf)

44import Data.List (isPrefixOf, isSuffixOf)

48−import Data.Maybe

49−import Debug.Trace

50−import Text.Parser.Char (anyChar)

51−import Text.Parser.Combinators

52−import Text.Trifecta (Result(..), parseString)

53−import Text.Trifecta.Delta

55-- | Given a variable to split, and a term application, return a list

46-- | Given a variable to split, and a term application, return a list

56-- of variable updates, paired with a flag to say whether the given

47-- of variable updates, paired with a flag to say whether the given

@@ -109,11 +100,11 @@ data MergeState = MS { namemap :: [(Name, Name)],

109 explicit :: [Name],

100 explicit :: [Name],

110 updates :: [(Name, PTerm)] }

101 updates :: [(Name, PTerm)] }

111

102

112−addUpdate :: Name -> Idris.AbsSyntaxTree.PTerm -> State MergeState ()

103+addUpdate :: Name -> PTerm -> State MergeState ()

113addUpdate n tm = do ms <- get

104addUpdate n tm = do ms <- get

114 put (ms { updates = ((n, stripNS tm) : updates ms) } )

105 put (ms { updates = ((n, stripNS tm) : updates ms) } )

115

106

116−inventName :: Idris.AbsSyntaxTree.IState -> Maybe Name -> Name -> State MergeState Name

107+inventName :: IState -> Maybe Name -> Name -> State MergeState Name

117inventName ist ty n =

108inventName ist ty n =

118 do ms <- get

109 do ms <- get

119 let supp = case ty of

110 let supp = case ty of

@@ -142,7 +133,7 @@ mkSupply ns = mkSupply' ns (map nextName ns)

142varlist :: [Name]

133varlist :: [Name]

143varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

134varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

144

135

145−stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm

136+stripNS :: PTerm -> PTerm

146stripNS tm = mapPT dens tm where

137stripNS tm = mapPT dens tm where

147 dens (PRef fc hls n) = PRef fc hls (nsroot n)

138 dens (PRef fc hls n) = PRef fc hls (nsroot n)

148 dens t = t

139 dens t = t

@@ -395,17 +386,19 @@ getClause :: Int -- ^ line number that the type is declared on

395 -> Name -- ^ User given name

386 -> Name -- ^ User given name

396 -> FilePath -- ^ Source file name

387 -> FilePath -- ^ Source file name

397 -> Idris String

388 -> Idris String

398−getClause l fn un fp

389+getClause l _ un fp

399 = do i <- getIState

390 = do i <- getIState

391+ indentClause <- getIndentClause

392+-- runIO . traceIO $ "indentClause = " ++ show indentClause

400 case lookupCtxt un (idris_interfaces i) of

393 case lookupCtxt un (idris_interfaces i) of

401− [c] -> return (mkInterfaceBodies i (interface_methods c))

394+ [c] -> return (mkInterfaceBodies indentClause i (interface_methods c))

402 _ -> do ty_in <- getInternalApp fp l

395 _ -> do ty_in <- getInternalApp fp l

403 let ty = case ty_in of

396 let ty = case ty_in of

404− PTyped n t -> t

397+ PTyped _ t -> t

405 x -> x

398 x -> x

406 ist <- get

399 ist <- get

407− let ap = mkApp ist ty []

400+ let app = mkApp ist ty []

408− return (showLHSName un ++ " " ++ ap ++ "= ?"

401+ return (showLHSName un ++ " " ++ app ++ "= ?"

409 ++ showRHSName un ++ "_rhs")

402 ++ showRHSName un ++ "_rhs")

410 where mkApp :: IState -> PTerm -> [Name] -> String

403 where mkApp :: IState -> PTerm -> [Name] -> String

411 mkApp i (PPi (Exp _ _ False _) (MN _ _) _ ty sc) used

404 mkApp i (PPi (Exp _ _ False _) (MN _ _) _ ty sc) used

@@ -431,11 +424,11 @@ getClause l fn un fp

431 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",

424 getNameFrom i used _ = uniqueNameFrom (mkSupply [sUN "x", sUN "y",

432 sUN "z"]) used

425 sUN "z"]) used

433

426

434− -- write method declarations, indent with 4 spaces

427+ -- write method declarations, indent with `indent` spaces.

435− mkInterfaceBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String

428+ mkInterfaceBodies :: Int -> IState -> [(Name, (Bool, FnOpts, PTerm))] -> String

436− mkInterfaceBodies i ns

429+ mkInterfaceBodies indent i ns

437 = showSep "\n"

430 = showSep "\n"

438− (zipWith (\(n, (_, _, ty)) m -> " " ++

431+ (zipWith (\(n, (_, _, ty)) m -> replicate indent ' ' ++

439 def (show (nsroot n)) ++ " "

432 def (show (nsroot n)) ++ " "

440 ++ mkApp i ty []

433 ++ mkApp i ty []

441 ++ "= ?"

434 ++ "= ?"

@@ -460,9 +453,9 @@ getProofClause l fn fp

460-- Purely syntactic - turn a pattern match clause into a with and a new

453-- Purely syntactic - turn a pattern match clause into a with and a new

461-- match clause

454-- match clause

462

455

463−mkWith :: String -> Name -> String

456+mkWith :: String -> Name -> Int -> String

464−mkWith str n = let str' = replaceRHS str "with (_)"

457+mkWith str n indent = let str' = replaceRHS str "with (_)"

465− in str' ++ "\n" ++ newpat str

458+ in str' ++ "\n" ++ newpat str

466

459

467 where replaceRHS [] str = str

460 where replaceRHS [] str = str

468 replaceRHS ('?':'=': rest) str = str

461 replaceRHS ('?':'=': rest) str = str

@@ -471,8 +464,7 @@ mkWith str n = let str' = replaceRHS str "with (_)"

471 replaceRHS (x : rest) str = x : replaceRHS rest str

464 replaceRHS (x : rest) str = x : replaceRHS rest str

472

465

473 newpat ('>':patstr) = '>':newpat patstr

466 newpat ('>':patstr) = '>':newpat patstr

474− newpat patstr =

467+ newpat patstr = replicate indent ' ' ++

475− " " ++

476 replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"

468 replaceRHS patstr "| with_pat = ?" ++ showRHSName n ++ "_rhs"

477

469

478-- Replace _ with names in missing clauses

470-- Replace _ with names in missing clauses

src/Idris/CmdOptions.hs+45−30

@@ -5,7 +5,9 @@ Description : A parser for the CmdOptions for the Idris executable.

5License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE Arrows #-}

9{-# LANGUAGE Arrows #-}

10+

9module Idris.CmdOptions

11module Idris.CmdOptions

10 (

12 (

11 module Idris.CmdOptions

13 module Idris.CmdOptions

@@ -19,7 +21,6 @@ import Idris.AbsSyntax (getClient, getIBCSubDir, getPkg, getPkgCheck,

19 getPort, opt)

21 getPort, opt)

20import Idris.AbsSyntaxTree

22import Idris.AbsSyntaxTree

21import Idris.Info (getIdrisVersion)

23import Idris.Info (getIdrisVersion)

22−-- import Idris.REPL

23import IRTS.CodegenCommon

24import IRTS.CodegenCommon

25import Control.Monad.Trans (lift)

26import Control.Monad.Trans (lift)

@@ -33,8 +34,10 @@ import Data.Monoid ((<>))

33import Options.Applicative

34import Options.Applicative

34import Options.Applicative.Arrows

35import Options.Applicative.Arrows

35import Options.Applicative.Types (ReadM(..))

36import Options.Applicative.Types (ReadM(..))

36−import Safe (lastMay)

37+

37import Text.ParserCombinators.ReadP hiding (many, option)

38import Text.ParserCombinators.ReadP hiding (many, option)

39+

40+import Safe (lastMay)

38import qualified Text.PrettyPrint.ANSI.Leijen as PP

41import qualified Text.PrettyPrint.ANSI.Leijen as PP

40runArgParser :: IO [Opt]

43runArgParser :: IO [Opt]

@@ -97,14 +100,15 @@ parseFlags = many $

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

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

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

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

102

103+ -- Client flags

100− <|> (Client <$> strOption (long "client"))

104+ <|> Client <$> strOption (long "client")

101

105

102 -- Logging Flags

106 -- Logging Flags

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

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

104− <|> (OLogCats <$> option (str >>= parseLogCats)

108+ <|> OLogCats <$> option (str >>= parseLogCats)

105 (long "logging-categories"

109 (long "logging-categories"

106 <> metavar "CATS"

110 <> metavar "CATS"

107− <> help "Colon separated logging categories. Use --listlogcats to see list."))

111+ <> help "Colon separated logging categories. Use --listlogcats to see list.")

108

112

109 -- Turn off things

113 -- Turn off things

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

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

@@ -113,7 +117,7 @@ parseFlags = many $

113

117

114 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

118 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

115

119

116− <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

120+ <|> Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file")

117

121

118 -- <|> flag' TypeCase (long "typecase")

122 -- <|> flag' TypeCase (long "typecase")

119 <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

123 <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

@@ -138,33 +142,41 @@ parseFlags = many $

138 <|> flag' (Verbose 2) (long "V1" <> help "Louder verbosity")

142 <|> flag' (Verbose 2) (long "V1" <> help "Louder verbosity")

139 <|> flag' (Verbose 1) (short 'V' <> long "V0" <>long "verbose" <> help "Loud verbosity")

143 <|> flag' (Verbose 1) (short 'V' <> long "V0" <>long "verbose" <> help "Loud verbosity")

140

144

141− <|> (IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory"))

145+ <|> IBCSubDir <$> strOption (long "ibcsubdir" <> metavar "FILE" <> help "Write IBC files into sub directory")

142− <|> (ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths"))

146+ <|> ImportDir <$> strOption (short 'i' <> long "idrispath" <> help "Add directory to the list of import paths")

143− <|> (SourceDir <$> strOption (long "sourcepath" <> help "Add directory to the list of source search paths"))

147+ <|> SourceDir <$> strOption (long "sourcepath" <> help "Add directory to the list of source search paths")

144

148

145 <|> flag' WarnOnly (long "warn")

149 <|> flag' WarnOnly (long "warn")

146

150

147− <|> (Pkg <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency"))

151+ <|> Pkg <$> strOption (short 'p' <> long "package" <> help "Add package as a dependency")

148− <|> (Port <$> option portReader (long "port" <> metavar "PORT" <> help "REPL TCP port - pass \"none\" to not bind any port"))

152+ <|> Port <$> option portReader (long "port" <> metavar "PORT" <> help "REPL TCP port - pass \"none\" to not bind any port")

149

153

150 -- Package commands

154 -- Package commands

151− <|> (PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package"))

155+ <|> PkgBuild <$> strOption (long "build" <> metavar "IPKG" <> help "Build package")

152− <|> (PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package"))

156+ <|> PkgInstall <$> strOption (long "install" <> metavar "IPKG" <> help "Install package")

153− <|> (PkgREPL <$> strOption (long "repl" <> metavar "IPKG" <> help "Launch REPL, only for executables"))

157+ <|> PkgREPL <$> strOption (long "repl" <> metavar "IPKG" <> help "Launch REPL, only for executables")

154− <|> (PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package"))

158+ <|> PkgClean <$> strOption (long "clean" <> metavar "IPKG" <> help "Clean package")

155 <|> (PkgDocBuild <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

159 <|> (PkgDocBuild <$> strOption (long "mkdoc" <> metavar "IPKG" <> help "Generate IdrisDoc for package"))

156− <|> (PkgDocInstall <$> strOption (long "installdoc" <> metavar "IPKG" <> help "Install IdrisDoc for package"))

160+ <|> PkgDocInstall <$> strOption (long "installdoc" <> metavar "IPKG" <> help "Install IdrisDoc for package")

157− <|> (PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only"))

161+ <|> PkgCheck <$> strOption (long "checkpkg" <> metavar "IPKG" <> help "Check package only")

158− <|> (PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package"))

162+ <|> PkgTest <$> strOption (long "testpkg" <> metavar "IPKG" <> help "Run tests for package")

163+

164+ -- Interactive Editing Flags

165+ <|> IndentWith <$> option auto (long "indent-with"

166+ <> metavar "INDENT"

167+ <> help "Indentation to use with :makewith (default 2)")

168+ <|> IndentClause <$> option auto (long "indent-clause"

169+ <> metavar "INDENT"

170+ <> help "Indentation to use with :addclause (default 2)")

159

171

160 -- Misc options

172 -- Misc options

161− <|> (BCAsm <$> strOption (long "bytecode"))

173+ <|> BCAsm <$> strOption (long "bytecode")

162

174

163 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

175 <|> flag' (OutputTy Raw) (short 'S' <> long "codegenonly" <> help "Do no further compilation of code generator output")

164 <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")

176 <|> flag' (OutputTy Object) (short 'c' <> long "compileonly" <> help "Compile to object files rather than an executable")

165

177

166− <|> (DumpDefun <$> strOption (long "dumpdefuns"))

178+ <|> DumpDefun <$> strOption (long "dumpdefuns")

167− <|> (DumpCases <$> strOption (long "dumpcases"))

179+ <|> DumpCases <$> strOption (long "dumpcases")

168

180

169 <|> (UseCodegen . parseCodegen) <$> strOption (long "codegen"

181 <|> (UseCodegen . parseCodegen) <$> strOption (long "codegen"

170 <> metavar "TARGET"

182 <> metavar "TARGET"

@@ -174,14 +186,17 @@ parseFlags = many $

174 <> metavar "TARGET"

186 <> metavar "TARGET"

175 <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))

187 <> help "Pass the name of the code generator. This option is for codegens that take JSON formatted IR."))

176

188

177− <|> (CodegenArgs <$> strOption (long "cg-opt"

189+ <|> CodegenArgs <$> strOption (long "cg-opt"

178− <> metavar "ARG"

190+ <> metavar "ARG"

179− <> help "Arguments to pass to code generator"))

191+ <> help "Arguments to pass to code generator")

180

192

193+ <|> EvalExpr <$> strOption (long "eval"

194+ <> short 'e'

195+ <> metavar "EXPR"

181− <|> (EvalExpr <$> strOption (long "eval" <> short 'e' <> metavar "EXPR" <> help "Evaluate an expression without loading the REPL"))

196+ <> help "Evaluate an expression without loading the REPL")

182

197

183 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

198 <|> flag' (InterpretScript "Main.main") (long "execute" <> help "Execute as idris")

184− <|> (InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris"))

199+ <|> InterpretScript <$> strOption (long "exec" <> metavar "EXPR" <> help "Execute as idris")

185

200

186 <|> ((Extension . getExt) <$> strOption (long "extension"

201 <|> ((Extension . getExt) <$> strOption (long "extension"

187 <> short 'X'

202 <> short 'X'

@@ -197,10 +212,10 @@ parseFlags = many $

197 <|> flag' (AddOpt PETransform) (long "partial-eval")

212 <|> flag' (AddOpt PETransform) (long "partial-eval")

198 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

213 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")

199

214

200− <|> (OptLevel <$> option auto (short 'O' <> long "level"))

215+ <|> OptLevel <$> option auto (short 'O' <> long "level")

201

216

202− <|> (TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple."))

217+ <|> TargetTriple <$> strOption (long "target" <> metavar "TRIPLE" <> help "If supported the codegen will target the named triple.")

203− <|> (TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "If supported the codegen will target the named CPU e.g. corei7 or cortex-m3"))

218+ <|> TargetCPU <$> strOption (long "cpu" <> metavar "CPU" <> help "If supported the codegen will target the named CPU e.g. corei7 or cortex-m3")

204

219

205 -- Colour Options

220 -- Colour Options

206 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

221 <|> flag' (ColourREPL True) (long "colour" <> long "color" <> help "Force coloured output")

src/Idris/DeepSeq.hs+1

@@ -108,3 +108,4 @@ instance NFData Using

108instance NFData SyntaxInfo

109instance NFData DefaultTotality

110instance NFData IState

111+instance NFData InteractiveOpts

src/Idris/Docs.hs+7−3

@@ -5,16 +5,21 @@ Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE DeriveFunctor, MultiWayIf, PatternGuards #-}

9{-# LANGUAGE DeriveFunctor, MultiWayIf, PatternGuards #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

11+

10module Idris.Docs (

12module Idris.Docs (

11 pprintDocs

13 pprintDocs

12 , getDocs, pprintConstDocs, pprintTypeDoc

14 , getDocs, pprintConstDocs, pprintTypeDoc

13 , FunDoc, FunDoc'(..), Docs, Docs'(..)

15 , FunDoc, FunDoc'(..), Docs, Docs'(..)

14 ) where

16 ) where

16−import Idris.AbsSyntax

18+import Idris.AbsSyntax (FixDecl(..), Fixity, HowMuchDocs(..), IState(..), Idris,

17−import Idris.AbsSyntaxTree

19+ InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),

20+ PTerm(..), Plicity(..), RecordInfo(..), basename,

21+ getIState, modDocName, ppOptionIst, pprintPTerm,

22+ prettyIst, prettyName, type1Doc, typeDescription)

18import Idris.Core.Evaluate

23import Idris.Core.Evaluate

19import Idris.Core.TT

24import Idris.Core.TT

20import Idris.Delaborate

25import Idris.Delaborate

@@ -26,7 +31,6 @@ import Util.Pretty

27import Prelude hiding ((<$>))

32import Prelude hiding ((<$>))

29−import Control.Arrow (first)

30import Data.List

34import Data.List

31import Data.Maybe

35import Data.Maybe

32import qualified Data.Text as T

36import qualified Data.Text as T

src/Idris/Interactive.hs+21−24

@@ -32,10 +32,7 @@ import Util.System

33import Data.Char

34import Data.List (isSuffixOf)

35−import Data.Maybe (fromMaybe)

36−import Debug.Trace

37import System.Directory

35import System.Directory

38−import System.FilePath

39import System.IO

36import System.IO

41caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

38caseSplitAt :: FilePath -> Bool -> Int -> Name -> Idris ()

@@ -60,8 +57,8 @@ addClauseFrom fn updatefile l n = do

60 ist <- getIState

57 ist <- getIState

61 cl <- getInternalApp fn l

58 cl <- getInternalApp fn l

62 let fulln = getAppName cl

59 let fulln = getAppName cl

63−

64− case lookup fulln (idris_metavars ist) of

60+ let metavars = lookup fulln (idris_metavars ist)

61+ case metavars of

65 Nothing -> addMissing fn updatefile l n

62 Nothing -> addMissing fn updatefile l n

66 Just _ -> do

63 Just _ -> do

67 src <- runIO $ readSource fn

64 src <- runIO $ readSource fn

@@ -164,22 +161,25 @@ addMissing fn updatefile l n

164

161

165

162

166makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

163makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

167−makeWith fn updatefile l n

164+makeWith fn updatefile l n = do

168− = do src <- runIO $ readSource fn

165+ src <- runIO $ readSource fn

166+ i <- getIState

167+ indentWith <- getIndentWith

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

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

170− let ind = getIndent tyline

169+ let ind = getIndent tyline

170+-- runIO . traceIO $ "indentWith = " ++ show indentWith

171− let with = mkWith tyline n

171+ let with = mkWith tyline n indentWith

172− -- add clause before first blank line in 'later',

172+ -- add clause before first blank line in 'later',

173− -- or (TODO) before first line with same indentation as tyline

173+ -- or (TODO) before first line with same indentation as tyline

174− let (nonblank, rest) = span (\x -> not (all isSpace x) &&

174+ let (nonblank, rest) = span (\x -> not (all isSpace x) &&

175− not (ind == getIndent x)) later

175+ not (ind == getIndent x)) later

176− if updatefile then

176+ if updatefile

177+ then do

177− do let fb = fn ++ "~"

178+ let fb = fn ++ "~"

178− runIO $ writeSource fb (unlines (before ++ nonblank)

179+ runIO $ writeSource fb (unlines (before ++ nonblank) ++

179− ++ with ++ "\n" ++

180− unlines rest)

180+ with ++ "\n" ++ unlines rest)

181− runIO $ copyFile fb fn

181+ runIO $ copyFile fb fn

182− else iPrintResult (with ++ "\n")

182+ else iPrintResult (with ++ "\n")

183 where getIndent s = length (takeWhile isSpace s)

184

185-- Replace the given metavariable on the given line with a 'case'

@@ -221,9 +221,6 @@ makeCase fn updatefile l n

221 findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs

222

223

224−

225−

226−

227doProofSearch :: FilePath -> Bool -> Bool ->

224doProofSearch :: FilePath -> Bool -> Bool ->

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

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

229doProofSearch fn updatefile rec l n hints Nothing

226doProofSearch fn updatefile rec l n hints Nothing

src/Idris/Main.hs+11−11

@@ -31,8 +31,6 @@ import IRTS.CodegenCommon

32import Util.System

34−import Prelude hiding (id, (.), (<$>))

35−

36import Control.Category

34import Control.Category

37import Control.DeepSeq

35import Control.DeepSeq

38import Control.Monad

36import Control.Monad

@@ -40,6 +38,7 @@ import Control.Monad.Trans (lift)

40import Control.Monad.Trans.Except (runExceptT)

38import Control.Monad.Trans.Except (runExceptT)

41import Control.Monad.Trans.State.Strict (execStateT)

39import Control.Monad.Trans.State.Strict (execStateT)

42import Data.Maybe

40import Data.Maybe

41+import Prelude hiding (id, (.), (<$>))

43import System.Console.Haskeline as H

42import System.Console.Haskeline as H

44import System.Directory

43import System.Directory

45import System.Exit

44import System.Exit

@@ -56,7 +55,6 @@ runMain prog = do res <- runExceptT $ execStateT prog idrisInit

56 exitFailure

55 exitFailure

57 Right _ -> return ()

56 Right _ -> return ()

59−

60-- | The main function of Idris that when given a set of Options will

58-- | The main function of Idris that when given a set of Options will

61-- launch Idris into the desired interaction mode either: REPL;

59-- launch Idris into the desired interaction mode either: REPL;

62-- Compiler; Script execution; or IDE Mode.

60-- Compiler; Script execution; or IDE Mode.

@@ -215,14 +213,16 @@ idrisMain opts =

215 ok <- noErrors

213 ok <- noErrors

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

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

217 where

215 where

218− makeOption (OLogging i) = setLogLevel i

216+ makeOption (OLogging i) = setLogLevel i

219− makeOption (OLogCats cs) = setLogCats cs

217+ makeOption (OLogCats cs) = setLogCats cs

220− makeOption (Verbose v) = setVerbose v

218+ makeOption (Verbose v) = setVerbose v

221− makeOption TypeCase = setTypeCase True

219+ makeOption TypeCase = setTypeCase True

222− makeOption TypeInType = setTypeInType True

220+ makeOption TypeInType = setTypeInType True

223− makeOption NoCoverage = setCoverage False

221+ makeOption NoCoverage = setCoverage False

224− makeOption ErrContext = setErrContext True

222+ makeOption ErrContext = setErrContext True

223+ makeOption (IndentWith n) = setIndentWith n

224+ makeOption (IndentClause n) = setIndentClause n

225− makeOption _ = return ()

225+ makeOption _ = return ()

226

227 processOptimisation :: (Bool,Optimisation) -> Idris ()

228 processOptimisation (True, p) = addOptimise p

src/Idris/REPL.hs+27−33

@@ -4,8 +4,9 @@ Description : Entry Point for the Idris REPL and CLI.

4License : BSD3

5Maintainer : The Idris Community.

6-}

7−{-# LANGUAGE CPP, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,

8− PatternGuards #-}

8+{-# LANGUAGE PatternGuards #-}

9module Idris.REPL

10module Idris.REPL

10 ( idemodeStart

11 ( idemodeStart

11 , startServer

12 , startServer

@@ -16,6 +17,23 @@ module Idris.REPL

16 , proofs

17 , proofs

17 ) where

18 ) where

20+import Control.Category

21+import Control.Concurrent

22+import Control.Concurrent.Async (race)

23+import Control.DeepSeq

24+import qualified Control.Exception as X

25+import Control.Monad

26+import Control.Monad.Trans (lift)

27+import Control.Monad.Trans.Except (runExceptT)

28+import Control.Monad.Trans.State.Strict (evalStateT, get, put)

29+import Data.Char

30+import Data.Either (partitionEithers)

31+import Data.List hiding (group)

32+import Data.List.Split (splitOn)

33+import Data.Maybe

34+import qualified Data.Set as S

35+import qualified Data.Text as T

36+import Data.Version

19import Idris.AbsSyntax

37import Idris.AbsSyntax

20import Idris.Apropos (apropos, aproposModules)

38import Idris.Apropos (apropos, aproposModules)

21import Idris.ASTUtils

39import Idris.ASTUtils

@@ -29,7 +47,7 @@ import Idris.Core.Unify

29import Idris.Core.WHNF

47import Idris.Core.WHNF

30import Idris.Coverage

48import Idris.Coverage

31import Idris.Delaborate

49import Idris.Delaborate

32−import Idris.Docs hiding (Doc)

50+import Idris.Docs

33import Idris.Docstrings (overview, renderDocTerm, renderDocstring)

51import Idris.Docstrings (overview, renderDocTerm, renderDocstring)

34import Idris.Elab.Clause

52import Idris.Elab.Clause

35import Idris.Elab.Term

53import Idris.Elab.Term

@@ -55,36 +73,8 @@ import Idris.Termination

55import Idris.TypeSearch (searchByType)

73import Idris.TypeSearch (searchByType)

56import Idris.WhoCalls

74import Idris.WhoCalls

57import IRTS.Compiler

75import IRTS.Compiler

58−

59−import Util.DynamicLinker

60−import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

61−import Util.Pretty hiding ((</>))

62−import Util.System

63−

64−import Version_idris (gitHash)

65−

66−import Prelude hiding (id, (.), (<$>))

67−

68−import Control.Category

69−import Control.Concurrent

70−import Control.Concurrent.Async (race)

71−import Control.Concurrent.MVar

72−import Control.DeepSeq

73−import qualified Control.Exception as X

74−import Control.Monad

75−import Control.Monad.Trans (lift)

76−import Control.Monad.Trans.Except (ExceptT, runExceptT)

77−import Control.Monad.Trans.State.Strict (StateT, evalStateT, execStateT, get,

78− put)

79−import Data.Char

80−import Data.Either (partitionEithers)

81−import Data.List hiding (group)

82−import Data.List.Split (splitOn)

83−import Data.Maybe

84−import qualified Data.Set as S

85−import qualified Data.Text as T

86−import Data.Version

87import Network

76import Network

77+import Prelude hiding (id, (.), (<$>))

88import System.Console.Haskeline as H

78import System.Console.Haskeline as H

89import System.Directory

79import System.Directory

90import System.Environment

80import System.Environment

@@ -96,6 +86,11 @@ import System.FSNotify.Devel (allEvents, doAllEvents)

96import System.IO

86import System.IO

97import System.Process

87import System.Process

98import Text.Trifecta.Result (ErrInfo(..), Result(..))

88import Text.Trifecta.Result (ErrInfo(..), Result(..))

89+import Util.DynamicLinker

90+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

91+import Util.Pretty hiding ((</>))

92+import Util.System

93+import Version_idris (gitHash)

100-- | Run the REPL

95-- | Run the REPL

101repl :: IState -- ^ The initial state

96repl :: IState -- ^ The initial state

@@ -1457,7 +1452,6 @@ process fn (PPrint fmt width t)

1457 ty' = normaliseC ctxt [] ty

1452 ty' = normaliseC ctxt [] ty

1458 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

1453 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)

1459

1454

1460−

1461showTotal :: Totality -> IState -> Doc OutputAnnotation

1455showTotal :: Totality -> IState -> Doc OutputAnnotation

1462showTotal t@(Partial (Other ns)) i

1456showTotal t@(Partial (Other ns)) i

1463 = text "possibly not total due to:" <$>

1457 = text "possibly not total due to:" <$>

src/Idris/REPL/Parser.hs+2−7

@@ -122,6 +122,8 @@ parserCommandsForHelp =

122 ]

123 where optionsList = intercalate ", " $ map fst setOptions

124

125+

126+parserCommands :: CommandTable

125parserCommands =

127parserCommands =

126 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

128 [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

127 , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"

129 , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"

@@ -239,8 +241,6 @@ exprArg cmd name = do

239 return $ Right (cmd t)

241 return $ Right (cmd t)

240 try noArg <|> try justOperator <|> properArg

242 try noArg <|> try justOperator <|> properArg

241

243

242−

243−

244genArg :: String -> P.IdrisParser a -> (a -> Command)

245 -> String -> P.IdrisParser (Either String Command)

246genArg argName argParser cmd name = do

@@ -337,16 +337,13 @@ cmd_execute name = do

337 where

338 maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

339

340−

341cmd_dynamic :: String -> P.IdrisParser (Either String Command)

340cmd_dynamic :: String -> P.IdrisParser (Either String Command)

342cmd_dynamic name = do

341cmd_dynamic name = do

343 let optArg = do l <- many anyChar

342 let optArg = do l <- many anyChar

344 if (l /= "")

343 if (l /= "")

345 then return $ Right (DynamicLink l)

344 then return $ Right (DynamicLink l)

346 else return $ Right ListDynamic

345 else return $ Right ListDynamic

347−

348 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

346 let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"

349−

350 try optArg <|> failure

347 try optArg <|> failure

351

348

352cmd_pprint :: String -> P.IdrisParser (Either String Command)

349cmd_pprint :: String -> P.IdrisParser (Either String Command)

@@ -363,8 +360,6 @@ cmd_pprint name = do

363 ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

360 ppFormat = (discard (P.symbol "html") >> return HTMLOutput)

364 <|> (discard (P.symbol "latex") >> return LaTeXOutput)

361 <|> (discard (P.symbol "latex") >> return LaTeXOutput)

365

362

366−

367−

368cmd_compile :: String -> P.IdrisParser (Either String Command)

363cmd_compile :: String -> P.IdrisParser (Either String Command)

369cmd_compile name = do

364cmd_compile name = do

370 let defaultCodegen = Via IBCFormat "c"

365 let defaultCodegen = Via IBCFormat "c"

test/interactive001/expected+1−1

@@ -5,7 +5,7 @@ isElem x (y :: xs) = ?isElem_rhs_3

6f x :: map f xs

7isElem2 x (y :: ys) with (_)

8− isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

8+ isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

10 isElem3 y (y :: ys) | (Yes Refl) = ?isElem3_rhs_3

test/interactive001/input+8−8

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

1−:cs 12 xs

1+:casesplit 12 xs

2−:cs 18 ys

2+:casesplit 18 ys

3−:ps 22 maprhs

3+:proofsearch 22 maprhs

4−:mw 26 isElem2

4+:makewith 26 isElem2

5−:cs 31 p

5+:casesplit 31 p

6−:cs 36 xs'

6+:casesplit 36 xs'

7−:cs 39 x

7+:casesplit 39 x

8−:cs 43 case_val

8+:casesplit 43 case_val

test/interactive001/test032.idr → test/interactive001/interactive001.idrrenamed

The content is the same.

test/interactive001/run+3−1

@@ -1,3 +1,5 @@

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --port none test032.idr < input

3+${IDRIS:-idris} $@ --quiet --port none --indent-with 8 interactive001.idr < input

3rm -f *.ibc

5rm -f *.ibc

test/interactive011/.gitignorenew file+1

@@ -0,0 +1 @@

1+interactive011

test/interactive011/input+2−2

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

1−:ac 5 Show

1+:addclause 8 Show

2−:ac 7 append

2+:addclause 10 append

test/interactive011/interactive011.ipkgnew file+8

@@ -0,0 +1,8 @@

1+package interactive011

3+opts = "--quiet --indent-clause 4 --indent-with 8"

5+sourcedir = src

6+modules = Foo

7+main = Main

8+executable = interactive011

test/interactive011/run+4−1

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

1#!/usr/bin/env bash

3+cd src

2−${IDRIS:-idris} $@ --quiet --port none interactive011.idr < input

4+${IDRIS:-idris} "$@" --quiet --port none --indent-clause 4 Main.idr <../input

3rm -f *.ibc

6rm -f *.ibc

test/interactive011/src/Foo.idrnew file+5

@@ -0,0 +1,5 @@

1+module Foo

3+export

4+foo : IO ()

5+foo = putStrLn "Hello foo"

test/interactive011/interactive011.idr → test/interactive011/src/Main.idrrenamed+5−2

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

1+module Main

1import Data.Vect

3import Data.Vect

4+import Foo

3data Foo = Bar | Baz

6data Foo = Bar | Baz

@@ -7,5 +10,5 @@ implementation Show Foo where

7append : Vect n a -> Vect m a -> Vect (n + m) a

10append : Vect n a -> Vect m a -> Vect (n + m) a

8append (x :: xs) ys = ?append_rhs_2

11append (x :: xs) ys = ?append_rhs_2

10−

13+main : IO ()

11−

14+main = foo