1fa2dfa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

More concise 'with' syntax if patterns are repeated from previous line

commit1fa2dfa40fda16189d25bb4b3164b4601d522bb4 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 18 Dec 2011, 16:19 (15 years ago) parent001e2d5

4 files changed+48−11

compare with master

unifiedsplit

lib/prelude/list.idr+2−2 lib/prelude/vect.idr+1−1 src/Idris/AbsSyntax.hs+2−1 src/Idris/Parser.hs+43−7

lib/prelude/list.idr+2−2

@@ -34,8 +34,8 @@ map f (x :: xs) = f x :: map f xs;

3434filter : (y -> Bool) -> List y -> List y;

3535filter pred [] = [];

3636filter pred (x :: xs) with (pred x, filter pred xs) {

37− filter pred (x :: xs) | (True, fxs) = x :: fxs;

38− filter pred (x :: xs) | (False, fxs) = fxs;

37+ | (True, fxs) = x :: fxs;

38+ | (False, fxs) = fxs;

3939}

4040

4141

lib/prelude/vect.idr+1−1

@@ -31,7 +31,7 @@ app (x :: xs) ys = x :: app xs ys;

3131filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

3232filter p [] = ( _ ** [] );

3333filter p (x :: xs) with (filter p xs) {

34− filter p (x :: xs) | ( _ ** xs' )

34+ | ( _ ** xs' )

3535 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

3636}

3737

src/Idris/AbsSyntax.hs+2−1

@@ -49,6 +49,7 @@ data IState = IState { tt_ctxt :: Context,

4949 idris_hdrs :: [String],

5050 last_proof :: Maybe (Name, [String]),

5151 errLine :: Maybe Int,

52+ lastParse :: Maybe (Name, PTerm, [PTerm]),

5253 ibc_write :: [IBCWrite]

5354 }

5455

@@ -67,7 +68,7 @@ data IBCWrite = IBCFix FixDecl

6768 deriving Show

6869

6970idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

70− "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing []

71+ "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing Nothing []

7172

7273-- The monad for the main REPL - reading and processing files and updating

7374-- global state (hence the IO inner monad).

src/Idris/Parser.hs+43−7

@@ -751,22 +751,53 @@ pClause syn

751751 (wheres, nmap) <- choice [pWhereblock n wsyn,

752752 do lchar ';'

753753 return ([], [])]

754− return $ PClause n (PApp fc (PRef fc n)

755− (iargs ++ cargs ++ map pexp args)) wargs rhs wheres)

754+ let capp = PApp fc (PRef fc n)

755+ (iargs ++ cargs ++ map pexp args)

756+ setState (ist { lastParse = Just (n, capp, wargs) })

757+ return $ PClause n capp wargs rhs wheres)

758+ <|> try (do wargs <- many (pWExpr syn)

759+ ist <- getState

760+ (n, capp, owargs) <- case lastParse ist of

761+ Just t -> return t

762+ Nothing -> fail "Invalid clause"

763+ rhs <- pRHS syn n

764+ let ctxt = tt_ctxt ist

765+ let wsyn = syn { syn_namespace = [] }

766+ (wheres, nmap) <- choice [pWhereblock n wsyn,

767+ do lchar ';'

768+ return ([], [])]

769+ return $ PClause n capp (owargs ++ wargs) rhs wheres)

770+

756771 <|> try (do n_in <- pfName; let n = expandNS syn n_in

757772 cargs <- many (pConstraintArg syn)

758773 iargs <- many (pImplicitArg syn)

759774 fc <- pfc

760775 args <- many (pArgExpr syn)

761776 wargs <- many (pWExpr syn)

777+ let capp = PApp fc (PRef fc n)

778+ (iargs ++ cargs ++ map pexp args)

779+ ist <- getState

780+ setState (ist { lastParse = Just (n, capp, wargs) })

762781 reserved "with"

763782 wval <- pExpr syn

764783 lchar '{'

765784 ds <- many1 $ pFunDecl syn

766785 let withs = concat ds

767786 lchar '}'

768− return $ PWith n (PApp fc (PRef fc n)

769− (iargs ++ cargs ++ map pexp args)) wargs wval withs)

787+ return $ PWith n capp wargs wval withs)

788+

789+ <|> try (do wargs <- many (pWExpr syn)

790+ reserved "with"

791+ ist <- getState

792+ (n, capp, owargs) <- case lastParse ist of

793+ Just t -> return t

794+ Nothing -> fail "Invalid clause"

795+ wval <- pExpr syn

796+ lchar '{'

797+ ds <- many1 $ pFunDecl syn

798+ let withs = concat ds

799+ lchar '}'

800+ return $ PWith n capp (owargs ++ wargs) wval withs)

770801

771802 <|> do l <- pArgExpr syn

772803 op <- operator

@@ -779,8 +810,10 @@ pClause syn

779810 (wheres, nmap) <- choice [pWhereblock n wsyn,

780811 do lchar ';'

781812 return ([], [])]

782− return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])

783− wargs rhs wheres

813+ ist <- getState

814+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]

815+ setState (ist { lastParse = Just (n, capp, wargs) })

816+ return $ PClause n capp wargs rhs wheres

784817

785818 <|> do l <- pArgExpr syn

786819 op <- operator

@@ -794,7 +827,10 @@ pClause syn

794827 ds <- many1 $ pFunDecl syn

795828 let withs = concat ds

796829 lchar '}'

797− return $ PWith n (PApp fc (PRef fc n) [pexp l, pexp r]) wargs wval withs

830+ ist <- getState

831+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]

832+ setState (ist { lastParse = Just (n, capp, wargs) })

833+ return $ PWith n capp wargs wval withs

798834

799835pWExpr :: SyntaxInfo -> IParser PTerm

800836pWExpr syn = do lchar '|'; pExpr' syn