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

git.iko.soy/Idris-dev

Added an :unlet/:undefine command.

Idris> :let nat : Nat; nat = 6; hands = S nat; feet = S hands Idris> :undefine Idris> hands -- error Alternately: Idris> :let nat : Nat; nat = 6; hands = S nat; feet = S hands Idris> :undefine nat feet Idris> hands 7 Idris> feet -- error

commit5c4f5d2f79b2cc5a8202207efb9c776d4ed9d877 authorAlyssa Carter <trillionalyssa@gmail.com> dateSat 19 Jul 2014, 16:51 (12 years ago) parenta0ba488

4 files changed+48−3

compare with master

unifiedsplit

src/Idris/ASTUtils.hs+15 src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/REPL.hs+27−1 src/Idris/REPLParser.hs+2

src/Idris/ASTUtils.hs+15

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

3838import Prelude hiding (id, (.))

3939

4040import Idris.Core.TT

41+import Idris.Core.Evaluate

4142import Idris.AbsSyntaxTree

4243

4344data Field rec fld = Field

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

132133opts_idrisCmdline =

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

134135 . 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 {

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

192192 idris_postulates :: S.Set Name,

193193 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

195196 }

196197

197198data SizeChange = Smaller | Same | Bigger | Unknown

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

266267 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

267268 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput

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

269− AutomaticWidth S.empty Nothing Nothing

270+ AutomaticWidth S.empty Nothing Nothing []

270271

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

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

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

288289 | Help

289290 | Eval PTerm

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

292+ | Undefine [Name]

291293 | Check PTerm

292294 | DocStr (Either Name Const)

293295 | TotCheck Name

src/Idris/REPL.hs+27−1

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

4949import IRTS.CodegenCommon

5050import IRTS.System

5151

52+import Control.Category

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

5254import Data.List.Split (splitOn)

5355import Data.List (groupBy)

5456import qualified Data.Text as T

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

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

682684 elabDecl EAll toplevel tyDecl

683685 elabClauses toplevel fc opts name (concatMap getClauses decls)

686+ setReplDefined (getName tyDecl)

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

685688 let pterm = getRHS clause

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

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

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

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

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

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

694+ setReplDefined (Just $ getClauseName clause)

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

692696 elabData toplevel syn doc argdocs fc opts decl

697+ setReplDefined (getName def)

693698 getClauses (PClauses fc opts name clauses) = clauses

694699 getClauses _ = []

695700 getRHS :: PClause -> PTerm

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

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

698703 getRHS (PClauseR fc with rhs whereBlock) = rhs

699704 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

700726

701727process h fn (ExecVal t)

702728 = do ctxt <- getContext

src/Idris/REPLParser.hs+2

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

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

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

5555 return (NewDefn defn))

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

57+ Undefine `fmap` many P.name)

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

5759 toline <- P.natural

5860 f <- many anyChar;