c1277c8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Handling more forms of definition.

In particular, it should now be possible to define multiple names at once, and to leave off type declarations when the type can be inferred.

commitc1277c8035fa3f9f2418aa3556f8814d2782aeb9 authorAlyssa Carter <trillionalyssa@gmail.com> dateFri 4 Jul 2014, 11:55 (12 years ago) parenta5e8ca3

3 files changed+53−22

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/REPL.hs+50−19 src/Idris/REPLParser.hs+2−2

src/Idris/AbsSyntaxTree.hs+1−1

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

287287data Command = Quit

288288 | Help

289289 | Eval PTerm

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

290+ | NewDefn [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+50−19

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

5050import IRTS.System

5151

5252import Data.List.Split (splitOn)

53+import Data.List (groupBy)

5354import qualified Data.Text as T

5455

5556import Text.Trifecta.Result(Result(..))

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

663664 tyDoc = pprintDelab ist ty'

664665 ihPrintTermWithType h tmDoc tyDoc

665666

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

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 _ = Nothing

674+ -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

675+ getClauseName (PClause fc name whole with rhs whereBlock) = name

676+ getClauseName (PWith fc name whole with rhs whereBlock) = name

677+ defineName :: [PDecl] -> Idris ()

678+ defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

679+ elabDecl EAll toplevel tyDecl

680+ elabClauses toplevel fc opts name (concatMap getClauses decls)

681+ defineName [PClauses fc opts _ [clause]] = do

682+ let pterm = getRHS clause

683+ (tm,ty) <- elabVal toplevel False pterm

684+ ctxt <- getContext

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

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

687+ updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))

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

689+ getClauses _ = []

690+ getRHS :: PClause -> PTerm

691+ getRHS (PClause fc name whole with rhs whereBlock) = rhs

692+ getRHS (PWith fc name whole with rhs whereBlock) = rhs

693+ getRHS (PClauseR fc with rhs whereBlock) = rhs

694+ getRHS (PWithR fc with rhs whereBlock) = rhs

695+

696+-- process h fn (NewDefn (tyDecl:decls)) | isTyDecl tyDecl = do

697+-- elabDecl EAll toplevel tyDecl

698+-- (name, fc) <- getInfo tyDecl

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

700+-- logLvl 5 $ "Using this definition: " ++ show decls

701+-- elabClauses toplevel fc [] name defn

702+-- where getInfo (PTy docs argdocs syn fc opts name ty) = return (name, fc)

703+-- getInfo _ = fail "New definitions must begin with a type declaration"

704+-- isTyDecl PTy{} = True

705+-- isTyDecl _ = False

706+-- defn = concatMap getClauses decls

707+-- getClauses (PClauses fc opts name clauses) = clauses

708+-- getClauses _ = []

709+

710+-- process h fn (NewDefn [PCAF fc name val])

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

712+-- ctxt <- getContext

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

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

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

685716

686717process h fn (ExecVal t)

687718 = do ctxt <- getContext

src/Idris/REPLParser.hs+2−2

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

12module Idris.REPLParser(parseCmd) where

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

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

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

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

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

53− fc <- P.getFC

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

55− return (NewDefn fc defn))

55+ return (NewDefn defn))

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

5757 toline <- P.natural

5858 f <- many anyChar;