e260741 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Preliminary support for a :let command in the repl

commite26074179c531553e555a12836b563bc3de0d7d7 authorAlyssa Carter <trillionalyssa@gmail.com> dateWed 2 Jul 2014, 16:12 (12 years ago) parentf2e30f2

3 files changed+14

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1

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

287287data Command = Quit

288288 | Help

289289 | Eval PTerm

290+ | NewDefn Name PTerm

290291 | Check PTerm

291292 | DocStr (Either Name Const)

292293 | TotCheck Name

src/Idris/REPL.hs+7

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

663663 tyDoc = pprintDelab ist ty'

664664 ihPrintTermWithType h tmDoc tyDoc

665665

666+process h fn (NewDefn name val)

667+ = do (tm, ty) <- elabVal toplevel False val

668+ ctxt <- getContext

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

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

671+ updateContext (addCtxtDef name (Function ty' tm'))

672+

666673process h fn (ExecVal t)

667674 = do ctxt <- getContext

668675 ist <- getIState

src/Idris/REPLParser.hs+6

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

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

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

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

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

53+ name <- P.name

54+ P.lchar '='

55+ val <- P.fullExpr defaultSyntax

56+ eof

57+ return (NewDefn name val))

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

5359 toline <- P.natural

5460 f <- many anyChar;