Parsing class and instance (but no elaboration yet)

samples/interp.idr

@@ -42,7 +42,7 @@ using (G : Vect Ty n) {
   eId = Lam (Var fO);
    
   eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));
-  eAdd = Lam (Lam (Op' (Var fO) (Var (fS fO)) prim__addInt));
+  eAdd = Lam (Lam (Op (+) (Var fO) (Var (fS fO))));
   
 --   eDouble : Expr G (TyFun TyInt TyInt);
 --   eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var fO) (Var (fS fO))))) (Var fO)) (Var fO));

src/Idris/AbsSyntax.hs

@@ -184,6 +184,10 @@ data PDecl' t = PFix     FC Fixity [String] -- fixity declaration
               | PClauses FC Name [PClause' t]    -- pattern clause
               | PData    SyntaxInfo FC (PData' t)      -- data declaration
               | PParams  FC [(Name, t)] [PDecl' t] -- params block
+              | PClass   FC Name
+                         [(Name, t)] -- parameters
+                         [PDecl' t] -- declarations
+              | PInstance FC Name t [PDecl' t]
               | PSyntax  FC Syntax
     deriving Functor
 
@@ -827,6 +831,8 @@ dumpDecl (PClauses _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (sh
 dumpDecl (PData _ _ d) = showDImp True d
 dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"
 dumpDecl (PSyntax _ syn) = "syntax " ++ show syn
+dumpDecl (PClass _ n ps ds) = "class " ++ show n ++ " " ++ show ps ++ "\n" ++ dumpDecls ds
+dumpDecl (PInstance _ n t ds) = "instance " ++ show n ++ " " ++ show t ++ "\n" ++ dumpDecls ds
 -- dumpDecl (PImport i) = "import " ++ i
 
 -- syntactic match of a against b, returning pair of variables in a 

src/Idris/Parser.hs

@@ -144,7 +144,9 @@ collect (c@(PClauses _ _ _) : ds)
         cname (PClauses fc _ [PWith   n _ _ _ _]) = n
         getfc (PClauses fc _ _) = fc
 
-collect (PParams f ns ps : ds) = PParams f ns (collect ps) : (collect ds)
+collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
+collect (PClass f n ps ds : ds') = PClass f n ps (collect ds) : collect ds'
+collect (PInstance f n t ds : ds') = PInstance f n t (collect ds) : collect ds'
 collect (d : ds) = d : collect ds
 collect [] = []
 
@@ -160,8 +162,10 @@ pDecl syn
            i <- getState
            let d' = fmap (desugar syn i) d
            return [d']
-    <|> try (pUsing syn)
-    <|> try (pParams syn)
+    <|> pUsing syn
+    <|> pParams syn
+    <|> pClass syn
+    <|> pInstance syn
     <|> try (do reserved "import"
                 fp <- identifier
                 lchar ';'
@@ -278,6 +282,36 @@ fixity = try (do reserved "infixl"; return Infixl)
      <|> try (do reserved "infix";  return InfixN)
      <|> try (do reserved "prefix"; return PrefixN)
 
+--------- Tyoe classes ---------
+
+pClass :: SyntaxInfo -> IParser [PDecl]
+pClass syn = do reserved "class"
+                fc <- pfc
+                n <- pName
+                cs <- many1 carg
+                reserved "where"; lchar '{'
+                ds <- many1 $ pFunDecl syn;
+                lchar '}'
+                return [PClass fc n cs (concat ds)]
+  where
+    carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
+              return (i, ty)
+       <|> do i <- pName;
+              return (i, PSet)
+
+pInstance :: SyntaxInfo -> IParser [PDecl]
+pInstance syn = do reserved "instance"
+                   fc <- pfc
+                   cs <- pConstList syn
+                   cn <- pName
+                   args <- many1 (pSimpleExpr syn)
+                   let sc = PApp fc (PRef fc cn) (map pexp args)
+                   let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
+                   reserved "where"; lchar '{'
+                   ds <- many1 $ pFunDecl syn;
+                   lchar '}'
+                   return [PInstance fc cn t (concat ds)]
+
 --------- Expressions ---------
 
 pExpr syn = do i <- getState