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

git.iko.soy/Idris-dev

Parsing class and instance (but no elaboration yet)

commit33710ab0f920df39d173fe38e9291f58d7fbc41a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 7 Nov 2011, 15:23 (15 years ago) parent27fc1f2

3 files changed+44−4

compare with master

unifiedsplit

samples/interp.idr+1−1 src/Idris/AbsSyntax.hs+6 src/Idris/Parser.hs+37−3

samples/interp.idr+1−1

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

4242 eId = Lam (Var fO);

4343

4444 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))));

4646

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

4848-- 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

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

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

186186 | 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]

187191 | PSyntax FC Syntax

188192 deriving Functor

189193

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

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

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

829833dumpDecl (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

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

831837

832838-- 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)

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

145145 getfc (PClauses fc _ _) = fc

146146

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'

148150collect (d : ds) = d : collect ds

149151collect [] = []

150152

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

160162 i <- getState

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

162164 return [d']

163− <|> try (pUsing syn)

164− <|> try (pParams syn)

165+ <|> pUsing syn

166+ <|> pParams syn

167+ <|> pClass syn

168+ <|> pInstance syn

165169 <|> try (do reserved "import"

166170 fp <- identifier

167171 lchar ';'

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

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

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

280284

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+

281315--------- Expressions ---------

282316

283317pExpr syn = do i <- getState