5c4f5d2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added an :unlet/:undefine command.

5c4f5d2Alyssa Carter12 years ago

src/Idris/ASTUtils.hs+15

compare with master

unifiedsplit

@@ -38,6 +38,7 @@ import Data.Maybe

38import Prelude hiding (id, (.))

40import Idris.Core.TT

41+import Idris.Core.Evaluate

41import Idris.AbsSyntaxTree

42import Idris.AbsSyntaxTree

43data Field rec fld = Field

44data Field rec fld = Field

@@ -132,3 +133,17 @@ opts_idrisCmdline :: Field IState [Opt]

132opts_idrisCmdline =

133opts_idrisCmdline =

133 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })

134 Field opt_cmdline (\v opts -> opts{ opt_cmdline = v })

134 . Field idris_options (\v ist -> ist{ idris_options = v })

135 . Field idris_options (\v ist -> ist{ idris_options = v })

136+

137+-- TT Context

138+-------------

139+-- This has a terrible name, but I'm not sure of a better one that isn't

140+-- confusingly close to tt_ctxt

141+known_terms :: Field IState (Ctxt (Def, Accessibility, Totality, MetaInformation))

142+known_terms = Field (definitions . tt_ctxt)

143+ (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

144+

145+

146+-- Names defined at the repl

147+----------------------------

148+repl_definitions :: Field IState [Name]

149+repl_definitions = Field idris_repl_defs (\v state -> state {idris_repl_defs = v})

src/Idris/AbsSyntaxTree.hs+4−2

@@ -191,7 +191,8 @@ data IState = IState {

191 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?

192 idris_postulates :: S.Set Name,

193 idris_whocalls :: Maybe (M.Map Name [Name]),

194− idris_callswho :: Maybe (M.Map Name [Name])

194+ idris_callswho :: Maybe (M.Map Name [Name]),

195+ idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined

195 }

196 }

196

197

197data SizeChange = Smaller | Same | Bigger | Unknown

198data SizeChange = Smaller | Same | Bigger | Unknown

@@ -266,7 +267,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

266 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

267 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

267 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

268 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

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

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

269− AutomaticWidth S.empty Nothing Nothing

270+ AutomaticWidth S.empty Nothing Nothing []

270

271

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

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

272-- global state (hence the IO inner monad).

273-- global state (hence the IO inner monad).

@@ -288,6 +289,7 @@ data Command = Quit

288 | Help

289 | Help

289 | Eval PTerm

290 | Eval PTerm

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

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

292+ | Undefine [Name]

291 | Check PTerm

293 | Check PTerm

292 | DocStr (Either Name Const)

294 | DocStr (Either Name Const)

293 | TotCheck Name

295 | TotCheck Name

src/Idris/REPL.hs+27−1

@@ -49,6 +49,8 @@ import IRTS.Compiler

49import IRTS.CodegenCommon

50import IRTS.System

52+import Control.Category

53+import Prelude hiding ((.), id)

52import Data.List.Split (splitOn)

54import Data.List.Split (splitOn)

53import Data.List (groupBy)

55import Data.List (groupBy)

54import qualified Data.Text as T

56import qualified Data.Text as T

@@ -681,6 +683,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

681 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

683 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

682 elabDecl EAll toplevel tyDecl

684 elabDecl EAll toplevel tyDecl

683 elabClauses toplevel fc opts name (concatMap getClauses decls)

685 elabClauses toplevel fc opts name (concatMap getClauses decls)

686+ setReplDefined (getName tyDecl)

684 defineName [PClauses fc opts _ [clause]] = do

687 defineName [PClauses fc opts _ [clause]] = do

685 let pterm = getRHS clause

688 let pterm = getRHS clause

686 (tm,ty) <- elabVal toplevel ERHS pterm

689 (tm,ty) <- elabVal toplevel ERHS pterm

@@ -688,8 +691,10 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

688 let tm' = force (normaliseAll ctxt [] tm)

691 let tm' = force (normaliseAll ctxt [] tm)

689 let ty' = force (normaliseAll ctxt [] ty)

692 let ty' = force (normaliseAll ctxt [] ty)

690 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))

693 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))

694+ setReplDefined (Just $ getClauseName clause)

691− defineName [PData doc argdocs syn fc opts decl] = do

695+ defineName [def @ (PData doc argdocs syn fc opts decl)] = do

692 elabData toplevel syn doc argdocs fc opts decl

696 elabData toplevel syn doc argdocs fc opts decl

697+ setReplDefined (getName def)

693 getClauses (PClauses fc opts name clauses) = clauses

698 getClauses (PClauses fc opts name clauses) = clauses

694 getClauses _ = []

699 getClauses _ = []

695 getRHS :: PClause -> PTerm

700 getRHS :: PClause -> PTerm

@@ -697,6 +702,27 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++

697 getRHS (PWith fc name whole with rhs whereBlock) = rhs

702 getRHS (PWith fc name whole with rhs whereBlock) = rhs

698 getRHS (PClauseR fc with rhs whereBlock) = rhs

703 getRHS (PClauseR fc with rhs whereBlock) = rhs

699 getRHS (PWithR fc with rhs whereBlock) = rhs

704 getRHS (PWithR fc with rhs whereBlock) = rhs

705+ setReplDefined :: Maybe Name -> Idris ()

706+ setReplDefined Nothing = return ()

707+ setReplDefined (Just n) = do

708+ oldState <- get

709+ put oldState { idris_repl_defs = n : idris_repl_defs oldState }

710+

711+process h fn (Undefine names) = undefine names

712+ where

713+ undefine :: [Name] -> Idris ()

714+ undefine [] = do

715+ allDefined <- idris_repl_defs `fmap` get

716+ undefine' allDefined

717+ undefine names = undefine' names

718+ undefine' [] = return ()

719+ undefine' (n:names) = do

720+ allDefined <- idris_repl_defs `fmap` get

721+ if n `elem` allDefined

722+ then fputState (ctxt_lookup n . known_terms) Nothing

723+ else tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")

724+ fmodifyState repl_definitions (delete n)

725+ undefine' names

700

726

701process h fn (ExecVal t)

727process h fn (ExecVal t)

702 = do ctxt <- getContext

728 = do ctxt <- getContext

src/Idris/REPLParser.hs+2

@@ -53,6 +53,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

53 <|> try (do cmd ["let"]

54 defn <- concat <$> many (P.decl defaultSyntax)

55 return (NewDefn defn))

56+ <|> try (do cmd ["unlet","undefine"]

57+ Undefine `fmap` many P.name)

56 <|> try (do cmd ["lto", "loadto"];

58 <|> try (do cmd ["lto", "loadto"];

57 toline <- P.natural

59 toline <- P.natural

58 f <- many anyChar;

60 f <- many anyChar;