fb33d8c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Indentation configuration via command line args.

- `--indent-with INDENT` - `--indent-clause INDENT` Plus some boy scouting.

commitfb33d8ca77935e734eacfdd0bcde2193e2182d79 authorSteven Shaw <steven@steshaw.org> dateThu 8 Sep 2016, 22:03 (10 years ago) parentc86bf98

20 files changed+300−231

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+70−61

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

9− PatternGuards, TypeSynonymInstances #-}

9+{-# LANGUAGE DeriveFunctor #-}

10+{-# LANGUAGE PatternGuards #-}

1011

1112module Idris.AbsSyntax(

1213 module Idris.AbsSyntax

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

1516

1617import Idris.AbsSyntaxTree

1718import Idris.Colours

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

1919import Idris.Core.Evaluate

2020import Idris.Core.TT

21−import Idris.Core.Typecheck

2221import Idris.Docstrings

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

2423import IRTS.CodegenCommon

2524

26−import Util.DynamicLinker

27−import Util.Pretty

28−import Util.ScreenSize

29−import Util.System

25+import System.Directory (canonicalizePath, doesFileExist)

26+import System.IO

3027

3128import Control.Applicative

32−import Control.Monad (liftM3)

3329import Control.Monad.State

34−import Data.Char

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

31+

3532import Data.Either

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

3733import Data.List hiding (insert, union)

3834import qualified Data.Map as M

3935import Data.Maybe

4036import qualified Data.Set as S

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

4945

5046getContext :: Idris Context

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

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

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

9288 return (Left x)

9389 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

90+ findDyLib [] _ = Nothing

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

92+ | otherwise = findDyLib libs' l

9793

9894getAutoImports :: Idris [FilePath]

9995getAutoImports = do i <- getIState

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

10298addAutoImport :: FilePath -> Idris ()

10399addAutoImport fp = do i <- getIState

104100 let opts = idris_options i

105− let autoimps = opt_autoImport opts

106101 put (i { idris_options = opts { opt_autoImport =

107102 fp : opt_autoImport opts } } )

108103

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

250245 let cs = idris_coercions i

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

252247 findCoercions fn cs

253− where findCoercions t [] = []

248+ where findCoercions _ [] = []

254249 findCoercions t (n : ns) =

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

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

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

322317 do let (fx, _) = unApply x

323318 let (fy, _) = unApply y

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

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

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

329324 _ -> return ()

330325

331326 where errWhen True

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

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

354349 putIState $ i { idris_function_errorhandlers = newHandlers }

355350

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−

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

363352getAllNames :: Name -> Idris [Name]

364353getAllNames n = do i <- getIState

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

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

415404

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

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

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

418407getNameHints i n =

419408 case lookupCtxt n (idris_namehints i) of

420409 [ns] -> ns

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

430419 i <- getIState

431420 return $ lookupCtxtExact n (idris_deprecated i)

432421

433−

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

435423addFragile n reason = do

436424 i <- getIState

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

442430 return $ lookupCtxtExact n (idris_fragile i)

443431

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

445−push_estack n impl

433+push_estack n implementation

446434 = do i <- getIState

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

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

448436

449437pop_estack :: Idris ()

450438pop_estack = do i <- getIState

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

452440 where ptail [] = []

453− ptail (x : xs) = xs

441+ ptail (_ : xs) = xs

454442

455443-- | Add an interface implementation function.

456444--

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

546534 when (notDef (ibc_write i)) $

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

548536 where notDef [] = True

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

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

550538 notDef (_ : is) = notDef is

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

552540

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

683671clearPTypes = do i <- get

684672 let ctxt = tt_ctxt i

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

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

688676 pErase x = x

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

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

699687 _ -> return ()

700688

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

702−isUndefined fc n

690+isUndefined _ n

703691 = do i <- getContext

704692 case lookupTyExact n i of

705693 Just _ -> return False

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

756744 tidyNames used (Bind n b sc)

757745 = let n' = uniqueNameSet n used in

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

759− tidyNames used b = b

747+ tidyNames _ b = b

760748

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

762750solveDeferred fc n

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

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

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

11461134

1147−

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

11491136logLvl = logLvlCats []

11501137

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

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

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

11801167 -> Idris ()

1181−logLvlCats cs l str = do

1168+logLvlCats cs l msg = do

11821169 i <- getIState

11831170 let lvl = opt_logLevel (idris_options i)

11841171 let cats = opt_logcats (idris_options i)

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

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

11871174 case idris_outputmode i of

11881175 RawOutput h -> do

1189− runIO $ hPutStrLn h str

1176+ runIO $ hPutStrLn h msg

11901177 IdeMode n h -> do

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

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

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

11931180 where

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

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

12101197 let opt' = opts { opt_typecase = t }

12111198 putIState $ i { idris_options = opt' }

12121199

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

12131223

12141224-- Dealing with parameters

12151225

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

22262236instance Monad (EitherErr a) where

22272237 return = RightOK

22282238

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

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

22302240 RightOK v >>= k = k v

22312241

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

22322243toEither (LeftErr e) = Left e

22332244toEither (RightOK ho) = Right ho

22342245

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

24392450 -- looking for too long...)

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

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

2442− initN n l = n

2453+ initN n _ = n

24432454

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

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

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

25472558

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

25492560

2550−

25512561getFile :: Opt -> Maybe String

2552−getFile (Filename str) = Just str

2562+getFile (Filename s) = Just s

25532563getFile _ = Nothing

25542564

25552565getBC :: Opt -> Maybe String

2556−getBC (BCAsm str) = Just str

2566+getBC (BCAsm s) = Just s

25572567getBC _ = Nothing

25582568

25592569getOutput :: Opt -> Maybe String

2560−getOutput (Output str) = Just str

2570+getOutput (Output s) = Just s

25612571getOutput _ = Nothing

25622572

25632573getIBCSubDir :: Opt -> Maybe String

2564−getIBCSubDir (IBCSubDir str) = Just str

2574+getIBCSubDir (IBCSubDir s) = Just s

25652575getIBCSubDir _ = Nothing

25662576

25672577getImportDir :: Opt -> Maybe String

2568−getImportDir (ImportDir str) = Just str

2578+getImportDir (ImportDir s) = Just s

25692579getImportDir _ = Nothing

25702580

25712581getSourceDir :: Opt -> Maybe String

2572−getSourceDir (SourceDir str) = Just str

2582+getSourceDir (SourceDir s) = Just s

25732583getSourceDir _ = Nothing

25742584

25752585getPkgDir :: Opt -> Maybe String

2576−getPkgDir (Pkg str) = Just str

2586+getPkgDir (Pkg s) = Just s

25772587getPkgDir _ = Nothing

25782588

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

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

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

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

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

25822592getPkg _ = Nothing

25832593

25842594getPkgClean :: Opt -> Maybe String

2585−getPkgClean (PkgClean str) = Just str

2595+getPkgClean (PkgClean s) = Just s

25862596getPkgClean _ = Nothing

25872597

25882598getPkgREPL :: Opt -> Maybe String

2589−getPkgREPL (PkgREPL str) = Just str

2599+getPkgREPL (PkgREPL s) = Just s

25902600getPkgREPL _ = Nothing

25912601

25922602getPkgCheck :: Opt -> Maybe String

2593−getPkgCheck (PkgCheck str) = Just str

2603+getPkgCheck (PkgCheck s) = Just s

25942604getPkgCheck _ = Nothing

25952605

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

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

26182628getConsoleWidth (UseConsoleWidth x) = Just x

26192629getConsoleWidth _ = Nothing

26202630

2621−

26222631getExecScript :: Opt -> Maybe String

26232632getExecScript (InterpretScript expr) = Just expr

26242633getExecScript _ = Nothing

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

26672676-- Get the first valid port

26682677getPort :: [Opt] -> Maybe REPLPort

26692678getPort [] = Nothing

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

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

26712680getPort (_ : xs) = getPort xs

26722681

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

src/Idris/AbsSyntaxTree.hs+45−20

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

9− FlexibleInstances, MultiParamTypeClasses, PatternGuards,

10− TypeSynonymInstances #-}

9+{-# LANGUAGE DeriveDataTypeable #-}

10+{-# LANGUAGE DeriveFunctor #-}

11+{-# LANGUAGE DeriveGeneric #-}

12+{-# LANGUAGE PatternGuards #-}

1113

1214module Idris.AbsSyntaxTree where

1315

14−import Idris.Colours

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

1617import Idris.Core.Evaluate

1718import Idris.Core.TT

18−import Idris.Core.Typecheck

1919import Idris.Docstrings

2020import IRTS.CodegenCommon

2121import IRTS.Lang

2222import Util.DynamicLinker

2323import Util.Pretty

2424

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

25+import Idris.Colours

26+

27+import System.IO

28+

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

2630

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

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

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

3034import Control.Monad.Trans.State.Strict

3135import Data.Char

3236import Data.Data (Data)

33−import Data.Either

37+

3438import Data.Foldable (Foldable)

3539import Data.Function (on)

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

3741import Data.List hiding (group)

3842import qualified Data.Map.Strict as M

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

43+import Data.Maybe (mapMaybe, maybeToList)

4044import qualified Data.Set as S

4145import qualified Data.Text as T

4246import Data.Traversable (Traversable)

4347import Data.Typeable

44−import Data.Word (Word)

45−import Debug.Trace

4648import GHC.Generics (Generic)

4749import Network.Socket (PortNumber)

48−import System.Console.Haskeline

49−import System.IO

50−import Text.PrettyPrint.Annotated.Leijen

50+

5151

5252data ElabWhat = ETypes | EDefns | EAll

5353 deriving (Show, Eq)

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

112112 , opt_autoimpls :: Bool

113113 } deriving (Show, Eq, Generic)

114114

115+defaultOpts :: IOption

115116defaultOpts = IOption { opt_logLevel = 0

116117 , opt_logcats = []

117118 , opt_typecase = False

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

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

152153 deriving (Show, Eq, Generic)

153154

155+defaultOptimise :: [Optimisation]

154156defaultOptimise = [PETransform]

155157

156158-- | Pretty printing options with default verbosity.

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

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

207209 deriving (Show, Eq, Generic)

208210

211+-- | Configuration options for interactive editing.

212+data InteractiveOpts = InteractiveOpts {

213+ interactiveOpts_indentWith :: Int

214+ , interactiveOpts_indentClause :: Int

215+} deriving (Show, Generic)

216+

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

210218data IState = IState {

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

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

294302 , idris_repl_defs :: [Name]

295303

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

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

299307

300308

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

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

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

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

309− }

310− deriving Generic

317+ , idris_interactiveOpts :: InteractiveOpts

318+ } deriving Generic

311319

312320-- Required for parsers library, and therefore trifecta

313321instance Show IState where

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

332340deriving instance Binary CGInfo

333341!-}

334342

343+primDefs :: [Name]

335344primDefs = [ sUN "unsafePerformPrimIO"

336345 , sUN "mkLazyForeignPrim"

337346 , sUN "mkForeignPrim"

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

390399 | IBCConstraint FC UConstraint

391400 deriving (Show, Generic)

392401

402+initialInteractiveOpts :: InteractiveOpts

403+initialInteractiveOpts = InteractiveOpts {

404+ interactiveOpts_indentWith = 2

405+ , interactiveOpts_indentClause = 2

406+}

407+

393408-- | The initial state for the compiler

394409idrisInit :: IState

395410idrisInit = IState initContext S.empty []

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

402417 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

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

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

405− emptyContext S.empty M.empty emptyContext

420+ emptyContext S.empty M.empty emptyContext initialInteractiveOpts

406421

407422

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

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

488503 | ColourREPL Bool

489504 | Idemode

490505 | IdemodeSocket

506+ | IndentWith Int

507+ | IndentClause Int

491508 | ShowAll

492509 | ShowLibs

493510 | ShowLibDir

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

627644is_scoped _ = Nothing

628645

629646-- Top level implicit

647+impl :: Plicity

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

631649-- Machine generated top level implicit

650+impl_gen :: Plicity

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

633652

634653-- Scoped implicits

654+forall_imp :: Plicity

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

656+forall_constraint :: Plicity

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

637658

659+expl :: Plicity

638660expl = Exp [] Dynamic False RigW

661+expl_param :: Plicity

639662expl_param = Exp [] Dynamic True RigW

640663

664+constraint :: Plicity

641665constraint = Constraint [] Static RigW

642666

667+tacimpl :: PTerm -> Plicity

643668tacimpl t = TacImp [] Dynamic t RigW

644669

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

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

14101435-- Interface data

14111436

14121437data InterfaceInfo = CI {

1413− implementationCtorName :: Name

1438+ implementationCtorName :: Name

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

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

14161441 , interface_default_super_interfaces :: [PDecl]

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

22692294

22702295getShowArgs :: [PArg] -> [PArg]

22712296getShowArgs [] = []

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

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

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

22742299 | PImp _ _ _ _ tm <- e

22752300 , containsHole tm = e : getShowArgs xs

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

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

25872612getErasureInfo ist n =

25882613 case lookupCtxtExact n (idris_optimisation ist) of

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

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

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

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

55License : BSD3

66Maintainer : The Idris Community.

77-}

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

9+{-# LANGUAGE DeriveFunctor #-}

10+{-# LANGUAGE MultiWayIf #-}

11+{-# LANGUAGE PatternGuards #-}

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

13+

1014module Idris.Docs (

1115 pprintDocs

1216 , getDocs, pprintConstDocs, pprintTypeDoc

1317 , FunDoc, FunDoc'(..), Docs, Docs'(..)

1418 ) where

1519

16−import Idris.AbsSyntax

17−import Idris.AbsSyntaxTree

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

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

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

23+ getIState, modDocName, ppOptionIst, pprintPTerm,

24+ prettyIst, prettyName, type1Doc, typeDescription)

1825import Idris.Core.Evaluate

1926import Idris.Core.TT

2027import Idris.Delaborate

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

2633

2734import Prelude hiding ((<$>))

2835

29−import Control.Arrow (first)

3036import Data.List

3137import Data.Maybe

3238import qualified Data.Text as T

src/Idris/Interactive.hs+33−23

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

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

5552

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

5754addClauseFrom 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+-}

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

5964 -- adding a new definition.

6065 ist <- getIState

6166 cl <- getInternalApp fn l

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

6268 let fulln = getAppName cl

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

6370

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

6574 Nothing -> addMissing fn updatefile l n

6675 Just _ -> do

6776 src <- runIO $ readSource fn

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

6978 let indent = getIndent 0 (show n) tyline

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

7080 cl <- getClause l fulln n fn

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

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

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

164174

165175

166176makeWith :: 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")

177+makeWith fn updatefile l n = do

178+ src <- runIO $ readSource fn

179+ i <- getIState

180+ indentWith <- getIndentWith

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

182+ let ind = getIndent tyline

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

184+ let with = mkWith tyline n indentWith

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

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

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

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

189+ if updatefile

190+ then do

191+ let fb = fn ++ "~"

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

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

194+ runIO $ copyFile fb fn

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

183196 where getIndent s = length (takeWhile isSpace s)

184197

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

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

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

222235

223236

224−

225−

226−

227237doProofSearch :: FilePath -> Bool -> Bool ->

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

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