50ad8a7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3352 from jfdm/structural-changes

50ad8a7Niklas Larsson10 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -206,6 +206,7 @@ Library

206 , Idris.Reflection

207 , Idris.REPL

208 , Idris.REPL.Parser

209+ , Idris.REPL.Commands

209 , Idris.Transforms

210 , Idris.Transforms

210 , Idris.TypeSearch

211 , Idris.TypeSearch

211 , Idris.Unlit

212 , Idris.Unlit

main/Main.hs−1

@@ -6,7 +6,6 @@ import Control.Monad ( when )

7import Idris.AbsSyntax

8import Idris.REPL

9−-- import Idris.Imports

10import Idris.Error

9import Idris.Error

11import Idris.CmdOptions

10import Idris.CmdOptions

12import Idris.Info

11import Idris.Info

src/Idris/AbsSyntax.hs+125

@@ -47,6 +47,8 @@ import Debug.Trace

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

50+import Network (PortID(PortNumber))

51+

50import Util.Pretty

52import Util.Pretty

51import Util.ScreenSize

53import Util.ScreenSize

52import Util.System

54import Util.System

@@ -2496,3 +2498,126 @@ mkUniqueNames env shadows tm

2496 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)

2498 mkUniq ql nmap (PUnquote tm) = fmap PUnquote (mkUniq (ql - 1) nmap tm)

2497

2499

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

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

2501+

2502+

2503+getFile :: Opt -> Maybe String

2504+getFile (Filename str) = Just str

2505+getFile _ = Nothing

2506+

2507+getBC :: Opt -> Maybe String

2508+getBC (BCAsm str) = Just str

2509+getBC _ = Nothing

2510+

2511+getOutput :: Opt -> Maybe String

2512+getOutput (Output str) = Just str

2513+getOutput _ = Nothing

2514+

2515+getIBCSubDir :: Opt -> Maybe String

2516+getIBCSubDir (IBCSubDir str) = Just str

2517+getIBCSubDir _ = Nothing

2518+

2519+getImportDir :: Opt -> Maybe String

2520+getImportDir (ImportDir str) = Just str

2521+getImportDir _ = Nothing

2522+

2523+getPkgDir :: Opt -> Maybe String

2524+getPkgDir (Pkg str) = Just str

2525+getPkgDir _ = Nothing

2526+

2527+getPkg :: Opt -> Maybe (Bool, String)

2528+getPkg (PkgBuild str) = Just (False, str)

2529+getPkg (PkgInstall str) = Just (True, str)

2530+getPkg _ = Nothing

2531+

2532+getPkgClean :: Opt -> Maybe String

2533+getPkgClean (PkgClean str) = Just str

2534+getPkgClean _ = Nothing

2535+

2536+getPkgREPL :: Opt -> Maybe String

2537+getPkgREPL (PkgREPL str) = Just str

2538+getPkgREPL _ = Nothing

2539+

2540+getPkgCheck :: Opt -> Maybe String

2541+getPkgCheck (PkgCheck str) = Just str

2542+getPkgCheck _ = Nothing

2543+

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

2545+-- Otherwise returns Just x, where x is the contents of PkgMkDoc

2546+getPkgMkDoc :: Opt -- ^ Opt to extract

2547+ -> Maybe String -- ^ Result

2548+getPkgMkDoc (PkgMkDoc str) = Just str

2549+getPkgMkDoc _ = Nothing

2550+

2551+getPkgTest :: Opt -- ^ the option to extract

2552+ -> Maybe String -- ^ the package file to test

2553+getPkgTest (PkgTest f) = Just f

2554+getPkgTest _ = Nothing

2555+

2556+getCodegen :: Opt -> Maybe Codegen

2557+getCodegen (UseCodegen x) = Just x

2558+getCodegen _ = Nothing

2559+

2560+getCodegenArgs :: Opt -> Maybe String

2561+getCodegenArgs (CodegenArgs args) = Just args

2562+getCodegenArgs _ = Nothing

2563+

2564+getConsoleWidth :: Opt -> Maybe ConsoleWidth

2565+getConsoleWidth (UseConsoleWidth x) = Just x

2566+getConsoleWidth _ = Nothing

2567+

2568+

2569+getExecScript :: Opt -> Maybe String

2570+getExecScript (InterpretScript expr) = Just expr

2571+getExecScript _ = Nothing

2572+

2573+getPkgIndex :: Opt -> Maybe FilePath

2574+getPkgIndex (PkgIndex file) = Just file

2575+getPkgIndex _ = Nothing

2576+

2577+getEvalExpr :: Opt -> Maybe String

2578+getEvalExpr (EvalExpr expr) = Just expr

2579+getEvalExpr _ = Nothing

2580+

2581+getOutputTy :: Opt -> Maybe OutputType

2582+getOutputTy (OutputTy t) = Just t

2583+getOutputTy _ = Nothing

2584+

2585+getLanguageExt :: Opt -> Maybe LanguageExt

2586+getLanguageExt (Extension e) = Just e

2587+getLanguageExt _ = Nothing

2588+

2589+getTriple :: Opt -> Maybe String

2590+getTriple (TargetTriple x) = Just x

2591+getTriple _ = Nothing

2592+

2593+getCPU :: Opt -> Maybe String

2594+getCPU (TargetCPU x) = Just x

2595+getCPU _ = Nothing

2596+

2597+getOptLevel :: Opt -> Maybe Int

2598+getOptLevel (OptLevel x) = Just x

2599+getOptLevel _ = Nothing

2600+

2601+getOptimisation :: Opt -> Maybe (Bool,Optimisation)

2602+getOptimisation (AddOpt p) = Just (True, p)

2603+getOptimisation (RemoveOpt p) = Just (False, p)

2604+getOptimisation _ = Nothing

2605+

2606+getColour :: Opt -> Maybe Bool

2607+getColour (ColourREPL b) = Just b

2608+getColour _ = Nothing

2609+

2610+getClient :: Opt -> Maybe String

2611+getClient (Client x) = Just x

2612+getClient _ = Nothing

2613+

2614+-- Get the first valid port

2615+getPort :: [Opt] -> Maybe PortID

2616+getPort [] = Nothing

2617+getPort (Port p:xs)

2618+ | all (`elem` ['0'..'9']) p = Just (PortNumber $ fromIntegral (read p))

2619+ | otherwise = getPort xs

2620+getPort (_:xs) = getPort xs

2621+

2622+opt :: (Opt -> Maybe a) -> [Opt] -> [a]

2623+opt = mapMaybe

src/Idris/AbsSyntaxTree.hs+12−82

@@ -433,77 +433,6 @@ data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)

433

434data HowMuchDocs = FullDocs | OverviewDocs

435

436−-- | REPL commands

437−data Command = Quit

438− | Help

439− | Eval PTerm

440− | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

441− | Undefine [Name]

442− | Check PTerm

443− | Core PTerm

444− | DocStr (Either Name Const) HowMuchDocs

445− | TotCheck Name

446− | Reload

447− | Watch

448− | Load FilePath (Maybe Int) -- up to maximum line number

449− | ChangeDirectory FilePath

450− | ModImport String

451− | Edit

452− | Compile Codegen String

453− | Execute PTerm

454− | ExecVal PTerm

455− | Metavars

456− | Prove Bool Name -- ^ If false, use prover, if true, use elab shell

457− | AddProof (Maybe Name)

458− | RmProof Name

459− | ShowProof Name

460− | Proofs

461− | Universes

462− | LogLvl Int

463− | LogCategory [LogCat]

464− | Spec PTerm

465− | WHNF PTerm

466− | TestInline PTerm

467− | Defn Name

468− | Missing Name

469− | DynamicLink FilePath

470− | ListDynamic

471− | Pattelab PTerm

472− | Search [String] PTerm

473− | CaseSplitAt Bool Int Name

474− | AddClauseFrom Bool Int Name

475− | AddProofClauseFrom Bool Int Name

476− | AddMissing Bool Int Name

477− | MakeWith Bool Int Name

478− | MakeCase Bool Int Name

479− | MakeLemma Bool Int Name

480− | DoProofSearch Bool -- update file

481− Bool -- recursive search

482− Int -- depth

483− Name -- top level name

484− [Name] -- hints

485− | SetOpt Opt

486− | UnsetOpt Opt

487− | NOP

488− | SetColour ColourType IdrisColour

489− | ColourOn

490− | ColourOff

491− | ListErrorHandlers

492− | SetConsoleWidth ConsoleWidth

493− | SetPrinterDepth (Maybe Int)

494− | Apropos [String] String

495− | WhoCalls Name

496− | CallsWho Name

497− | Browse [String]

498− | MakeDoc String -- IdrisDoc

499− | Warranty

500− | PrintDef Name

501− | PPrint OutputFmt Int PTerm

502− | TransformInfo Name

503− -- Debugging commands

504− | DebugInfo Name

505− | DebugUnify PTerm PTerm

506−

507data OutputFmt = HTMLOutput | LaTeXOutput

436data OutputFmt = HTMLOutput | LaTeXOutput

508

437

509-- | Recognised logging categories for the Idris compiler.

438-- | Recognised logging categories for the Idris compiler.

@@ -544,6 +473,18 @@ loggingCatsStr = unlines

544 , (strLogCat IIBC)

473 , (strLogCat IIBC)

545 ]

474 ]

546

475

476+

477+data ElabShellCmd = EQED

478+ | EAbandon

479+ | EUndo

480+ | EProofState

481+ | EProofTerm

482+ | EEval PTerm

483+ | ECheck PTerm

484+ | ESearch PTerm

485+ | EDocStr (Either Name Const)

486+ deriving (Show, Eq)

487+

547data Opt = Filename String

488data Opt = Filename String

548 | Quiet

489 | Quiet

549 | NoBanner

490 | NoBanner

@@ -613,17 +554,6 @@ data Opt = Filename String

613 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

554 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics

614 deriving (Show, Eq, Generic)

555 deriving (Show, Eq, Generic)

615

556

616−data ElabShellCmd = EQED

617− | EAbandon

618− | EUndo

619− | EProofState

620− | EProofTerm

621− | EEval PTerm

622− | ECheck PTerm

623− | ESearch PTerm

624− | EDocStr (Either Name Const)

625− deriving (Show, Eq)

626−

627-- Parsed declarations

557-- Parsed declarations

628

558

629data Fixity = Infixl { prec :: Int }

559data Fixity = Infixl { prec :: Int }

src/Idris/CmdOptions.hs+11−4

@@ -1,15 +1,22 @@

1{-|

2Module : Idris.CmdOptions

3−Description : CLI for the Idris executable.

3+Description : A parser for the CmdOptions for the Idris executable.

4−Copyright :

5License : BSD3

4License : BSD3

6Maintainer : The Idris Community.

5Maintainer : The Idris Community.

7-}

6-}

8{-# LANGUAGE Arrows #-}

7{-# LANGUAGE Arrows #-}

9−module Idris.CmdOptions where

8+module Idris.CmdOptions

9+ (

10+ module Idris.CmdOptions

11+ , opt

12+ , getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc

13+ , getPkgREPL, getPkgTest, getPort, getIBCSubDir

14+ ) where

11import Idris.AbsSyntaxTree

16import Idris.AbsSyntaxTree

12−import Idris.REPL

17+import Idris.AbsSyntax (opt, getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc

18+ , getPkgREPL, getPkgTest, getPort, getIBCSubDir)

19+-- import Idris.REPL

13import Idris.Info (getIdrisVersion)

20import Idris.Info (getIdrisVersion)

15import IRTS.CodegenCommon

22import IRTS.CodegenCommon

src/Idris/Coverage.hs+2−2

@@ -489,7 +489,7 @@ verifyTotality (fc, n)

489

490 case getPartial ist [] ns of

491 Nothing -> return ()

492− Just bad -> do let t' = Partial (Other bad)

492+ Just bad -> do let t' = Partial (Other bad)

493 logCoverage 2 $ "Set to " ++ show t'

494 setTotality n t'

495 addIBC (IBCTotal n t')

@@ -503,7 +503,7 @@ verifyTotality (fc, n)

503

504 getPartial ist [] [] = Nothing

505 getPartial ist bad [] = Just bad

506− getPartial ist bad (n : ns)

506+ getPartial ist bad (n : ns)

507 = case lookupTotalExact n (tt_ctxt ist) of

508 Just (Partial _) -> getPartial ist (n : bad) ns

509 _ -> getPartial ist bad ns

src/Idris/Package/Common.hs+3−4

@@ -1,15 +1,14 @@

1{-|

2Module : Idris.Package.Common

3Description : Data structures common to all `iPKG` file formats.

4−Copyright :

5License : BSD3

4License : BSD3

6Maintainer : The Idris Community.

5Maintainer : The Idris Community.

7-}

6-}

8module Idris.Package.Common where

7module Idris.Package.Common where

10−import Idris.Core.TT

9+import Idris.Core.TT (Name)

11−import Idris.REPL

10+

12−import Idris.AbsSyntaxTree

11+import Idris.AbsSyntaxTree (Opt(..))

14-- | Description of an Idris package.

13-- | Description of an Idris package.

15data PkgDesc = PkgDesc {

14data PkgDesc = PkgDesc {

src/Idris/REPL.hs+17−134

@@ -9,10 +9,8 @@ Maintainer : The Idris Community.

9 PatternGuards, CPP #-}

11module Idris.REPL(

12− getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc

13− , getPkgREPL, getPkgTest, getPort, getIBCSubDir

14− , idris, idrisMain, loadInputs

12+ idris, idrisMain, loadInputs

15− , opt, runClient, runMain

13+ , runClient, runMain

16 ) where

14 ) where

18import Idris.AbsSyntax

16import Idris.AbsSyntax

@@ -47,6 +45,7 @@ import Idris.TypeSearch (searchByType)

47import Idris.IBC (loadPkgIndex, writePkgIndex)

45import Idris.IBC (loadPkgIndex, writePkgIndex)

49import Idris.REPL.Browse (namesInNS, namespacesInNS)

47import Idris.REPL.Browse (namesInNS, namespacesInNS)

48+import Idris.REPL.Commands

51import Idris.ElabDecls

50import Idris.ElabDecls

52import Idris.Elab.Type

51import Idris.Elab.Type

@@ -226,9 +225,10 @@ processNetCmd orig i h fn cmd

226 IdeMode n _ -> ist {idris_outputmode = IdeMode n h}

225 IdeMode n _ -> ist {idris_outputmode = IdeMode n h}

227

226

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

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

229−runClient :: PortID -> String -> IO ()

228+runClient :: Maybe PortID -> String -> IO ()

230runClient port str = withSocketsDo $ do

229runClient port str = withSocketsDo $ do

230+ let port' = fromMaybe defaultPort port

231− res <- X.try (connectTo "localhost" port)

231+ res <- X.try (connectTo "localhost" port')

232 case res of

233 Right h -> do

234 hSetEncoding h utf8

@@ -1707,14 +1707,19 @@ idrisMain opts =

1707 let cgFlags = opt getCodegenArgs opts

1708

1709 -- Now set/unset specifically chosen optimisations

1710− sequence_ (opt getOptimisation opts)

1710+ let os = opt getOptimisation opts

1711+

1712+ mapM_ processOptimisation os

1713+

1711 script <- case opt getExecScript opts of

1714 script <- case opt getExecScript opts of

1712 [] -> return Nothing

1715 [] -> return Nothing

1713 x:y:xs -> do iputStrLn "More than one interpreter expression found."

1716 x:y:xs -> do iputStrLn "More than one interpreter expression found."

1714 runIO $ exitWith (ExitFailure 1)

1717 runIO $ exitWith (ExitFailure 1)

1715 [expr] -> return (Just expr)

1718 [expr] -> return (Just expr)

1716 let immediate = opt getEvalExpr opts

1719 let immediate = opt getEvalExpr opts

1717− let port = getPort opts

1720+ let port = case getPort opts of

1721+ Nothing -> defaultPort

1722+ Just p -> p

1718

1723

1719 when (DefaultTotal `elem` opts) $ do i <- getIState

1724 when (DefaultTotal `elem` opts) $ do i <- getIState

1720 putIState (i { default_total = DefaultCheckingTotal })

1725 putIState (i { default_total = DefaultCheckingTotal })

@@ -1829,6 +1834,10 @@ idrisMain opts =

1829 makeOption ErrContext = setErrContext True

1834 makeOption ErrContext = setErrContext True

1830 makeOption _ = return ()

1835 makeOption _ = return ()

1831

1836

1837+ processOptimisation :: (Bool,Optimisation) -> Idris ()

1838+ processOptimisation (True, p) = addOptimise p

1839+ processOptimisation (False, p) = removeOptimise p

1840+

1832 addPkgDir :: String -> Idris ()

1841 addPkgDir :: String -> Idris ()

1833 addPkgDir p = do ddir <- runIO getIdrisLibDir

1842 addPkgDir p = do ddir <- runIO getIdrisLibDir

1834 addImportDir (ddir </> p)

1843 addImportDir (ddir </> p)

@@ -1882,133 +1891,7 @@ initScript = do script <- runIO $ getIdrisInitScript

1882 Success (Right cmd ) -> process [] cmd

1891 Success (Right cmd ) -> process [] cmd

1883 Success (Left err) -> runIO $ print err

1892 Success (Left err) -> runIO $ print err

1884

1893

1885−getFile :: Opt -> Maybe String

1886−getFile (Filename str) = Just str

1887−getFile _ = Nothing

1888

1894

1889−getBC :: Opt -> Maybe String

1890−getBC (BCAsm str) = Just str

1891−getBC _ = Nothing

1892−

1893−getOutput :: Opt -> Maybe String

1894−getOutput (Output str) = Just str

1895−getOutput _ = Nothing

1896−

1897−getIBCSubDir :: Opt -> Maybe String

1898−getIBCSubDir (IBCSubDir str) = Just str

1899−getIBCSubDir _ = Nothing

1900−

1901−getImportDir :: Opt -> Maybe String

1902−getImportDir (ImportDir str) = Just str

1903−getImportDir _ = Nothing

1904−

1905−getPkgDir :: Opt -> Maybe String

1906−getPkgDir (Pkg str) = Just str

1907−getPkgDir _ = Nothing

1908−

1909−getPkg :: Opt -> Maybe (Bool, String)

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

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

1912−getPkg _ = Nothing

1913−

1914−getPkgClean :: Opt -> Maybe String

1915−getPkgClean (PkgClean str) = Just str

1916−getPkgClean _ = Nothing

1917−

1918−getPkgREPL :: Opt -> Maybe String

1919−getPkgREPL (PkgREPL str) = Just str

1920−getPkgREPL _ = Nothing

1921−

1922−getPkgCheck :: Opt -> Maybe String

1923−getPkgCheck (PkgCheck str) = Just str

1924−getPkgCheck _ = Nothing

1925−

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

1927−-- Otherwise returns Just x, where x is the contents of PkgMkDoc

1928−getPkgMkDoc :: Opt -- ^ Opt to extract

1929− -> Maybe String -- ^ Result

1930−getPkgMkDoc (PkgMkDoc str) = Just str

1931−getPkgMkDoc _ = Nothing

1932−

1933−getPkgTest :: Opt -- ^ the option to extract

1934− -> Maybe String -- ^ the package file to test

1935−getPkgTest (PkgTest f) = Just f

1936−getPkgTest _ = Nothing

1937−

1938−getCodegen :: Opt -> Maybe Codegen

1939−getCodegen (UseCodegen x) = Just x

1940−getCodegen _ = Nothing

1941−

1942−getCodegenArgs :: Opt -> Maybe String

1943−getCodegenArgs (CodegenArgs args) = Just args

1944−getCodegenArgs _ = Nothing

1945−

1946−getConsoleWidth :: Opt -> Maybe ConsoleWidth

1947−getConsoleWidth (UseConsoleWidth x) = Just x

1948−getConsoleWidth _ = Nothing

1949−

1950−

1951−getExecScript :: Opt -> Maybe String

1952−getExecScript (InterpretScript expr) = Just expr

1953−getExecScript _ = Nothing

1954−

1955−getPkgIndex :: Opt -> Maybe FilePath

1956−getPkgIndex (PkgIndex file) = Just file

1957−getPkgIndex _ = Nothing

1958−

1959−getEvalExpr :: Opt -> Maybe String

1960−getEvalExpr (EvalExpr expr) = Just expr

1961−getEvalExpr _ = Nothing

1962−

1963−getOutputTy :: Opt -> Maybe OutputType

1964−getOutputTy (OutputTy t) = Just t

1965−getOutputTy _ = Nothing

1966−

1967−getLanguageExt :: Opt -> Maybe LanguageExt

1968−getLanguageExt (Extension e) = Just e

1969−getLanguageExt _ = Nothing

1970−

1971−getTriple :: Opt -> Maybe String

1972−getTriple (TargetTriple x) = Just x

1973−getTriple _ = Nothing

1974−

1975−getCPU :: Opt -> Maybe String

1976−getCPU (TargetCPU x) = Just x

1977−getCPU _ = Nothing

1978−

1979−getOptLevel :: Opt -> Maybe Int

1980−getOptLevel (OptLevel x) = Just x

1981−getOptLevel _ = Nothing

1982−

1983−getOptimisation :: Opt -> Maybe (Idris ())

1984−getOptimisation (AddOpt p) = Just $ addOptimise p

1985−getOptimisation (RemoveOpt p) = Just $ removeOptimise p

1986−getOptimisation _ = Nothing

1987−

1988−getColour :: Opt -> Maybe Bool

1989−getColour (ColourREPL b) = Just b

1990−getColour _ = Nothing

1991−

1992−getClient :: Opt -> Maybe String

1993−getClient (Client x) = Just x

1994−getClient _ = Nothing

1995−

1996−-- Get the first valid port

1997−getPort :: [Opt] -> PortID

1998−getPort [] = defaultPort

1999−getPort (Port p:xs)

2000− | all (`elem` ['0'..'9']) p = PortNumber $ fromIntegral (read p)

2001− | otherwise = getPort xs

2002−getPort (_:xs) = getPort xs

2003−

2004−opt :: (Opt -> Maybe a) -> [Opt] -> [a]

2005−opt = mapMaybe

2006−

2007−{-

2008−ver = showVersion version ++ suffix

2009− where

2010− suffix = if gitHash =="" then "" else "-" ++ gitHash

2011−-}

2012defaultPort :: PortID

1895defaultPort :: PortID

2013defaultPort = PortNumber (fromIntegral 4294)

1896defaultPort = PortNumber (fromIntegral 4294)

2014

1897

src/Idris/REPL/Commands.hsnew file+76

@@ -0,0 +1,76 @@

1+module Idris.REPL.Commands where

3+import Idris.Core.TT

4+import Idris.Colours

5+import Idris.AbsSyntaxTree

7+-- | REPL commands

8+data Command = Quit

9+ | Help

10+ | Eval PTerm

11+ | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.

12+ | Undefine [Name]

13+ | Check PTerm

14+ | Core PTerm

15+ | DocStr (Either Name Const) HowMuchDocs

16+ | TotCheck Name

17+ | Reload

18+ | Watch

19+ | Load FilePath (Maybe Int) -- up to maximum line number

20+ | ChangeDirectory FilePath

21+ | ModImport String

22+ | Edit

23+ | Compile Codegen String

24+ | Execute PTerm

25+ | ExecVal PTerm

26+ | Metavars

27+ | Prove Bool Name -- ^ If false, use prover, if true, use elab shell

28+ | AddProof (Maybe Name)

29+ | RmProof Name

30+ | ShowProof Name

31+ | Proofs

32+ | Universes

33+ | LogLvl Int

34+ | LogCategory [LogCat]

35+ | Spec PTerm

36+ | WHNF PTerm

37+ | TestInline PTerm

38+ | Defn Name

39+ | Missing Name

40+ | DynamicLink FilePath

41+ | ListDynamic

42+ | Pattelab PTerm

43+ | Search [String] PTerm

44+ | CaseSplitAt Bool Int Name

45+ | AddClauseFrom Bool Int Name

46+ | AddProofClauseFrom Bool Int Name

47+ | AddMissing Bool Int Name

48+ | MakeWith Bool Int Name

49+ | MakeCase Bool Int Name

50+ | MakeLemma Bool Int Name

51+ | DoProofSearch Bool -- update file

52+ Bool -- recursive search

53+ Int -- depth

54+ Name -- top level name

55+ [Name] -- hints

56+ | SetOpt Opt

57+ | UnsetOpt Opt

58+ | NOP

59+ | SetColour ColourType IdrisColour

60+ | ColourOn

61+ | ColourOff

62+ | ListErrorHandlers

63+ | SetConsoleWidth ConsoleWidth

64+ | SetPrinterDepth (Maybe Int)

65+ | Apropos [String] String

66+ | WhoCalls Name

67+ | CallsWho Name

68+ | Browse [String]

69+ | MakeDoc String -- IdrisDoc

70+ | Warranty

71+ | PrintDef Name

72+ | PPrint OutputFmt Int PTerm

73+ | TransformInfo Name

74+ -- Debugging commands

75+ | DebugInfo Name

76+ | DebugUnify PTerm PTerm

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

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

1{-|

2Module : Idris.REPL.Parser

3Description : Parser for the REPL commands.

4−Copyright :

5License : BSD3

4License : BSD3

6Maintainer : The Idris Community.

5Maintainer : The Idris Community.

7-}

6-}

@@ -21,6 +20,8 @@ import Idris.Core.TT

21import Idris.Help

20import Idris.Help

22import qualified Idris.Parser as P

21import qualified Idris.Parser as P

23+import Idris.REPL.Commands

24+

24import Control.Applicative

25import Control.Applicative

25import Control.Monad.State.Strict

26import Control.Monad.State.Strict