c03fa21 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Enable configuration of indentation in interactive mode

commitc03fa2199a0b632f7cf72c2a5329db1ff7270300 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateSun 15 Jan 2017, 16:47 (10 years ago) parentbc91270 a463bb1

20 files changed+281−231

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+69−61

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

9− PatternGuards, TypeSynonymInstances #-}

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

1010

1111module Idris.AbsSyntax(

1212 module Idris.AbsSyntax

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

1515

1616import Idris.AbsSyntaxTree

1717import Idris.Colours

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

1918import Idris.Core.Evaluate

2019import Idris.Core.TT

21−import Idris.Core.Typecheck

2220import Idris.Docstrings

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

2422import IRTS.CodegenCommon

2523

26−import Util.DynamicLinker

27−import Util.Pretty

28−import Util.ScreenSize

29−import Util.System

24+import System.Directory (canonicalizePath, doesFileExist)

25+import System.IO

3026

3127import Control.Applicative

32−import Control.Monad (liftM3)

3328import Control.Monad.State

34−import Data.Char

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

30+

3531import Data.Either

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

3732import Data.List hiding (insert, union)

3833import qualified Data.Map as M

3934import Data.Maybe

4035import qualified Data.Set as S

4136import 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

4944

5045getContext :: Idris Context

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

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

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

9287 return (Left x)

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

94− findDyLib [] l = Nothing

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

96− | otherwise = findDyLib libs l

89+ findDyLib [] _ = Nothing

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

91+ | otherwise = findDyLib libs' l

9792

9893getAutoImports :: Idris [FilePath]

9994getAutoImports = do i <- getIState

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

10297addAutoImport :: FilePath -> Idris ()

10398addAutoImport fp = do i <- getIState

10499 let opts = idris_options i

105− let autoimps = opt_autoImport opts

106100 put (i { idris_options = opts { opt_autoImport =

107101 fp : opt_autoImport opts } } )

108102

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

250244 let cs = idris_coercions i

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

252246 findCoercions fn cs

253− where findCoercions t [] = []

247+ where findCoercions _ [] = []

254248 findCoercions t (n : ns) =

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

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

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

322316 do let (fx, _) = unApply x

323317 let (fy, _) = unApply y

324318 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')?

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

327321 (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')?

329323 _ -> return ()

330324

331325 where errWhen True

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

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

354348 putIState $ i { idris_function_errorhandlers = newHandlers }

355349

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−

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

363351getAllNames :: Name -> Idris [Name]

364352getAllNames n = do i <- getIState

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

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

415403

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

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

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

418406getNameHints i n =

419407 case lookupCtxt n (idris_namehints i) of

420408 [ns] -> ns

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

430418 i <- getIState

431419 return $ lookupCtxtExact n (idris_deprecated i)

432420

433−

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

435422addFragile n reason = do

436423 i <- getIState

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

442429 return $ lookupCtxtExact n (idris_fragile i)

443430

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

445−push_estack n impl

432+push_estack n implementation

446433 = do i <- getIState

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

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

448435

449436pop_estack :: Idris ()

450437pop_estack = do i <- getIState

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

452439 where ptail [] = []

453− ptail (x : xs) = xs

440+ ptail (_ : xs) = xs

454441

455442-- | Add an interface implementation function.

456443--

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

546533 when (notDef (ibc_write i)) $

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

548535 where notDef [] = True

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

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

550537 notDef (_ : is) = notDef is

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

552539

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

683670clearPTypes = do i <- get

684671 let ctxt = tt_ctxt i

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

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

688675 pErase x = x

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

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

699686 _ -> return ()

700687

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

702−isUndefined fc n

689+isUndefined _ n

703690 = do i <- getContext

704691 case lookupTyExact n i of

705692 Just _ -> return False

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

756743 tidyNames used (Bind n b sc)

757744 = let n' = uniqueNameSet n used in

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

759− tidyNames used b = b

746+ tidyNames _ b = b

760747

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

762749solveDeferred fc n

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

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

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

11461133

1147−

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

11491135logLvl = logLvlCats []

11501136

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

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

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

11801166 -> Idris ()

1181−logLvlCats cs l str = do

1167+logLvlCats cs l msg = do

11821168 i <- getIState

11831169 let lvl = opt_logLevel (idris_options i)

11841170 let cats = opt_logcats (idris_options i)

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

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

11871173 case idris_outputmode i of

11881174 RawOutput h -> do

1189− runIO $ hPutStrLn h str

1175+ runIO $ hPutStrLn h msg

11901176 IdeMode n h -> do

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

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

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

11931179 where

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

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

12101196 let opt' = opts { opt_typecase = t }

12111197 putIState $ i { idris_options = opt' }

12121198

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

12131222

12141223-- Dealing with parameters

12151224

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

22262235instance Monad (EitherErr a) where

22272236 return = RightOK

22282237

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

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

22302239 RightOK v >>= k = k v

22312240

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

22322242toEither (LeftErr e) = Left e

22332243toEither (RightOK ho) = Right ho

22342244

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

24392449 -- looking for too long...)

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

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

2442− initN n l = n

2452+ initN n _ = n

24432453

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

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

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

25472557

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

25492559

2550−

25512560getFile :: Opt -> Maybe String

2552−getFile (Filename str) = Just str

2561+getFile (Filename s) = Just s

25532562getFile _ = Nothing

25542563

25552564getBC :: Opt -> Maybe String

2556−getBC (BCAsm str) = Just str

2565+getBC (BCAsm s) = Just s

25572566getBC _ = Nothing

25582567

25592568getOutput :: Opt -> Maybe String

2560−getOutput (Output str) = Just str

2569+getOutput (Output s) = Just s

25612570getOutput _ = Nothing

25622571

25632572getIBCSubDir :: Opt -> Maybe String

2564−getIBCSubDir (IBCSubDir str) = Just str

2573+getIBCSubDir (IBCSubDir s) = Just s

25652574getIBCSubDir _ = Nothing

25662575

25672576getImportDir :: Opt -> Maybe String

2568−getImportDir (ImportDir str) = Just str

2577+getImportDir (ImportDir s) = Just s

25692578getImportDir _ = Nothing

25702579

25712580getSourceDir :: Opt -> Maybe String

2572−getSourceDir (SourceDir str) = Just str

2581+getSourceDir (SourceDir s) = Just s

25732582getSourceDir _ = Nothing

25742583

25752584getPkgDir :: Opt -> Maybe String

2576−getPkgDir (Pkg str) = Just str

2585+getPkgDir (Pkg s) = Just s

25772586getPkgDir _ = Nothing

25782587

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

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

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

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

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

25822591getPkg _ = Nothing

25832592

25842593getPkgClean :: Opt -> Maybe String

2585−getPkgClean (PkgClean str) = Just str

2594+getPkgClean (PkgClean s) = Just s

25862595getPkgClean _ = Nothing

25872596

25882597getPkgREPL :: Opt -> Maybe String

2589−getPkgREPL (PkgREPL str) = Just str

2598+getPkgREPL (PkgREPL s) = Just s

25902599getPkgREPL _ = Nothing

25912600

25922601getPkgCheck :: Opt -> Maybe String

2593−getPkgCheck (PkgCheck str) = Just str

2602+getPkgCheck (PkgCheck s) = Just s

25942603getPkgCheck _ = Nothing

25952604

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

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

26182627getConsoleWidth (UseConsoleWidth x) = Just x

26192628getConsoleWidth _ = Nothing

26202629

2621−

26222630getExecScript :: Opt -> Maybe String

26232631getExecScript (InterpretScript expr) = Just expr

26242632getExecScript _ = Nothing

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

26672675-- Get the first valid port

26682676getPort :: [Opt] -> Maybe REPLPort

26692677getPort [] = Nothing

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

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

26712679getPort (_ : xs) = getPort xs

26722680

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

src/Idris/AbsSyntaxTree.hs+42−20

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

9− FlexibleInstances, MultiParamTypeClasses, PatternGuards,

10− TypeSynonymInstances #-}

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

1110

1211module Idris.AbsSyntaxTree where

1312

14−import Idris.Colours

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

1614import Idris.Core.Evaluate

1715import Idris.Core.TT

18−import Idris.Core.Typecheck

1916import Idris.Docstrings

2017import IRTS.CodegenCommon

2118import IRTS.Lang

2219import Util.DynamicLinker

2320import Util.Pretty

2421

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

22+import Idris.Colours

23+

24+import System.IO

25+

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

2627

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

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

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

3031import Control.Monad.Trans.State.Strict

3132import Data.Char

3233import Data.Data (Data)

33−import Data.Either

34+

3435import Data.Foldable (Foldable)

3536import Data.Function (on)

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

3738import Data.List hiding (group)

3839import qualified Data.Map.Strict as M

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

40+import Data.Maybe (mapMaybe, maybeToList)

4041import qualified Data.Set as S

4142import qualified Data.Text as T

4243import Data.Traversable (Traversable)

4344import Data.Typeable

44−import Data.Word (Word)

45−import Debug.Trace

4645import GHC.Generics (Generic)

4746import Network.Socket (PortNumber)

48−import System.Console.Haskeline

49−import System.IO

50−import Text.PrettyPrint.Annotated.Leijen

47+

5148

5249data ElabWhat = ETypes | EDefns | EAll

5350 deriving (Show, Eq)

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

112109 , opt_autoimpls :: Bool

113110 } deriving (Show, Eq, Generic)

114111

112+defaultOpts :: IOption

115113defaultOpts = IOption { opt_logLevel = 0

116114 , opt_logcats = []

117115 , opt_typecase = False

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

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

152150 deriving (Show, Eq, Generic)

153151

152+defaultOptimise :: [Optimisation]

154153defaultOptimise = [PETransform]

155154

156155-- | Pretty printing options with default verbosity.

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

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

207206 deriving (Show, Eq, Generic)

208207

208+-- | Configuration options for interactive editing.

209+data InteractiveOpts = InteractiveOpts {

210+ interactiveOpts_indentWith :: Int

211+ , interactiveOpts_indentClause :: Int

212+} deriving (Show, Generic)

213+

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

210215data IState = IState {

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

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

294299 , idris_repl_defs :: [Name]

295300

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

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

299304

300305

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

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

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

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

309− }

310− deriving Generic

314+ , idris_interactiveOpts :: InteractiveOpts

315+ } deriving Generic

311316

312317-- Required for parsers library, and therefore trifecta

313318instance Show IState where

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

332337deriving instance Binary CGInfo

333338!-}

334339

340+primDefs :: [Name]

335341primDefs = [ sUN "unsafePerformPrimIO"

336342 , sUN "mkLazyForeignPrim"

337343 , sUN "mkForeignPrim"

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

390396 | IBCConstraint FC UConstraint

391397 deriving (Show, Generic)

392398

399+initialInteractiveOpts :: InteractiveOpts

400+initialInteractiveOpts = InteractiveOpts {

401+ interactiveOpts_indentWith = 2

402+ , interactiveOpts_indentClause = 2

403+}

404+

393405-- | The initial state for the compiler

394406idrisInit :: IState

395407idrisInit = IState initContext S.empty []

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

402414 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

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

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

405− emptyContext S.empty M.empty emptyContext

417+ emptyContext S.empty M.empty emptyContext initialInteractiveOpts

406418

407419

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

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

488500 | ColourREPL Bool

489501 | Idemode

490502 | IdemodeSocket

503+ | IndentWith Int

504+ | IndentClause Int

491505 | ShowAll

492506 | ShowLibs

493507 | ShowLibDir

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

627641is_scoped _ = Nothing

628642

629643-- Top level implicit

644+impl :: Plicity

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

631646-- Machine generated top level implicit

647+impl_gen :: Plicity

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

633649

634650-- Scoped implicits

651+forall_imp :: Plicity

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

653+forall_constraint :: Plicity

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

637655

656+expl :: Plicity

638657expl = Exp [] Dynamic False RigW

658+expl_param :: Plicity

639659expl_param = Exp [] Dynamic True RigW

640660

661+constraint :: Plicity

641662constraint = Constraint [] Static RigW

642663

664+tacimpl :: PTerm -> Plicity

643665tacimpl t = TacImp [] Dynamic t RigW

644666

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

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

14101432-- Interface data

14111433

14121434data InterfaceInfo = CI {

1413− implementationCtorName :: Name

1435+ implementationCtorName :: Name

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

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

14161438 , interface_default_super_interfaces :: [PDecl]

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

22692291

22702292getShowArgs :: [PArg] -> [PArg]

22712293getShowArgs [] = []

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

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

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

22742296 | PImp _ _ _ _ tm <- e

22752297 , containsHole tm = e : getShowArgs xs

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

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

25872609getErasureInfo ist n =

25882610 case lookupCtxtExact n (idris_optimisation ist) of

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

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

25902612 Nothing -> []

src/Idris/CaseSplit.hs+19−27

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

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

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

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

18−

1918-}

19+

2020{-# LANGUAGE PatternGuards #-}

2121

2222module Idris.CaseSplit(

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

2828 ) where

2929

3030import Idris.AbsSyntax

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

3231import Idris.Core.Evaluate

3332import Idris.Core.TT

34−import Idris.Core.Typecheck

3533import Idris.Delaborate

3634import Idris.Elab.Term

3735import Idris.Elab.Value

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

3937import Idris.Error

4038import Idris.Output

4139import Idris.Parser

42−import Idris.Parser.Helpers

4340

4441import Control.Monad

4542import Control.Monad.State.Strict

4643import Data.Char

4744import 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

5445

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

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

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

109100 explicit :: [Name],

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

111102

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

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

113104addUpdate n tm = do ms <- get

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

115106

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

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

117108inventName ist ty n =

118109 do ms <- get

119110 let supp = case ty of

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

142133varlist :: [Name]

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

144135

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

136+stripNS :: PTerm -> PTerm

146137stripNS tm = mapPT dens tm where

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

148139 dens t = t

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

395386 -> Name -- ^ User given name

396387 -> FilePath -- ^ Source file name

397388 -> Idris String

398−getClause l fn un fp

389+getClause l _ un fp

399390 = do i <- getIState

391+ indentClause <- getIndentClause

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

400393 case lookupCtxt un (idris_interfaces i) of

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

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

402395 _ -> do ty_in <- getInternalApp fp l

403396 let ty = case ty_in of

404− PTyped n t -> t

397+ PTyped _ t -> t

405398 x -> x

406399 ist <- get

407− let ap = mkApp ist ty []

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

400+ let app = mkApp ist ty []

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

409402 ++ showRHSName un ++ "_rhs")

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

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

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

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

432425 sUN "z"]) used

433426

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

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

436− mkInterfaceBodies i ns

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

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

429+ mkInterfaceBodies indent i ns

437430 = showSep "\n"

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

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

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

440433 ++ mkApp i ty []

441434 ++ "= ?"

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

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

461454-- match clause

462455

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

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

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

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

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

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

466459

467460 where replaceRHS [] str = str

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

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

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

472465

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

474− newpat patstr =

475− " " ++

467+ newpat patstr = replicate indent ' ' ++

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

477469

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

89{-# LANGUAGE Arrows #-}

10+

911module Idris.CmdOptions

1012 (

1113 module Idris.CmdOptions

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

1921 getPort, opt)

2022import Idris.AbsSyntaxTree

2123import Idris.Info (getIdrisVersion)

22−-- import Idris.REPL

2324import IRTS.CodegenCommon

2425

2526import Control.Monad.Trans (lift)

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

3334import Options.Applicative

3435import Options.Applicative.Arrows

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

36−import Safe (lastMay)

37+

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

39+

40+import Safe (lastMay)

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

3942

4043runArgParser :: IO [Opt]

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

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

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

99102

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

103+ -- Client flags

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

101105

102106 -- Logging Flags

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

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

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

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

105109 (long "logging-categories"

106110 <> metavar "CATS"

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

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

108112

109113 -- Turn off things

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

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

113117

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

115119

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

117121

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

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

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

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

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

140144

141− <|> (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"))

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

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

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

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

144148

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

146150

147− <|> (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"))

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

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

149153

150154 -- Package commands

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

159171

160172 -- Misc options

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

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

162174

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

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

165177

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

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

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

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

168180

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

170182 <> metavar "TARGET"

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

174186 <> metavar "TARGET"

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

176188

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

178− <> metavar "ARG"

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

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

190+ <> metavar "ARG"

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

180192

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

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

194+ <> short 'e'

195+ <> metavar "EXPR"

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

182197

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

185200

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

187202 <> short 'X'

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

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

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

199214

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

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

201216

202− <|> (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"))

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

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

204219

205220 -- Colour Options

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

src/Idris/DeepSeq.hs+1

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

108108instance NFData SyntaxInfo

109109instance NFData DefaultTotality

110110instance NFData IState

111+instance NFData InteractiveOpts

src/Idris/Docs.hs+7−3

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

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

11+

1012module Idris.Docs (

1113 pprintDocs

1214 , getDocs, pprintConstDocs, pprintTypeDoc

1315 , FunDoc, FunDoc'(..), Docs, Docs'(..)

1416 ) where

1517

16−import Idris.AbsSyntax

17−import Idris.AbsSyntaxTree

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

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

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

21+ getIState, modDocName, ppOptionIst, pprintPTerm,

22+ prettyIst, prettyName, type1Doc, typeDescription)

1823import Idris.Core.Evaluate

1924import Idris.Core.TT

2025import Idris.Delaborate

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

2631

2732import Prelude hiding ((<$>))

2833

29−import Control.Arrow (first)

3034import Data.List

3135import Data.Maybe

3236import qualified Data.Text as T

src/Idris/Interactive.hs+21−24

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

3232

3333import Data.Char

3434import Data.List (isSuffixOf)

35−import Data.Maybe (fromMaybe)

36−import Debug.Trace

3735import System.Directory

38−import System.FilePath

3936import System.IO

4037

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

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

6057 ist <- getIState

6158 cl <- getInternalApp fn l

6259 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

6562 Nothing -> addMissing fn updatefile l n

6663 Just _ -> do

6764 src <- runIO $ readSource fn

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

164161

165162

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

167−makeWith fn updatefile l n

168− = do src <- runIO $ readSource fn

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

170− let ind = getIndent tyline

171− let with = mkWith tyline n

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

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

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

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

176− if updatefile then

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

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

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

180− unlines rest)

181− runIO $ copyFile fb fn

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

164+makeWith fn updatefile l n = do

165+ src <- runIO $ readSource fn

166+ i <- getIState

167+ indentWith <- getIndentWith

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

169+ let ind = getIndent tyline

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

171+ let with = mkWith tyline n indentWith

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

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

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

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

176+ if updatefile

177+ then do

178+ let fb = fn ++ "~"

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

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

181+ runIO $ copyFile fb fn

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

183183 where getIndent s = length (takeWhile isSpace s)

184184

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

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

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

222222

223223

224−

225−

226−

227224doProofSearch :: FilePath -> Bool -> Bool ->

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

229226doProofSearch fn updatefile rec l n hints Nothing

src/Idris/Main.hs+11−11

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

3131

3232import Util.System

3333

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

35−

3634import Control.Category

3735import Control.DeepSeq

3836import Control.Monad

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

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

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

4240import Data.Maybe

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

4342import System.Console.Haskeline as H

4443import System.Directory

4544import System.Exit

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

5655 exitFailure

5756 Right _ -> return ()

5857

59−

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

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

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

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

215213 ok <- noErrors

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

217215 where

218− makeOption (OLogging i) = setLogLevel i

219− makeOption (OLogCats cs) = setLogCats cs

220− makeOption (Verbose v) = setVerbose v

221− makeOption TypeCase = setTypeCase True

222− makeOption TypeInType = setTypeInType True

223− makeOption NoCoverage = setCoverage False

224− makeOption ErrContext = setErrContext True

225− makeOption _ = return ()

216+ makeOption (OLogging i) = setLogLevel i

217+ makeOption (OLogCats cs) = setLogCats cs

218+ makeOption (Verbose v) = setVerbose v

219+ makeOption TypeCase = setTypeCase True

220+ makeOption TypeInType = setTypeInType True

221+ makeOption NoCoverage = setCoverage False

222+ makeOption ErrContext = setErrContext True

223+ makeOption (IndentWith n) = setIndentWith n

224+ makeOption (IndentClause n) = setIndentClause n

225+ makeOption _ = return ()

226226

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

228228 processOptimisation (True, p) = addOptimise p

src/Idris/REPL.hs+27−33

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

44License : BSD3

55Maintainer : The Idris Community.

66-}

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

8− PatternGuards #-}

8+{-# LANGUAGE PatternGuards #-}

910module Idris.REPL

1011 ( idemodeStart

1112 , startServer

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

1617 , proofs

1718 ) where

1819

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

1937import Idris.AbsSyntax

2038import Idris.Apropos (apropos, aproposModules)

2139import Idris.ASTUtils

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

2947import Idris.Core.WHNF

3048import Idris.Coverage

3149import Idris.Delaborate

32−import Idris.Docs hiding (Doc)

50+import Idris.Docs

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

3452import Idris.Elab.Clause

3553import Idris.Elab.Term

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

5573import Idris.TypeSearch (searchByType)

5674import Idris.WhoCalls

5775import 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

8776import Network

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

8878import System.Console.Haskeline as H

8979import System.Directory

9080import System.Environment

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

9686import System.IO

9787import System.Process

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

9994

10095-- | Run the REPL

10196repl :: IState -- ^ The initial state

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

14571452 ty' = normaliseC ctxt [] ty

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

14591454

1460−

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

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

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

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

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

122122 ]

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

124124

125+

126+parserCommands :: CommandTable

125127parserCommands =

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

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

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

239241 return $ Right (cmd t)

240242 try noArg <|> try justOperator <|> properArg

241243

242−

243−

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

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

246246genArg argName argParser cmd name = do

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

337337 where

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

339339

340−

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

342341cmd_dynamic name = do

343342 let optArg = do l <- many anyChar

344343 if (l /= "")

345344 then return $ Right (DynamicLink l)

346345 else return $ Right ListDynamic

347−

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

349−

350347 try optArg <|> failure

351348

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

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

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

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

365362

366−

367−

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

369364cmd_compile name = do

370365 let defaultCodegen = Via IBCFormat "c"

test/interactive001/expected+1−1

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

66f x :: map f xs

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

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

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

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

1111

test/interactive001/input+8−8

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

1−:cs 12 xs

2−:cs 18 ys

3−:ps 22 maprhs

4−:mw 26 isElem2

5−:cs 31 p

6−:cs 36 xs'

7−:cs 39 x

8−:cs 43 case_val

1+:casesplit 12 xs

2+:casesplit 18 ys

3+:proofsearch 22 maprhs

4+:makewith 26 isElem2

5+:casesplit 31 p

6+:casesplit 36 xs'

7+:casesplit 39 x

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

11#!/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

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

2−:ac 7 append

1+:addclause 8 Show

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

11#!/usr/bin/env bash

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

3+cd src

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

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

13import Data.Vect

4+import Foo

36data Foo = Bar | Baz

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

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

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

912

10−

11−

13+main : IO ()

14+main = foo