c1277c8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Handling more forms of definition.

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

291 | Check PTerm

292 | DocStr (Either Name Const)

293 | TotCheck Name

src/Idris/REPL.hs+50−19

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

50import IRTS.System

52import Data.List.Split (splitOn)

53+import Data.List (groupBy)

53import qualified Data.Text as T

54import qualified Data.Text as T

55import Text.Trifecta.Result(Result(..))

56import Text.Trifecta.Result(Result(..))

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

663 tyDoc = pprintDelab ist ty'

664 tyDoc = pprintDelab ist ty'

664 ihPrintTermWithType h tmDoc tyDoc

665 ihPrintTermWithType h tmDoc tyDoc

665

666

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

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+

667− | isTyDecl tyDecl = do

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

668− elabDecl EAll toplevel tyDecl

697+-- elabDecl EAll toplevel tyDecl

669− name <- getName tyDecl

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

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

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

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

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

672− elabClauses toplevel fc [] name defn

701+-- elabClauses toplevel fc [] name defn

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

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

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

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

675− isTyDecl PTy{} = True

704+-- isTyDecl PTy{} = True

676− isTyDecl _ = False

705+-- isTyDecl _ = False

677− defn = concatMap getClauses decls

706+-- defn = concatMap getClauses decls

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

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

679− getClauses _ = []

708+-- getClauses _ = []

709+

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

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

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

681− -- ctxt <- getContext

712+-- ctxt <- getContext

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

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

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

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

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

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

685

716

686process h fn (ExecVal t)

717process h fn (ExecVal t)

687 = do ctxt <- getContext

718 = do ctxt <- getContext

src/Idris/REPLParser.hs+2−2

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

1module Idris.REPLParser(parseCmd) where

2module Idris.REPLParser(parseCmd) where

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

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

@@ -50,9 +51,8 @@ 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 ["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 ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

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

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

53− fc <- P.getFC

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

55− return (NewDefn fc defn))

55+ return (NewDefn defn))

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

57 toline <- P.natural

58 f <- many anyChar;