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

git.iko.soy/Idris-dev

on master help sign in

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

1fa2dfaEdwin Brady15 years ago

lib/prelude/list.idr+2−2

compare with master

unifiedsplit

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

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

35filter pred [] = [];

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

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

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

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

38+ | (False, fxs) = fxs;

39}

lib/prelude/vect.idr+1−1

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

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

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

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

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

34+ | ( _ ** xs' )

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

36}

src/Idris/AbsSyntax.hs+2−1

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

49 idris_hdrs :: [String],

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

51 errLine :: Maybe Int,

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

52 ibc_write :: [IBCWrite]

53 ibc_write :: [IBCWrite]

53 }

54 }

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

67 deriving Show

68 deriving Show

69idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

70idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

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

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

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

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

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

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

src/Idris/Parser.hs+43−7

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

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

752 do lchar ';'

753 return ([], [])]

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

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

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

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+

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

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

757 cargs <- many (pConstraintArg syn)

772 cargs <- many (pConstraintArg syn)

758 iargs <- many (pImplicitArg syn)

773 iargs <- many (pImplicitArg syn)

759 fc <- pfc

774 fc <- pfc

760 args <- many (pArgExpr syn)

775 args <- many (pArgExpr syn)

761 wargs <- many (pWExpr syn)

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

762 reserved "with"

781 reserved "with"

763 wval <- pExpr syn

782 wval <- pExpr syn

764 lchar '{'

783 lchar '{'

765 ds <- many1 $ pFunDecl syn

784 ds <- many1 $ pFunDecl syn

766 let withs = concat ds

785 let withs = concat ds

767 lchar '}'

786 lchar '}'

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

787+ return $ PWith n capp wargs wval withs)

769− (iargs ++ cargs ++ map pexp args)) 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)

770

801

771 <|> do l <- pArgExpr syn

802 <|> do l <- pArgExpr syn

772 op <- operator

803 op <- operator

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

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

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

780 do lchar ';'

811 do lchar ';'

781 return ([], [])]

812 return ([], [])]

813+ ist <- getState

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

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

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

783− wargs rhs wheres

816+ return $ PClause n capp wargs rhs wheres

784

817

785 <|> do l <- pArgExpr syn

818 <|> do l <- pArgExpr syn

786 op <- operator

819 op <- operator

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

794 ds <- many1 $ pFunDecl syn

827 ds <- many1 $ pFunDecl syn

795 let withs = concat ds

828 let withs = concat ds

796 lchar '}'

829 lchar '}'

830+ ist <- getState

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

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

798

834

799pWExpr :: SyntaxInfo -> IParser PTerm

835pWExpr :: SyntaxInfo -> IParser PTerm

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

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