fb33d8c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Indentation configuration via command line args.

fb33d8cSteven Shaw10 years ago

src/Idris/AbsSyntax.hs+70−61

compare with master

unifiedsplit

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

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

9+{-# LANGUAGE DeriveFunctor #-}

9− PatternGuards, TypeSynonymInstances #-}

10+{-# LANGUAGE PatternGuards #-}

11module Idris.AbsSyntax(

12module Idris.AbsSyntax(

12 module Idris.AbsSyntax

13 module Idris.AbsSyntax

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

16import Idris.AbsSyntaxTree

17import Idris.AbsSyntaxTree

17import Idris.Colours

18import Idris.Colours

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

19import Idris.Core.Evaluate

20import Idris.Core.TT

21−import Idris.Core.Typecheck

22import Idris.Docstrings

21import Idris.Docstrings

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

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

24import IRTS.CodegenCommon

23import IRTS.CodegenCommon

26−import Util.DynamicLinker

25+import System.Directory (canonicalizePath, doesFileExist)

27−import Util.Pretty

28−import Util.ScreenSize

29−import Util.System

26+import System.IO

31import Control.Applicative

28import Control.Applicative

32−import Control.Monad (liftM3)

33import Control.Monad.State

29import Control.Monad.State

34−import Data.Char

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

31+

35import Data.Either

32import Data.Either

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

37import Data.List hiding (insert, union)

33import Data.List hiding (insert, union)

38import qualified Data.Map as M

34import qualified Data.Map as M

39import Data.Maybe

35import Data.Maybe

40import qualified Data.Set as S

36import qualified Data.Set as S

41import qualified Data.Text as T

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

38+import System.IO.Error (tryIOError)

39+

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

41+

42+import Util.DynamicLinker

43+import Util.Pretty

44+import Util.System

50getContext :: Idris Context

46getContext :: Idris Context

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

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

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

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

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

92 return (Left x)

88 return (Left x)

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

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

94− findDyLib [] l = Nothing

90+ findDyLib [] _ = Nothing

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

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

96− | otherwise = findDyLib libs l

92+ | otherwise = findDyLib libs' l

98getAutoImports :: Idris [FilePath]

94getAutoImports :: Idris [FilePath]

99getAutoImports = do i <- getIState

95getAutoImports = do i <- getIState

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

102addAutoImport :: FilePath -> Idris ()

98addAutoImport :: FilePath -> Idris ()

103addAutoImport fp = do i <- getIState

99addAutoImport fp = do i <- getIState

104 let opts = idris_options i

100 let opts = idris_options i

105− let autoimps = opt_autoImport opts

106 put (i { idris_options = opts { opt_autoImport =

101 put (i { idris_options = opts { opt_autoImport =

107 fp : opt_autoImport opts } } )

102 fp : opt_autoImport opts } } )

108

103

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

250 let cs = idris_coercions i

245 let cs = idris_coercions i

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

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

252 findCoercions fn cs

247 findCoercions fn cs

253− where findCoercions t [] = []

248+ where findCoercions _ [] = []

254 findCoercions t (n : ns) =

249 findCoercions t (n : ns) =

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

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

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

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

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

322 do let (fx, _) = unApply x

317 do let (fx, _) = unApply x

323 let (fy, _) = unApply y

318 let (fy, _) = unApply y

324 case (fx, fy) of

319 case (fx, fy) of

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

320+ (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

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

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

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

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

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

329 _ -> return ()

324 _ -> return ()

330

325

331 where errWhen True

326 where errWhen True

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

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

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

354 putIState $ i { idris_function_errorhandlers = newHandlers }

349 putIState $ i { idris_function_errorhandlers = newHandlers }

355

350

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

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

363getAllNames :: Name -> Idris [Name]

352getAllNames :: Name -> Idris [Name]

364getAllNames n = do i <- getIState

353getAllNames n = do i <- getIState

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

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

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

415

404

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

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

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

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

418getNameHints i n =

407getNameHints i n =

419 case lookupCtxt n (idris_namehints i) of

408 case lookupCtxt n (idris_namehints i) of

420 [ns] -> ns

409 [ns] -> ns

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

430 i <- getIState

419 i <- getIState

431 return $ lookupCtxtExact n (idris_deprecated i)

420 return $ lookupCtxtExact n (idris_deprecated i)

432

421

433−

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

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

435addFragile n reason = do

423addFragile n reason = do

436 i <- getIState

424 i <- getIState

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

442 return $ lookupCtxtExact n (idris_fragile i)

430 return $ lookupCtxtExact n (idris_fragile i)

443

431

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

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

445−push_estack n impl

433+push_estack n implementation

446 = do i <- getIState

434 = do i <- getIState

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

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

448

436

449pop_estack :: Idris ()

437pop_estack :: Idris ()

450pop_estack = do i <- getIState

438pop_estack = do i <- getIState

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

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

452 where ptail [] = []

440 where ptail [] = []

453− ptail (x : xs) = xs

441+ ptail (_ : xs) = xs

454

442

455-- | Add an interface implementation function.

443-- | Add an interface implementation function.

456--

444--

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

546 when (notDef (ibc_write i)) $

534 when (notDef (ibc_write i)) $

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

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

548 where notDef [] = True

536 where notDef [] = True

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

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

550 notDef (_ : is) = notDef is

538 notDef (_ : is) = notDef is

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

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

552

540

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

683clearPTypes = do i <- get

671clearPTypes = do i <- get

684 let ctxt = tt_ctxt i

672 let ctxt = tt_ctxt i

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

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

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

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

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

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

688 pErase x = x

676 pErase x = x

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

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

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

699 _ -> return ()

687 _ -> return ()

700

688

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

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

702−isUndefined fc n

690+isUndefined _ n

703 = do i <- getContext

691 = do i <- getContext

704 case lookupTyExact n i of

692 case lookupTyExact n i of

705 Just _ -> return False

693 Just _ -> return False

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

756 tidyNames used (Bind n b sc)

744 tidyNames used (Bind n b sc)

757 = let n' = uniqueNameSet n used in

745 = let n' = uniqueNameSet n used in

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

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

759− tidyNames used b = b

747+ tidyNames _ b = b

760

748

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

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

762solveDeferred fc n

750solveDeferred fc n

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

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

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

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

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

1146

1134

1147−

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

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

1149logLvl = logLvlCats []

1136logLvl = logLvlCats []

1150

1137

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

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

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

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

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

1180 -> Idris ()

1167 -> Idris ()

1181−logLvlCats cs l str = do

1168+logLvlCats cs l msg = do

1182 i <- getIState

1169 i <- getIState

1183 let lvl = opt_logLevel (idris_options i)

1170 let lvl = opt_logLevel (idris_options i)

1184 let cats = opt_logcats (idris_options i)

1171 let cats = opt_logcats (idris_options i)

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

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

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

1187 case idris_outputmode i of

1174 case idris_outputmode i of

1188 RawOutput h -> do

1175 RawOutput h -> do

1189− runIO $ hPutStrLn h str

1176+ runIO $ hPutStrLn h msg

1190 IdeMode n h -> do

1177 IdeMode n h -> do

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

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

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

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

1193 where

1180 where

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

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

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

1210 let opt' = opts { opt_typecase = t }

1197 let opt' = opts { opt_typecase = t }

1211 putIState $ i { idris_options = opt' }

1198 putIState $ i { idris_options = opt' }

1212

1199

1200+getIndentWith :: Idris Int

1201+getIndentWith = do

1202+ i <- getIState

1203+ return $ interactiveOpts_indentWith (idris_interactiveOpts i)

1204+

1205+setIndentWith :: Int -> Idris ()

1206+setIndentWith indentWith = do

1207+ i <- getIState

1208+ let opts = idris_interactiveOpts i

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

1210+ putIState $ i { idris_interactiveOpts = opts' }

1211+

1212+getIndentClause :: Idris Int

1213+getIndentClause = do

1214+ i <- getIState

1215+ return $ interactiveOpts_indentClause (idris_interactiveOpts i)

1216+

1217+setIndentClause :: Int -> Idris ()

1218+setIndentClause indentClause = do

1219+ i <- getIState

1220+ let opts = idris_interactiveOpts i

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

1222+ putIState $ i { idris_interactiveOpts = opts' }

1213

1223

1214-- Dealing with parameters

1224-- Dealing with parameters

1215

1225

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

2226instance Monad (EitherErr a) where

2236instance Monad (EitherErr a) where

2227 return = RightOK

2237 return = RightOK

2228

2238

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

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

2230 RightOK v >>= k = k v

2240 RightOK v >>= k = k v

2231

2241

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

2232toEither (LeftErr e) = Left e

2243toEither (LeftErr e) = Left e

2233toEither (RightOK ho) = Right ho

2244toEither (RightOK ho) = Right ho

2234

2245

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

2439 -- looking for too long...)

2450 -- looking for too long...)

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

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

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

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

2442− initN n l = n

2453+ initN n _ = n

2443

2454

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

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

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

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

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

2547

2558

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

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

2549

2560

2550−

2551getFile :: Opt -> Maybe String

2561getFile :: Opt -> Maybe String

2552−getFile (Filename str) = Just str

2562+getFile (Filename s) = Just s

2553getFile _ = Nothing

2563getFile _ = Nothing

2554

2564

2555getBC :: Opt -> Maybe String

2565getBC :: Opt -> Maybe String

2556−getBC (BCAsm str) = Just str

2566+getBC (BCAsm s) = Just s

2557getBC _ = Nothing

2567getBC _ = Nothing

2558

2568

2559getOutput :: Opt -> Maybe String

2569getOutput :: Opt -> Maybe String

2560−getOutput (Output str) = Just str

2570+getOutput (Output s) = Just s

2561getOutput _ = Nothing

2571getOutput _ = Nothing

2562

2572

2563getIBCSubDir :: Opt -> Maybe String

2573getIBCSubDir :: Opt -> Maybe String

2564−getIBCSubDir (IBCSubDir str) = Just str

2574+getIBCSubDir (IBCSubDir s) = Just s

2565getIBCSubDir _ = Nothing

2575getIBCSubDir _ = Nothing

2566

2576

2567getImportDir :: Opt -> Maybe String

2577getImportDir :: Opt -> Maybe String

2568−getImportDir (ImportDir str) = Just str

2578+getImportDir (ImportDir s) = Just s

2569getImportDir _ = Nothing

2579getImportDir _ = Nothing

2570

2580

2571getSourceDir :: Opt -> Maybe String

2581getSourceDir :: Opt -> Maybe String

2572−getSourceDir (SourceDir str) = Just str

2582+getSourceDir (SourceDir s) = Just s

2573getSourceDir _ = Nothing

2583getSourceDir _ = Nothing

2574

2584

2575getPkgDir :: Opt -> Maybe String

2585getPkgDir :: Opt -> Maybe String

2576−getPkgDir (Pkg str) = Just str

2586+getPkgDir (Pkg s) = Just s

2577getPkgDir _ = Nothing

2587getPkgDir _ = Nothing

2578

2588

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

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

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

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

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

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

2582getPkg _ = Nothing

2592getPkg _ = Nothing

2583

2593

2584getPkgClean :: Opt -> Maybe String

2594getPkgClean :: Opt -> Maybe String

2585−getPkgClean (PkgClean str) = Just str

2595+getPkgClean (PkgClean s) = Just s

2586getPkgClean _ = Nothing

2596getPkgClean _ = Nothing

2587

2597

2588getPkgREPL :: Opt -> Maybe String

2598getPkgREPL :: Opt -> Maybe String

2589−getPkgREPL (PkgREPL str) = Just str

2599+getPkgREPL (PkgREPL s) = Just s

2590getPkgREPL _ = Nothing

2600getPkgREPL _ = Nothing

2591

2601

2592getPkgCheck :: Opt -> Maybe String

2602getPkgCheck :: Opt -> Maybe String

2593−getPkgCheck (PkgCheck str) = Just str

2603+getPkgCheck (PkgCheck s) = Just s

2594getPkgCheck _ = Nothing

2604getPkgCheck _ = Nothing

2595

2605

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

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

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

2618getConsoleWidth (UseConsoleWidth x) = Just x

2628getConsoleWidth (UseConsoleWidth x) = Just x

2619getConsoleWidth _ = Nothing

2629getConsoleWidth _ = Nothing

2620

2630

2621−

2622getExecScript :: Opt -> Maybe String

2631getExecScript :: Opt -> Maybe String

2623getExecScript (InterpretScript expr) = Just expr

2632getExecScript (InterpretScript expr) = Just expr

2624getExecScript _ = Nothing

2633getExecScript _ = Nothing

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

2667-- Get the first valid port

2676-- Get the first valid port

2668getPort :: [Opt] -> Maybe REPLPort

2677getPort :: [Opt] -> Maybe REPLPort

2669getPort [] = Nothing

2678getPort [] = Nothing

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

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

2671getPort (_ : xs) = getPort xs

2680getPort (_ : xs) = getPort xs

2672

2681

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

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

src/Idris/AbsSyntaxTree.hs+45−20

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

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

9+{-# LANGUAGE DeriveDataTypeable #-}

9− FlexibleInstances, MultiParamTypeClasses, PatternGuards,

10+{-# LANGUAGE DeriveFunctor #-}

10− TypeSynonymInstances #-}

11+{-# LANGUAGE DeriveGeneric #-}

12+{-# LANGUAGE PatternGuards #-}

12module Idris.AbsSyntaxTree where

14module Idris.AbsSyntaxTree where

14−import Idris.Colours

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

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

16import Idris.Core.Evaluate

17import Idris.Core.Evaluate

17import Idris.Core.TT

18import Idris.Core.TT

18−import Idris.Core.Typecheck

19import Idris.Docstrings

20import IRTS.CodegenCommon

21import IRTS.Lang

22import Util.DynamicLinker

23import Util.Pretty

25+import Idris.Colours

26+

27+import System.IO

28+

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

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

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

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

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

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

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

30import Control.Monad.Trans.State.Strict

34import Control.Monad.Trans.State.Strict

31import Data.Char

35import Data.Char

32import Data.Data (Data)

36import Data.Data (Data)

33−import Data.Either

37+

34import Data.Foldable (Foldable)

38import Data.Foldable (Foldable)

35import Data.Function (on)

39import Data.Function (on)

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

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

37import Data.List hiding (group)

41import Data.List hiding (group)

38import qualified Data.Map.Strict as M

42import qualified Data.Map.Strict as M

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

43+import Data.Maybe (mapMaybe, maybeToList)

40import qualified Data.Set as S

44import qualified Data.Set as S

41import qualified Data.Text as T

45import qualified Data.Text as T

42import Data.Traversable (Traversable)

46import Data.Traversable (Traversable)

43import Data.Typeable

47import Data.Typeable

44−import Data.Word (Word)

45−import Debug.Trace

46import GHC.Generics (Generic)

48import GHC.Generics (Generic)

47import Network.Socket (PortNumber)

49import Network.Socket (PortNumber)

48−import System.Console.Haskeline

50+

49−import System.IO

50−import Text.PrettyPrint.Annotated.Leijen

52data ElabWhat = ETypes | EDefns | EAll

53 deriving (Show, Eq)

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

112 , opt_autoimpls :: Bool

113 } deriving (Show, Eq, Generic)

114

115+defaultOpts :: IOption

115defaultOpts = IOption { opt_logLevel = 0

116defaultOpts = IOption { opt_logLevel = 0

116 , opt_logcats = []

117 , opt_logcats = []

117 , opt_typecase = False

118 , opt_typecase = False

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

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

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

152 deriving (Show, Eq, Generic)

153 deriving (Show, Eq, Generic)

153

154

155+defaultOptimise :: [Optimisation]

154defaultOptimise = [PETransform]

156defaultOptimise = [PETransform]

155

157

156-- | Pretty printing options with default verbosity.

158-- | Pretty printing options with default verbosity.

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

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

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

207 deriving (Show, Eq, Generic)

209 deriving (Show, Eq, Generic)

208

210

211+-- | Configuration options for interactive editing.

212+data InteractiveOpts = InteractiveOpts {

213+ interactiveOpts_indentWith :: Int

214+ , interactiveOpts_indentClause :: Int

215+} deriving (Show, Generic)

216+

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

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

210data IState = IState {

218data IState = IState {

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

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

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

294 , idris_repl_defs :: [Name]

302 , idris_repl_defs :: [Name]

295

303

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

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

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

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

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

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

299

307

300

308

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

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

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

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

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

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

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

309− }

317+ , idris_interactiveOpts :: InteractiveOpts

310− deriving Generic

318+ } deriving Generic

311

319

312-- Required for parsers library, and therefore trifecta

320-- Required for parsers library, and therefore trifecta

313instance Show IState where

321instance Show IState where

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

332deriving instance Binary CGInfo

340deriving instance Binary CGInfo

333!-}

341!-}

334

342

343+primDefs :: [Name]

335primDefs = [ sUN "unsafePerformPrimIO"

344primDefs = [ sUN "unsafePerformPrimIO"

336 , sUN "mkLazyForeignPrim"

345 , sUN "mkLazyForeignPrim"

337 , sUN "mkForeignPrim"

346 , sUN "mkForeignPrim"

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

390 | IBCConstraint FC UConstraint

399 | IBCConstraint FC UConstraint

391 deriving (Show, Generic)

400 deriving (Show, Generic)

392

401

402+initialInteractiveOpts :: InteractiveOpts

403+initialInteractiveOpts = InteractiveOpts {

404+ interactiveOpts_indentWith = 2

405+ , interactiveOpts_indentClause = 2

406+}

407+

393-- | The initial state for the compiler

408-- | The initial state for the compiler

394idrisInit :: IState

409idrisInit :: IState

395idrisInit = IState initContext S.empty []

410idrisInit = IState initContext S.empty []

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

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

417 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

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

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

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

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

405− emptyContext S.empty M.empty emptyContext

420+ emptyContext S.empty M.empty emptyContext initialInteractiveOpts

406

421

407

422

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

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

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

488 | ColourREPL Bool

503 | ColourREPL Bool

489 | Idemode

504 | Idemode

490 | IdemodeSocket

505 | IdemodeSocket

506+ | IndentWith Int

507+ | IndentClause Int

491 | ShowAll

508 | ShowAll

492 | ShowLibs

509 | ShowLibs

493 | ShowLibDir

510 | ShowLibDir

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

627is_scoped _ = Nothing

644is_scoped _ = Nothing

628

645

629-- Top level implicit

646-- Top level implicit

647+impl :: Plicity

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

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

631-- Machine generated top level implicit

649-- Machine generated top level implicit

650+impl_gen :: Plicity

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

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

633

652

634-- Scoped implicits

653-- Scoped implicits

654+forall_imp :: Plicity

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

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

656+forall_constraint :: Plicity

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

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

637

658

659+expl :: Plicity

638expl = Exp [] Dynamic False RigW

660expl = Exp [] Dynamic False RigW

661+expl_param :: Plicity

639expl_param = Exp [] Dynamic True RigW

662expl_param = Exp [] Dynamic True RigW

640

663

664+constraint :: Plicity

641constraint = Constraint [] Static RigW

665constraint = Constraint [] Static RigW

642

666

667+tacimpl :: PTerm -> Plicity

643tacimpl t = TacImp [] Dynamic t RigW

668tacimpl t = TacImp [] Dynamic t RigW

644

669

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

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

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

1410-- Interface data

1435-- Interface data

1411

1436

1412data InterfaceInfo = CI {

1437data InterfaceInfo = CI {

1413− implementationCtorName :: Name

1438+ implementationCtorName :: Name

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

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

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

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

1416 , interface_default_super_interfaces :: [PDecl]

1441 , interface_default_super_interfaces :: [PDecl]

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

2269

2294

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

2295getShowArgs :: [PArg] -> [PArg]

2271getShowArgs [] = []

2296getShowArgs [] = []

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

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

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

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

2274 | PImp _ _ _ _ tm <- e

2299 | PImp _ _ _ _ tm <- e

2275 , containsHole tm = e : getShowArgs xs

2300 , containsHole tm = e : getShowArgs xs

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

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

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

2587getErasureInfo ist n =

2612getErasureInfo ist n =

2588 case lookupCtxtExact n (idris_optimisation ist) of

2613 case lookupCtxtExact n (idris_optimisation ist) of

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

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

2590 Nothing -> []

2615 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+10−4

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

5License : BSD3

6Maintainer : The Idris Community.

7-}

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

9+{-# LANGUAGE DeriveFunctor #-}

10+{-# LANGUAGE MultiWayIf #-}

11+{-# LANGUAGE PatternGuards #-}

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

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

13+

10module Idris.Docs (

14module Idris.Docs (

11 pprintDocs

15 pprintDocs

12 , getDocs, pprintConstDocs, pprintTypeDoc

16 , getDocs, pprintConstDocs, pprintTypeDoc

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

17 , FunDoc, FunDoc'(..), Docs, Docs'(..)

14 ) where

18 ) where

16−import Idris.AbsSyntax

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

17−import Idris.AbsSyntaxTree

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

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

23+ getIState, modDocName, ppOptionIst, pprintPTerm,

24+ prettyIst, prettyName, type1Doc, typeDescription)

18import Idris.Core.Evaluate

25import Idris.Core.Evaluate

19import Idris.Core.TT

26import Idris.Core.TT

20import Idris.Delaborate

27import Idris.Delaborate

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

27import Prelude hiding ((<$>))

34import Prelude hiding ((<$>))

29−import Control.Arrow (first)

30import Data.List

36import Data.List

31import Data.Maybe

37import Data.Maybe

32import qualified Data.Text as T

38import qualified Data.Text as T

src/Idris/Interactive.hs+33−23

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

@@ -55,18 +52,31 @@ caseSplitAt fn updatefile l n

56addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

53addClauseFrom :: FilePath -> Bool -> Int -> Name -> Idris ()

57addClauseFrom fn updatefile l n = do

54addClauseFrom fn updatefile l n = do

55+{-

56+ runIO . traceIO $ "addClauseFrom: " ++ show (M.fromList

57+ [ ("fn", fn)

58+ , ("updatefile", show updatefile)

59+ , ("line", show l)

60+ , ("name", show n)

61+ ])

62+-}

58 -- if a definition already exists, add missing cases rather than

63 -- if a definition already exists, add missing cases rather than

59 -- adding a new definition.

64 -- adding a new definition.

60 ist <- getIState

65 ist <- getIState

61 cl <- getInternalApp fn l

66 cl <- getInternalApp fn l

67+-- runIO . traceIO $ "cl = " ++ show cl

62 let fulln = getAppName cl

68 let fulln = getAppName cl

69+-- runIO . traceIO $ "fulln = " ++ show fulln

64− case lookup fulln (idris_metavars ist) of

71+ let metavars = lookup fulln (idris_metavars ist)

72+-- runIO . traceIO $ "metavars = " ++ show metavars

73+ case metavars of

65 Nothing -> addMissing fn updatefile l n

74 Nothing -> addMissing fn updatefile l n

66 Just _ -> do

75 Just _ -> do

67 src <- runIO $ readSource fn

76 src <- runIO $ readSource fn

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

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

69 let indent = getIndent 0 (show n) tyline

78 let indent = getIndent 0 (show n) tyline

79+-- runIO . traceIO $ "getIndent => " ++ show indent

70 cl <- getClause l fulln n fn

80 cl <- getClause l fulln n fn

71 -- add clause before first blank line in 'later'

81 -- add clause before first blank line in 'later'

72 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

82 let (nonblank, rest) = span (not . all isSpace) (tyline:later)

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

164

174

165

175

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

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

167−makeWith fn updatefile l n

177+makeWith fn updatefile l n = do

168− = do src <- runIO $ readSource fn

178+ src <- runIO $ readSource fn

179+ i <- getIState

180+ indentWith <- getIndentWith

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

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

170− let ind = getIndent tyline

182+ let ind = getIndent tyline

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

171− let with = mkWith tyline n

184+ let with = mkWith tyline n indentWith

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

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

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

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

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

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

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

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

176− if updatefile then

189+ if updatefile

190+ then do

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

191+ let fb = fn ++ "~"

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

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

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

180− unlines rest)

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

181− runIO $ copyFile fb fn

194+ runIO $ copyFile fb fn

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

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

183 where getIndent s = length (takeWhile isSpace s)

196 where getIndent s = length (takeWhile isSpace s)

184

197

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

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

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

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

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

222

235

223

236

224−

225−

226−

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

237doProofSearch :: FilePath -> Bool -> Bool ->

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

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

229doProofSearch fn updatefile rec l n hints Nothing

239doProofSearch 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