git.iko.soy/Idris-dev
on master help sign in
Collect all pattern clauses for a function
commit8e8d57a274e4c77cc279fad8f0bb327510f9d906 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 7 Oct 2011, 12:18 (15 years ago) parent1b6709f
3 files changed+43−19
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+19−8 src/Idris/Parser.hs+22−9 src/Main.hs+2−2
src/Idris/AbsSyntax.hs+19−8
@@ -72,10 +72,13 @@ instance Ord FixDecl where
7272
7373data Plicity = Imp | Exp deriving Show
7474
75−data PDecl' t = PFix Fixity [String] -- fixity declaration
76− | PTy Name t -- type declaration
77− | PClause t t -- pattern clause
78− | PData (PData' t) -- data declaration
75+data PDecl' t = PFix Fixity [String] -- fixity declaration
76+ | PTy Name t -- type declaration
77+ | PClauses [PClause' t] -- pattern clause
78+ | PData (PData' t) -- data declaration
79+ deriving Functor
80+
81+data PClause' t = PClause Name t t
7982 deriving Functor
8083
8184data PData' t = PDatadecl { d_name :: Name,
@@ -86,9 +89,9 @@ data PData' t = PDatadecl { d_name :: Name,
8689-- Handy to get a free function for applying PTerm -> PTerm functions
8790-- across a program, by deriving Functor
8891
89−type PDecl = PDecl' PTerm
90−type PData = PData' PTerm
91−
92+type PDecl = PDecl' PTerm
93+type PData = PData' PTerm
94+type PClause = PClause' PTerm
9295-- High level language terms
9396
9497data PTerm = PQuote Raw
@@ -100,18 +103,26 @@ data PTerm = PQuote Raw
100103 | PSet
101104 | Placeholder
102105
106+--- Pretty printing declarations and terms
107+
103108instance Show PTerm where
104109 show tm = showImp False tm
105110
106111instance Show PDecl where
107112 show (PFix f ops) = show f ++ " " ++ showSep ", " ops
108113 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)
110115 show (PData d) = show d
111116
117+instance Show PClause where
118+ show c = showCImp False c
119+
112120instance Show PData where
113121 show d = showDImp False d
114122
123+showCImp :: Bool -> PClause -> String
124+showCImp impl (PClause n l r) = showImp impl l ++ " = " ++ showImp impl r
125+
115126showDImp :: Bool -> PData -> String
116127showDImp impl (PDatadecl n ty cons)
117128 = "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
4545 return (ps, i')) i fname file) of
4646 Left err -> fail (show err)
4747 Right (x, i) -> do put i
48− return x
48+ return (collect x)
4949
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
5057
5158pFullExpr = do x <- pExpr; eof; return x
5259
5360pDecl :: IParser PDecl
54−pDecl = do d <- pDecl'; lchar ';';
61+pDecl = do d <- pDecl'
62+ lchar ';'
5563 i <- getState
5664 return (fmap (addImpl i) d)
5765
@@ -190,18 +198,23 @@ pSimpleCon = do cn <- pfName
190198--------- Pattern match clauses ---------
191199
192200pPattern :: IParser PDecl
193−pPattern = try (do n <- pfName
194− iargs <- many pImplicitArg
195− args <- many pHSimpleExpr
196− lchar '='
197− rhs <- pExpr
198− return $ PClause (PApp (PRef n) iargs args) rhs)
201+pPattern = do clause <- pClause
202+ return (PClauses [clause]) -- collect together later
203+
204+pClause :: IParser PClause
205+pClause = try (do n <- pfName
206+ iargs <- many pImplicitArg
207+ args <- many pHSimpleExpr
208+ lchar '='
209+ rhs <- pExpr
210+ return $ PClause n (PApp (PRef n) iargs args) rhs)
199211 <|> do l <- pSimpleExpr
200212 op <- operator
213+ let n = UN [op]
201214 r <- pSimpleExpr
202215 lchar '='
203216 rhs <- pExpr
204− return $ PClause (PApp (PRef (UN [op])) [] [l,r]) rhs
217+ return $ PClause n (PApp (PRef n) [] [l,r]) rhs
205218
206219-- Dealing with implicit arguments
207220
src/Main.hs+2−2
@@ -53,8 +53,8 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds
5353
5454dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops
5555dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t
56−dumpDecl (PClause l r) = "pat " ++ showImp True l ++ " = " ++ showImp True r
57−dumpDecl (PData d) = "data " ++ showDImp True d
56+dumpDecl (PClauses cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)
57+dumpDecl (PData d) = showDImp True d
5858
5959getFile :: Opt -> Maybe String
6060getFile (Filename str) = Just str