3c4bd14 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1361 from trillioneyes/repl-definitions

Repl definitions

commit3c4bd14521b4a3211ad98824012124fadd67eceb authorEdwin Brady <edwin.brady@gmail.com> dateSun 6 Jul 2014, 16:10 (12 years ago) parentd9513aa 204ebf5

3 files changed+38

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/REPL.hs+33 src/Idris/REPLParser.hs+4

src/Idris/AbsSyntaxTree.hs+1

@@ -287,6 +287,7 @@ data Codegen = ViaC

287287data Command = Quit

288288 | Help

289289 | Eval PTerm

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

290291 | Check PTerm

291292 | DocStr (Either Name Const)

292293 | TotCheck Name

src/Idris/REPL.hs+33

@@ -50,6 +50,7 @@ import IRTS.CodegenCommon

5050import IRTS.System

5151

5252import Data.List.Split (splitOn)

53+import Data.List (groupBy)

5354import qualified Data.Text as T

5455

5556import Text.Trifecta.Result(Result(..))

@@ -663,6 +664,38 @@ process h fn (Eval t)

663664 tyDoc = pprintDelab ist ty'

664665 ihPrintTermWithType h tmDoc tyDoc

665666

667+

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

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

670+ getName :: PDecl -> Maybe Name

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

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

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

674+ getName _ = Nothing

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

676+ getClauseName (PClause fc name whole with rhs whereBlock) = name

677+ getClauseName (PWith fc name whole with rhs whereBlock) = name

678+ defineName :: [PDecl] -> Idris ()

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

680+ elabDecl EAll toplevel tyDecl

681+ elabClauses toplevel fc opts name (concatMap getClauses decls)

682+ defineName [PClauses fc opts _ [clause]] = do

683+ let pterm = getRHS clause

684+ (tm,ty) <- elabVal toplevel False pterm

685+ ctxt <- getContext

686+ let tm' = force (normaliseAll ctxt [] tm)

687+ let ty' = force (normaliseAll ctxt [] ty)

688+ updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))

689+ defineName [PData doc argdocs syn fc opts decl] = do

690+ elabData toplevel syn doc argdocs fc opts decl

691+ getClauses (PClauses fc opts name clauses) = clauses

692+ getClauses _ = []

693+ getRHS :: PClause -> PTerm

694+ getRHS (PClause fc name whole with rhs whereBlock) = rhs

695+ getRHS (PWith fc name whole with rhs whereBlock) = rhs

696+ getRHS (PClauseR fc with rhs whereBlock) = rhs

697+ getRHS (PWithR fc with rhs whereBlock) = rhs

698+

666699process h fn (ExecVal t)

667700 = do ctxt <- getContext

668701 ist <- getIState

src/Idris/REPLParser.hs+4

@@ -1,3 +1,4 @@

12module Idris.REPLParser(parseCmd) where

34import System.FilePath ((</>))

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

4950 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

5051 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

5152 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

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

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

55+ return (NewDefn defn))

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

5357 toline <- P.natural

5458 f <- many anyChar;