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

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1361 from trillioneyes/repl-definitions

3c4bd14Edwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

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

287data Command = Quit

288 | Help

289 | Eval PTerm

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

290 | Check PTerm

291 | Check PTerm

291 | DocStr (Either Name Const)

292 | DocStr (Either Name Const)

292 | TotCheck Name

293 | TotCheck Name

src/Idris/REPL.hs+33

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

50import IRTS.System

52import Data.List.Split (splitOn)

53+import Data.List (groupBy)

53import qualified Data.Text as T

54import qualified Data.Text as T

55import Text.Trifecta.Result(Result(..))

56import Text.Trifecta.Result(Result(..))

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

663 tyDoc = pprintDelab ist ty'

664 tyDoc = pprintDelab ist ty'

664 ihPrintTermWithType h tmDoc tyDoc

665 ihPrintTermWithType h tmDoc tyDoc

665

666

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+

666process h fn (ExecVal t)

699process h fn (ExecVal t)

667 = do ctxt <- getContext

700 = do ctxt <- getContext

668 ist <- getIState

701 ist <- getIState

src/Idris/REPLParser.hs+4

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

1module Idris.REPLParser(parseCmd) where

2module Idris.REPLParser(parseCmd) where

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

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

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

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

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

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

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

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

52 <|> 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))

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

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

53 toline <- P.natural

57 toline <- P.natural

54 f <- many anyChar;

58 f <- many anyChar;