e260741 · Idris-dev · git.iko.soy

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 Name PTerm

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+7

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

663 tyDoc = pprintDelab ist ty'

664 ihPrintTermWithType h tmDoc tyDoc

665

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+

666process h fn (ExecVal t)

673process h fn (ExecVal t)

667 = do ctxt <- getContext

674 = do ctxt <- getContext

668 ist <- getIState

675 ist <- getIState

src/Idris/REPLParser.hs+6

@@ -49,6 +49,12 @@ 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 ["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 ["let"]

53+ name <- P.name

54+ P.lchar '='

55+ val <- P.fullExpr defaultSyntax

56+ eof

57+ return (NewDefn name val))

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

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

53 toline <- P.natural

59 toline <- P.natural

54 f <- many anyChar;

60 f <- many anyChar;