8d9f0ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1428 from trillioneyes/repl-definitions

8d9f0aeDavid Christiansen12 years ago

CONTRIBUTORS+1

compare with master

unifiedsplit

@@ -35,3 +35,4 @@ Dirk Ullrich

35Leif Warner

36Daniel Waterworth

37Jonas Westerlund

38+Alyssa Carter

src/Idris/ASTUtils.hs+22

@@ -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,24 @@ 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+known_classes :: Field IState (Ctxt ClassInfo)

146+known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})

147+

148+

149+-- Names defined at the repl

150+----------------------------

151+repl_definitions :: Field IState [Name]

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

153+

154+-- Fixity declarations in an IState

155+idris_fixities :: Field IState [FixDecl]

156+idris_fixities = Field idris_infixes (\v state -> state {idris_infixes = v})

src/Idris/AbsSyntaxTree.hs+4−2

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

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

202 idris_postulates :: S.Set Name,

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

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

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

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

205 }

206 }

206

207

207-- Required for parsers library, and therefore trifecta

208-- Required for parsers library, and therefore trifecta

@@ -280,7 +281,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

280 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

281 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

281 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

282 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

283− AutomaticWidth S.empty Nothing Nothing

284+ AutomaticWidth S.empty Nothing Nothing []

284

285

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

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

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

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

@@ -302,6 +303,7 @@ data Command = Quit

302 | Help

303 | Help

303 | Eval PTerm

304 | Eval PTerm

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

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

306+ | Undefine [Name]

305 | Check PTerm

307 | Check PTerm

306 | DocStr (Either Name Const)

308 | DocStr (Either Name Const)

307 | TotCheck Name

309 | TotCheck Name

src/Idris/Help.hs+11−1

@@ -11,6 +11,10 @@ data CmdArg = ExprArg -- ^ The command takes an expression

11 | NoArg -- ^ No completion (yet!?)

12 | SpecialHeaderArg -- ^ do not use

13 | ConsoleWidthArg -- ^ The width of the console

14+ | DeclArg -- ^ An Idris declaration, as might be contained in a file

15+ | ManyArgs CmdArg -- ^ Zero or more of one kind of argument

16+ | OptionalArg CmdArg -- ^ Zero or one of one kind of argument

17+ | SeqArgs CmdArg CmdArg -- ^ One kind of argument followed by another

15instance Show CmdArg where

19instance Show CmdArg where

16 show ExprArg = "<expr>"

20 show ExprArg = "<expr>"

@@ -24,6 +28,10 @@ instance Show CmdArg where

24 show NoArg = ""

28 show NoArg = ""

25 show SpecialHeaderArg = "Arguments"

29 show SpecialHeaderArg = "Arguments"

26 show ConsoleWidthArg = "auto|infinite|<number>"

30 show ConsoleWidthArg = "auto|infinite|<number>"

31+ show DeclArg = "<top-level declaration>"

32+ show (ManyArgs a) = "(" ++ show a ++ ")..."

33+ show (OptionalArg a) = "[" ++ show a ++ "]"

34+ show (SeqArgs a b) = show a ++ " " ++ show b

28help :: [([String], CmdArg, String)]

36help :: [([String], CmdArg, String)]

29help =

37help =

@@ -59,7 +67,9 @@ help =

59 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

67 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

60 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

68 ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

61 ([":q",":quit"], NoArg, "Exit the Idris system"),

69 ([":q",":quit"], NoArg, "Exit the Idris system"),

62− ([":w", ":warranty"], NoArg, "Displays warranty information")

70+ ([":w", ":warranty"], NoArg, "Displays warranty information"),

71+ ([":let"], ManyArgs DeclArg, "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"),

72+ ([":undefine",":unlet"], ManyArgs NameArg, "Remove the listed repl definitions, or all repl definitions if no names given")

63 ]

73 ]

65-- | Use these for completion, but don't show them in :help

75-- | Use these for completion, but don't show them in :help

src/Idris/Output.hs+6

@@ -164,3 +164,9 @@ warnTotality :: Idris ()

164warnTotality = do ist <- getIState

165 mapM_ (warn ist) (nub (idris_totcheckfail ist))

166 where warn ist (fc, e) = iWarn fc (pprintErr ist (Msg e))

167+

168+

169+printUndefinedNames :: [Name] -> Doc OutputAnnotation

170+printUndefinedNames ns = text "Undefined " <> names <> text "."

171+ where names = encloseSep empty empty (char ',') $ map ppName ns

172+ ppName = prettyName True True []

src/Idris/REPL.hs+67−3

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

54import IRTS.CodegenCommon

55import IRTS.System

57+import Control.Category

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

57import Data.List.Split (splitOn)

59import Data.List.Split (splitOn)

58import Data.List (groupBy)

60import Data.List (groupBy)

59import qualified Data.Text as T

61import qualified Data.Text as T

@@ -701,12 +703,15 @@ process fn (Eval t)

701 iPrintTermWithType tmDoc tyDoc

703 iPrintTermWithType tmDoc tyDoc

702

704

703

705

706+process fn (NewDefn decls) = do

707+ logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))

704−process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ show namedGroups) >> mapM_ defineName namedGroups where

708+ mapM_ defineName namedGroups where

705 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

709 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

706 getName :: PDecl -> Maybe Name

710 getName :: PDecl -> Maybe Name

707 getName (PTy docs argdocs syn fc opts name ty) = Just name

711 getName (PTy docs argdocs syn fc opts name ty) = Just name

708 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

712 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

709 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

713 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

714+ getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name

710 getName _ = Nothing

715 getName _ = Nothing

711 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

716 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

712 getClauseName (PClause fc name whole with rhs whereBlock) = name

717 getClauseName (PClause fc name whole with rhs whereBlock) = name

@@ -715,6 +720,7 @@ process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ s

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

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

716 elabDecl EAll recinfo tyDecl

721 elabDecl EAll recinfo tyDecl

717 elabClauses recinfo fc opts name (concatMap getClauses decls)

722 elabClauses recinfo fc opts name (concatMap getClauses decls)

723+ setReplDefined (Just name)

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

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

719 let pterm = getRHS clause

725 let pterm = getRHS clause

720 (tm,ty) <- elabVal recinfo ERHS pterm

726 (tm,ty) <- elabVal recinfo ERHS pterm

@@ -722,8 +728,16 @@ process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ s

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

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

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

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

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

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

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

731+ setReplDefined (Just $ getClauseName clause)

726− elabData recinfo syn doc argdocs fc opts decl

732+ defineName (PClauses{} : _) = tclift $ tfail (Msg "Only one function body is allowed without a type declaration.")

733+ -- fixity and syntax declarations are ignored by elabDecls, so they'll have to be handled some other way

734+ defineName (PFix fc fixity strs : defns) = do

735+ fmodifyState idris_fixities (map (Fix fixity) strs ++)

736+ unless (null defns) $ defineName defns

737+ defineName (PSyntax{}:_) = tclift $ tfail (Msg "That kind of declaration is not supported. If you feel it should be supported, please submit an issue at https://github.com/idris-lang/Idris-dev.")

738+ defineName decls = do

739+ elabDecls toplevel (map fixClauses decls)

740+ setReplDefined (getName (head decls))

727 getClauses (PClauses fc opts name clauses) = clauses

741 getClauses (PClauses fc opts name clauses) = clauses

728 getClauses _ = []

742 getClauses _ = []

729 getRHS :: PClause -> PTerm

743 getRHS :: PClause -> PTerm

@@ -731,6 +745,56 @@ process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ s

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

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

732 getRHS (PClauseR fc with rhs whereBlock) = rhs

746 getRHS (PClauseR fc with rhs whereBlock) = rhs

733 getRHS (PWithR fc with rhs whereBlock) = rhs

747 getRHS (PWithR fc with rhs whereBlock) = rhs

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

749+ setReplDefined Nothing = return ()

750+ setReplDefined (Just n) = do

751+ oldState <- get

752+ fmodifyState repl_definitions (n:)

753+ -- the "name" field of PClauses seems to always be MN 2 "__", so we need to

754+ -- retrieve the actual name from deeper inside.

755+ -- This should really be a full recursive walk through the structure of PDecl, but

756+ -- I think it should work this way and I want to test sooner. Also lazy.

757+ fixClauses :: PDecl' t -> PDecl' t

758+ fixClauses (PClauses fc opts _ css@(clause:cs)) =

759+ PClauses fc opts (getClauseName clause) css

760+ fixClauses (PInstance syn fc constraints cls parms ty instName decls) =

761+ PInstance syn fc constraints cls parms ty instName (map fixClauses decls)

762+ fixClauses decl = decl

763+

764+process fn (Undefine names) = undefine names

765+ where

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

767+ undefine [] = do

768+ allDefined <- idris_repl_defs `fmap` get

769+ undefine' allDefined []

770+ -- Keep track of which names you've removed so you can

771+ -- print them out to the user afterward

772+ undefine names = undefine' names []

773+ undefine' [] list = do iRenderOutput $ printUndefinedNames list

774+ return ()

775+ undefine' (n:names) already = do

776+ allDefined <- idris_repl_defs `fmap` get

777+ if n `elem` allDefined

778+ then do undefinedJustNow <- undefClosure n

779+ undefine' names (undefinedJustNow ++ already)

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

781+ undefine' names already

782+ undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing

783+ -- for now just assume it's a class. Eventually we'll want some kind of

784+ -- smart detection of exactly what kind of name we're undefining.

785+ fputState (ctxt_lookup n . known_classes) Nothing

786+ fmodifyState repl_definitions (delete n)

787+ undefClosure n =

788+ do replDefs <- idris_repl_defs `fmap` get

789+ callGraph <- whoCalls n

790+ let users = case lookup n callGraph of

791+ Just ns -> nub ns

792+ Nothing -> fail ("Tried to undefine nonexistent name" ++ show n)

793+ undefinedJustNow <- concat `fmap` mapM undefClosure users

794+ undefOne n

795+ return (nub (n : undefinedJustNow))

796+

797+

734

798

735process fn (ExecVal t)

799process fn (ExecVal t)

736 = do ctxt <- getContext

800 = do ctxt <- getContext

src/Idris/REPLParser.hs+3

@@ -32,6 +32,7 @@ cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length

32 docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs

34pCmd :: P.IdrisParser Command

35+

35pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

36pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

36 <|> do cmd ["h", "?", "help"]; eof; return Help

37 <|> do cmd ["h", "?", "help"]; eof; return Help

37 <|> do cmd ["w", "warranty"]; eof; return Warranty

38 <|> do cmd ["w", "warranty"]; eof; return Warranty

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

53 <|> do cmd ["let"]

54 <|> do cmd ["let"]

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

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

55 return (NewDefn defn)

56 return (NewDefn defn)

57+ <|> do cmd ["unlet","undefine"]

58+ Undefine `fmap` many P.name

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

59 <|> do cmd ["lto", "loadto"];

57 toline <- P.natural

60 toline <- P.natural

58 f <- many anyChar;

61 f <- many anyChar;