33710ab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Parsing class and instance (but no elaboration yet)

33710abEdwin Brady15 years ago

samples/interp.idr+1−1

compare with master

unifiedsplit

@@ -42,7 +42,7 @@ using (G : Vect Ty n) {

42 eId = Lam (Var fO);

44 eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

45− eAdd = Lam (Lam (Op' (Var fO) (Var (fS fO)) prim__addInt));

45+ eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));

47-- eDouble : Expr G (TyFun TyInt TyInt);

48-- eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

src/Idris/AbsSyntax.hs+6

@@ -184,6 +184,10 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

184 | PClauses FC Name [PClause' t] -- pattern clause

185 | PData SyntaxInfo FC (PData' t) -- data declaration

186 | PParams FC [(Name, t)] [PDecl' t] -- params block

187+ | PClass FC Name

188+ [(Name, t)] -- parameters

189+ [PDecl' t] -- declarations

190+ | PInstance FC Name t [PDecl' t]

187 | PSyntax FC Syntax

191 | PSyntax FC Syntax

188 deriving Functor

192 deriving Functor

189

193

@@ -827,6 +831,8 @@ dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (sh

827dumpDecl (PData _ _ d) = showDImp True d

831dumpDecl (PData _ _ d) = showDImp True d

828dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

832dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

829dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

833dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

834+dumpDecl (PClass _ n ps ds) = "class " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds

835+dumpDecl (PInstance _ n t ds) = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds

830-- dumpDecl (PImport i) = "import " ++ i

836-- dumpDecl (PImport i) = "import " ++ i

831

837

832-- syntactic match of a against b, returning pair of variables in a

838-- syntactic match of a against b, returning pair of variables in a

src/Idris/Parser.hs+37−3

@@ -144,7 +144,9 @@ collect (c@(PClauses _ _ _) : ds)

144 cname (PClauses fc _ [PWith n _ _ _ _]) = n

145 getfc (PClauses fc _ _) = fc

146

147−collect (PParams f ns ps : ds) = PParams f ns (collect ps) : (collect ds)

147+collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

148+collect (PClass f n ps ds : ds') = PClass f n ps (collect ds) : collect ds'

149+collect (PInstance f n t ds : ds') = PInstance f n t (collect ds) : collect ds'

148collect (d : ds) = d : collect ds

150collect (d : ds) = d : collect ds

149collect [] = []

151collect [] = []

150

152

@@ -160,8 +162,10 @@ pDecl syn

160 i <- getState

162 i <- getState

161 let d' = fmap (desugar syn i) d

163 let d' = fmap (desugar syn i) d

162 return [d']

164 return [d']

163− <|> try (pUsing syn)

165+ <|> pUsing syn

164− <|> try (pParams syn)

166+ <|> pParams syn

167+ <|> pClass syn

168+ <|> pInstance syn

165 <|> try (do reserved "import"

169 <|> try (do reserved "import"

166 fp <- identifier

170 fp <- identifier

167 lchar ';'

171 lchar ';'

@@ -278,6 +282,36 @@ fixity = try (do reserved "infixl"; return Infixl)

278 <|> try (do reserved "infix"; return InfixN)

282 <|> try (do reserved "infix"; return InfixN)

279 <|> try (do reserved "prefix"; return PrefixN)

283 <|> try (do reserved "prefix"; return PrefixN)

280

284

285+--------- Tyoe classes ---------

286+

287+pClass :: SyntaxInfo -> IParser [PDecl]

288+pClass syn = do reserved "class"

289+ fc <- pfc

290+ n <- pName

291+ cs <- many1 carg

292+ reserved "where"; lchar '{'

293+ ds <- many1 $ pFunDecl syn;

294+ lchar '}'

295+ return [PClass fc n cs (concat ds)]

296+ where

297+ carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

298+ return (i, ty)

299+ <|> do i <- pName;

300+ return (i, PSet)

301+

302+pInstance :: SyntaxInfo -> IParser [PDecl]

303+pInstance syn = do reserved "instance"

304+ fc <- pfc

305+ cs <- pConstList syn

306+ cn <- pName

307+ args <- many1 (pSimpleExpr syn)

308+ let sc = PApp fc (PRef fc cn) (map pexp args)

309+ let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc

310+ reserved "where"; lchar '{'

311+ ds <- many1 $ pFunDecl syn;

312+ lchar '}'

313+ return [PInstance fc cn t (concat ds)]

314+

281--------- Expressions ---------

315--------- Expressions ---------

282

316

283pExpr syn = do i <- getState

317pExpr syn = do i <- getState