a5e8ca3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

It is no longer possible to leave off the type declaration. This will be fixed soon.

commita5e8ca30aad3426f297e7ac99fa89c5903c1e58b authorAlyssa Carter <trillionalyssa@gmail.com> dateThu 3 Jul 2014, 15:32 (12 years ago) parente260741

3 files changed+23−12

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/REPL.hs+19−6 src/Idris/REPLParser.hs+3−5

src/Idris/AbsSyntaxTree.hs+1−1

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

287287data Command = Quit

288288 | Help

289289 | 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.

291291 | Check PTerm

292292 | DocStr (Either Name Const)

293293 | TotCheck Name

src/Idris/REPL.hs+19−6

@@ -663,12 +663,25 @@ 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'))

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 _ = []

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

681+ -- ctxt <- getContext

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

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

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

672685

673686process h fn (ExecVal t)

674687 = 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)

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

5252 <|> try (do cmd ["let"]

53− name <- P.name

54− P.lchar '='

55− val <- P.fullExpr defaultSyntax

56− eof

57− return (NewDefn name val))

53+ fc <- P.getFC

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

55+ return (NewDefn fc defn))

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

5957 toline <- P.natural

6058 f <- many anyChar;