2eb5b52 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Pattern clause parser

2eb5b52Edwin Brady15 years ago

decls.mi+6−5

compare with master

unifiedsplit

@@ -11,15 +11,16 @@ data Vect : Set -> Nat -> Set where

11 | (::) : a -> Vect a k -> Vect a (S k);

13plus : Nat -> Nat -> Nat;

14−{-

15plus O y = y;

14plus O y = y;

16plus (S k) y = S (plus k y);

15plus (S k) y = S (plus k y);

17−-}

19app : Vect a n -> Vect a m -> Vect a (plus n m);

17app : Vect a n -> Vect a m -> Vect a (plus n m);

20−{-

21app VNil ys = ys;

18app VNil ys = ys;

22app (x :: xs) ys = x :: (app xs ys);

19app (x :: xs) ys = x :: (app xs ys);

23−-}

25−(::) : a -> Vect a k -> Vect a (S k);

21+infixl 5 .+. ;

22+

23+(.+.) : Nat -> Nat -> Nat;

24+O .+. y = y;

25+(S k) .+. y = S (k .+. y);

26+

src/Idris/AbsSyntax.hs+1

@@ -82,6 +82,7 @@ data PTerm = PQuote Raw

82 | PLam Name PTerm PTerm

83 | PPi Plicity Name PTerm PTerm

84 | PApp PTerm [(Name, PTerm)] [PTerm]

85+ | PHidden PTerm -- irrelevant or hidden pattern

85 | PSet

86 | PSet

86 | Placeholder

87 | Placeholder

87 deriving Show

88 deriving Show

src/Idris/Parser.hs+20

@@ -40,6 +40,7 @@ parseProg :: String -> Idris [PDecl]

40parseProg fname = do file <- lift $ readFile fname

41 i <- get

42 case (runParser (do ps <- many1 pDecl

43+ eof

43 i' <- getState

44 i' <- getState

44 return (ps, i')) i fname file) of

45 return (ps, i')) i fname file) of

45 Left err -> fail (show err)

46 Left err -> fail (show err)

@@ -59,6 +60,7 @@ pDecl' = try pFixity

59 <|> try (do n <- pfName; ty <- pTSig

60 <|> try (do n <- pfName; ty <- pTSig

60 return (PTy n ty))

61 return (PTy n ty))

61 <|> try pData

62 <|> try pData

63+ <|> try pPattern

63-------- Fixity --------

65-------- Fixity --------

@@ -98,6 +100,11 @@ pSimpleExpr =

98 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)

100 <|> try (do lchar '('; e <- pExpr; lchar ')'; return e)

99 <|> try (do reserved "Set"; return PSet)

101 <|> try (do reserved "Set"; return PSet)

100

102

103+pHSimpleExpr = try pSimpleExpr

104+ <|> do lchar '.'

105+ e <- pSimpleExpr

106+ return $ PHidden e

107+

101pApp = do f <- pSimpleExpr

108pApp = do f <- pSimpleExpr

102 args <- many1 pSimpleExpr

109 args <- many1 pSimpleExpr

103 return (PApp f [] args)

110 return (PApp f [] args)

@@ -168,3 +175,16 @@ pSimpleCon = do cn <- pfName

168

175

169--------- Pattern match clauses ---------

176--------- Pattern match clauses ---------

170

177

178+pPattern :: IParser PDecl

179+pPattern = try (do n <- pfName

180+ args <- many pHSimpleExpr

181+ lchar '='

182+ rhs <- pExpr

183+ return $ PClause (PApp (PRef n) [] args) rhs)

184+ <|> do l <- pSimpleExpr

185+ op <- operator

186+ r <- pSimpleExpr

187+ lchar '='

188+ rhs <- pExpr

189+ return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs

190+