@@ -5,14 +5,44 @@ module Idris.AbsSyntax where
55import Core.TT
66import Core.Evaluate
77
8+import Control.Monad.State
9+import Data.List
10+
11+data IOption = Logging
12+ deriving (Show, Eq)
13+
814data 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]
1019 }
11−
12−{- Plan:
13− Treat it as a theorem prover - one definition at a time, parse, elaborate,
14− and add to context. Since elaboration can be affected by definitions we've
15− added (e.g. plicity) -}
20+
21+idrisInit = IState emptyContext [] emptyContext "" []
22+
23+-- The monad for the main REPL - reading and processing files and updating
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
1646
1747-- Parsed declarations
1848