a5e8ca3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Changed :let to work with an arbitrary number of `PDecl`s (though only one name at a time for now).

a5e8ca3Alyssa Carter12 years ago

src/Idris/AbsSyntaxTree.hs+1−1

compare with master

unifiedsplit

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

287data Command = Quit

288 | Help

289 | Eval PTerm

290− | NewDefn Name PTerm

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

291 | Check PTerm

292 | DocStr (Either Name Const)

293 | TotCheck Name

src/Idris/REPL.hs+19−6

@@ -663,12 +663,25 @@ process h fn (Eval t)

663 tyDoc = pprintDelab ist ty'

664 ihPrintTermWithType h tmDoc tyDoc

665

666−process h fn (NewDefn name val)

666+process h fn (NewDefn fc (tyDecl:decls))

667+ | isTyDecl tyDecl = do

668+ elabDecl EAll toplevel tyDecl

669+ name <- getName tyDecl

670+ logLvl 3 $ "Defining " ++ show name ++ " with this type decl: " ++ show tyDecl

671+ logLvl 5 $ "Using this definition: " ++ show decls

672+ elabClauses toplevel fc [] name defn

673+ where getName (PTy docs argdocs syn fc opts name ty) = return name

674+ getName _ = fail "New definitions must begin with a type declaration"

675+ isTyDecl PTy{} = True

676+ isTyDecl _ = False

677+ defn = concatMap getClauses decls

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

679+ getClauses _ = []

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

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

668− ctxt <- getContext

681+ -- ctxt <- getContext

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

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

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

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

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

684+ -- updateContext (addCtxtDef name (Function ty' tm'))

672

685

673process h fn (ExecVal t)

686process h fn (ExecVal t)

674 = do ctxt <- getContext

687 = do ctxt <- getContext

src/Idris/REPLParser.hs+3−5

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

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

53+ fc <- P.getFC

54− P.lchar '='

55− val <- P.fullExpr defaultSyntax

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

56− eof

57− return (NewDefn name val))

55+ return (NewDefn fc defn))

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

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

59 toline <- P.natural

57 toline <- P.natural

60 f <- many anyChar;

58 f <- many anyChar;