git.iko.soy/Idris-dev
on master help sign in
Collect all pattern clauses for a function
8e8d57aEdwin Brady
src/Idris/AbsSyntax.hs+19−8
compare with master
unifiedsplit
@@ -72,10 +72,13 @@ instance Ord FixDecl where
72
72
73data Plicity = Imp | Exp deriving Show
73data Plicity = Imp | Exp deriving Show
74
74
75−data PDecl' t = PFix Fixity [String] -- fixity declaration
75+data PDecl' t = PFix Fixity [String] -- fixity declaration
76− | PTy Name t -- type declaration
76+ | PTy Name t -- type declaration
77− | PClause t t -- pattern clause
77+ | PClauses [PClause' t] -- pattern clause
78− | PData (PData' t) -- data declaration
78+ | PData (PData' t) -- data declaration
79+ deriving Functor
80+
81+data PClause' t = PClause Name t t
79 deriving Functor
82 deriving Functor
80
83
81data PData' t = PDatadecl { d_name :: Name,
84data PData' t = PDatadecl { d_name :: Name,
@@ -86,9 +89,9 @@ data PData' t = PDatadecl { d_name :: Name,
86-- Handy to get a free function for applying PTerm -> PTerm functions
89-- Handy to get a free function for applying PTerm -> PTerm functions
87-- across a program, by deriving Functor
90-- across a program, by deriving Functor
88
91
89−type PDecl = PDecl' PTerm
92+type PDecl = PDecl' PTerm
90−type PData = PData' PTerm
93+type PData = PData' PTerm
91−
94+type PClause = PClause' PTerm
92-- High level language terms
95-- High level language terms
93
96
94data PTerm = PQuote Raw
97data PTerm = PQuote Raw
@@ -100,18 +103,26 @@ data PTerm = PQuote Raw
100 | PSet
103 | PSet
101 | Placeholder
104 | Placeholder
102
105
106+--- Pretty printing declarations and terms
107+
103instance Show PTerm where
108instance Show PTerm where
104 show tm = showImp False tm
109 show tm = showImp False tm
105
110
106instance Show PDecl where
111instance Show PDecl where
107 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
112 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
108 show (PTy n ty) = show n ++ " : " ++ show ty
113 show (PTy n ty) = show n ++ " : " ++ show ty
109− show (PClause l r) = show l ++ " = " ++ show r
114+ show (PClauses c) = showSep "\n" (map show c)
110 show (PData d) = show d
115 show (PData d) = show d
111
116
117+instance Show PClause where
118+ show c = showCImp False c
119+
112instance Show PData where
120instance Show PData where
113 show d = showDImp False d
121 show d = showDImp False d
114
122
123+showCImp :: Bool -> PClause -> String
124+showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r
125+
115showDImp :: Bool -> PData -> String
126showDImp :: Bool -> PData -> String
116showDImp impl (PDatadecl n ty cons)
127showDImp impl (PDatadecl n ty cons)
117 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
128 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
src/Idris/Parser.hs+22−9
@@ -45,13 +45,21 @@ parseProg fname = do file <- lift $ readFile fname
45 return (ps, i')) i fname file) of
45 return (ps, i')) i fname file) of
46 Left err -> fail (show err)
46 Left err -> fail (show err)
47 Right (x, i) -> do put i
47 Right (x, i) -> do put i
48− return x
48+ return (collect x)
49
49
50+-- Collect PClauses with the same function name
51+collect :: [PDecl] -> [PDecl]
52+collect (PClauses [c@(PClause n l r)] : ds) = clauses n [c] ds
53+ where clauses n acc (PClauses [c@(PClause n' l r)] : ds)
54+ | n == n' = clauses n (c : acc) ds
55+ clauses n acc xs = PClauses (reverse acc) : collect xs
56+collect (d : ds) = d : collect ds
50
57
51pFullExpr = do x <- pExpr; eof; return x
58pFullExpr = do x <- pExpr; eof; return x
52
59
53pDecl :: IParser PDecl
60pDecl :: IParser PDecl
54−pDecl = do d <- pDecl'; lchar ';';
61+pDecl = do d <- pDecl'
62+ lchar ';'
55 i <- getState
63 i <- getState
56 return (fmap (addImpl i) d)
64 return (fmap (addImpl i) d)
57
65
@@ -190,18 +198,23 @@ pSimpleCon = do cn <- pfName
190--------- Pattern match clauses ---------
198--------- Pattern match clauses ---------
191
199
192pPattern :: IParser PDecl
200pPattern :: IParser PDecl
201+pPattern = do clause <- pClause
202+ return (PClauses [clause]) -- collect together later
203+
204+pClause :: IParser PClause
193−pPattern = try (do n <- pfName
205+pClause = try (do n <- pfName
194− iargs <- many pImplicitArg
206+ iargs <- many pImplicitArg
195− args <- many pHSimpleExpr
207+ args <- many pHSimpleExpr
196− lchar '='
208+ lchar '='
197− rhs <- pExpr
209+ rhs <- pExpr
198− return $ PClause (PApp (PRef n) iargs args) rhs)
210+ return $ PClause n (PApp (PRef n) iargs args) rhs)
199 <|> do l <- pSimpleExpr
211 <|> do l <- pSimpleExpr
200 op <- operator
212 op <- operator
213+ let n = UN [op]
201 r <- pSimpleExpr
214 r <- pSimpleExpr
202 lchar '='
215 lchar '='
203 rhs <- pExpr
216 rhs <- pExpr
204− return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs
217+ return $ PClause n (PApp (PRef n) [] [l,r]) rhs
205
218
206-- Dealing with implicit arguments
219-- Dealing with implicit arguments
207
220
src/Main.hs+2−2
@@ -53,8 +53,8 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
53
53
54dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
54dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
55dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
55dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
56−dumpDecl (PClause l r) = "pat " ++ showImp True l ++ " = " ++ showImp True r
56+dumpDecl (PClauses cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
57−dumpDecl (PData d) = "data " ++ showDImp True d
57+dumpDecl (PData d) = showDImp True d
58
58
59getFile :: Opt -> Maybe String
59getFile :: Opt -> Maybe String
60getFile (Filename str) = Just str
60getFile (Filename str) = Just str