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

miniidris.cabal+2−2

compare with master

unifiedsplit

@@ -21,10 +21,10 @@ Executable miniidris

21 Core.ProofShell, Core.ProofState, Core.CoreParser,

22 Core.ShellParser, Core.Unify, Core.Elaborate,

23

24− Idris.AbsSyntax Idris.Parser

24+ Idris.AbsSyntax, Idris.Parser, Idris.REPL

25

26 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

27− containers

27+ containers, process

28

29 Extensions: MultiParamTypeClasses, FunctionalDependencies,

30 FlexibleInstances

src/Core/Elaborate.hs+4−2

@@ -143,8 +143,10 @@ movelast n = processTactic' (MoveLast n)

143proofstate :: Elab ()

144proofstate = processTactic' ProofState

145

146−qed :: Elab ()

146+qed :: Elab Term

147−qed = processTactic' QED

147+qed = do processTactic' QED

148+ (p, _) <- get

149+ return (pterm p)

148

150

149undo :: Elab ()

151undo :: Elab ()

150undo = processTactic' Undo

152undo = processTactic' Undo

src/Core/ShellParser.hs+2−1

@@ -10,6 +10,7 @@ import Text.ParserCombinators.Parsec

10import Text.ParserCombinators.Parsec.Expr

11import Text.ParserCombinators.Parsec.Language

12import qualified Text.ParserCombinators.Parsec.Token as PTok

13+import Control.Monad

13

14

14import Debug.Trace

15import Debug.Trace

15

16

@@ -65,7 +66,7 @@ pTactic = do reserved "attack"; return attack

65 <|> do reserved "focus"; n <- iName; return (focus n)

66 <|> do reserved "focus"; n <- iName; return (focus n)

66 <|> do reserved "state"; return proofstate

67 <|> do reserved "state"; return proofstate

67 <|> do reserved "undo"; return undo

68 <|> do reserved "undo"; return undo

68− <|> do reserved "qed"; return qed

69+ <|> do reserved "qed"; return (void qed)

69

70

70pArgType :: Parser Bool

71pArgType :: Parser Bool

71pArgType = do lchar '_'; return True -- implicit (machine fills in)

72pArgType = do lchar '_'; return True -- implicit (machine fills in)

src/Idris/AbsSyntax.hs+36−6

@@ -5,14 +5,44 @@ module Idris.AbsSyntax where

5import Core.TT

6import Core.Evaluate

7

8+import Control.Monad.State

9+import Data.List

10+

11+data IOption = Logging

12+ deriving (Show, Eq)

13+

8data IState = IState { tt_ctxt :: Context,

14data IState = IState { tt_ctxt :: Context,

9− tt_infixes :: [FixDecl]

15+ idris_infixes :: [FixDecl],

16+ idris_implicits :: Ctxt [Name],

17+ idris_log :: String,

18+ idris_options :: [IOption]

10 }

19 }

11−

20+

12−{- Plan:

21+idrisInit = IState emptyContext [] emptyContext "" []

13− Treat it as a theorem prover - one definition at a time, parse, elaborate,

22+

14− and add to context. Since elaboration can be affected by definitions we've

23+-- The monad for the main REPL - reading and processing files and updating

15− added (e.g. plicity) -}

24+-- global state (hence the IO inner monad).

25+type Idris a = StateT IState IO a

26+

27+iputStrLn :: String -> Idris ()

28+iputStrLn = lift.putStrLn

29+

30+setOpt :: IOption -> Bool -> Idris ()

31+setOpt o True = do i <- get

32+ put (i { idris_options = nub (o : idris_options i) })

33+setOpt o False = do i <- get

34+ put (i { idris_options = idris_options i \\ [o] })

35+

36+iLOG :: String -> Idris ()

37+iLOG str = do i <- get

38+ when (Logging `elem` idris_options i)

39+ $ do lift (putStrLn str)

40+ put (i { idris_log = idris_log i ++ str ++ "\n" } )

41+

42+-- Commands in the REPL

43+

44+data Command = Quit

45+ | Help

16

46

17-- Parsed declarations

47-- Parsed declarations

18

48

src/Idris/REPL.hsnew file+32

@@ -0,0 +1,32 @@

1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}

2+

3+module Idris.REPL where

4+

5+import Idris.AbsSyntax

6+import Idris.REPLParser

7+

8+import System.Console.Readline

9+import Control.Monad

10+import Control.Monad.State

11+

12+

13+repl :: Idris ()

14+repl = do x <- lift $ readline "Idris> "

15+ case x of

16+ Nothing -> repl

17+ Just input -> do continue <- processInput input

18+ when continue repl

19+

20+processInput :: String -> Idris Bool

21+processInput cmd

22+ = case parseCmd cmd of

23+ Left err -> do lift $ print err

24+ return True

25+ Right Quit -> do iputStrLn "Bye bye"

26+ return False

27+ Right cmd -> do process cmd

28+ return True

29+

30+process :: Command -> Idris ()

31+process Help = iputStrLn "At some point I'll write some help text. Thanks for asking though."

32+

src/Idris/REPLParser.hsnew file+24

@@ -0,0 +1,24 @@

1+module Idris.REPLParser(parseCmd) where

2+

3+import Idris.Parser

4+import Idris.AbsSyntax

5+import Control.Monad

6+

7+import Text.ParserCombinators.Parsec

8+import Text.ParserCombinators.Parsec.Expr

9+import Text.ParserCombinators.Parsec.Language

10+import qualified Text.ParserCombinators.Parsec.Token as PTok

11+

12+import Debug.Trace

13+

14+parseCmd = parse pCmd "(input)"

15+

16+cmd :: [String] -> Parser ()

17+cmd xs = do lchar ':'; docmd xs

18+ where docmd [] = fail "No such command"

19+ docmd (x:xs) = try (void (symbol x)) <|> docmd xs

20+

21+pCmd :: Parser Command

22+pCmd = try (do cmd ["q", "quit"]; return Quit)

23+ <|> try (do cmd ["h", "?", "help"]; return Help)

24+

src/Main.hs+48−5

@@ -1,6 +1,12 @@

1module Main where

2

3import System.Console.Readline

4+import System.IO

5+import System.Environment

6+import System.Exit

7+

8+import Data.Maybe

9+import Control.Monad.State

4

10

5import Core.CoreParser

11import Core.CoreParser

6import Core.ShellParser

12import Core.ShellParser

@@ -11,13 +17,48 @@ import Core.Evaluate

11

17

12import Idris.AbsSyntax

18import Idris.AbsSyntax

13import Idris.Parser

19import Idris.Parser

20+import Idris.REPL

14

21

15−main = do Just x <- readline "> "

16− case parseExpr x of

17− Left err -> print err

18− Right d -> print d

19− main

20

22

23+-- Main program reads command line options, parses the main program, and gets

24+-- on with the REPL.

25+

26+data Opt = Filename String

27+ | Version

28+ | OLogging

29+ deriving Eq

30+

31+main = do xs <- getArgs

32+ opts <- parseArgs xs

33+ execStateT (runIdris opts) idrisInit

34+

35+runIdris :: [Opt] -> Idris ()

36+runIdris opts =

37+ do let inputs = opt getFile opts

38+ when (OLogging `elem` opts) (setOpt Logging True)

39+ mapM_ loadModule inputs

40+ repl

41+

42+loadModule :: FilePath -> Idris ()

43+loadModule f = do iLOG ("Reading " ++ show f)

44+ return ()

45+

46+getFile :: Opt -> Maybe String

47+getFile (Filename str) = Just str

48+getFile _ = Nothing

49+

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

51+opt = mapMaybe

52+

53+usage = do putStrLn "You're doing it wrong"

54+ exitWith (ExitFailure 1)

55+

56+parseArgs :: [String] -> IO [Opt]

57+parseArgs [] = return []

58+parseArgs ("--log":ns) = liftM (OLogging : ) (parseArgs ns)

59+parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

60+

61+{-

21main'

62main'

22 = do f <- readFile "test.mi"

63 = do f <- readFile "test.mi"

23 case parseFile f of

64 case parseFile f of

@@ -29,3 +70,5 @@ main'

29 runShell (initState ctxt)

70 runShell (initState ctxt)

30 return ()

71 return ()

31 err -> print err

72 err -> print err

73+ -}

74+