@@ -54,6 +54,8 @@ import IRTS.Compiler
5454import IRTS.CodegenCommon
5555import IRTS.System
5656
57+import Control.Category
58+import Prelude hiding ((.), id)
5759import Data.List.Split (splitOn)
5860import Data.List (groupBy)
5961import qualified Data.Text as T
@@ -701,12 +703,15 @@ process fn (Eval t)
701703 iPrintTermWithType tmDoc tyDoc
702704
703705
704−process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ show namedGroups) >> mapM_ defineName namedGroups where
706+process fn (NewDefn decls) = do
707+ logLvl 3 ("Defining names using these decls: " ++ show (showDecls verbosePPOption decls))
708+ mapM_ defineName namedGroups where
705709 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls
706710 getName :: PDecl -> Maybe Name
707711 getName (PTy docs argdocs syn fc opts name ty) = Just name
708712 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
709713 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
710715 getName _ = Nothing
711716 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
712717 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
715720 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do
716721 elabDecl EAll recinfo tyDecl
717722 elabClauses recinfo fc opts name (concatMap getClauses decls)
723+ setReplDefined (Just name)
718724 defineName [PClauses fc opts _ [clause]] = do
719725 let pterm = getRHS clause
720726 (tm,ty) <- elabVal recinfo ERHS pterm
@@ -722,8 +728,16 @@ process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ s
722728 let tm' = force (normaliseAll ctxt [] tm)
723729 let ty' = force (normaliseAll ctxt [] ty)
724730 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
725− defineName [PData doc argdocs syn fc opts decl] = do
726− elabData recinfo syn doc argdocs fc opts decl
731+ setReplDefined (Just $ getClauseName clause)
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))
727741 getClauses (PClauses fc opts name clauses) = clauses
728742 getClauses _ = []
729743 getRHS :: PClause -> PTerm
@@ -731,6 +745,56 @@ process fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++ s
731745 getRHS (PWith fc name whole with rhs whereBlock) = rhs
732746 getRHS (PClauseR fc with rhs whereBlock) = rhs
733747 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+
734798
735799process fn (ExecVal t)
736800 = do ctxt <- getContext